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 [Name]
subsuming [Name]
unifying Name
fun = do
  [Given]
unifyingInfos <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [Name]
unifying forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (UnificationType -> Name -> DType -> Given
Given UnificationType
Unifying)) forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Name -> Q (Name, DType)
reifyVal
    String
"Argument"
  [Given]
subsumingInfos <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [Name]
subsuming forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (UnificationType -> Name -> DType -> Given
Given UnificationType
Subsuming)) forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Name -> Q (Name, DType)
reifyVal
    String
"Argument"
  Function
funInfo <- forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Name -> DType -> Function
Function forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> Name -> Q (Name, DType)
reifyVal String
"Function" Name
fun
  [Given] -> Function -> Q Exp
autoapply1 ([Given]
unifyingInfos 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 String -> String
getNewName [Name]
subsuming [Name]
unifying [Name]
funs = do
  [Given]
unifyingInfos <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [Name]
unifying forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (UnificationType -> Name -> DType -> Given
Given UnificationType
Unifying)) forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Name -> Q (Name, DType)
reifyVal
    String
"Argument"
  [Given]
subsumingInfos <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [Name]
subsuming forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (UnificationType -> Name -> DType -> Given
Given UnificationType
Subsuming)) forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Name -> Q (Name, DType)
reifyVal
    String
"Argument"
  [Function]
funInfos <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [Name]
funs forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Name -> DType -> Function
Function) forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Name -> Q (Name, DType)
reifyVal String
"Function"
  let mkFun :: Function -> Q Dec
mkFun Function
fun = do
        Exp
exp' <- [Given] -> Function -> Q Exp
autoapply1 ([Given]
unifyingInfos forall a. Semigroup a => a -> a -> a
<> [Given]
subsumingInfos) Function
fun
        forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Name -> [Clause] -> Dec
FunD (String -> Name
mkName forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
getNewName forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> String
nameBase forall b c a. (b -> c) -> (a -> b) -> a -> c
. Function -> Name
fName forall a b. (a -> b) -> a -> b
$ Function
fun)
                    [[Pat] -> Body -> [Dec] -> Clause
Clause [] (Exp -> Body
NormalB Exp
exp') []]
  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
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
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
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 [Given]
givens 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
    (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DTyVarBndrUnit -> Name
varBndrName -> [Name]
cmdVarNames, [DType]
preds, [DType]
args, DType
ret) = DType -> ([DTyVarBndrUnit], [DType], [DType], DType)
unravel (Function -> DType
fType Function
fun)
    defaultMaybe :: f a -> f (Maybe a)
defaultMaybe f a
m = (forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f a
m) forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Maybe a
Nothing
    liftQ :: Q a -> IntBindingT TypeF (LogicT Q) a
    liftQ :: forall a. Q a -> IntBindingT TypeF (LogicT Q) a
liftQ = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
T.lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 ExceptT (UFailure TypeF IntVar) m b
go = forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT ExceptT (UFailure TypeF IntVar) m b
go forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Left  (UFailure TypeF IntVar
_ :: UFailure TypeF IntVar) -> forall (f :: * -> *) a. Alternative f => f a
empty
      Right b
x                            -> 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 UTerm TypeF IntVar
t = do
      [IntVar]
vs <- forall (t :: * -> *) v (m :: * -> *).
BindingMonad t v m =>
UTerm t v -> m [v]
getFreeVars UTerm TypeF IntVar
t
      forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ [IntVar]
vs forall a b. (a -> b) -> a -> b
$ \IntVar
v -> forall (t :: * -> *) v (m :: * -> *).
BindingMonad t v m =>
v -> UTerm t v -> m ()
bindVar IntVar
v forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (t :: * -> *) v. t (UTerm t v) -> UTerm t v
UTerm forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Name -> TypeF a
VarF) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a. Q a -> IntBindingT TypeF (LogicT Q) a
liftQ (forall (m :: * -> *). Quote m => String -> m Name
newName String
"a")


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

      UTerm TypeF IntVar
cmdM       <- forall (t :: * -> *) v. v -> UTerm t v
UVar forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) v (m :: * -> *). BindingMonad t v m => m v
freeVar
      UTerm TypeF IntVar
