module AutoApply
  ( autoapply
  , autoapplyDecs
  ) where

import           Control.Applicative
import           Control.Arrow                  ( (>>>) )
import           Control.Monad
import           Control.Monad.Logic            ( LogicT
                                                , observeManyT
                                                )
import           Control.Monad.Trans           as T
import           Control.Monad.Trans.Except
import           Control.Unification
import           Control.Unification.IntVar
import           Control.Unification.Types
import           Data.Foldable
import           Data.Functor
import           Data.Functor.Fixedpoint
import           Data.Maybe
import           Data.Traversable
import           Language.Haskell.TH
import           Language.Haskell.TH.Desugar
import           Prelude                 hiding ( pred )

-- | @autoapply argsSubsuming argsUnifying fun@ creates an expression which is
-- equal to @fun@ applied to as many of the values in @argsSubsuming@ and
-- @argsUnifying@ as possible.
--
-- The types of first list of args must subsume the type of the argument
-- they're passed to. The types of the second list must merely unify.
autoapply
  :: [Name]
  -- ^ Values which will be used if their type subsumes the argument type
  -> [Name]
  -- ^ Values which will be used if their type unifies with the argument type
  -> Name
  -- ^ A function to apply to some values
  -> Q Exp
autoapply :: [Name] -> [Name] -> Name -> Q Exp
autoapply subsuming :: [Name]
subsuming unifying :: [Name]
unifying fun :: Name
fun = do
  [Given]
unifyingInfos <- [Name] -> (Name -> Q Given) -> Q [Given]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [Name]
unifying ((Name -> Q Given) -> Q [Given]) -> (Name -> Q Given) -> Q [Given]
forall a b. (a -> b) -> a -> b
$ ((Name, DType) -> Given) -> Q (Name, DType) -> Q Given
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Name -> DType -> Given) -> (Name, DType) -> Given
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (UnificationType -> Name -> DType -> Given
Given UnificationType
Unifying)) (Q (Name, DType) -> Q Given)
-> (Name -> Q (Name, DType)) -> Name -> Q Given
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Name -> Q (Name, DType)
reifyVal
    "Argument"
  [Given]
subsumingInfos <- [Name] -> (Name -> Q Given) -> Q [Given]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [Name]
subsuming ((Name -> Q Given) -> Q [Given]) -> (Name -> Q Given) -> Q [Given]
forall a b. (a -> b) -> a -> b
$ ((Name, DType) -> Given) -> Q (Name, DType) -> Q Given
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Name -> DType -> Given) -> (Name, DType) -> Given
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (UnificationType -> Name -> DType -> Given
Given UnificationType
Subsuming)) (Q (Name, DType) -> Q Given)
-> (Name -> Q (Name, DType)) -> Name -> Q Given
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Name -> Q (Name, DType)
reifyVal
    "Argument"
  Function
funInfo <- (Name -> DType -> Function) -> (Name, DType) -> Function
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Name -> DType -> Function
Function ((Name, DType) -> Function) -> Q (Name, DType) -> Q Function
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> Name -> Q (Name, DType)
reifyVal "Function" Name
fun
  [Given] -> Function -> Q Exp
autoapply1 ([Given]
unifyingInfos [Given] -> [Given] -> [Given]
forall a. Semigroup a => a -> a -> a
<> [Given]
subsumingInfos) Function
funInfo

-- | @autoapplyDecs mkName argsSubsuming argsUnifying funs@ will wrap every
-- function in @funs@ by applying it to as many of the values in
-- @argsSubsuming@ and @argsUnifying@ as possible. The new function name will
-- be @mkName@ applied to the wrapped function name.
--
-- The types of first list of args must subsume the type of the argument
-- they're passed to. The types of the second list must merely unify.
--
-- Type signatures are not generated, so you may want to add these yourself or
-- turn on @NoMonomorphismRestriction@ if you have polymorphic constraints.
autoapplyDecs
  :: (String -> String)
  -- ^ A function to generate a new name for the wrapping function
  -> [Name]
  -- ^ A list of values which will be passed to any arguments their type subsumes
  -> [Name]
  -- ^ A list of values which will be passed to any arguments their type unify with
  -> [Name]
  -- ^ A list of function to wrap with the above parameters
  -> Q [Dec]
autoapplyDecs :: (String -> String) -> [Name] -> [Name] -> [Name] -> Q [Dec]
autoapplyDecs getNewName :: String -> String
getNewName subsuming :: [Name]
subsuming unifying :: [Name]
unifying funs :: [Name]
funs = do
  [Given]
unifyingInfos <- [Name] -> (Name -> Q Given) -> Q [Given]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [Name]
unifying ((Name -> Q Given) -> Q [Given]) -> (Name -> Q Given) -> Q [Given]
forall a b. (a -> b) -> a -> b
$ ((Name, DType) -> Given) -> Q (Name, DType) -> Q Given
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Name -> DType -> Given) -> (Name, DType) -> Given
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (UnificationType -> Name -> DType -> Given
Given UnificationType
Unifying)) (Q (Name, DType) -> Q Given)
-> (Name -> Q (Name, DType)) -> Name -> Q Given
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Name -> Q (Name, DType)
reifyVal
    "Argument"
  [Given]
subsumingInfos <- [Name] -> (Name -> Q Given) -> Q [Given]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [Name]
subsuming ((Name -> Q Given) -> Q [Given]) -> (Name -> Q Given) -> Q [Given]
forall a b. (a -> b) -> a -> b
$ ((Name, DType) -> Given) -> Q (Name, DType) -> Q Given
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Name -> DType -> Given) -> (Name, DType) -> Given
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (UnificationType -> Name -> DType -> Given
Given UnificationType
Subsuming)) (Q (Name, DType) -> Q Given)
-> (Name -> Q (Name, DType)) -> Name -> Q Given
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Name -> Q (Name, DType)
reifyVal
    "Argument"
  [Function]
funInfos <- [Name] -> (Name -> Q Function) -> Q [Function]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [Name]
funs ((Name -> Q Function) -> Q [Function])
-> (Name -> Q Function) -> Q [Function]
forall a b. (a -> b) -> a -> b
$ ((Name, DType) -> Function) -> Q (Name, DType) -> Q Function
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Name -> DType -> Function) -> (Name, DType) -> Function
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Name -> DType -> Function
Function) (Q (Name, DType) -> Q Function)
-> (Name -> Q (Name, DType)) -> Name -> Q Function
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Name -> Q (Name, DType)
reifyVal "Function"
  let mkFun :: Function -> Q Dec
mkFun fun :: Function
fun = do
        Exp
