module AutoApply
  ( autoapply
  , autoapplyDecs
  ) where

import           Control.Applicative
import           Control.Arrow                  ( (>>>) )
import           Control.Monad
import           Control.Monad.Logic            ( LogicT
                                                , observeManyT
                                                )
import           Control.Monad.Logic.Class      ( ifte )
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

-- | @autoapply args fun@ creates an expression which is equal to @fun@ applied
-- to as many of the values in @args@ as possible.
autoapply :: [Name] -> Name -> Q Exp
autoapply :: [Name] -> Name -> Q Exp
autoapply givens :: [Name]
givens fun :: Name
fun = do
  [Given]
givenInfos <- [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]
givens ((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 Name -> DType -> Given
Given) (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]
givenInfos Function
funInfo

-- | @autoapplyDecs mkName args funs@ will wrap every function in @funs@ by
-- applying it to as many of the values in @args@ as possible. The new function
-- name will be @mkName@ applied to the wrapped function name.
--
-- 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) -> [Name] -> [Name] -> Q [Dec]
autoapplyDecs :: (String -> String) -> [Name] -> [Name] -> Q [Dec]
autoapplyDecs getNewName :: String -> String
getNewName givens :: [Name]
givens funs :: [Name]
funs = do
  [Given]
givenInfos <- [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]
givens ((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 Name -> DType -> Given
Given) (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]
givenInfos 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 -> 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)

-- | 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 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]
cmdVars, _preds :: [DType]
_preds, args :: [DType]
args, ret :: DType
ret) = DType -> ([DTyVarBndr], [DType], [DType], DType)
unravel (Function -> DType
fType Function
fun)
      defaultMaybe :: m a -> m (Maybe a)
defaultMaybe m :: m a
m = m a -> (a -> m (Maybe a)) -> m (Maybe a) -> m (Maybe a)
forall (m :: * -> *) a b.
MonadLogic m =>
m a -> (a -> m b) -> m b -> m b
ifte m a
m (Maybe a -> m (Maybe a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe a -> m (Maybe a)) -> (a -> Maybe a) -> a -> m (Maybe a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Maybe a
forall a. a -> Maybe a
Just) (Maybe a -> m (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

      -- 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
        [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 -> IntBindingT TypeF (LogicT Q) (UTerm TypeF IntVar)
forall (m :: * -> *).
BindingMonad TypeF IntVar m =>
[Name] -> Fix TypeF -> m (UTerm TypeF IntVar)
inst [Name]
cmdVars (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]
args

        -- This is @Just (m, a)@ when m is Applicative
        Maybe (UTerm TypeF IntVar, UTerm TypeF IntVar)
retMonad <- case DType
ret of
          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, UTerm TypeF IntVar)))
-> IntBindingT
     TypeF (LogicT Q) (Maybe (UTerm TypeF IntVar, UTerm TypeF IntVar))
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
            False -> Maybe (UTerm TypeF IntVar, UTerm TypeF IntVar)
-> IntBindingT
     TypeF (LogicT Q) (Maybe (UTerm TypeF IntVar, UTerm TypeF IntVar))
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (UTerm TypeF IntVar, UTerm TypeF IntVar)
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]
cmdVars (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]
cmdVars (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
              Maybe (UTerm TypeF IntVar, UTerm TypeF IntVar)
-> IntBindingT
     TypeF (LogicT Q) (Maybe (UTerm TypeF IntVar, UTerm TypeF IntVar))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (UTerm TypeF IntVar, UTerm TypeF IntVar)
 -> IntBindingT
      TypeF (LogicT Q) (Maybe (UTerm TypeF IntVar, UTerm TypeF IntVar)))
-> Maybe (UTerm TypeF IntVar, UTerm TypeF IntVar)
-> IntBindingT
     TypeF (LogicT Q) (Maybe (UTerm TypeF IntVar, UTerm TypeF IntVar))
forall a b. (a -> b) -> a -> b
$ (UTerm TypeF IntVar, UTerm TypeF IntVar)
-> Maybe (UTerm TypeF IntVar, UTerm TypeF IntVar)
forall a. a -> Maybe a
Just (UTerm TypeF IntVar
m', UTerm TypeF IntVar
a')
          _ -> Maybe (UTerm TypeF IntVar, UTerm TypeF IntVar)
-> IntBindingT
     TypeF (LogicT Q) (Maybe (UTerm TypeF IntVar, UTerm TypeF IntVar))
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (UTerm TypeF IntVar, UTerm TypeF IntVar)
forall a. Maybe a
Nothing

        -- 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) | Just (cmdM :: UTerm TypeF IntVar
cmdM, _) <- Maybe (UTerm TypeF IntVar, UTerm TypeF IntVar)
retMonad ->
              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 (m :: * -> *) a. MonadLogic m => m a -> m (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) ->
            ExceptT
  (UFailure TypeF IntVar)
  (IntBindingT TypeF (LogicT Q))
  (UTerm TypeF IntVar)
-> IntBindingT
     TypeF
     (LogicT Q)
     (Either (UFailure TypeF IntVar) (UTerm TypeF IntVar))
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT
                (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
                  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
                )
              IntBindingT
  TypeF
  (LogicT Q)
  (Either (UFailure TypeF IntVar) (UTerm TypeF IntVar))
-> (Either (UFailure TypeF IntVar) (UTerm TypeF IntVar)
    -> IntBindingT TypeF (LogicT Q) ArgProvenance)
-> IntBindingT TypeF (LogicT Q) ArgProvenance
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
                    Left  (UFailure TypeF IntVar
_ :: UFailure TypeF IntVar) -> IntBindingT TypeF (LogicT Q) ArgProvenance
forall (f :: * -> *) a. Alternative f => f a
empty
                    Right _                            -> ArgProvenance -> IntBindingT TypeF (LogicT Q) ArgProvenance
forall (f :: * -> *) a. Applicative f => a -> f a
pure ArgProvenance
g
        [(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"
    (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)

----------------------------------------------------------------
-- 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"
    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"

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 = ([DTyVarBndr] -> [DType] -> DType -> DType)
-> ([DTyVarBndr], [DType], DType) -> DType
forall a b c d. (a -> b -> c -> d) -> (a, b, c) -> d
uncurry3 [DTyVarBndr] -> [DType] -> DType -> DType
DForallT (([DTyVarBndr], [DType], DType) -> DType)
-> (DType -> ([DTyVarBndr], [DType], DType)) -> DType -> DType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DType -> ([DTyVarBndr], [DType], DType)
go
 where
  go :: DType -> ([DTyVarBndr], [DType], DType)
go = \case
    DForallT vs :: [DTyVarBndr]
vs 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 [DTyVarBndr] -> [DTyVarBndr] -> [DTyVarBndr]
forall a. Semigroup a => a -> a -> a
<> [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 ]
  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)
  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
$ 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 _ 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)
  ty :: DType
ty               -> ([], DType
ty)

uncurry3 :: (a -> b -> c -> d) -> (a, b, c) -> d
uncurry3 :: (a -> b -> c -> d) -> (a, b, c) -> d
uncurry3 f :: a -> b -> c -> d
f (a :: a
a, b :: b
b, c :: c
c) = a -> b -> c -> d
f a
a b
b c
c

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