retInst    <- forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([(Name, IntVar)] -> Fix TypeF -> UTerm TypeF IntVar
instWithVars [(Name, IntVar)]
cmdVars forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Q a -> IntBindingT TypeF (LogicT Q) a
liftQ forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *). MonadFail m => DType -> m ([Name], Fix TypeF)
typeDtoF 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 <- forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [Given]
givens forall a b. (a -> b) -> a -> b
$ \g :: Given
g@Given {Name
DType
UnificationType
gType :: DType
gName :: Name
gUnificationType :: UnificationType
gType :: Given -> DType
gName :: Given -> Name
gUnificationType :: Given -> UnificationType
..} -> do
        -- The Given applied as is
        (UTerm TypeF IntVar,
 ExceptT (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) (),
 ArgProvenance)
nonApp <- do
          UTerm TypeF IntVar
instTy <- forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall (m :: * -> *).
BindingMonad TypeF IntVar m =>
[Name] -> Fix TypeF -> m (UTerm TypeF IntVar)
inst forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall a. Q a -> IntBindingT TypeF (LogicT Q) a
liftQ forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *). MonadFail m => DType -> m ([Name], Fix TypeF)
typeDtoF forall a b. (a -> b) -> a -> b
$ DType
gType
          Name
v      <- forall a. Q a -> IntBindingT TypeF (LogicT Q) a
liftQ forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Quote m => String -> m Name
newName String
"g"
          forall (f :: * -> *) a. Applicative f => a -> f a
pure (UTerm TypeF IntVar
instTy, 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
          ([Name]
vars, DAppT DType
m DType
a) ->
            forall a. Q a -> IntBindingT TypeF (LogicT Q) a
liftQ (Name -> [Type] -> Q Bool
isInstance ''Applicative [forall th ds. Desugar th ds => ds -> th
sweeten DType
m]) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
              Bool
False -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Maybe a
Nothing
              Bool
True  -> do
                UTerm TypeF IntVar
m' <- forall (m :: * -> *).
BindingMonad TypeF IntVar m =>
[Name] -> Fix TypeF -> m (UTerm TypeF IntVar)
inst [Name]
vars forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall a. Q a -> IntBindingT TypeF (LogicT Q) a
liftQ forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *). MonadFail m => DType -> m ([Name], Fix TypeF)
typeDtoF forall a b. (a -> b) -> a -> b
$ DType
m
                UTerm TypeF IntVar
a' <- forall (m :: * -> *).
BindingMonad TypeF IntVar m =>
[Name] -> Fix TypeF -> m (UTerm TypeF IntVar)
inst [Name]
vars forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall a. Q a -> IntBindingT TypeF (LogicT Q) a
liftQ forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *). MonadFail m => DType -> m ([Name], Fix TypeF)
typeDtoF forall a b. (a -> b) -> a -> b
$ DType
a
                Name
v  <- forall a. Q a -> IntBindingT TypeF (LogicT Q) a
liftQ forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Quote m => String -> m Name
newName String
"g"
                let predicate :: ExceptT (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) ()
predicate = do
                      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
                      forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
                forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ 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)
          ([Name], DType)
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Maybe a
Nothing
        forall (f :: * -> *) a. Applicative f => a -> f a
pure ([(UTerm TypeF IntVar,
 ExceptT (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) (),
 ArgProvenance)
nonApp] forall a. Semigroup a => a -> a -> a
<> 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 <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [UTerm TypeF IntVar]
instArgs forall a b. (a -> b) -> a -> b
$ \UTerm TypeF IntVar
argTy ->
        forall {f :: * -> *} {a}. Alternative f => f a -> f (Maybe a)
defaultMaybe forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Alternative f) =>
t (f a) -> f a
asum forall a b. (a -> b) -> a -> b
$ [(UTerm TypeF IntVar,
  ExceptT (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) (),
  ArgProvenance)]
instGivens forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \(UTerm TypeF IntVar
givenTy, ExceptT (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) ()
predicate, ArgProvenance
g) -> do
          forall {m :: * -> *} {b}.
(Monad m, Alternative m) =>
ExceptT (UFailure TypeF IntVar) m b -> m b
errorToLogic forall a b. (a -> b) -> a -> b
$ do
            ExceptT (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) ()
predicate
            UTerm TypeF IntVar
freshGivenTy <- 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     Name
_ Given {Name
DType
UnificationType
gType :: DType
gName :: Name
gUnificationType :: UnificationType
gType :: Given -> DType
gName :: Given -> Name
gUnificationType :: Given -> UnificationType
..} -> UnificationType
gUnificationType
                  BoundPure Name