exp' <- [Given] -> Function -> Q Exp
autoapply1 ([Given]
unifyingInfos [Given] -> [Given] -> [Given]
forall a. Semigroup a => a -> a -> a
<> [Given]
subsumingInfos) Function
fun
        Dec -> Q Dec
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Dec -> Q Dec) -> Dec -> Q Dec
forall a b. (a -> b) -> a -> b
$ Name -> [Clause] -> Dec
FunD (String -> Name
mkName (String -> Name) -> (Function -> String) -> Function -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
getNewName (String -> String) -> (Function -> String) -> Function -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> String
nameBase (Name -> String) -> (Function -> Name) -> Function -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Function -> Name
fName (Function -> Name) -> Function -> Name
forall a b. (a -> b) -> a -> b
$ Function
fun)
                    [[Pat] -> Body -> [Dec] -> Clause
Clause [] (Exp -> Body
NormalB Exp
exp') []]
  (Function -> Q Dec) -> [Function] -> Q [Dec]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Function -> Q Dec
mkFun [Function]
funInfos

-- | A given is something we can try to pass as an argument
data Given = Given
  { Given -> UnificationType
gUnificationType :: UnificationType
  , Given -> Name
gName            :: Name
  , Given -> DType
gType            :: DType
  }
  deriving Int -> Given -> String -> String
[Given] -> String -> String
Given -> String
(Int -> Given -> String -> String)
-> (Given -> String) -> ([Given] -> String -> String) -> Show Given
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [Given] -> String -> String
$cshowList :: [Given] -> String -> String
show :: Given -> String
$cshow :: Given -> String
showsPrec :: Int -> Given -> String -> String
$cshowsPrec :: Int -> Given -> String -> String
Show

data UnificationType = Unifying | Subsuming
  deriving Int -> UnificationType -> String -> String
[UnificationType] -> String -> String
UnificationType -> String
(Int -> UnificationType -> String -> String)
-> (UnificationType -> String)
-> ([UnificationType] -> String -> String)
-> Show UnificationType
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [UnificationType] -> String -> String
$cshowList :: [UnificationType] -> String -> String
show :: UnificationType -> String
$cshow :: UnificationType -> String
showsPrec :: Int -> UnificationType -> String -> String
$cshowsPrec :: Int -> UnificationType -> String -> String
Show

-- | A function we are wrapping
data Function = Function
  { Function -> Name
fName :: Name
  , Function -> DType
fType :: DType
  }
  deriving (Int -> Function -> String -> String
[Function] -> String -> String
Function -> String
(Int -> Function -> String -> String)
-> (Function -> String)
-> ([Function] -> String -> String)
-> Show Function
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [Function] -> String -> String
$cshowList :: [Function] -> String -> String
show :: Function -> String
$cshow :: Function -> String
showsPrec :: Int -> Function -> String -> String
$cshowsPrec :: Int -> Function -> String -> String
Show)

autoapply1 :: [Given] -> Function -> Q Exp
autoapply1 :: [Given] -> Function -> Q Exp
autoapply1 givens :: [Given]
givens fun :: Function
fun = do
  -- In this function we:
  --
  -- - Instantiate the command type with new unification variables
  -- - Split it into arguments and return type
  -- - Try to unify or subsume it with every 'Given' at every argument
  --   - If we can unify the monad of the 'Given' with that of the functions and
  --     unify the argument type, use that.
  --   - If nothing matches we just use an 'Argument'
  -- - Take the first result of all these tries

  let
    ((DTyVarBndr -> Name) -> [DTyVarBndr] -> [Name]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DTyVarBndr -> Name
varBndrName -> [Name]
cmdVarNames, preds :: [DType]
preds, args :: [DType]
args, ret :: DType
ret) = DType -> ([DTyVarBndr], [DType], [DType], DType)
unravel (Function -> DType
fType Function
fun)
    defaultMaybe :: f a -> f (Maybe a)
defaultMaybe m :: f a
m = (a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> f a -> f (Maybe a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f a
m) f (Maybe a) -> f (Maybe a) -> f (Maybe a)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Maybe a -> f (Maybe a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe a
forall a. Maybe a
Nothing
    liftQ :: Q a -> IntBindingT TypeF (LogicT Q) a
    liftQ :: Q a -> IntBindingT TypeF (LogicT Q) a
liftQ = LogicT Q a -> IntBindingT TypeF (LogicT Q) a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
T.lift (LogicT Q a -> IntBindingT TypeF (LogicT Q) a)
-> (Q a -> LogicT Q a) -> Q a -> IntBindingT TypeF (LogicT Q) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Q a -> LogicT Q a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
T.lift
    errorToLogic :: ExceptT (UFailure TypeF IntVar) m b -> m b
errorToLogic go :: ExceptT (UFailure TypeF IntVar) m b
go = ExceptT (UFailure TypeF IntVar) m b
-> m (Either (UFailure TypeF IntVar) b)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT ExceptT (UFailure TypeF IntVar) m b
go m (Either (UFailure TypeF IntVar) b)
-> (Either (UFailure TypeF IntVar) b -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Left  (UFailure TypeF IntVar
_ :: UFailure TypeF IntVar) -> m b
forall (f :: * -> *) a. Alternative f => f a
empty
      Right x :: b
x                            -> b -> m b
forall (f :: * -> *) a. Applicative f => a -> f a
pure b
x
    -- Quant will invent new variable names for any unification variables
    -- still free
    quant :: UTerm TypeF IntVar -> IntBindingT TypeF (LogicT Q) ()
quant t :: UTerm TypeF IntVar
t = do
      [IntVar]
vs <- UTerm TypeF IntVar -> IntBindingT TypeF (LogicT Q) [IntVar]
forall (t :: * -> *) v (m :: * -> *).
BindingMonad t v m =>
UTerm t v -> m [v]
getFreeVars UTerm TypeF IntVar
t
      [IntVar]
-> (IntVar -> IntBindingT TypeF (LogicT Q) ())
-> IntBindingT TypeF (LogicT Q) ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ [IntVar]
vs ((IntVar -> IntBindingT TypeF (LogicT Q) ())
 -> IntBindingT TypeF (LogicT Q) ())
-> (IntVar -> IntBindingT TypeF (LogicT Q) ())
-> IntBindingT TypeF (LogicT Q) ()
forall a b. (a -> b) -> a -> b
$ \v :: IntVar
v -> IntVar -> UTerm TypeF IntVar -> IntBindingT TypeF (LogicT Q) ()
forall (t :: * -> *) v (m :: * -> *).
BindingMonad t v m =>
v -> UTerm t v -> m ()
bindVar IntVar
v (UTerm TypeF IntVar -> IntBindingT TypeF (LogicT Q) ())
-> (Name -> UTerm TypeF IntVar)
-> Name
-> IntBindingT TypeF (LogicT Q) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TypeF (UTerm TypeF IntVar) -> UTerm TypeF IntVar
forall (t :: * -> *) v. t (UTerm t v) -> UTerm t v
UTerm (TypeF (UTerm TypeF IntVar) -> UTerm TypeF IntVar)
-> (Name -> TypeF (UTerm TypeF IntVar))
-> Name
-> UTerm TypeF IntVar
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> TypeF (UTerm TypeF IntVar)
forall a. Name -> TypeF a
VarF) (Name -> IntBindingT TypeF (LogicT Q) ())
-> IntBindingT TypeF (LogicT Q) Name
-> IntBindingT TypeF (LogicT Q) ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Q Name -> IntBindingT TypeF (LogicT Q) Name
forall a. Q a -> IntBindingT TypeF (LogicT Q) a
liftQ (String -> Q Name
newName "a")


    -- Use LogicT so we can backtrack on failure
    genProvs :: LogicT Q [ArgProvenance]
    genProvs :: LogicT Q [ArgProvenance]
genProvs = IntBindingT TypeF (LogicT Q) [ArgProvenance]
-> LogicT Q [ArgProvenance]
forall (m :: * -> *) (t :: * -> *) a.
Monad m =>
IntBindingT t m a -> m a
evalIntBindingT (IntBindingT TypeF (LogicT Q) [ArgProvenance]
 -> LogicT Q [ArgProvenance])
-> IntBindingT TypeF (LogicT Q) [ArgProvenance]
-> LogicT Q [ArgProvenance]
forall a b. (a -> b) -> a -> b
$ do
      [(Name, IntVar)]
cmdVars  <- [IntBindingT TypeF (LogicT Q) (Name, IntVar)]
-> IntBindingT TypeF (LogicT Q) [(Name, IntVar)]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [ (Name
n, ) (IntVar -> (Name, IntVar))
-> IntBindingT TypeF (LogicT Q) IntVar
-> IntBindingT TypeF (LogicT Q) (Name, IntVar)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IntBindingT TypeF (LogicT Q) IntVar
forall (t :: * -> *) v (m :: * -> *). BindingMonad t v m => m v
freeVar | Name
n <- [Name]
cmdVarNames ]
      [UTerm TypeF IntVar]
instArgs <- (DType -> IntBindingT TypeF (LogicT Q) (UTerm TypeF IntVar))
-> [DType] -> IntBindingT TypeF (LogicT Q) [UTerm TypeF IntVar]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse
        ((([Name], Fix TypeF) -> UTerm TypeF IntVar)
-> IntBindingT TypeF (LogicT Q) ([Name], Fix TypeF)
-> IntBindingT TypeF (LogicT Q) (UTerm TypeF IntVar)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([(Name, IntVar)] -> Fix TypeF -> UTerm TypeF IntVar
instWithVars [(Name, IntVar)]
cmdVars (Fix TypeF -> UTerm TypeF IntVar)
-> (([Name], Fix TypeF) -> Fix TypeF)
-> ([Name], Fix TypeF)
-> UTerm TypeF IntVar
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Name], Fix TypeF) -> Fix TypeF
forall a b. (a, b) -> b
snd) (IntBindingT TypeF (LogicT Q) ([Name], Fix TypeF)
 -> IntBindingT TypeF (LogicT Q) (UTerm TypeF IntVar))
-> (DType -> IntBindingT TypeF (LogicT Q) ([Name], Fix TypeF))
-> DType
-> IntBindingT TypeF (LogicT Q) (UTerm TypeF IntVar)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Q ([Name], Fix TypeF)
-> IntBindingT TypeF (LogicT Q) ([Name], Fix TypeF)
forall a. Q a -> IntBindingT TypeF (LogicT Q) a
liftQ (Q ([Name], Fix TypeF)
 -> IntBindingT TypeF (LogicT Q) ([Name], Fix TypeF))
-> (DType -> Q ([Name], Fix TypeF))
-> DType
-> IntBindingT TypeF (LogicT Q) ([Name], Fix TypeF)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DType -> Q ([Name], Fix TypeF)
forall (m :: * -> *). MonadFail m => DType -> m ([Name], Fix TypeF)
typeDtoF)
        [DType]
args

      UTerm TypeF IntVar
cmdM       <- IntVar -> UTerm TypeF IntVar
forall (t :: * -> *) v. v -> UTerm t v
UVar (IntVar -> UTerm TypeF IntVar)
-> IntBindingT TypeF (LogicT Q) IntVar
-> IntBindingT TypeF (LogicT Q) (UTerm TypeF IntVar)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IntBindingT TypeF (LogicT Q) IntVar
forall (t :: * -> *) v (m :: * -> *). BindingMonad t v m => m v
freeVar
      UTerm TypeF IntVar
retInst    <- (([Name], Fix TypeF) -> UTerm TypeF IntVar)
-> IntBindingT TypeF (LogicT Q) ([Name], Fix TypeF)
-> IntBindingT TypeF (LogicT Q) (UTerm TypeF IntVar)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([(Name, IntVar)] -> Fix TypeF -> UTerm TypeF IntVar
instWithVars [(Name, IntVar)]
cmdVars (Fix TypeF -> UTerm TypeF IntVar)
-> (([Name], Fix TypeF) -> Fix TypeF)
-> ([Name], Fix TypeF)
-> UTerm TypeF IntVar
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Name], Fix TypeF) -> Fix TypeF
forall a b. (a, b) -> b
snd) (IntBindingT TypeF (LogicT Q) ([Name], Fix TypeF)
 -> IntBindingT TypeF (LogicT Q) (UTerm TypeF IntVar))
-> (DType -> IntBindingT TypeF (LogicT Q) ([Name], Fix TypeF))
-> DType
-> IntBindingT TypeF (LogicT Q) (UTerm TypeF IntVar)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Q ([Name], Fix TypeF)
-> IntBindingT TypeF (LogicT Q) ([Name], Fix TypeF)
forall a. Q a -> IntBindingT TypeF (LogicT Q) a
liftQ (Q ([Name], Fix TypeF)
 -> IntBindingT TypeF (LogicT Q) ([Name], Fix TypeF))
-> (DType -> Q ([Name], Fix TypeF))
-> DType
-> IntBindingT TypeF (LogicT Q) ([Name], Fix TypeF)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DType -> Q ([Name], Fix TypeF)
forall (m :: * -> *). MonadFail m => DType -> m ([Name], Fix TypeF)
typeDtoF (DType -> IntBindingT TypeF (LogicT Q) (UTerm TypeF IntVar))
-> DType -> IntBindingT TypeF (LogicT Q) (UTerm TypeF IntVar)
forall a b. (a -> b) -> a -> b
$ DType
ret

      -- A list of
      -- ( type to unify
      -- , predicate to use this match
      -- , the given providing the value
      -- )
      --
      -- The predicate is there to make sure we only match unifiable monads
      [(UTerm TypeF IntVar,
  ExceptT (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) (),
  ArgProvenance)]
instGivens <- ([[(UTerm TypeF IntVar,
    ExceptT (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) (),
    ArgProvenance)]]
 -> [(UTerm TypeF IntVar,
      ExceptT (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) (),
      ArgProvenance)])
-> IntBindingT
     TypeF
     (LogicT Q)
     [[(UTerm TypeF IntVar,
        ExceptT (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) (),
        ArgProvenance)]]
-> IntBindingT
     TypeF
     (LogicT Q)
     [(UTerm TypeF IntVar,
       ExceptT (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) (),
       ArgProvenance)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [[(UTerm TypeF IntVar,
   ExceptT (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) (),
   ArgProvenance)]]
-> [(UTerm TypeF IntVar,
     ExceptT (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) (),
     ArgProvenance)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (IntBindingT
   TypeF
   (LogicT Q)
   [[(UTerm TypeF IntVar,
      ExceptT (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) (),
      ArgProvenance)]]
 -> IntBindingT
      TypeF
      (LogicT Q)
      [(UTerm TypeF IntVar,
        ExceptT (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) (),
        ArgProvenance)])
-> ((Given
     -> IntBindingT
          TypeF
          (LogicT Q)
          [(UTerm TypeF IntVar,
            ExceptT (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) (),
            ArgProvenance)])
    -> IntBindingT
         TypeF
         (LogicT Q)
         [[(UTerm TypeF IntVar,
            ExceptT (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) (),
            ArgProvenance)]])
-> (Given
    -> IntBindingT
         TypeF
         (LogicT Q)
         [(UTerm TypeF IntVar,
           ExceptT (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) (),
           ArgProvenance)])
-> IntBindingT
     TypeF
     (LogicT Q)
     [(UTerm TypeF IntVar,
       ExceptT (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) (),
       ArgProvenance)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Given]
-> (Given
    -> IntBindingT
         TypeF
         (LogicT Q)
         [(UTerm TypeF IntVar,
           ExceptT (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) (),
           ArgProvenance)])
-> IntBindingT
     TypeF
     (LogicT Q)
     [[(UTerm TypeF IntVar,
        ExceptT (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) (),
        ArgProvenance)]]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [Given]
givens ((Given
  -> IntBindingT
       TypeF
       (LogicT Q)
       [(UTerm TypeF IntVar,
         ExceptT (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) (),
         ArgProvenance)])
 -> IntBindingT
      TypeF
      (LogicT Q)
      [(UTerm TypeF IntVar,
        ExceptT (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) (),
        ArgProvenance)])
-> (Given
    -> IntBindingT
         TypeF
         (LogicT Q)
         [(UTerm TypeF IntVar,
           ExceptT (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) (),
           ArgProvenance)])
-> IntBindingT
     TypeF
     (LogicT Q)
     [(UTerm TypeF IntVar,
       ExceptT (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) (),
       ArgProvenance)]
forall a b. (a -> b) -> a -> b
$ \g :: Given
g@Given {..} -> do
        -- The Given applied as is
        (UTerm TypeF IntVar,
 ExceptT (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) (),
 ArgProvenance)
nonApp <- do
          UTerm TypeF IntVar
instTy <- ([Name]
 -> Fix TypeF -> IntBindingT TypeF (LogicT Q) (UTerm TypeF IntVar))
-> ([Name], Fix TypeF)
-> IntBindingT TypeF (LogicT Q) (UTerm TypeF IntVar)
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry [Name]
-> Fix TypeF -> IntBindingT TypeF (LogicT Q) (UTerm TypeF IntVar)
forall (m :: * -> *).
BindingMonad TypeF IntVar m =>
[Name] -> Fix TypeF -> m (UTerm TypeF IntVar)
inst (([Name], Fix TypeF)
 -> IntBindingT TypeF (LogicT Q) (UTerm TypeF IntVar))
-> (DType -> IntBindingT TypeF (LogicT Q) ([Name], Fix TypeF))
-> DType
-> IntBindingT TypeF (LogicT Q) (UTerm TypeF IntVar)
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Q ([Name], Fix TypeF)
-> IntBindingT TypeF (LogicT Q) ([Name], Fix TypeF)
forall a. Q a -> IntBindingT TypeF (LogicT Q) a
liftQ (Q ([Name], Fix TypeF)
 -> IntBindingT TypeF (LogicT Q) ([Name], Fix TypeF))
-> (DType -> Q ([Name], Fix TypeF))
-> DType
-> IntBindingT TypeF (LogicT Q) ([Name], Fix TypeF)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DType -> Q ([Name], Fix TypeF)
forall (m :: * -> *). MonadFail m => DType -> m ([Name], Fix TypeF)
typeDtoF (DType -> IntBindingT TypeF (LogicT Q) (UTerm TypeF IntVar))
-> DType -> IntBindingT TypeF (LogicT Q) (UTerm TypeF IntVar)
forall a b. (a -> b) -> a -> b
$ DType
gType
          Name
v      <- Q Name -> IntBindingT TypeF (LogicT Q) Name
forall a. Q a -> IntBindingT TypeF (LogicT Q) a
liftQ (Q Name -> IntBindingT TypeF (LogicT Q) Name)
-> Q Name -> IntBindingT TypeF (LogicT Q) Name
forall a b. (a -> b) -> a -> b
$ String -> Q Name
newName "g"
          (UTerm TypeF IntVar,
 ExceptT (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) (),
 ArgProvenance)
-> IntBindingT
     TypeF
     (LogicT Q)
     (UTerm TypeF IntVar,
      ExceptT (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) (),
      ArgProvenance)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (UTerm TypeF IntVar
instTy, ()
-> ExceptT
     (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure (), Name -> Given -> ArgProvenance
BoundPure Name
v Given
g)
        -- The given, but in an applicative context, only possible if we can
        -- unify the monad and there is a Monad instance
        Maybe
  (UTerm TypeF IntVar,
   ExceptT (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) (),
   ArgProvenance)
app <- case DType -> ([Name], DType)
stripForall DType
gType of
          (vars :: [Name]
vars, DAppT m :: DType
m a :: DType
a) ->
            Q Bool -> IntBindingT TypeF (LogicT Q) Bool
forall a. Q a -> IntBindingT TypeF (LogicT Q) a
liftQ (Name -> [Type] -> Q Bool
isInstance ''Applicative [DType -> Type
forall th ds. Desugar th ds => ds -> th
sweeten DType
m]) IntBindingT TypeF (LogicT Q) Bool
-> (Bool
    -> IntBindingT
         TypeF
         (LogicT Q)
         (Maybe
            (UTerm TypeF IntVar,
             ExceptT (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) (),
             ArgProvenance)))
-> IntBindingT
     TypeF
     (LogicT Q)
     (Maybe
        (UTerm TypeF IntVar,
         ExceptT (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) (),
         ArgProvenance))
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
              False -> Maybe
  (UTerm TypeF IntVar,
   ExceptT (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) (),
   ArgProvenance)
-> IntBindingT
     TypeF
     (LogicT Q)
     (Maybe
        (UTerm TypeF IntVar,
         ExceptT (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) (),
         ArgProvenance))
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe
  (UTerm TypeF IntVar,
   ExceptT (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) (),
   ArgProvenance)
forall a. Maybe a
Nothing
              True  -> do
                UTerm TypeF IntVar
m' <- [Name]
-> Fix TypeF -> IntBindingT TypeF (LogicT Q) (UTerm TypeF IntVar)
forall (m :: * -> *).
BindingMonad TypeF IntVar m =>
[Name] -> Fix TypeF -> m (UTerm TypeF IntVar)
inst [Name]
vars (Fix TypeF -> IntBindingT TypeF (LogicT Q) (UTerm TypeF IntVar))
-> (([Name], Fix TypeF) -> Fix TypeF)
-> ([Name], Fix TypeF)
-> IntBindingT TypeF (LogicT Q) (UTerm TypeF IntVar)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Name], Fix TypeF) -> Fix TypeF
forall a b. (a, b) -> b
snd (([Name], Fix TypeF)
 -> IntBindingT TypeF (LogicT Q) (UTerm TypeF IntVar))
-> (DType -> IntBindingT TypeF (LogicT Q) ([Name], Fix TypeF))
-> DType
-> IntBindingT TypeF (LogicT Q) (UTerm TypeF IntVar)
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Q ([Name], Fix TypeF)
-> IntBindingT TypeF (LogicT Q) ([Name], Fix TypeF)
forall a. Q a -> IntBindingT TypeF (LogicT Q) a
liftQ (Q ([Name], Fix TypeF)
 -> IntBindingT TypeF (LogicT Q) ([Name], Fix TypeF))
-> (DType -> Q ([Name], Fix TypeF))
-> DType
-> IntBindingT TypeF (LogicT Q) ([Name], Fix TypeF)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DType -> Q ([Name], Fix TypeF)
forall (m :: * -> *). MonadFail m => DType -> m ([Name], Fix TypeF)
typeDtoF (DType -> IntBindingT TypeF (LogicT Q) (UTerm TypeF IntVar))
-> DType -> IntBindingT TypeF (LogicT Q) (UTerm TypeF IntVar)
forall a b. (a -> b) -> a -> b
$ DType
m
                UTerm TypeF IntVar
a' <- [Name]
-> Fix TypeF -> IntBindingT TypeF (LogicT Q) (UTerm TypeF IntVar)
forall (m :: * -> *).
BindingMonad TypeF IntVar m =>
[Name] -> Fix TypeF -> m (UTerm TypeF IntVar)
inst [Name]
vars (Fix TypeF -> IntBindingT TypeF (LogicT Q) (UTerm TypeF IntVar))
-> (([Name], Fix TypeF) -> Fix TypeF)
-> ([Name], Fix TypeF)
-> IntBindingT TypeF (LogicT Q) (UTerm TypeF IntVar)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Name], Fix TypeF) -> Fix TypeF
forall a b. (a, b) -> b
snd (([Name], Fix TypeF)
 -> IntBindingT TypeF (LogicT Q) (UTerm TypeF IntVar))
-> (DType -> IntBindingT TypeF (LogicT Q) ([Name], Fix TypeF))
-> DType
-> IntBindingT TypeF (LogicT Q) (UTerm TypeF IntVar)
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Q ([Name], Fix TypeF)
-> IntBindingT TypeF (LogicT Q) ([Name], Fix TypeF)
forall a. Q a -> IntBindingT TypeF (LogicT Q) a
liftQ (Q ([Name], Fix TypeF)
 -> IntBindingT TypeF (LogicT Q) ([Name], Fix TypeF))
-> (DType -> Q ([Name], Fix TypeF))
-> DType
-> IntBindingT TypeF (LogicT Q) ([Name], Fix TypeF)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DType -> Q ([Name], Fix TypeF)
forall (m :: * -> *). MonadFail m => DType -> m ([Name], Fix TypeF)
typeDtoF (DType -> IntBindingT TypeF (LogicT Q) (UTerm TypeF IntVar))
-> DType -> IntBindingT TypeF (LogicT Q) (UTerm TypeF IntVar)
forall a b. (a -> b) -> a -> b
$ DType
a
                Name
v  <- Q Name -> IntBindingT TypeF (LogicT Q) Name
forall a. Q a -> IntBindingT TypeF (LogicT Q) a
liftQ (Q Name -> IntBindingT TypeF (LogicT Q) Name)
-> Q Name -> IntBindingT TypeF (LogicT Q) Name
forall a b. (a -> b) -> a -> b
$ String -> Q Name
newName "g"
                let predicate :: ExceptT (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) ()
predicate = do
                      UTerm TypeF IntVar
_ <- UTerm TypeF IntVar
-> UTerm TypeF IntVar
-> ExceptT
     (UFailure TypeF IntVar)
     (IntBindingT TypeF (LogicT Q))
     (UTerm TypeF IntVar)
forall (t :: * -> *) v (m :: * -> *) e (em :: (* -> *) -> * -> *).
(BindingMonad t v m, Fallible t v e, MonadTrans em, Functor (em m),
 MonadError e (em m)) =>
UTerm t v -> UTerm t v -> em m (UTerm t v)
unify UTerm TypeF IntVar
m' UTerm TypeF IntVar
cmdM
                      ()
-> ExceptT
     (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
                Maybe
  (UTerm TypeF IntVar,
   ExceptT (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) (),
   ArgProvenance)
-> IntBindingT
     TypeF
     (LogicT Q)
     (Maybe
        (UTerm TypeF IntVar,
         ExceptT (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) (),
         ArgProvenance))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe
   (UTerm TypeF IntVar,
    ExceptT (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) (),
    ArgProvenance)
 -> IntBindingT
      TypeF
      (LogicT Q)
      (Maybe
         (UTerm TypeF IntVar,
          ExceptT (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) (),
          ArgProvenance)))
-> Maybe
     (UTerm TypeF IntVar,
      ExceptT (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) (),
      ArgProvenance)