_ Given {Name
DType
UnificationType
gType :: DType
gName :: Name
gUnificationType :: UnificationType
gType :: Given -> DType
gName :: Given -> Name
gUnificationType :: Given -> UnificationType
..} -> UnificationType
gUnificationType
                  Argument  Name
_ DType
_          -> UnificationType
Unifying
            case UnificationType
u of
              UnificationType
Unifying  -> forall (f :: * -> *) a. Functor f => f a -> f ()
void forall a b. (a -> b) -> a -> b
$ 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
              UnificationType
Subsuming -> do
                Bool
s <- 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
                forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *). Alternative f => Bool -> f ()
guard Bool
s
          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.
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ArgProvenance -> Bool
isMonadicBind (forall a. [Maybe a] -> [a]
catMaybes [Maybe ArgProvenance]
as)) forall a b. (a -> b) -> a -> b
$ do
        UTerm TypeF IntVar
a    <- forall (t :: * -> *) v. v -> UTerm t v
UVar forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) v (m :: * -> *). BindingMonad t v m => m v
freeVar
        UTerm TypeF IntVar
ret' <- forall {m :: * -> *} {b}.
(Monad m, Alternative m) =>
ExceptT (UFailure TypeF IntVar) m b -> m b
errorToLogic forall a b. (a -> b) -> a -> b
$ 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 (forall (t :: * -> *) v. t (UTerm t v) -> UTerm t v
UTerm (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 <- forall (t :: * -> *) v. Traversable t => UTerm t v -> Maybe (Fix t)
freeze forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {m :: * -> *} {b}.
(Monad m, Alternative m) =>
ExceptT (UFailure TypeF IntVar) m b -> m b
errorToLogic (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 Fix TypeF
m Fix TypeF
_)) -> do
            let typeD :: DType
typeD = Fix TypeF -> DType
typeFtoD Fix TypeF
m
            forall a. Q a -> IntBindingT TypeF (LogicT Q) a
liftQ (Name -> [Type] -> Q Bool
isInstance ''Applicative [forall th ds. Desugar th ds => ds -> th
sweeten DType
typeD]) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
              Bool
False -> forall (f :: * -> *) a. Alternative f => f a
empty
              Bool
True  -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
          Maybe (Fix TypeF)
Nothing ->
            forall a. Q a -> IntBindingT TypeF (LogicT Q) a
liftQ
              forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. MonadFail m => String -> m a
fail
                  String
"\"impossible\", return type didn't freeze while checking monadic bindings"
          Maybe (Fix TypeF)
_ -> 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.
      forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ [DType]
preds forall a b. (a -> b) -> a -> b
$ \DType
pred -> do

        -- Get the constraint with the correct unification variables
        UTerm TypeF IntVar
instPred <- forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([(Name, IntVar)] -> Fix TypeF -> UTerm TypeF IntVar
instWithVars [(Name, IntVar)]
cmdVars forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Q a -> IntBindingT TypeF (LogicT Q) a
liftQ forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *). MonadFail m => DType -> m ([Name], Fix TypeF)
typeDtoF 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 <- forall (t :: * -> *) v. Traversable t => UTerm t v -> Maybe (Fix t)
freeze forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {m :: * -> *} {b}.
(Monad m, Alternative m) =>
ExceptT (UFailure TypeF IntVar) m b -> m b
errorToLogic (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 Fix TypeF
f -> do
            let (DType
class', [DTypeArg]
predArgs) = DType -> (DType, [DTypeArg])
unfoldDType (Fix TypeF -> DType
typeFtoD Fix TypeF
f)
                typeArgs :: [DType]
typeArgs           = [ DType
a | DTANormal DType
a <- [DTypeArg]
predArgs ]
            Name
className <- case DType
class' of
              DConT Name
n -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Name
n
              DType
_ -> forall a. Q a -> IntBindingT TypeF (LogicT Q) a
liftQ forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"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
            forall a. Q a -> IntBindingT TypeF (LogicT Q) a
liftQ (forall (q :: * -> *). (Quasi q, MonadFail q) => Name -> q Info
reifyWithWarning Name
className) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
              ClassI Dec
_ [Dec]
_ ->
                forall a. Q a -> IntBindingT TypeF (LogicT Q) a
liftQ (Name -> [Type] -> Q Bool
isInstance Name
className (forall th ds. Desugar th ds => ds -> th
sweeten forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [DType]
typeArgs)) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
                  Bool
False -> forall (f :: * -> *) a. Alternative f => f a
empty
                  Bool
True  -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
              FamilyI Dec
_ [Dec]
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
              Info
_ -> forall a. Q a -> IntBindingT TypeF (LogicT Q) a
liftQ forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Predicate name isn't a class or a type family"
          Maybe (Fix TypeF)
Nothing ->
            forall a. Q a -> IntBindingT TypeF (LogicT Q) a
liftQ
              forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. MonadFail m => String -> m a
fail
                  String
"\"impossible\": predicate didn't freeze while checking predicates"


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

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

  let bindGiven :: ArgProvenance -> Maybe Stmt
bindGiven = \case
        BoundPure Name
_ Given
_ -> forall a. Maybe a
Nothing
        Bound     Name
n Given
g -> forall a. a -> Maybe a
Just 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  Name
_ DType
_ -> forall a. Maybe a
Nothing
      bs :: [Stmt]
bs   = forall a. [Maybe a] -> [a]
catMaybes (ArgProvenance -> Maybe Stmt
bindGiven 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 forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case
          Bound     Name
n Given
_             -> Name -> DExp
DVarE Name
n
          BoundPure Name
_ (Given UnificationType
_ Name
n DType
_) -> Name -> DExp
DVarE Name
n
          Argument  Name
n DType
_             -> Name -> DExp
DVarE Name
n
        )
  DExp
exp' <- forall (q :: * -> *).
DsMonad q =>
Maybe ModName -> [Stmt] -> q DExp
dsDoStmts forall a. Maybe a
Nothing ([Stmt]
bs forall a. Semigroup a => a -> a -> a
<> [Exp -> Stmt
NoBindS (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@
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ [Pat] -> Exp -> Exp
LamE [ Pat -> Type -> Pat
SigP (Name -> Pat
VarP Name
n) (forall th ds. Desugar th ds => ds -> th
sweeten DType
t) | Argument Name
n DType
t <- [ArgProvenance]
argProvenances ]
              (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
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 Name
_ Given
_ -> Bool
True
  ArgProvenance
_         -> 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
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, 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
<$ :: forall a b. a -> TypeF b -> TypeF a
$c<$ :: forall a b. a -> TypeF b -> TypeF a
fmap :: forall a b. (a -> b) -> TypeF a -> TypeF b
$cfmap :: forall a b. (a -> b) -> TypeF a -> TypeF b
Functor, 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 :: forall a. Num a => TypeF a -> a
$cproduct :: forall a. Num a => TypeF a -> a
sum :: forall a. Num a => TypeF a -> a
$csum :: forall a. Num a => TypeF a -> a
minimum :: forall a. Ord a => TypeF a -> a
$cminimum :: forall a. Ord a => TypeF a -> a
maximum :: forall a. Ord a => TypeF a -> a
$cmaximum :: forall a. Ord a => TypeF a -> a
elem :: forall a. Eq a => a -> TypeF a -> Bool
$celem :: forall a. Eq a => a -> TypeF a -> Bool
length :: forall a. TypeF a -> Int
$clength :: forall a. TypeF a -> Int
null :: forall a. TypeF a -> Bool
$cnull :: forall a. TypeF a -> Bool
toList :: forall a. TypeF a -> [a]
$ctoList :: forall a. TypeF a -> [a]
foldl1 :: forall a. (a -> a -> a) -> TypeF a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> TypeF a -> a
foldr1 :: forall a. (a -> a -> a) -> TypeF a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> TypeF a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> TypeF a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> TypeF a -> b
foldl :: forall b a. (b -> a -> b) -> b -> TypeF a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> TypeF a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> TypeF a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> TypeF a -> b
foldr :: forall a b. (a -> b -> b) -> b -> TypeF a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> TypeF a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> TypeF a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> TypeF a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> TypeF a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> TypeF a -> m
fold :: forall m. Monoid m => TypeF m -> m
$cfold :: forall m. Monoid m => TypeF m -> m
Foldable, Functor TypeF
Foldable TypeF
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 :: forall (m :: * -> *) a. Monad m => TypeF (m a) -> m (TypeF a)
$csequence :: forall (m :: * -> *) a. Monad m => TypeF (m a) -> m (TypeF a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> TypeF a -> m (TypeF b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> TypeF a -> m (TypeF b)
sequenceA :: forall (f :: * -> *) a. Applicative f => TypeF (f a) -> f (TypeF a)
$csequenceA :: forall (f :: * -> *) a. Applicative f => TypeF (f a) -> f (TypeF a)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> TypeF a -> f (TypeF b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> TypeF a -> f (TypeF b)
Traversable)

-- TODO: Derive this with generics
instance Unifiable TypeF where
  zipMatch :: forall a. TypeF a -> TypeF a -> Maybe (TypeF (Either a (a, a)))
zipMatch (AppF a
l1 a
r1) (AppF a
l2 a
r2) =
    forall a. a -> Maybe a
Just (forall a. a -> a -> TypeF a
AppF (forall a b. b -> Either a b
Right (a
l1, a
l2)) (forall a b. b -> Either a b
Right (a
r1, a
r2)))
  zipMatch (VarF Name
n1) (VarF Name
n2) | Name
n1 forall a. Eq a => a -> a -> Bool
== Name
n2 = forall a. a -> Maybe a
Just (forall a. Name -> TypeF a
VarF Name
n1)
  zipMatch (ConF Name
n1) (ConF Name
n2) | Name
n1 forall a. Eq a => a -> a -> Bool
== Name
n2 = forall a. a -> Maybe a
Just (forall a. Name -> TypeF a
ConF Name
n1)
  zipMatch TypeF a
ArrowF TypeF a
ArrowF                  = forall a. a -> Maybe a
Just forall a. TypeF a
ArrowF
  zipMatch (LitF TyLit
l1) (LitF TyLit
l2) | TyLit
l1 forall a. Eq a => a -> a -> Bool
== TyLit
l2 = forall a. a -> Maybe a
Just (forall a. TyLit -> TypeF a
LitF TyLit
l1)
  zipMatch TypeF a
_ TypeF 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 :: forall (m :: * -> *). MonadFail m => DType -> m ([Name], Fix TypeF)
typeDtoF = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse DType -> m (Fix TypeF)
go forall b c a. (b -> c) -> (a -> b) -> a -> c
. DType -> ([Name], DType)
stripForall
 where
  go :: DType -> m (Fix TypeF)
go = \case
    DForallT{}      -> forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"TODO: Higher ranked types"
    DConstrainedT{} -> forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"TODO: Higher ranked types"
    DAppT DType
l DType
r       -> do
      Fix TypeF
l' <- DType -> m (Fix TypeF)
go DType
l
      Fix TypeF
r' <- DType -> m (Fix TypeF)
go DType
r
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *). f (Fix f) -> Fix f
Fix (forall a. a -> a -> TypeF a
AppF Fix TypeF
l' Fix TypeF
r')
    DAppKindT DType
t DType
_ -> DType -> m (Fix TypeF)
go DType
t
    DSigT     DType
t DType
_ -> DType -> m (Fix TypeF)
go DType
t
    DVarT Name
n       -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *). f (Fix f) -> Fix f
Fix forall a b. (a -> b) -> a -> b
$ forall a. Name -> TypeF a
VarF Name
n
    DConT Name
n       -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *). f (Fix f) -> Fix f
Fix forall a b. (a -> b) -> a -> b
$ forall a. Name -> TypeF a
ConF Name
n
    DType
DArrowT       -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *). f (Fix f) -> Fix f
Fix forall a b. (a -> b) -> a -> b
$ forall a. TypeF a
ArrowF
    DLitT TyLit
l       -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *). f (Fix f) -> Fix f
Fix forall a b. (a -> b) -> a -> b
$ forall a. TyLit -> TypeF a
LitF TyLit
l
    DType
DWildCardT    -> forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"TODO: Wildcards"

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

varBndrName :: DTyVarBndrUnit -> Name
varBndrName :: DTyVarBndrUnit -> Name
varBndrName = \case
  DPlainTV Name
n ()   -> Name
n
  DKindedTV Name
n () DType
_ -> 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 -> ([DTyVarBndrUnit], [DType], DType)
go forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> \case
  ([DTyVarBndrUnit]
vs, [DType]
ctx, DType
t) -> DForallTelescope -> DType -> DType
DForallT ([DTyVarBndrUnit] -> DForallTelescope
DForallVis [DTyVarBndrUnit]
vs) forall b c a. (b -> c) -> (a -> b) -> a -> c
. [DType] -> DType -> DType
DConstrainedT [DType]
ctx forall a b. (a -> b) -> a -> b
$ DType
t
 where
  go :: DType -> ([DTyVarBndrUnit], [DType], DType)
go = \case
    DForallT DForallTelescope
vs DType
t -> let ([DTyVarBndrUnit]
vs', [DType]
ctx', DType
t') = DType -> ([DTyVarBndrUnit], [DType], DType)
go DType
t in (DForallTelescope -> [DTyVarBndrUnit]
telescopeBndrs DForallTelescope
vs forall a. Semigroup a => a -> a -> a
<> [DTyVarBndrUnit]
vs', [DType]
ctx', DType
t')
    DConstrainedT [DType]
ctx DType
t ->
      let ([DTyVarBndrUnit]
vs', [DType]
ctx', DType
t') = DType -> ([DTyVarBndrUnit], [DType], DType)
go DType
t in ([DTyVarBndrUnit]
vs', [DType]
ctx forall a. Semigroup a => a -> a -> a
<> [DType]
ctx', DType
t')
    DType
l :~> DType
r -> let ([DTyVarBndrUnit]
vs, [DType]
ctx, DType
r') = DType -> ([DTyVarBndrUnit], [DType], DType)
go DType
r in ([DTyVarBndrUnit]
vs, [DType]
ctx, DType
l DType -> DType -> DType
:~> DType
r')
    DType
t       -> ([], [], DType
t)

pattern (:~>) :: DType -> DType -> DType
pattern l $b:~> :: DType -> DType -> DType
$m:~> :: forall {r}. DType -> (DType -> DType -> r) -> ((# #) -> 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 :: forall (m :: * -> *).
BindingMonad TypeF IntVar m =>
[Name] -> Fix TypeF -> m (UTerm TypeF IntVar)
inst [Name]
ns Fix TypeF
t = do
  [(Name, IntVar)]
vs <- forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [ (Name
n, ) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) v (m :: * -> *). BindingMonad t v m => m v
freeVar | Name
n <- [Name]
ns ]
  forall (f :: * -> *) a. Applicative f => a -> f a
pure 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 [(Name, IntVar)]
vs Fix TypeF
t =
  let go :: Fix TypeF -> UTerm TypeF IntVar
go (Fix TypeF (Fix TypeF)
f) = case TypeF (Fix TypeF)
f of
        AppF Fix TypeF
l Fix TypeF
r                       -> forall (t :: * -> *) v. t (UTerm t v) -> UTerm t v
UTerm (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 Name
n | Just IntVar
v <- forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n [(Name, IntVar)]
vs -> forall (t :: * -> *) v. v -> UTerm t v
UVar IntVar
v
        VarF Name
n                         -> forall (t :: * -> *) v. t (UTerm t v) -> UTerm t v
UTerm (forall a. Name -> TypeF a
VarF Name
n)
        ConF Name
n                         -> forall (t :: * -> *) v. t (UTerm t v) -> UTerm t v
UTerm (forall a. Name -> TypeF a
ConF Name
n)
        TypeF (Fix TypeF)
ArrowF                         -> forall (t :: * -> *) v. t (UTerm t v) -> UTerm t v
UTerm forall a. TypeF a
ArrowF
        LitF TyLit
l                         -> forall (t :: * -> *) v. t (UTerm t v) -> UTerm t v
UTerm (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 String
d Name
n = forall (q :: * -> *). DsMonad q => Name -> q (Maybe DInfo)
dsReify Name
n forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  Just (DVarI Name
name DType
ty Maybe Name
_) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Name
name, DType
ty)
  Maybe DInfo
_                      -> forall (m :: * -> *) a. MonadFail m => String -> m a
fail forall a b. (a -> b) -> a -> b
$ String
d forall a. Semigroup a => a -> a -> a
<> String
" " forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show Name
n forall a. Semigroup a => a -> a -> a
<> String
" isn't a value"

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

telescopeBndrs :: DForallTelescope -> [DTyVarBndrUnit]
telescopeBndrs :: DForallTelescope -> [DTyVarBndrUnit]
telescopeBndrs = \case
  DForallVis [DTyVarBndrUnit]
vs -> [DTyVarBndrUnit]
vs
  DForallInvis [DTyVarBndrSpec]
vs -> (() forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [DTyVarBndrSpec]
vs

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

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