-> IntBindingT
     TypeF
     (LogicT Q)
     (Maybe
        (UTerm TypeF IntVar,
         ExceptT (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) (),
         ArgProvenance))
forall a b. (a -> b) -> a -> b
$ (UTerm TypeF IntVar,
 ExceptT (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) (),
 ArgProvenance)
-> Maybe
     (UTerm TypeF IntVar,
      ExceptT (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) (),
      ArgProvenance)
forall a. a -> Maybe a
Just (UTerm TypeF IntVar
a', ExceptT (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) ()
predicate, Name -> Given -> ArgProvenance
Bound Name
v Given
g)
          _ -> Maybe
  (UTerm TypeF IntVar,
   ExceptT (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) (),
   ArgProvenance)
-> IntBindingT
     TypeF
     (LogicT Q)
     (Maybe
        (UTerm TypeF IntVar,
         ExceptT (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) (),
         ArgProvenance))
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe
  (UTerm TypeF IntVar,
   ExceptT (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) (),
   ArgProvenance)
forall a. Maybe a
Nothing
        [(UTerm TypeF IntVar,
  ExceptT (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) (),
  ArgProvenance)]
-> IntBindingT
     TypeF
     (LogicT Q)
     [(UTerm TypeF IntVar,
       ExceptT (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) (),
       ArgProvenance)]
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([(UTerm TypeF IntVar,
 ExceptT (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) (),
 ArgProvenance)
nonApp] [(UTerm TypeF IntVar,
  ExceptT (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) (),
  ArgProvenance)]
-> [(UTerm TypeF IntVar,
     ExceptT (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) (),
     ArgProvenance)]
-> [(UTerm TypeF IntVar,
     ExceptT (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) (),
     ArgProvenance)]
forall a. Semigroup a => a -> a -> a
<> Maybe
  (UTerm TypeF IntVar,
   ExceptT (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) (),
   ArgProvenance)
-> [(UTerm TypeF IntVar,
     ExceptT (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) (),
     ArgProvenance)]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Maybe
  (UTerm TypeF IntVar,
   ExceptT (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) (),
   ArgProvenance)
app)

      [Maybe ArgProvenance]
as <- [UTerm TypeF IntVar]
-> (UTerm TypeF IntVar
    -> IntBindingT TypeF (LogicT Q) (Maybe ArgProvenance))
-> IntBindingT TypeF (LogicT Q) [Maybe ArgProvenance]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [UTerm TypeF IntVar]
instArgs ((UTerm TypeF IntVar
  -> IntBindingT TypeF (LogicT Q) (Maybe ArgProvenance))
 -> IntBindingT TypeF (LogicT Q) [Maybe ArgProvenance])
-> (UTerm TypeF IntVar
    -> IntBindingT TypeF (LogicT Q) (Maybe ArgProvenance))
-> IntBindingT TypeF (LogicT Q) [Maybe ArgProvenance]
forall a b. (a -> b) -> a -> b
$ \argTy :: UTerm TypeF IntVar
argTy ->
        IntBindingT TypeF (LogicT Q) ArgProvenance
-> IntBindingT TypeF (LogicT Q) (Maybe ArgProvenance)
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
defaultMaybe (IntBindingT TypeF (LogicT Q) ArgProvenance
 -> IntBindingT TypeF (LogicT Q) (Maybe ArgProvenance))
-> ([IntBindingT TypeF (LogicT Q) ArgProvenance]
    -> IntBindingT TypeF (LogicT Q) ArgProvenance)
-> [IntBindingT TypeF (LogicT Q) ArgProvenance]
-> IntBindingT TypeF (LogicT Q) (Maybe ArgProvenance)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [IntBindingT TypeF (LogicT Q) ArgProvenance]
-> IntBindingT TypeF (LogicT Q) ArgProvenance
forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Alternative f) =>
t (f a) -> f a
asum ([IntBindingT TypeF (LogicT Q) ArgProvenance]
 -> IntBindingT TypeF (LogicT Q) (Maybe ArgProvenance))
-> [IntBindingT TypeF (LogicT Q) ArgProvenance]
-> IntBindingT TypeF (LogicT Q) (Maybe ArgProvenance)
forall a b. (a -> b) -> a -> b
$ [(UTerm TypeF IntVar,
  ExceptT (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) (),
  ArgProvenance)]
instGivens [(UTerm TypeF IntVar,
  ExceptT (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) (),
  ArgProvenance)]
-> ((UTerm TypeF IntVar,
     ExceptT (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) (),
     ArgProvenance)
    -> IntBindingT TypeF (LogicT Q) ArgProvenance)
-> [IntBindingT TypeF (LogicT Q) ArgProvenance]
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \(givenTy :: UTerm TypeF IntVar
givenTy, predicate :: ExceptT (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) ()
predicate, g :: ArgProvenance
g) -> do
          ExceptT (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) ()
-> IntBindingT TypeF (LogicT Q) ()
forall (m :: * -> *) b.
(Monad m, Alternative m) =>
ExceptT (UFailure TypeF IntVar) m b -> m b
errorToLogic (ExceptT (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) ()
 -> IntBindingT TypeF (LogicT Q) ())
-> ExceptT
     (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) ()
-> IntBindingT TypeF (LogicT Q) ()
forall a b. (a -> b) -> a -> b
$ do
            ExceptT (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) ()
predicate
            UTerm TypeF IntVar
freshGivenTy <- UTerm TypeF IntVar
-> ExceptT
     (UFailure TypeF IntVar)
     (IntBindingT TypeF (LogicT Q))
     (UTerm TypeF IntVar)
forall (t :: * -> *) v (m :: * -> *) e (em :: (* -> *) -> * -> *).
(BindingMonad t v m, Fallible t v e, MonadTrans em, Functor (em m),
 MonadError e (em m)) =>
UTerm t v -> em m (UTerm t v)
freshen UTerm TypeF IntVar
givenTy
            let u :: UnificationType
u = case ArgProvenance
g of
                  Bound     _ Given {..} -> UnificationType
gUnificationType
                  BoundPure _ Given {..} -> UnificationType
gUnificationType
                  Argument  _ _          -> UnificationType
Unifying
            case UnificationType
u of
              Unifying  -> ExceptT
  (UFailure TypeF IntVar)
  (IntBindingT TypeF (LogicT Q))
  (UTerm TypeF IntVar)
-> ExceptT
     (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (ExceptT
   (UFailure TypeF IntVar)
   (IntBindingT TypeF (LogicT Q))
   (UTerm TypeF IntVar)
 -> ExceptT
      (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) ())
-> ExceptT
     (UFailure TypeF IntVar)
     (IntBindingT TypeF (LogicT Q))
     (UTerm TypeF IntVar)
-> ExceptT
     (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) ()
forall a b. (a -> b) -> a -> b
$ UTerm TypeF IntVar
-> UTerm TypeF IntVar
-> ExceptT
     (UFailure TypeF IntVar)
     (IntBindingT TypeF (LogicT Q))
     (UTerm TypeF IntVar)
forall (t :: * -> *) v (m :: * -> *) e (em :: (* -> *) -> * -> *).
(BindingMonad t v m, Fallible t v e, MonadTrans em, Functor (em m),
 MonadError e (em m)) =>
UTerm t v -> UTerm t v -> em m (UTerm t v)
unify UTerm TypeF IntVar
freshGivenTy UTerm TypeF IntVar
argTy
              Subsuming -> do
                Bool
s <- UTerm TypeF IntVar
-> UTerm TypeF IntVar
-> ExceptT
     (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) Bool
forall (t :: * -> *) v (m :: * -> *) e (em :: (* -> *) -> * -> *).
(BindingMonad t v m, Fallible t v e, MonadTrans em, Functor (em m),
 MonadError e (em m)) =>
UTerm t v -> UTerm t v -> em m Bool
subsumes UTerm TypeF IntVar
freshGivenTy UTerm TypeF IntVar
argTy
                IntBindingT TypeF (LogicT Q) ()
-> ExceptT
     (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IntBindingT TypeF (LogicT Q) ()
 -> ExceptT
      (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) ())
-> IntBindingT TypeF (LogicT Q) ()
-> ExceptT
     (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) ()
forall a b. (a -> b) -> a -> b
$ Bool -> IntBindingT TypeF (LogicT Q) ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard Bool
s
          ArgProvenance -> IntBindingT TypeF (LogicT Q) ArgProvenance
forall (f :: * -> *) a. Applicative f => a -> f a
pure ArgProvenance
g

      -- If we used any monadic bindings, we must have a Monad instance for
      -- the return variable. If it's polymorphic then assume an instance.
      Bool
-> IntBindingT TypeF (LogicT Q) ()
-> IntBindingT TypeF (LogicT Q) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ((ArgProvenance -> Bool) -> [ArgProvenance] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ArgProvenance -> Bool
isMonadicBind ([Maybe ArgProvenance] -> [ArgProvenance]
forall a. [Maybe a] -> [a]
catMaybes [Maybe ArgProvenance]
as)) (IntBindingT TypeF (LogicT Q) ()
 -> IntBindingT TypeF (LogicT Q) ())
-> IntBindingT TypeF (LogicT Q) ()
-> IntBindingT TypeF (LogicT Q) ()
forall a b. (a -> b) -> a -> b
$ do
        UTerm TypeF IntVar
a    <- IntVar -> UTerm TypeF IntVar
forall (t :: * -> *) v. v -> UTerm t v
UVar (IntVar -> UTerm TypeF IntVar)
-> IntBindingT TypeF (LogicT Q) IntVar
-> IntBindingT TypeF (LogicT Q) (UTerm TypeF IntVar)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IntBindingT TypeF (LogicT Q) IntVar
forall (t :: * -> *) v (m :: * -> *). BindingMonad t v m => m v
freeVar
        UTerm TypeF IntVar
ret' <- ExceptT
  (UFailure TypeF IntVar)
  (IntBindingT TypeF (LogicT Q))
  (UTerm TypeF IntVar)
-> IntBindingT TypeF (LogicT Q) (UTerm TypeF IntVar)
forall (m :: * -> *) b.
(Monad m, Alternative m) =>
ExceptT (UFailure TypeF IntVar) m b -> m b
errorToLogic (ExceptT
   (UFailure TypeF IntVar)
   (IntBindingT TypeF (LogicT Q))
   (UTerm TypeF IntVar)
 -> IntBindingT TypeF (LogicT Q) (UTerm TypeF IntVar))
-> ExceptT
     (UFailure TypeF IntVar)
     (IntBindingT TypeF (LogicT Q))
     (UTerm TypeF IntVar)
-> IntBindingT TypeF (LogicT Q) (UTerm TypeF IntVar)
forall a b. (a -> b) -> a -> b
$ UTerm TypeF IntVar
-> UTerm TypeF IntVar
-> ExceptT
     (UFailure TypeF IntVar)
     (IntBindingT TypeF (LogicT Q))
     (UTerm TypeF IntVar)
forall (t :: * -> *) v (m :: * -> *) e (em :: (* -> *) -> * -> *).
(BindingMonad t v m, Fallible t v e, MonadTrans em, Functor (em m),
 MonadError e (em m)) =>
UTerm t v -> UTerm t v -> em m (UTerm t v)
unify UTerm TypeF IntVar
retInst (TypeF (UTerm TypeF IntVar) -> UTerm TypeF IntVar
forall (t :: * -> *) v. t (UTerm t v) -> UTerm t v
UTerm (UTerm TypeF IntVar
-> UTerm TypeF IntVar -> TypeF (UTerm TypeF IntVar)
forall a. a -> a -> TypeF a
AppF UTerm TypeF IntVar
cmdM UTerm TypeF IntVar
a))
        UTerm TypeF IntVar -> IntBindingT TypeF (LogicT Q) ()
quant UTerm TypeF IntVar
ret'
        Maybe (Fix TypeF)
retFrozen <- UTerm TypeF IntVar -> Maybe (Fix TypeF)
forall (t :: * -> *) v. Traversable t => UTerm t v -> Maybe (Fix t)
freeze (UTerm TypeF IntVar -> Maybe (Fix TypeF))
-> IntBindingT TypeF (LogicT Q) (UTerm TypeF IntVar)
-> IntBindingT TypeF (LogicT Q) (Maybe (Fix TypeF))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExceptT
  (UFailure TypeF IntVar)
  (IntBindingT TypeF (LogicT Q))
  (UTerm TypeF IntVar)
-> IntBindingT TypeF (LogicT Q) (UTerm TypeF IntVar)
forall (m :: * -> *) b.
(Monad m, Alternative m) =>
ExceptT (UFailure TypeF IntVar) m b -> m b
errorToLogic (UTerm TypeF IntVar
-> ExceptT
     (UFailure TypeF IntVar)
     (IntBindingT TypeF (LogicT Q))
     (UTerm TypeF IntVar)
forall (t :: * -> *) v (m :: * -> *) e (em :: (* -> *) -> * -> *).
(BindingMonad t v m, Fallible t v e, MonadTrans em, Functor (em m),
 MonadError e (em m)) =>
UTerm t v -> em m (UTerm t v)
applyBindings UTerm TypeF IntVar
ret')
        case Maybe (Fix TypeF)
retFrozen of
          Just (Fix (AppF m :: Fix TypeF
m _)) -> do
            let typeD :: DType
typeD = Fix TypeF -> DType
typeFtoD Fix TypeF
m
            Q Bool -> IntBindingT TypeF (LogicT Q) Bool
forall a. Q a -> IntBindingT TypeF (LogicT Q) a
liftQ (Name -> [Type] -> Q Bool
isInstance ''Applicative [DType -> Type
forall th ds. Desugar th ds => ds -> th
sweeten DType
typeD]) IntBindingT TypeF (LogicT Q) Bool
-> (Bool -> IntBindingT TypeF (LogicT Q) ())
-> IntBindingT TypeF (LogicT Q) ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
              False -> IntBindingT TypeF (LogicT Q) ()
forall (f :: * -> *) a. Alternative f => f a
empty
              True  -> () -> IntBindingT TypeF (LogicT Q) ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
          Nothing ->
            Q () -> IntBindingT TypeF (LogicT Q) ()
forall a. Q a -> IntBindingT TypeF (LogicT Q) a
liftQ
              (Q () -> IntBindingT TypeF (LogicT Q) ())
-> Q () -> IntBindingT TypeF (LogicT Q) ()
forall a b. (a -> b) -> a -> b
$ String -> Q ()
forall (m :: * -> *) a. MonadFail m => String -> m a
fail
                  "\"impossible\", return type didn't freeze while checking monadic bindings"
          _ -> IntBindingT TypeF (LogicT Q) ()
forall (f :: * -> *) a. Alternative f => f a
empty

      -- Guard on all the instances being satisfiable
      --
      -- This must come after the Monadic binding checker so that the (possibly
      -- new) return type has been constrained a little.
      [DType]
-> (DType -> IntBindingT TypeF (LogicT Q) ())
-> IntBindingT TypeF (LogicT Q) ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ [DType]
preds ((DType -> IntBindingT TypeF (LogicT Q) ())
 -> IntBindingT TypeF (LogicT Q) ())
-> (DType -> IntBindingT TypeF (LogicT Q) ())
-> IntBindingT TypeF (LogicT Q) ()
forall a b. (a -> b) -> a -> b
$ \pred :: DType
pred -> do

        -- Get the constraint with the correct unification variables
        UTerm TypeF IntVar
instPred <- (([Name], Fix TypeF) -> UTerm TypeF IntVar)
-> IntBindingT TypeF (LogicT Q) ([Name], Fix TypeF)
-> IntBindingT TypeF (LogicT Q) (UTerm TypeF IntVar)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([(Name, IntVar)] -> Fix TypeF -> UTerm TypeF IntVar
instWithVars [(Name, IntVar)]
cmdVars (Fix TypeF -> UTerm TypeF IntVar)
-> (([Name], Fix TypeF) -> Fix TypeF)
-> ([Name], Fix TypeF)
-> UTerm TypeF IntVar
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Name], Fix TypeF) -> Fix TypeF
forall a b. (a, b) -> b
snd) (IntBindingT TypeF (LogicT Q) ([Name], Fix TypeF)
 -> IntBindingT TypeF (LogicT Q) (UTerm TypeF IntVar))
-> (DType -> IntBindingT TypeF (LogicT Q) ([Name], Fix TypeF))
-> DType
-> IntBindingT TypeF (LogicT Q) (UTerm TypeF IntVar)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Q ([Name], Fix TypeF)
-> IntBindingT TypeF (LogicT Q) ([Name], Fix TypeF)
forall a. Q a -> IntBindingT TypeF (LogicT Q) a
liftQ (Q ([Name], Fix TypeF)
 -> IntBindingT TypeF (LogicT Q) ([Name], Fix TypeF))
-> (DType -> Q ([Name], Fix TypeF))
-> DType
-> IntBindingT TypeF (LogicT Q) ([Name], Fix TypeF)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DType -> Q ([Name], Fix TypeF)
forall (m :: * -> *). MonadFail m => DType -> m ([Name], Fix TypeF)
typeDtoF (DType -> IntBindingT TypeF (LogicT Q) (UTerm TypeF IntVar))
-> DType -> IntBindingT TypeF (LogicT Q) (UTerm TypeF IntVar)
forall a b. (a -> b) -> a -> b
$ DType
pred

        -- Quantify over any still free
        UTerm TypeF IntVar -> IntBindingT TypeF (LogicT Q) ()
quant UTerm TypeF IntVar
instPred

        -- Freeze it
        Maybe (Fix TypeF)
instFrozen <- UTerm TypeF IntVar -> Maybe (Fix TypeF)
forall (t :: * -> *) v. Traversable t => UTerm t v -> Maybe (Fix t)
freeze (UTerm TypeF IntVar -> Maybe (Fix TypeF))
-> IntBindingT TypeF (LogicT Q) (UTerm TypeF IntVar)
-> IntBindingT TypeF (LogicT Q) (Maybe (Fix TypeF))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExceptT
  (UFailure TypeF IntVar)
  (IntBindingT TypeF (LogicT Q))
  (UTerm TypeF IntVar)
-> IntBindingT TypeF (LogicT Q) (UTerm TypeF IntVar)
forall (m :: * -> *) b.
(Monad m, Alternative m) =>
ExceptT (UFailure TypeF IntVar) m b -> m b
errorToLogic (UTerm TypeF IntVar
-> ExceptT
     (UFailure TypeF IntVar)
     (IntBindingT TypeF (LogicT Q))
     (UTerm TypeF IntVar)
forall (t :: * -> *) v (m :: * -> *) e (em :: (* -> *) -> * -> *).
(BindingMonad t v m, Fallible t v e, MonadTrans em, Functor (em m),
 MonadError e (em m)) =>
UTerm t v -> em m (UTerm t v)
applyBindings UTerm TypeF IntVar
instPred)

        case Maybe (Fix TypeF)
instFrozen of
          Just f :: Fix TypeF
f -> do
            let (class' :: DType
class', predArgs :: [DTypeArg]
predArgs) = DType -> (DType, [DTypeArg])
unfoldDType (Fix TypeF -> DType
typeFtoD Fix TypeF
f)
                typeArgs :: [DType]
typeArgs           = [ DType
a | DTANormal a :: DType
a <- [DTypeArg]
predArgs ]
            Name
className <- case DType
class' of
              DConT n :: Name
n -> Name -> IntBindingT TypeF (LogicT Q) Name
forall (f :: * -> *) a. Applicative f => a -> f a
pure Name
n
              _ -> Q Name -> IntBindingT TypeF (LogicT Q) Name
forall a. Q a -> IntBindingT TypeF (LogicT Q) a
liftQ (Q Name -> IntBindingT TypeF (LogicT Q) Name)
-> Q Name -> IntBindingT TypeF (LogicT Q) Name
forall a b. (a -> b) -> a -> b
$ String -> Q Name
forall (m :: * -> *) a. MonadFail m => String -> m a
fail "unfolded predicate didn't begin with a ConT"

            -- Ignore when the name is a type family because of
            -- https://gitlab.haskell.org/ghc/ghc/issues/18153
            Q Info -> IntBindingT TypeF (LogicT Q) Info
forall a. Q a -> IntBindingT TypeF (LogicT Q) a
liftQ (Name -> Q Info
forall (q :: * -> *). (Quasi q, MonadFail q) => Name -> q Info
reifyWithWarning Name
className) IntBindingT TypeF (LogicT Q) Info
-> (Info -> IntBindingT TypeF (LogicT Q) ())
-> IntBindingT TypeF (LogicT Q) ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
              ClassI _ _ ->
                Q Bool -> IntBindingT TypeF (LogicT Q) Bool
forall a. Q a -> IntBindingT TypeF (LogicT Q) a
liftQ (Name -> [Type] -> Q Bool
isInstance Name
className (DType -> Type
forall th ds. Desugar th ds => ds -> th
sweeten (DType -> Type) -> [DType] -> [Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [DType]
typeArgs)) IntBindingT TypeF (LogicT Q) Bool
-> (Bool -> IntBindingT TypeF (LogicT Q) ())
-> IntBindingT TypeF (LogicT Q) ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
                  False -> IntBindingT TypeF (LogicT Q) ()
forall (f :: * -> *) a. Alternative f => f a
empty
                  True  -> () -> IntBindingT TypeF (LogicT Q) ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
              FamilyI _ _ -> () -> IntBindingT TypeF (LogicT Q) ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
              _ -> Q () -> IntBindingT TypeF (LogicT Q) ()
forall a. Q a -> IntBindingT TypeF (LogicT Q) a
liftQ (Q () -> IntBindingT TypeF (LogicT Q) ())
-> Q () -> IntBindingT TypeF (LogicT Q) ()
forall a b. (a -> b) -> a -> b
$ String -> Q ()
forall (m :: * -> *) a. MonadFail m => String -> m a
fail "Predicate name isn't a class or a type family"
          Nothing ->
            Q () -> IntBindingT TypeF (LogicT Q) ()
forall a. Q a -> IntBindingT TypeF (LogicT Q) a
liftQ
              (Q () -> IntBindingT TypeF (LogicT Q) ())
-> Q () -> IntBindingT TypeF (LogicT Q) ()
forall a b. (a -> b) -> a -> b
$ String -> Q ()
forall (m :: * -> *) a. MonadFail m => String -> m a
fail
                  "\"impossible\": predicate didn't freeze while checking predicates"


      [(DType, Maybe ArgProvenance)]
-> ((DType, Maybe ArgProvenance)
    -> IntBindingT TypeF (LogicT Q) ArgProvenance)
-> IntBindingT TypeF (LogicT Q) [ArgProvenance]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for ([DType] -> [Maybe ArgProvenance] -> [(DType, Maybe ArgProvenance)]
forall a b. [a] -> [b] -> [(a, b)]
zip [DType]
args [Maybe ArgProvenance]
as) (((DType, Maybe ArgProvenance)
  -> IntBindingT TypeF (LogicT Q) ArgProvenance)
 -> IntBindingT TypeF (LogicT Q) [ArgProvenance])
-> ((DType, Maybe ArgProvenance)
    -> IntBindingT TypeF (LogicT Q) ArgProvenance)
-> IntBindingT TypeF (LogicT Q) [ArgProvenance]
forall a b. (a -> b) -> a -> b
$ \case
        (_, Just p :: ArgProvenance
p ) -> ArgProvenance -> IntBindingT TypeF (LogicT Q) ArgProvenance
forall (f :: * -> *) a. Applicative f => a -> f a
pure ArgProvenance
p
        (t :: DType
t, Nothing) -> (Name -> DType -> ArgProvenance
`Argument` DType
t) (Name -> ArgProvenance)
-> IntBindingT TypeF (LogicT Q) Name
-> IntBindingT TypeF (LogicT Q) ArgProvenance
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Q Name -> IntBindingT TypeF (LogicT Q) Name
forall a. Q a -> IntBindingT TypeF (LogicT Q) a
liftQ (String -> Q Name
newName "a")

  [ArgProvenance]
argProvenances <-
    String -> Maybe [ArgProvenance] -> Q [ArgProvenance]
forall (m :: * -> *) a. MonadFail m => String -> Maybe a -> m a
note
      "\"Impossible\" Finding argument provenances failed (unless the function context containts a class with no instances)"
    (Maybe [ArgProvenance] -> Q [ArgProvenance])
-> ([[ArgProvenance]] -> Maybe [ArgProvenance])
-> [[ArgProvenance]]
-> Q [ArgProvenance]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.   [[ArgProvenance]] -> Maybe [ArgProvenance]
forall a. [a] -> Maybe a
listToMaybe
    ([[ArgProvenance]] -> Q [ArgProvenance])
-> Q [[ArgProvenance]] -> Q [ArgProvenance]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Int -> LogicT Q [ArgProvenance] -> Q [[ArgProvenance]]
forall (m :: * -> *) a. Monad m => Int -> LogicT m a -> m [a]
observeManyT 1 LogicT Q [ArgProvenance]
genProvs
  Bool -> Q () -> Q ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([ArgProvenance] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [ArgProvenance]
argProvenances Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [DType] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [DType]
args) (Q () -> Q ()) -> Q () -> Q ()
forall a b. (a -> b) -> a -> b
$ String -> Q ()
forall (m :: * -> *) a. MonadFail m => String -> m a
fail
    "\"Impossible\", incorrect number of argument provenances were found"

  let bindGiven :: ArgProvenance -> Maybe Stmt
bindGiven = \case
        BoundPure _ _ -> Maybe Stmt
forall a. Maybe a
Nothing
        Bound     n :: Name
n g :: Given
g -> Stmt -> Maybe Stmt
forall a. a -> Maybe a
Just (Stmt -> Maybe Stmt) -> Stmt -> Maybe Stmt
forall a b. (a -> b) -> a -> b
$ Pat -> Exp -> Stmt
BindS (Name -> Pat
VarP Name
n) (Name -> Exp
VarE (Given -> Name
gName Given
g))
        Argument  _ _ -> Maybe Stmt
forall a. Maybe a
Nothing
      bs :: [Stmt]
bs   = [Maybe Stmt] -> [Stmt]
forall a. [Maybe a] -> [a]
catMaybes (ArgProvenance -> Maybe Stmt
bindGiven (ArgProvenance -> Maybe Stmt) -> [ArgProvenance] -> [Maybe Stmt]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [ArgProvenance]
argProvenances)
      ret' :: DExp
ret' = DExp -> [DExp] -> DExp
applyDExp
        (Name -> DExp
DVarE (Function -> Name
fName Function
fun))
        ([ArgProvenance]
argProvenances [ArgProvenance] -> (ArgProvenance -> DExp) -> [DExp]
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case
          Bound     n :: Name
n _             -> Name -> DExp
DVarE Name
n
          BoundPure _ (Given _ n :: Name
n _) -> Name -> DExp
DVarE Name
n
          Argument  n :: Name
n _             -> Name -> DExp
DVarE Name
n
        )
  DExp
exp' <- [Stmt] -> Q DExp
forall (q :: * -> *). DsMonad q => [Stmt] -> q DExp
dsDoStmts ([Stmt]
bs [Stmt] -> [Stmt] -> [Stmt]
forall a. Semigroup a => a -> a -> a
<> [Exp -> Stmt
NoBindS (DExp -> Exp
forall th ds. Desugar th ds => ds -> th
sweeten DExp
ret')])

  -- Typing the arguments here is important, if we don't then some skolems
  -- might escape!
  --
  -- Consider wrapping @f :: (forall a. a) -> ()@ (and supplying no arguments).
  -- We end up with the splice @myF x = f x@, and the @a@ in the argument to
  -- @f@ escapes. We can fix this by typing the pattern explicitly, thusly @myF
  -- (x :: forall a. a) = f x@
  Exp -> Q Exp
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Exp -> Q Exp) -> Exp -> Q Exp
forall a b. (a -> b) -> a -> b
$ [Pat] -> Exp -> Exp
LamE [ Pat -> Type -> Pat
SigP (Name -> Pat
VarP Name
n) (DType -> Type
forall th ds. Desugar th ds => ds -> th
sweeten DType
t) | Argument n :: Name
n t :: DType
t <- [ArgProvenance]
argProvenances ]
              (DExp -> Exp
forall th ds. Desugar th ds => ds -> th
sweeten DExp
exp')

data ArgProvenance
  = Bound Name Given
    -- ^ Comes from a monadic binding
  | BoundPure Name Given
    -- ^ Comes from a pure binding, i.e. let ... in
  | Argument Name DType
    -- ^ Comes from an argument to the wrapped function
  deriving (Int -> ArgProvenance -> String -> String
[ArgProvenance] -> String -> String
ArgProvenance -> String
(Int -> ArgProvenance -> String -> String)
-> (ArgProvenance -> String)
-> ([ArgProvenance] -> String -> String)
-> Show ArgProvenance
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [ArgProvenance] -> String -> String
$cshowList :: [ArgProvenance] -> String -> String
show :: ArgProvenance -> String
$cshow :: ArgProvenance -> String
showsPrec :: Int -> ArgProvenance -> String -> String
$cshowsPrec :: Int -> ArgProvenance -> String -> String
Show)

isMonadicBind :: ArgProvenance -> Bool
isMonadicBind :: ArgProvenance -> Bool
isMonadicBind = \case
  Bound _ _ -> Bool
True
  _         -> Bool
False

----------------------------------------------------------------
-- Haskell types as a fixed point of TypeF
----------------------------------------------------------------

data TypeF a
  = AppF a a
  | VarF Name
  | ConF Name
  | ArrowF
  | LitF TyLit
  deriving (Int -> TypeF a -> String -> String
[TypeF a] -> String -> String
TypeF a -> String
(Int -> TypeF a -> String -> String)
-> (TypeF a -> String)
-> ([TypeF a] -> String -> String)
-> Show (TypeF a)
forall a. Show a => Int -> TypeF a -> String -> String
forall a. Show a => [TypeF a] -> String -> String
forall a. Show a => TypeF a -> String
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [TypeF a] -> String -> String
$cshowList :: forall a. Show a => [TypeF a] -> String -> String
show :: TypeF a -> String
$cshow :: forall a. Show a => TypeF a -> String
showsPrec :: Int -> TypeF a -> String -> String
$cshowsPrec :: forall a. Show a => Int -> TypeF a -> String -> String
Show, a -> TypeF b -> TypeF a
(a -> b) -> TypeF a -> TypeF b
(forall a b. (a -> b) -> TypeF a -> TypeF b)
-> (forall a b. a -> TypeF b -> TypeF a) -> Functor TypeF
forall a b. a -> TypeF b -> TypeF a
forall a b. (a -> b) -> TypeF a -> TypeF b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> TypeF b -> TypeF a
$c<$ :: forall a b. a -> TypeF b -> TypeF a
fmap :: (a -> b) -> TypeF a -> TypeF b
$cfmap :: forall a b. (a -> b) -> TypeF a -> TypeF b
Functor, TypeF a -> Bool
(a -> m) -> TypeF a -> m
(a -> b -> b) -> b -> TypeF a -> b
(forall m. Monoid m => TypeF m -> m)
-> (forall m a. Monoid m => (a -> m) -> TypeF a -> m)
-> (forall m a. Monoid m => (a -> m) -> TypeF a -> m)
-> (forall a b. (a -> b -> b) -> b -> TypeF a -> b)
-> (forall a b. (a -> b -> b) -> b -> TypeF a -> b)
-> (forall b a. (b -> a -> b) -> b -> TypeF a -> b)
-> (forall b a. (b -> a -> b) -> b -> TypeF a -> b)
-> (forall a. (a -> a -> a) -> TypeF a -> a)
-> (forall a. (a -> a -> a) -> TypeF a -> a)
-> (forall a. TypeF a -> [a])
-> (forall a. TypeF a -> Bool)
-> (forall a. TypeF a -> Int)
-> (forall a. Eq a => a -> TypeF a -> Bool)
-> (forall a. Ord a => TypeF a -> a)
-> (forall a. Ord a => TypeF a -> a)
-> (forall a. Num a => TypeF a -> a)
-> (forall a. Num a => TypeF a -> a)
-> Foldable TypeF
forall a. Eq a => a -> TypeF a -> Bool
forall a. Num a => TypeF a -> a
forall a. Ord a => TypeF a -> a
forall m. Monoid m => TypeF m -> m
forall a. TypeF a -> Bool
forall a. TypeF a -> Int
forall a. TypeF a -> [a]
forall a. (a -> a -> a) -> TypeF a -> a
forall m a. Monoid m => (a -> m) -> TypeF a -> m
forall b a. (b -> a -> b) -> b -> TypeF a -> b
forall a b. (a -> b -> b) -> b -> TypeF a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: TypeF a -> a
$cproduct :: forall a. Num a => TypeF a -> a
sum :: TypeF a -> a
$csum :: forall a. Num a => TypeF a -> a
minimum :: TypeF a -> a
$cminimum :: forall a. Ord a => TypeF a -> a
maximum :: TypeF a -> a
$cmaximum :: forall a. Ord a => TypeF a -> a
elem :: a -> TypeF a -> Bool
$celem :: forall a. Eq a => a -> TypeF a -> Bool
length :: TypeF a -> Int
$clength :: forall a. TypeF a -> Int
null :: TypeF a -> Bool
$cnull :: forall a. TypeF a -> Bool
toList :: TypeF a -> [a]
$ctoList :: forall a. TypeF a -> [a]
foldl1 :: (a -> a -> a) -> TypeF a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> TypeF a -> a
foldr1 :: (a -> a -> a) -> TypeF a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> TypeF a -> a
foldl' :: (b -> a -> b) -> b -> TypeF a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> TypeF a -> b
foldl :: (b -> a -> b) -> b -> TypeF a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> TypeF a -> b
foldr' :: (a -> b -> b) -> b -> TypeF a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> TypeF a -> b
foldr :: (a -> b -> b) -> b -> TypeF a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> TypeF a -> b
foldMap' :: (a -> m) -> TypeF a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> TypeF a -> m
foldMap :: (a -> m) -> TypeF a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> TypeF a -> m
fold :: TypeF m -> m
$cfold :: forall m. Monoid m => TypeF m -> m
Foldable, Functor TypeF
Foldable TypeF
(Functor TypeF, Foldable TypeF) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> TypeF a -> f (TypeF b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    TypeF (f a) -> f (TypeF a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> TypeF a -> m (TypeF b))
-> (forall (m :: * -> *) a. Monad m => TypeF (m a) -> m (TypeF a))
-> Traversable TypeF
(a -> f b) -> TypeF a -> f (TypeF b)
forall (t :: * -> *).
(Functor t, Foldable t) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => TypeF (m a) -> m (TypeF a)
forall (f :: * -> *) a. Applicative f => TypeF (f a) -> f (TypeF a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> TypeF a -> m (TypeF b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> TypeF a -> f (TypeF b)
sequence :: TypeF (m a) -> m (TypeF a)
$csequence :: forall (m :: * -> *) a. Monad m => TypeF (m a) -> m (TypeF a)
mapM :: (a -> m b) -> TypeF a -> m (TypeF b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> TypeF a -> m (TypeF b)
sequenceA :: TypeF (f a) -> f (TypeF a)
$csequenceA :: forall (f :: * -> *) a. Applicative f => TypeF (f a) -> f (TypeF a)
traverse :: (a -> f b) -> TypeF a -> f (TypeF b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> TypeF a -> f (TypeF b)
$cp2Traversable :: Foldable TypeF
$cp1Traversable :: Functor TypeF
Traversable)

-- TODO: Derive this with generics
instance Unifiable TypeF where
  zipMatch :: TypeF a -> TypeF a -> Maybe (TypeF (Either a (a, a)))
zipMatch (AppF l1 :: a
l1 r1 :: a
r1) (AppF l2 :: a
l2 r2 :: a
r2) =
    TypeF (Either a (a, a)) -> Maybe (TypeF (Either a (a, a)))
forall a. a -> Maybe a
Just (Either a (a, a) -> Either a (a, a) -> TypeF (Either a (a, a))
forall a. a -> a -> TypeF a
AppF ((a, a) -> Either a (a, a)
forall a b. b -> Either a b
Right (a
l1, a
l2)) ((a, a) -> Either a (a, a)
forall a b. b -> Either a b
Right (a
r1, a
r2)))
  zipMatch (VarF n1 :: Name
n1) (VarF n2 :: Name
n2) | Name
n1 Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
n2 = TypeF (Either a (a, a)) -> Maybe (TypeF (Either a (a, a)))
forall a. a -> Maybe a
Just (Name -> TypeF (Either a (a, a))
forall a. Name -> TypeF a
VarF Name
n1)
  zipMatch (ConF n1 :: Name
n1) (ConF n2 :: Name
n2) | Name
n1 Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
n2 = TypeF (Either a (a, a)) -> Maybe (TypeF (Either a (a, a)))
forall a. a -> Maybe a
Just (Name -> TypeF (Either a (a, a))
forall a. Name -> TypeF a
ConF Name
n1)
  zipMatch ArrowF ArrowF                  = TypeF (Either a (a, a)) -> Maybe (TypeF (Either a (a, a)))
forall a. a -> Maybe a
Just TypeF (Either a (a, a))
forall a. TypeF a
ArrowF
  zipMatch (LitF l1 :: TyLit
l1) (LitF l2 :: TyLit
l2) | TyLit
l1 TyLit -> TyLit -> Bool
forall a. Eq a => a -> a -> Bool
== TyLit
l2 = TypeF (Either a (a, a)) -> Maybe (TypeF (Either a (a, a)))
forall a. a -> Maybe a
Just (TyLit -> TypeF (Either a (a, a))
forall a. TyLit -> TypeF a
LitF TyLit
l1)
  zipMatch _ _                            = Maybe (TypeF (Either a (a, a)))
forall a. Maybe a
Nothing

-- | Returns the type as a @Fix TypeF@ along with any quantified names. Drops
-- any context.
typeDtoF :: MonadFail m => DType -> m ([Name], Fix TypeF)
typeDtoF :: DType -> m ([Name], Fix TypeF)
typeDtoF = (DType -> m (Fix TypeF))
-> ([Name], DType) -> m ([Name], Fix TypeF)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse DType -> m (Fix TypeF)
go (([Name], DType) -> m ([Name], Fix TypeF))
-> (DType -> ([Name], DType)) -> DType -> m ([Name], Fix TypeF)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DType -> ([Name], DType)
stripForall
 where
  go :: DType -> m (Fix TypeF)
go = \case
    DForallT{}      -> String -> m (Fix TypeF)
forall (m :: * -> *) a. MonadFail m => String -> m a
fail "TODO: Higher ranked types"
    DConstrainedT{} -> String -> m (Fix TypeF)
forall (m :: * -> *) a. MonadFail m => String -> m a
fail "TODO: Higher ranked types"
    DAppT l :: DType
l r :: DType
r       -> do
      Fix TypeF
l' <- DType -> m (Fix TypeF)
go DType
l
      Fix TypeF
r' <- DType -> m (Fix TypeF)
go DType
r
      Fix TypeF -> m (Fix TypeF)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Fix TypeF -> m (Fix TypeF)) -> Fix TypeF -> m (Fix TypeF)
forall a b. (a -> b) -> a -> b
$ TypeF (Fix TypeF) -> Fix TypeF
forall (f :: * -> *). f (Fix f) -> Fix f
Fix (Fix TypeF -> Fix TypeF -> TypeF (Fix TypeF)
forall a. a -> a -> TypeF a
AppF Fix TypeF
l' Fix TypeF
r')
    DAppKindT t :: DType
t _ -> DType -> m (Fix TypeF)
go DType
t
    DSigT     t :: DType
t _ -> DType -> m (Fix TypeF)
go DType
t
    DVarT n :: Name
n       -> Fix TypeF -> m (Fix TypeF)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Fix TypeF -> m (Fix TypeF))
-> (TypeF (Fix TypeF) -> Fix TypeF)
-> TypeF (Fix TypeF)
-> m (Fix TypeF)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeF (Fix TypeF) -> Fix TypeF
forall (f :: * -> *). f (Fix f) -> Fix f
Fix (TypeF (Fix TypeF) -> m (Fix TypeF))
-> TypeF (Fix TypeF) -> m (Fix TypeF)
forall a b. (a -> b) -> a -> b
$ Name -> TypeF (Fix TypeF)
forall a. Name -> TypeF a
VarF Name
n
    DConT n :: Name
n       -> Fix TypeF -> m (Fix TypeF)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Fix TypeF -> m (Fix TypeF))
-> (TypeF (Fix TypeF) -> Fix TypeF)
-> TypeF (Fix TypeF)
-> m (Fix TypeF)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeF (Fix TypeF) -> Fix TypeF
forall (f :: * -> *). f (Fix f) -> Fix f
Fix (TypeF (Fix TypeF) -> m (Fix TypeF))
-> TypeF (Fix TypeF) -> m (Fix TypeF)
forall a b. (a -> b) -> a -> b
$ Name -> TypeF (Fix TypeF)
forall a. Name -> TypeF a
ConF Name
n
    DArrowT       -> Fix TypeF -> m (Fix TypeF)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Fix TypeF -> m (Fix TypeF))
-> (TypeF (Fix TypeF) -> Fix TypeF)
-> TypeF (Fix TypeF)
-> m (Fix TypeF)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeF (Fix TypeF) -> Fix TypeF
forall (f :: * -> *). f (Fix f) -> Fix f
Fix (TypeF (Fix TypeF) -> m (Fix TypeF))
-> TypeF (Fix TypeF) -> m (Fix TypeF)
forall a b. (a -> b) -> a -> b
$ TypeF (Fix TypeF)
forall a. TypeF a
ArrowF
    DLitT l :: TyLit
l       -> Fix TypeF -> m (Fix TypeF)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Fix TypeF -> m (Fix TypeF))
-> (TypeF (Fix TypeF) -> Fix TypeF)
-> TypeF (Fix TypeF)
-> m (Fix TypeF)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeF (Fix TypeF) -> Fix TypeF
forall (f :: * -> *). f (Fix f) -> Fix f
Fix (TypeF (Fix TypeF) -> m (Fix TypeF))
-> TypeF (Fix TypeF) -> m (Fix TypeF)
forall a b. (a -> b) -> a -> b
$ TyLit -> TypeF (Fix TypeF)
forall a. TyLit -> TypeF a
LitF TyLit
l
    DWildCardT    -> String -> m (Fix TypeF)
forall (m :: * -> *) a. MonadFail m => String -> m a
fail "TODO: Wildcards"

typeFtoD :: Fix TypeF -> DType
typeFtoD :: Fix TypeF -> DType
typeFtoD = Fix TypeF -> TypeF (Fix TypeF)
forall (f :: * -> *). Fix f -> f (Fix f)
unFix (Fix TypeF -> TypeF (Fix TypeF))
-> (TypeF (Fix TypeF) -> DType) -> Fix TypeF -> DType
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> \case
  AppF l :: Fix TypeF
l r :: Fix TypeF
r -> DType -> DType -> DType
DAppT (Fix TypeF -> DType
typeFtoD Fix TypeF
l) (Fix TypeF -> DType
typeFtoD Fix TypeF
r)
  VarF n :: Name
n   -> Name -> DType
DVarT Name
n
  ConF n :: Name
n   -> Name -> DType
DConT Name
n
  ArrowF   -> DType
DArrowT
  LitF l :: TyLit
l   -> TyLit -> DType
DLitT TyLit
l

varBndrName :: DTyVarBndr -> Name
varBndrName :: DTyVarBndr -> Name
varBndrName = \case
  DPlainTV n :: Name
n    -> Name
n
  DKindedTV n :: Name
n _ -> Name
n

-- | Raise foralls on the spine of the function type to the top
--
-- For example @forall a. a -> forall b. b@ becomes @forall a b. a -> b@
raiseForalls :: DType -> DType
raiseForalls :: DType -> DType
raiseForalls = DType -> ([DTyVarBndr], [DType], DType)
go (DType -> ([DTyVarBndr], [DType], DType))
-> (([DTyVarBndr], [DType], DType) -> DType) -> DType -> DType
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> \case
  (vs :: [DTyVarBndr]
vs, ctx :: [DType]
ctx, t :: DType
t) -> ForallVisFlag -> [DTyVarBndr] -> DType -> DType
DForallT ForallVisFlag
ForallVis [DTyVarBndr]
vs (DType -> DType) -> (DType -> DType) -> DType -> DType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [DType] -> DType -> DType
DConstrainedT [DType]
ctx (DType -> DType) -> DType -> DType
forall a b. (a -> b) -> a -> b
$ DType
t
 where
  go :: DType -> ([DTyVarBndr], [DType], DType)
go = \case
    DForallT _ vs :: [DTyVarBndr]
vs t :: DType
t -> let (vs' :: [DTyVarBndr]
vs', ctx' :: [DType]
ctx', t' :: DType
t') = DType -> ([DTyVarBndr], [DType], DType)
go DType
t in ([DTyVarBndr]
vs [DTyVarBndr] -> [DTyVarBndr] -> [DTyVarBndr]
forall a. Semigroup a => a -> a -> a
<> [DTyVarBndr]
vs', [DType]
ctx', DType
t')
    DConstrainedT ctx :: [DType]
ctx t :: DType
t ->
      let (vs' :: [DTyVarBndr]
vs', ctx' :: [DType]
ctx', t' :: DType
t') = DType -> ([DTyVarBndr], [DType], DType)
go DType
t in ([DTyVarBndr]
vs', [DType]
ctx [DType] -> [DType] -> [DType]
forall a. Semigroup a => a -> a -> a
<> [DType]
ctx', DType
t')
    l :: DType
l :~> r :: DType
r -> let (vs :: [DTyVarBndr]
vs, ctx :: [DType]
ctx, r' :: DType
r') = DType -> ([DTyVarBndr], [DType], DType)
go DType
r in ([DTyVarBndr]
vs, [DType]
ctx, DType
l DType -> DType -> DType
:~> DType
r')
    t :: DType
t       -> ([], [], DType
t)

pattern (:~>) :: DType -> DType -> DType
pattern l $b:~> :: DType -> DType -> DType
$m:~> :: forall r. DType -> (DType -> DType -> r) -> (Void# -> r) -> r
:~> r = DArrowT `DAppT` l `DAppT` r

-- | Instantiate a type with unification variables
inst
  :: BindingMonad TypeF IntVar m
  => [Name]
  -> Fix TypeF
  -> m (UTerm TypeF IntVar)
inst :: [Name] -> Fix TypeF -> m (UTerm TypeF IntVar)
inst ns :: [Name]
ns t :: Fix TypeF
t = do
  [(Name, IntVar)]
vs <- [m (Name, IntVar)] -> m [(Name, IntVar)]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [ (Name
n, ) (IntVar -> (Name, IntVar)) -> m IntVar -> m (Name, IntVar)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m IntVar
forall (t :: * -> *) v (m :: * -> *). BindingMonad t v m => m v
freeVar | Name
n <- [Name]
ns ]
  UTerm TypeF IntVar -> m (UTerm TypeF IntVar)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (UTerm TypeF IntVar -> m (UTerm TypeF IntVar))
-> UTerm TypeF IntVar -> m (UTerm TypeF IntVar)
forall a b. (a -> b) -> a -> b
$ [(Name, IntVar)] -> Fix TypeF -> UTerm TypeF IntVar
instWithVars [(Name, IntVar)]
vs Fix TypeF
t

-- | Instantiate a type with unification variables
instWithVars :: [(Name, IntVar)] -> Fix TypeF -> UTerm TypeF IntVar
instWithVars :: [(Name, IntVar)] -> Fix TypeF -> UTerm TypeF IntVar
instWithVars vs :: [(Name, IntVar)]
vs t :: Fix TypeF
t =
  let go :: Fix TypeF -> UTerm TypeF IntVar
go (Fix f :: TypeF (Fix TypeF)
f) = case TypeF (Fix TypeF)
f of
        AppF l :: Fix TypeF
l r :: Fix TypeF
r                       -> TypeF (UTerm TypeF IntVar) -> UTerm TypeF IntVar
forall (t :: * -> *) v. t (UTerm t v) -> UTerm t v
UTerm (UTerm TypeF IntVar
-> UTerm TypeF IntVar -> TypeF (UTerm TypeF IntVar)
forall a. a -> a -> TypeF a
AppF (Fix TypeF -> UTerm TypeF IntVar
go Fix TypeF
l) (Fix TypeF -> UTerm TypeF IntVar
go Fix TypeF
r))
        VarF n :: Name
n | Just v :: IntVar
v <- Name -> [(Name, IntVar)] -> Maybe IntVar
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n [(Name, IntVar)]
vs -> IntVar -> UTerm TypeF IntVar
forall (t :: * -> *) v. v -> UTerm t v
UVar IntVar
v
        VarF n :: Name
n                         -> TypeF (UTerm TypeF IntVar) -> UTerm TypeF IntVar
forall (t :: * -> *) v. t (UTerm t v) -> UTerm t v
UTerm (Name -> TypeF (UTerm TypeF IntVar)
forall a. Name -> TypeF a
VarF Name
n)
        ConF n :: Name
n                         -> TypeF (UTerm TypeF IntVar) -> UTerm TypeF IntVar
forall (t :: * -> *) v. t (UTerm t v) -> UTerm t v
UTerm (Name -> TypeF (UTerm TypeF IntVar)
forall a. Name -> TypeF a
ConF Name
n)
        ArrowF                         -> TypeF (UTerm TypeF IntVar) -> UTerm TypeF IntVar
forall (t :: * -> *) v. t (UTerm t v) -> UTerm t v
UTerm TypeF (UTerm TypeF IntVar)
forall a. TypeF a
ArrowF
        LitF l :: TyLit
l                         -> TypeF (UTerm TypeF IntVar) -> UTerm TypeF IntVar
forall (t :: * -> *) v. t (UTerm t v) -> UTerm t v
UTerm (TyLit -> TypeF (UTerm TypeF IntVar)
forall a. TyLit -> TypeF a
LitF TyLit
l)
  in  Fix TypeF -> UTerm TypeF IntVar
go Fix TypeF
t

----------------------------------------------------------------
-- Utils
----------------------------------------------------------------

reifyVal :: String -> Name -> Q (Name, DType)
reifyVal :: String -> Name -> Q (Name, DType)
reifyVal d :: String
d n :: Name
n = Name -> Q (Maybe DInfo)
forall (q :: * -> *). DsMonad q => Name -> q (Maybe DInfo)
dsReify Name
n Q (Maybe DInfo)
-> (Maybe DInfo -> Q (Name, DType)) -> Q (Name, DType)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  Just (DVarI name :: Name
name ty :: DType
ty _) -> (Name, DType) -> Q (Name, DType)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Name
name, DType
ty)
  _                      -> String -> Q (Name, DType)
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> Q (Name, DType)) -> String -> Q (Name, DType)
forall a b. (a -> b) -> a -> b
$ String
d String -> String -> String
forall a. Semigroup a => a -> a -> a
<> " " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Name -> String
forall a. Show a => a -> String
show Name
n String -> String -> String
forall a. Semigroup a => a -> a -> a
<> " isn't a value"

stripForall :: DType -> ([Name], DType)
stripForall :: DType -> ([Name], DType)
stripForall = DType -> DType
raiseForalls (DType -> DType)
-> (DType -> ([Name], DType)) -> DType -> ([Name], DType)
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> \case
  DForallT _ vs :: [DTyVarBndr]
vs (DConstrainedT _ ty :: DType
ty) -> (DTyVarBndr -> Name
varBndrName (DTyVarBndr -> Name) -> [DTyVarBndr] -> [Name]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [DTyVarBndr]
vs, DType
ty)
  DForallT _ vs :: [DTyVarBndr]
vs ty :: DType
ty   -> (DTyVarBndr -> Name
varBndrName (DTyVarBndr -> Name) -> [DTyVarBndr] -> [Name]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [DTyVarBndr]
vs, DType
ty)
  DConstrainedT _ ty :: DType
ty -> ([], DType
ty)
  ty :: DType
ty                 -> ([], DType
ty)

unravel :: DType -> ([DTyVarBndr], [DPred], [DType], DType)
unravel :: DType -> ([DTyVarBndr], [DType], [DType], DType)
unravel t :: DType
t =
  let (argList :: DFunArgs
argList, ret :: DType
ret) = DType -> (DFunArgs, DType)
unravelDType DType
t
      go :: DFunArgs -> ([DTyVarBndr], [DType], [DType])
go             = \case
        DFANil             -> ([], [], [])
        DFAForalls _ vs :: [DTyVarBndr]
vs as :: DFunArgs
as -> ([DTyVarBndr]
vs, [], []) ([DTyVarBndr], [DType], [DType])
-> ([DTyVarBndr], [DType], [DType])
-> ([DTyVarBndr], [DType], [DType])
forall a. Semigroup a => a -> a -> a
<> DFunArgs -> ([DTyVarBndr], [DType], [DType])
go DFunArgs
as
        DFACxt  preds :: [DType]
preds as :: DFunArgs
as   -> ([], [DType]
preds, []) ([DTyVarBndr], [DType], [DType])
-> ([DTyVarBndr], [DType], [DType])
-> ([DTyVarBndr], [DType], [DType])
forall a. Semigroup a => a -> a -> a
<> DFunArgs -> ([DTyVarBndr], [DType], [DType])
go DFunArgs
as
        DFAAnon a :: DType
a     as :: DFunArgs
as   -> ([], [], [DType
a]) ([DTyVarBndr], [DType], [DType])
-> ([DTyVarBndr], [DType], [DType])
-> ([DTyVarBndr], [DType], [DType])
forall a. Semigroup a => a -> a -> a
<> DFunArgs -> ([DTyVarBndr], [DType], [DType])
go DFunArgs
as
  in  let (vs :: [DTyVarBndr]
vs, preds :: [DType]
preds, args :: [DType]
args) = DFunArgs -> ([DTyVarBndr], [DType], [DType])
go DFunArgs
argList in ([DTyVarBndr]
vs, [DType]
preds, [DType]
args, DType
ret)

note :: MonadFail m => String -> Maybe a -> m a
note :: String -> Maybe a -> m a
note s :: String
s = m a -> (a -> m a) -> Maybe a -> m a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (String -> m a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
s) a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure