{-# LANGUAGE TemplateHaskell #-}
-- | The rules for type checking and type inference.
module Glam.Rules.Term where

import Data.Traversable
import Data.Map (Map)
import Data.Map qualified as Map
import Data.Set qualified as Set
import Control.Monad
import Control.Monad.Except
import Control.Monad.Reader
import Control.Monad.State
import Control.Monad.Trans.Maybe
import Control.Lens hiding (Fold)
import Text.Megaparsec

import Glam.Utils
import Glam.Term
import Glam.Type

data Environment = Environment
    { Environment -> Map Var (Polytype, Constancy)
_termCtx :: Map Var (Polytype, Constancy) -- ^ The term context
    , Environment -> [(Var, Constancy)]
_typeCtx :: [(TVar, Constancy)] -- ^ The type context
    }

makeLenses ''Environment

-- | A metavariable: a placeholder for a type to be determined later (or generalised over).
data Meta = Meta
    { Meta -> Maybe Type
_solution :: Maybe Type -- ^ The metavariable's solution
    , Meta -> Constancy
_constant :: Constancy
    , Meta -> Int
_level :: Int -- ^ The de Bruijn level at which this metavariable was created.
                    -- Solutions may not contain variables introduced later, as they would escape their scope.
                    -- An invariant is that (currently) fixed point variables are never in scope of a metavariable, so we
                    -- don't have to worry about substitution.
    }

makeLenses ''Meta

data UnificationState = UnificationState
    { UnificationState -> Map Var Meta
_metas :: Map TVar Meta -- ^ Metavariables
    , UnificationState -> [Var]
_tvars :: [TVar] -- ^ A stream of fresh type variables
    }

makeLenses ''UnificationState

type MonadCheckTerm m = (MonadState UnificationState m, MonadReader Environment m, MonadError String m)

runUnification :: StateT UnificationState m a -> Set Var -> m a
runUnification StateT UnificationState m a
a Set Var
xs = StateT UnificationState m a -> UnificationState -> m a
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT StateT UnificationState m a
a (UnificationState -> m a) -> UnificationState -> m a
forall a b. (a -> b) -> a -> b
$ Map Var Meta -> [Var] -> UnificationState
UnificationState Map Var Meta
forall a. Monoid a => a
mempty (Set Var -> [Var]
freshTVarsFor Set Var
xs)

-- | Case split on whether a type variable is bound or is a metavariable.
-- Note that since we use the same constructor for both, conflicts are possible.
-- In that case, we prefer bound type variables. This is fragile and probably buggy.
viewTVar :: MonadCheckTerm m => TVar -> m (Either Meta Constancy)
viewTVar :: forall (m :: * -> *).
MonadCheckTerm m =>
Var -> m (Either Meta Constancy)
viewTVar Var
x = m (Either Meta Constancy)
-> (Either Meta Constancy -> m (Either Meta Constancy))
-> Maybe (Either Meta Constancy)
-> m (Either Meta Constancy)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Var -> m (Either Meta Constancy)
forall a. Var -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Var -> m (Either Meta Constancy))
-> Var -> m (Either Meta Constancy)
forall a b. (a -> b) -> a -> b
$ Var
"unbound type variable " Var -> Var -> Var
forall a. [a] -> [a] -> [a]
++ Var
x) Either Meta Constancy -> m (Either Meta Constancy)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (Either Meta Constancy) -> m (Either Meta Constancy))
-> m (Maybe (Either Meta Constancy)) -> m (Either Meta Constancy)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< MaybeT m (Either Meta Constancy)
-> m (Maybe (Either Meta Constancy))
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (
    Constancy -> Either Meta Constancy
forall a b. b -> Either a b
Right (Constancy -> Either Meta Constancy)
-> MaybeT m Constancy -> MaybeT m (Either Meta Constancy)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (Maybe Constancy) -> MaybeT m Constancy
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (Var -> [(Var, Constancy)] -> Maybe Constancy
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Var
x ([(Var, Constancy)] -> Maybe Constancy)
-> m [(Var, Constancy)] -> m (Maybe Constancy)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Getting [(Var, Constancy)] Environment [(Var, Constancy)]
-> m [(Var, Constancy)]
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting [(Var, Constancy)] Environment [(Var, Constancy)]
Lens' Environment [(Var, Constancy)]
typeCtx) MaybeT m (Either Meta Constancy)
-> MaybeT m (Either Meta Constancy)
-> MaybeT m (Either Meta Constancy)
forall a. MaybeT m a -> MaybeT m a -> MaybeT m a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Meta -> Either Meta Constancy
forall a b. a -> Either a b
Left (Meta -> Either Meta Constancy)
-> MaybeT m Meta -> MaybeT m (Either Meta Constancy)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (Maybe Meta) -> MaybeT m Meta
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (Getting (Maybe Meta) UnificationState (Maybe Meta)
-> m (Maybe Meta)
forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a
use ((Map Var Meta -> Const (Maybe Meta) (Map Var Meta))
-> UnificationState -> Const (Maybe Meta) UnificationState
Lens' UnificationState (Map Var Meta)
metas((Map Var Meta -> Const (Maybe Meta) (Map Var Meta))
 -> UnificationState -> Const (Maybe Meta) UnificationState)
-> ((Maybe Meta -> Const (Maybe Meta) (Maybe Meta))
    -> Map Var Meta -> Const (Maybe Meta) (Map Var Meta))
-> Getting (Maybe Meta) UnificationState (Maybe Meta)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Index (Map Var Meta)
-> Lens' (Map Var Meta) (Maybe (IxValue (Map Var Meta)))
forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
at Var
Index (Map Var Meta)
x)))

ifMeta :: MonadCheckTerm m => Type -> ((TVar, Meta) -> m ()) -> m () -> m ()
ifMeta :: forall (m :: * -> *).
MonadCheckTerm m =>
Type -> ((Var, Meta) -> m ()) -> m () -> m ()
ifMeta (TVar Var
x) (Var, Meta) -> m ()
y m ()
n = m () -> (Meta -> m ()) -> Maybe Meta -> m ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe m ()
n (((Var, Meta) -> m ()) -> Var -> Meta -> m ()
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (Var, Meta) -> m ()
y Var
x) (Maybe Meta -> m ()) -> m (Maybe Meta) -> m ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Getting (Maybe Meta) UnificationState (Maybe Meta)
-> m (Maybe Meta)
forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a
use ((Map Var Meta -> Const (Maybe Meta) (Map Var Meta))
-> UnificationState -> Const (Maybe Meta) UnificationState
Lens' UnificationState (Map Var Meta)
metas((Map Var Meta -> Const (Maybe Meta) (Map Var Meta))
 -> UnificationState -> Const (Maybe Meta) UnificationState)
-> ((Maybe Meta -> Const (Maybe Meta) (Maybe Meta))
    -> Map Var Meta -> Const (Maybe Meta) (Map Var Meta))
-> Getting (Maybe Meta) UnificationState (Maybe Meta)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Index (Map Var Meta)
-> Lens' (Map Var Meta) (Maybe (IxValue (Map Var Meta)))
forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
at Var
Index (Map Var Meta)
x)
ifMeta Type
_ (Var, Meta) -> m ()
_ m ()
n = m ()
n

freshTVar :: MonadCheckTerm m => m TVar
freshTVar :: forall (m :: * -> *). MonadCheckTerm m => m Var
freshTVar = [Var] -> Var
forall a. HasCallStack => [a] -> a
head ([Var] -> Var) -> m [Var] -> m Var
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (([Var] -> ([Var], [Var]))
-> UnificationState -> ([Var], UnificationState)
Lens' UnificationState [Var]
tvars (([Var] -> ([Var], [Var]))
 -> UnificationState -> ([Var], UnificationState))
-> ([Var] -> [Var]) -> m [Var]
forall (p :: * -> * -> *) s (m :: * -> *) a b.
(Strong p, MonadState s m) =>
Over p ((,) a) s s a b -> p a b -> m a
<<%= [Var] -> [Var]
forall a. HasCallStack => [a] -> [a]
tail)

-- | Create a new metavariable.
newMeta' :: MonadCheckTerm m => Constancy -> m Type
newMeta' :: forall (m :: * -> *). MonadCheckTerm m => Constancy -> m Type
newMeta' Constancy
c = do
    Var
x <- m Var
forall (m :: * -> *). MonadCheckTerm m => m Var
freshTVar
    Int
l <- [(Var, Constancy)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([(Var, Constancy)] -> Int) -> m [(Var, Constancy)] -> m Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Getting [(Var, Constancy)] Environment [(Var, Constancy)]
-> m [(Var, Constancy)]
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting [(Var, Constancy)] Environment [(Var, Constancy)]
Lens' Environment [(Var, Constancy)]
typeCtx
    (Map Var Meta -> Identity (Map Var Meta))
-> UnificationState -> Identity UnificationState
Lens' UnificationState (Map Var Meta)
metas((Map Var Meta -> Identity (Map Var Meta))
 -> UnificationState -> Identity UnificationState)
-> ((Maybe Meta -> Identity (Maybe Meta))
    -> Map Var Meta -> Identity (Map Var Meta))
-> (Maybe Meta -> Identity (Maybe Meta))
-> UnificationState
-> Identity UnificationState
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Index (Map Var Meta)
-> Lens' (Map Var Meta) (Maybe (IxValue (Map Var Meta)))
forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
at Var
Index (Map Var Meta)
x ((Maybe Meta -> Identity (Maybe Meta))
 -> UnificationState -> Identity UnificationState)
-> Meta -> m ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a (Maybe b) -> b -> m ()
?= Maybe Type -> Constancy -> Int -> Meta
Meta Maybe Type
forall a. Maybe a
Nothing Constancy
c Int
l
    pure (Var -> Type
TVar Var
x)
-- | Create a new not-necessarily-constant metavariable.
newMeta :: m Type
newMeta = Constancy -> m Type
forall (m :: * -> *). MonadCheckTerm m => Constancy -> m Type
newMeta' Constancy
False
newMetas :: Int -> m [Type]
newMetas Int
n = Int -> m Type -> m [Type]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
n m Type
forall {m :: * -> *}.
(MonadState UnificationState m, MonadReader Environment m,
 MonadError Var m) =>
m Type
newMeta

class Zonk t where
    -- | Recursively replace solved metavariables in a type with their solutions.
    zonk :: MonadCheckTerm m => t -> m t

instance Zonk Type where
    zonk :: forall (m :: * -> *). MonadCheckTerm m => Type -> m Type
zonk ty :: Type
ty@(TVar Var
x)  = Var -> m (Either Meta Constancy)
forall (m :: * -> *).
MonadCheckTerm m =>
Var -> m (Either Meta Constancy)
viewTVar Var
x m (Either Meta Constancy)
-> (Either Meta Constancy -> m Type) -> m Type
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Left Meta
m | Just Type
sol <- Meta
m Meta -> Getting (Maybe Type) Meta (Maybe Type) -> Maybe Type
forall s a. s -> Getting a s a -> a
^. Getting (Maybe Type) Meta (Maybe Type)
Lens' Meta (Maybe Type)
solution -> Type -> m Type
forall t (m :: * -> *). (Zonk t, MonadCheckTerm m) => t -> m t
forall (m :: * -> *). MonadCheckTerm m => Type -> m Type
zonk Type
sol
        Either Meta Constancy
_ -> Type -> m Type
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
ty
    zonk (Type
a :*: Type
b)    = Type -> Type -> Type
(:*:) (Type -> Type -> Type) -> m Type -> m (Type -> Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> m Type
forall t (m :: * -> *). (Zonk t, MonadCheckTerm m) => t -> m t
forall (m :: * -> *). MonadCheckTerm m => Type -> m Type
zonk Type
a m (Type -> Type) -> m Type -> m Type
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> m Type
forall t (m :: * -> *). (Zonk t, MonadCheckTerm m) => t -> m t
forall (m :: * -> *). MonadCheckTerm m => Type -> m Type
zonk Type
b
    zonk (Type
a :+: Type
b)    = Type -> Type -> Type
(:+:) (Type -> Type -> Type) -> m Type -> m (Type -> Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> m Type
forall t (m :: * -> *). (Zonk t, MonadCheckTerm m) => t -> m t
forall (m :: * -> *). MonadCheckTerm m => Type -> m Type
zonk Type
a m (Type -> Type) -> m Type -> m Type
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> m Type
forall t (m :: * -> *). (Zonk t, MonadCheckTerm m) => t -> m t
forall (m :: * -> *). MonadCheckTerm m => Type -> m Type
zonk Type
b
    zonk (Type
a :->: Type
b)   = Type -> Type -> Type
(:->:) (Type -> Type -> Type) -> m Type -> m (Type -> Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> m Type
forall t (m :: * -> *). (Zonk t, MonadCheckTerm m) => t -> m t
forall (m :: * -> *). MonadCheckTerm m => Type -> m Type
zonk Type
a m (Type -> Type) -> m Type -> m Type
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> m Type
forall t (m :: * -> *). (Zonk t, MonadCheckTerm m) => t -> m t
forall (m :: * -> *). MonadCheckTerm m => Type -> m Type
zonk Type
b
    zonk (Later Type
t)    = Type -> Type
Later (Type -> Type) -> m Type -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> m Type
forall t (m :: * -> *). (Zonk t, MonadCheckTerm m) => t -> m t
forall (m :: * -> *). MonadCheckTerm m => Type -> m Type
zonk Type
t
    zonk (Constant Type
t) = Type -> Type
Constant (Type -> Type) -> m Type -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> m Type
forall t (m :: * -> *). (Zonk t, MonadCheckTerm m) => t -> m t
forall (m :: * -> *). MonadCheckTerm m => Type -> m Type
zonk Type
t
    zonk (TFix Var
x Type
t)   = ([(Var, Constancy)] -> Identity [(Var, Constancy)])
-> Environment -> Identity Environment
Lens' Environment [(Var, Constancy)]
typeCtx (([(Var, Constancy)] -> Identity [(Var, Constancy)])
 -> Environment -> Identity Environment)
-> ([(Var, Constancy)] -> [(Var, Constancy)])
-> Environment
-> Environment
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ ((Var
x, Constancy
False):) (Environment -> Environment) -> m Type -> m Type
forall {r} {m :: * -> *} {a}.
MonadReader r m =>
(r -> r) -> m a -> m a
|- Var -> Type -> Type
TFix Var
x (Type -> Type) -> m Type -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> m Type
forall t (m :: * -> *). (Zonk t, MonadCheckTerm m) => t -> m t
forall (m :: * -> *). MonadCheckTerm m => Type -> m Type
zonk Type
t
    zonk Type
ty           = Type -> m Type
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
ty

instance Zonk Polytype where
    zonk :: forall (m :: * -> *). MonadCheckTerm m => Polytype -> m Polytype
zonk (Forall [(Var, Constancy)]
xs Type
ty) = ([(Var, Constancy)] -> Identity [(Var, Constancy)])
-> Environment -> Identity Environment
Lens' Environment [(Var, Constancy)]
typeCtx (([(Var, Constancy)] -> Identity [(Var, Constancy)])
 -> Environment -> Identity Environment)
-> ([(Var, Constancy)] -> [(Var, Constancy)])
-> Environment
-> Environment
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ ([(Var, Constancy)]
xs ++) (Environment -> Environment) -> m Polytype -> m Polytype
forall {r} {m :: * -> *} {a}.
MonadReader r m =>
(r -> r) -> m a -> m a
|- [(Var, Constancy)] -> Type -> Polytype
Forall [(Var, Constancy)]
xs (Type -> Polytype) -> m Type -> m Polytype
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> m Type
forall t (m :: * -> *). (Zonk t, MonadCheckTerm m) => t -> m t
forall (m :: * -> *). MonadCheckTerm m => Type -> m Type
zonk Type
ty

-- | Instantiate a polytype to a type by replacing polymorphic type variables with fresh metavariables.
instantiate :: MonadCheckTerm m => Polytype -> m Type
instantiate :: forall (m :: * -> *). MonadCheckTerm m => Polytype -> m Type
instantiate (Monotype Type
ty) = Type -> m Type
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
ty
instantiate (Forall [(Var, Constancy)]
xs Type
ty) = do
    [(Var, Type)]
s <- [(Var, Constancy)]
-> ((Var, Constancy) -> m (Var, Type)) -> m [(Var, Type)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [(Var, Constancy)]
xs \(Var
x, Constancy
c) -> (Var
x,) (Type -> (Var, Type)) -> m Type -> m (Var, Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Constancy -> m Type
forall (m :: * -> *). MonadCheckTerm m => Constancy -> m Type
newMeta' Constancy
c
    pure $ TSubst -> Type -> Type
substituteType ([(Var, Type)] -> TSubst
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Var, Type)]
s) Type
ty

-- | Generalise a type to a polytype by abstracting over its metavariables that aren't free in the context.
generalise :: MonadCheckTerm m => Type -> m Polytype
generalise :: forall (m :: * -> *). MonadCheckTerm m => Type -> m Polytype
generalise Type
ty = do
    Type
ty <- Type -> m Type
forall t (m :: * -> *). (Zonk t, MonadCheckTerm m) => t -> m t
forall (m :: * -> *). MonadCheckTerm m => Type -> m Type
zonk Type
ty
    Set Var
freeInCtx <- (Map Var Polytype -> Set Var)
-> m (Map Var Polytype) -> m (Set Var)
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Polytype -> Set Var) -> Map Var Polytype -> Set Var
forall m a. Monoid m => (a -> m) -> Map Var a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Polytype -> Set Var
forall t. HasTVars t => t -> Set Var
freeTVars) (m (Map Var Polytype) -> m (Set Var))
-> (Map Var (Polytype, Constancy) -> m (Map Var Polytype))
-> Map Var (Polytype, Constancy)
-> m (Set Var)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Polytype, Constancy) -> m Polytype)
-> Map Var (Polytype, Constancy) -> m (Map Var Polytype)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Map Var a -> f (Map Var b)
traverse (Polytype -> m Polytype
forall t (m :: * -> *). (Zonk t, MonadCheckTerm m) => t -> m t
forall (m :: * -> *). MonadCheckTerm m => Polytype -> m Polytype
zonk (Polytype -> m Polytype)
-> ((Polytype, Constancy) -> Polytype)
-> (Polytype, Constancy)
-> m Polytype
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Polytype, Constancy) -> Polytype
forall a b. (a, b) -> a
fst) (Map Var (Polytype, Constancy) -> m (Set Var))
-> m (Map Var (Polytype, Constancy)) -> m (Set Var)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Getting
  (Map Var (Polytype, Constancy))
  Environment
  (Map Var (Polytype, Constancy))
-> m (Map Var (Polytype, Constancy))
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting
  (Map Var (Polytype, Constancy))
  Environment
  (Map Var (Polytype, Constancy))
Lens' Environment (Map Var (Polytype, Constancy))
termCtx
    Map Var Meta
metas <- Getting (Map Var Meta) UnificationState (Map Var Meta)
-> m (Map Var Meta)
forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a
use Getting (Map Var Meta) UnificationState (Map Var Meta)
Lens' UnificationState (Map Var Meta)
metas
    let generalisable :: Map Var Meta
generalisable = Map Var Meta
metas Map Var Meta -> Set Var -> Map Var Meta
forall k a. Ord k => Map k a -> Set k -> Map k a
`Map.restrictKeys` Type -> Set Var
forall t. HasTVars t => t -> Set Var
freeTVars Type
ty Map Var Meta -> Set Var -> Map Var Meta
forall k a. Ord k => Map k a -> Set k -> Map k a
`Map.withoutKeys` Set Var
freeInCtx
    Polytype -> m Polytype
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Polytype -> m Polytype) -> Polytype -> m Polytype
forall a b. (a -> b) -> a -> b
$ [(Var, Constancy)] -> Type -> Polytype
Forall [(Var
x, Meta
m Meta -> Getting Constancy Meta Constancy -> Constancy
forall s a. s -> Getting a s a -> a
^. Getting Constancy Meta Constancy
Lens' Meta Constancy
constant) | (Var
x, Meta
m) <- Map Var Meta -> [(Var, Meta)]
forall k a. Map k a -> [(k, a)]
Map.toList Map Var Meta
generalisable] Type
ty

class Constant t where
    -- | Check whether a type or term is constant, optionally forcing it to be by marking its metavariables as constant.
    isConstant :: MonadCheckTerm m => Bool -> t -> m Constancy

-- | A type is constant if all uses of @▸@ occur under @■@.
instance Constant Type where
    isConstant :: forall (m :: * -> *).
MonadCheckTerm m =>
Constancy -> Type -> m Constancy
isConstant Constancy
force (TVar Var
x) = Var -> m (Either Meta Constancy)
forall (m :: * -> *).
MonadCheckTerm m =>
Var -> m (Either Meta Constancy)
viewTVar Var
x m (Either Meta Constancy)
-> (Either Meta Constancy -> m Constancy) -> m Constancy
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Left Meta
m | Just Type
sol <- Meta
m Meta -> Getting (Maybe Type) Meta (Maybe Type) -> Maybe Type
forall s a. s -> Getting a s a -> a
^. Getting (Maybe Type) Meta (Maybe Type)
Lens' Meta (Maybe Type)
solution ->
                    if Meta
m Meta -> Getting Constancy Meta Constancy -> Constancy
forall s a. s -> Getting a s a -> a
^. Getting Constancy Meta Constancy
Lens' Meta Constancy
constant then Constancy -> m Constancy
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Constancy
True else Constancy -> Type -> m Constancy
forall t (m :: * -> *).
(Constant t, MonadCheckTerm m) =>
Constancy -> t -> m Constancy
forall (m :: * -> *).
MonadCheckTerm m =>
Constancy -> Type -> m Constancy
isConstant Constancy
force Type
sol
               | Constancy
force -> (Map Var Meta -> Identity (Map Var Meta))
-> UnificationState -> Identity UnificationState
Lens' UnificationState (Map Var Meta)
metas((Map Var Meta -> Identity (Map Var Meta))
 -> UnificationState -> Identity UnificationState)
-> ((Constancy -> Identity Constancy)
    -> Map Var Meta -> Identity (Map Var Meta))
-> (Constancy -> Identity Constancy)
-> UnificationState
-> Identity UnificationState
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Index (Map Var Meta)
-> Traversal' (Map Var Meta) (IxValue (Map Var Meta))
forall m. Ixed m => Index m -> Traversal' m (IxValue m)
ix Var
Index (Map Var Meta)
x((Meta -> Identity Meta)
 -> Map Var Meta -> Identity (Map Var Meta))
-> ((Constancy -> Identity Constancy) -> Meta -> Identity Meta)
-> (Constancy -> Identity Constancy)
-> Map Var Meta
-> Identity (Map Var Meta)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(Constancy -> Identity Constancy) -> Meta -> Identity Meta
Lens' Meta Constancy
constant ((Constancy -> Identity Constancy)
 -> UnificationState -> Identity UnificationState)
-> Constancy -> m Constancy
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> b -> m b
<.= Constancy
True
               | Constancy
otherwise -> Constancy -> m Constancy
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Meta
m Meta -> Getting Constancy Meta Constancy -> Constancy
forall s a. s -> Getting a s a -> a
^. Getting Constancy Meta Constancy
Lens' Meta Constancy
constant)
        Right Constancy
c -> Constancy
c Constancy -> m () -> m Constancy
forall a b. a -> m b -> m a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Constancy -> m () -> m ()
forall (f :: * -> *). Applicative f => Constancy -> f () -> f ()
when (Constancy
force Constancy -> Constancy -> Constancy
&& Constancy -> Constancy
not Constancy
c) (Var -> m ()
forall a. Var -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Var -> m ()) -> Var -> m ()
forall a b. (a -> b) -> a -> b
$ Var
"non-constant type variable " Var -> Var -> Var
forall a. [a] -> [a] -> [a]
++ Var
x)
    isConstant Constancy
force (Type
t1 :*: Type
t2) = Constancy -> Constancy -> Constancy
(&&) (Constancy -> Constancy -> Constancy)
-> m Constancy -> m (Constancy -> Constancy)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Constancy -> Type -> m Constancy
forall t (m :: * -> *).
(Constant t, MonadCheckTerm m) =>
Constancy -> t -> m Constancy
forall (m :: * -> *).
MonadCheckTerm m =>
Constancy -> Type -> m Constancy
isConstant Constancy
force Type
t1 m (Constancy -> Constancy) -> m Constancy -> m Constancy
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Constancy -> Type -> m Constancy
forall t (m :: * -> *).
(Constant t, MonadCheckTerm m) =>
Constancy -> t -> m Constancy
forall (m :: * -> *).
MonadCheckTerm m =>
Constancy -> Type -> m Constancy
isConstant Constancy
force Type
t2
    isConstant Constancy
force (Type
t1 :+: Type
t2) = Constancy -> Constancy -> Constancy
(&&) (Constancy -> Constancy -> Constancy)
-> m Constancy -> m (Constancy -> Constancy)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Constancy -> Type -> m Constancy
forall t (m :: * -> *).
(Constant t, MonadCheckTerm m) =>
Constancy -> t -> m Constancy
forall (m :: * -> *).
MonadCheckTerm m =>
Constancy -> Type -> m Constancy
isConstant Constancy
force Type
t1 m (Constancy -> Constancy) -> m Constancy -> m Constancy
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Constancy -> Type -> m Constancy
forall t (m :: * -> *).
(Constant t, MonadCheckTerm m) =>
Constancy -> t -> m Constancy
forall (m :: * -> *).
MonadCheckTerm m =>
Constancy -> Type -> m Constancy
isConstant Constancy
force Type
t2
    isConstant Constancy
force (Type
_ :->: Type
t2) = Constancy -> Type -> m Constancy
forall t (m :: * -> *).
(Constant t, MonadCheckTerm m) =>
Constancy -> t -> m Constancy
forall (m :: * -> *).
MonadCheckTerm m =>
Constancy -> Type -> m Constancy
isConstant Constancy
force Type
t2
    isConstant Constancy
force ty :: Type
ty@Later{}
        | Constancy
force                    = Var -> m Constancy
forall a. Var -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Var -> m Constancy) -> Var -> m Constancy
forall a b. (a -> b) -> a -> b
$ Var
"non-constant type " Var -> Var -> Var
forall a. [a] -> [a] -> [a]
++ Type -> Var
forall a. Show a => a -> Var
show Type
ty
        | Constancy
otherwise                = Constancy -> m Constancy
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Constancy
False
    isConstant Constancy
force (TFix Var
x Type
t)  = ([(Var, Constancy)] -> Identity [(Var, Constancy)])
-> Environment -> Identity Environment
Lens' Environment [(Var, Constancy)]
typeCtx (([(Var, Constancy)] -> Identity [(Var, Constancy)])
 -> Environment -> Identity Environment)
-> ([(Var, Constancy)] -> [(Var, Constancy)])
-> Environment
-> Environment
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ ((Var
x, Constancy
False):) (Environment -> Environment) -> m Constancy -> m Constancy
forall {r} {m :: * -> *} {a}.
MonadReader r m =>
(r -> r) -> m a -> m a
|- Constancy -> Type -> m Constancy
forall t (m :: * -> *).
(Constant t, MonadCheckTerm m) =>
Constancy -> t -> m Constancy
forall (m :: * -> *).
MonadCheckTerm m =>
Constancy -> Type -> m Constancy
isConstant Constancy
force Type
t -- if the type is well-formed, we'll never encounter x
    isConstant Constancy
_     Type
_           = Constancy -> m Constancy
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Constancy
True

instance Constant Polytype where
    isConstant :: forall (m :: * -> *).
MonadCheckTerm m =>
Constancy -> Polytype -> m Constancy
isConstant Constancy
force (Forall [(Var, Constancy)]
xs Type
ty) = ([(Var, Constancy)] -> Identity [(Var, Constancy)])
-> Environment -> Identity Environment
Lens' Environment [(Var, Constancy)]
typeCtx (([(Var, Constancy)] -> Identity [(Var, Constancy)])
 -> Environment -> Identity Environment)
-> ([(Var, Constancy)] -> [(Var, Constancy)])
-> Environment
-> Environment
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ ([(Var, Constancy)]
xs ++) (Environment -> Environment) -> m Constancy -> m Constancy
forall {r} {m :: * -> *} {a}.
MonadReader r m =>
(r -> r) -> m a -> m a
|- Constancy -> Type -> m Constancy
forall t (m :: * -> *).
(Constant t, MonadCheckTerm m) =>
Constancy -> t -> m Constancy
forall (m :: * -> *).
MonadCheckTerm m =>
Constancy -> Type -> m Constancy
isConstant Constancy
force Type
ty

-- | A term is constant if it only refers to constant terms or terms with a constant type.
instance Constant Term where
    isConstant :: forall (m :: * -> *).
MonadCheckTerm m =>
Constancy -> Term -> m Constancy
isConstant Constancy
force Term
t = do
        Map Var (Polytype, Constancy)
ctx <- Getting
  (Map Var (Polytype, Constancy))
  Environment
  (Map Var (Polytype, Constancy))
-> m (Map Var (Polytype, Constancy))
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting
  (Map Var (Polytype, Constancy))
  Environment
  (Map Var (Polytype, Constancy))
Lens' Environment (Map Var (Polytype, Constancy))
termCtx
        Map Var Constancy -> Constancy
forall (t :: * -> *). Foldable t => t Constancy -> Constancy
and (Map Var Constancy -> Constancy)
-> m (Map Var Constancy) -> m Constancy
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Polytype, Constancy) -> m Constancy)
-> Map Var (Polytype, Constancy) -> m (Map Var Constancy)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Map Var a -> f (Map Var b)
traverse (Polytype, Constancy) -> m Constancy
forall {f :: * -> *} {t}.
(Constant t, MonadState UnificationState f,
 MonadReader Environment f, MonadError Var f) =>
(t, Constancy) -> f Constancy
constantBinding (Map Var (Polytype, Constancy)
ctx Map Var (Polytype, Constancy)
-> Set Var -> Map Var (Polytype, Constancy)
forall k a. Ord k => Map k a -> Set k -> Map k a
`Map.restrictKeys` Term -> Set Var
freeVars Term
t)
        where
        constantBinding :: (t, Constancy) -> f Constancy
constantBinding (t
_, Constancy
True) = Constancy -> f Constancy
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Constancy
True
        constantBinding (t
ty, Constancy
False) = Constancy -> t -> f Constancy
forall t (m :: * -> *).
(Constant t, MonadCheckTerm m) =>
Constancy -> t -> m Constancy
forall (m :: * -> *).
MonadCheckTerm m =>
Constancy -> t -> m Constancy
isConstant Constancy
force t
ty

-- * Unification

infix 5 !:=

-- | Attempt to assign a type to a metavariable.
-- Performs occurs check, scope check and constancy check.
(!:=) :: MonadCheckTerm m => (TVar, Meta) -> Type -> m ()
(Var
x, Meta
meta) !:= :: forall (m :: * -> *).
MonadCheckTerm m =>
(Var, Meta) -> Type -> m ()
!:= Type
ty
    | Just Type
sol <- Meta
meta Meta -> Getting (Maybe Type) Meta (Maybe Type) -> Maybe Type
forall s a. s -> Getting a s a -> a
^. Getting (Maybe Type) Meta (Maybe Type)
Lens' Meta (Maybe Type)
solution = Type
sol Type -> Type -> m ()
forall (m :: * -> *). MonadCheckTerm m => Type -> Type -> m ()
!~ Type
ty
    | Constancy
otherwise = Type -> m ()
forall {f :: * -> *}.
(MonadError Var f, MonadReader Environment f,
 MonadState UnificationState f) =>
Type -> f ()
assign (Type -> m ()) -> m Type -> m ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Type -> m Type
forall t (m :: * -> *). (Zonk t, MonadCheckTerm m) => t -> m t
forall (m :: * -> *). MonadCheckTerm m => Type -> m Type
zonk Type
ty where
    assign :: Type -> f ()
assign Type
ty
        | Type
ty Type -> Type -> Constancy
forall a. Eq a => a -> a -> Constancy
== Var -> Type
TVar Var
x = () -> f ()
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
        | Var
x Var -> Type -> Constancy
forall {t}. HasTVars t => Var -> t -> Constancy
`freeInType` Type
ty = Var -> f ()
forall a. Var -> f a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Var -> f ()) -> Var -> f ()
forall a b. (a -> b) -> a -> b
$ Var
"cannot construct infinite type " Var -> Var -> Var
forall a. [a] -> [a] -> [a]
++ Var
x Var -> Var -> Var
forall a. [a] -> [a] -> [a]
++ Var
" ~ " Var -> Var -> Var
forall a. [a] -> [a] -> [a]
++ Type -> Var
forall a. Show a => a -> Var
show Type
ty
        | Constancy
otherwise = do
            [(Var, Constancy)]
ctx <- Getting [(Var, Constancy)] Environment [(Var, Constancy)]
-> f [(Var, Constancy)]
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting [(Var, Constancy)] Environment [(Var, Constancy)]
Lens' Environment [(Var, Constancy)]
typeCtx
            let escaped :: [Var]
escaped = [Var
x | Var
x <- Set Var -> [Var]
forall a. Set a -> [a]
Set.toList (Type -> Set Var
forall t. HasTVars t => t -> Set Var
freeTVars Type
ty)
                             , Just (Constancy
_, Int
l) <- [Var -> [(Var, Constancy)] -> Maybe (Constancy, Int)
forall a b. Eq a => a -> [(a, b)] -> Maybe (b, Int)
lookupLevel Var
x [(Var, Constancy)]
ctx]
                             , Int
l Int -> Int -> Constancy
forall a. Ord a => a -> a -> Constancy
>= Meta
meta Meta -> Getting Int Meta Int -> Int
forall s a. s -> Getting a s a -> a
^. Getting Int Meta Int
Lens' Meta Int
level]
            Constancy -> f () -> f ()
forall (f :: * -> *). Applicative f => Constancy -> f () -> f ()
unless ([Var] -> Constancy
forall a. [a] -> Constancy
forall (t :: * -> *) a. Foldable t => t a -> Constancy
null [Var]
escaped) (f () -> f ()) -> f () -> f ()
forall a b. (a -> b) -> a -> b
$ Var -> f ()
forall a. Var -> f a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Var -> f ()) -> Var -> f ()
forall a b. (a -> b) -> a -> b
$
                Var
"cannot unify " Var -> Var -> Var
forall a. [a] -> [a] -> [a]
++ Var
x Var -> Var -> Var
forall a. [a] -> [a] -> [a]
++ Var
" with " Var -> Var -> Var
forall a. [a] -> [a] -> [a]
++ Type -> Var
forall a. Show a => a -> Var
show Type
ty Var -> Var -> Var
forall a. [a] -> [a] -> [a]
++ Var
": type variables " Var -> Var -> Var
forall a. [a] -> [a] -> [a]
++ [Type] -> Var
forall a. Show a => a -> Var
show ((Var -> Type) -> [Var] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Var -> Type
TVar [Var]
escaped) Var -> Var -> Var
forall a. [a] -> [a] -> [a]
++ Var
" would escape their scope"
            Constancy -> f () -> f ()
forall (f :: * -> *). Applicative f => Constancy -> f () -> f ()
when (Meta
meta Meta -> Getting Constancy Meta Constancy -> Constancy
forall s a. s -> Getting a s a -> a
^. Getting Constancy Meta Constancy
Lens' Meta Constancy
constant) (f () -> f ()) -> f () -> f ()
forall a b. (a -> b) -> a -> b
$ () () -> f Constancy -> f ()
forall a b. a -> f b -> f a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Constancy -> Type -> f Constancy
forall t (m :: * -> *).
(Constant t, MonadCheckTerm m) =>
Constancy -> t -> m Constancy
forall (m :: * -> *).
MonadCheckTerm m =>
Constancy -> Type -> m Constancy
isConstant Constancy
True Type
ty
            (Map Var Meta -> Identity (Map Var Meta))
-> UnificationState -> Identity UnificationState
Lens' UnificationState (Map Var Meta)
metas((Map Var Meta -> Identity (Map Var Meta))
 -> UnificationState -> Identity UnificationState)
-> ((Maybe Type -> Identity (Maybe Type))
    -> Map Var Meta -> Identity (Map Var Meta))
-> (Maybe Type -> Identity (Maybe Type))
-> UnificationState
-> Identity UnificationState
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Index (Map Var Meta)
-> Traversal' (Map Var Meta) (IxValue (Map Var Meta))
forall m. Ixed m => Index m -> Traversal' m (IxValue m)
ix Var
Index (Map Var Meta)
x((Meta -> Identity Meta)
 -> Map Var Meta -> Identity (Map Var Meta))
-> ((Maybe Type -> Identity (Maybe Type)) -> Meta -> Identity Meta)
-> (Maybe Type -> Identity (Maybe Type))
-> Map Var Meta
-> Identity (Map Var Meta)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(Maybe Type -> Identity (Maybe Type)) -> Meta -> Identity Meta
Lens' Meta (Maybe Type)
solution ((Maybe Type -> Identity (Maybe Type))
 -> UnificationState -> Identity UnificationState)
-> Type -> f ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a (Maybe b) -> b -> m ()
?= Type
ty

infix 4 !~

-- | Unify two types.
(!~) :: MonadCheckTerm m => Type -> Type -> m ()
Type
ta1 :*: Type
tb1  !~ :: forall (m :: * -> *). MonadCheckTerm m => Type -> Type -> m ()
!~ Type
ta2 :*: Type
tb2      = Type
ta1 Type -> Type -> m ()
forall (m :: * -> *). MonadCheckTerm m => Type -> Type -> m ()
!~ Type
ta2 m () -> m () -> m ()
forall a b. m a -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Type
tb1 Type -> Type -> m ()
forall (m :: * -> *). MonadCheckTerm m => Type -> Type -> m ()
!~ Type
tb2
Type
ta1 :+: Type
tb1  !~ Type
ta2 :+: Type
tb2      = Type
ta1 Type -> Type -> m ()
forall (m :: * -> *). MonadCheckTerm m => Type -> Type -> m ()
!~ Type
ta2 m () -> m () -> m ()
forall a b. m a -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Type
tb1 Type -> Type -> m ()
forall (m :: * -> *). MonadCheckTerm m => Type -> Type -> m ()
!~ Type
tb2
Type
ta1 :->: Type
tb1 !~ Type
ta2 :->: Type
tb2     = Type
ta1 Type -> Type -> m ()
forall (m :: * -> *). MonadCheckTerm m => Type -> Type -> m ()
!~ Type
ta2 m () -> m () -> m ()
forall a b. m a -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Type
tb1 Type -> Type -> m ()
forall (m :: * -> *). MonadCheckTerm m => Type -> Type -> m ()
!~ Type
tb2
Later Type
ty1    !~ Later Type
ty2        = Type
ty1 Type -> Type -> m ()
forall (m :: * -> *). MonadCheckTerm m => Type -> Type -> m ()
!~ Type
ty2
Constant Type
ty1 !~ Constant Type
ty2     = Type
ty1 Type -> Type -> m ()
forall (m :: * -> *). MonadCheckTerm m => Type -> Type -> m ()
!~ Type
ty2
TFix Var
x1 Type
tf1  !~ TFix Var
x2 Type
tf2      = ([(Var, Constancy)] -> Identity [(Var, Constancy)])
-> Environment -> Identity Environment
Lens' Environment [(Var, Constancy)]
typeCtx (([(Var, Constancy)] -> Identity [(Var, Constancy)])
 -> Environment -> Identity Environment)
-> ([(Var, Constancy)] -> [(Var, Constancy)])
-> Environment
-> Environment
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ ((Var
x1, Constancy
False):) (Environment -> Environment) -> m () -> m ()
forall {r} {m :: * -> *} {a}.
MonadReader r m =>
(r -> r) -> m a -> m a
|- Type
tf1 Type -> Type -> m ()
forall (m :: * -> *). MonadCheckTerm m => Type -> Type -> m ()
!~ Var -> Type -> Type -> Type
substituteType1 Var
x2 (Var -> Type
TVar Var
x1) Type
tf2
Type
ty1          !~ Type
ty2              = Type -> ((Var, Meta) -> m ()) -> m () -> m ()
forall (m :: * -> *).
MonadCheckTerm m =>
Type -> ((Var, Meta) -> m ()) -> m () -> m ()
ifMeta Type
ty1 ((Var, Meta) -> Type -> m ()
forall (m :: * -> *).
MonadCheckTerm m =>
(Var, Meta) -> Type -> m ()
!:= Type
ty2) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Type -> ((Var, Meta) -> m ()) -> m () -> m ()
forall (m :: * -> *).
MonadCheckTerm m =>
Type -> ((Var, Meta) -> m ()) -> m () -> m ()
ifMeta Type
ty2 ((Var, Meta) -> Type -> m ()
forall (m :: * -> *).
MonadCheckTerm m =>
(Var, Meta) -> Type -> m ()
!:= Type
ty1) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Constancy -> m () -> m ()
forall (f :: * -> *). Applicative f => Constancy -> f () -> f ()
unless (Type
ty1 Type -> Type -> Constancy
forall a. Eq a => a -> a -> Constancy
== Type
ty2) do
    Type
ty1 <- Type -> m Type
forall t (m :: * -> *). (Zonk t, MonadCheckTerm m) => t -> m t
forall (m :: * -> *). MonadCheckTerm m => Type -> m Type
zonk Type
ty1
    Type
ty2 <- Type -> m Type
forall t (m :: * -> *). (Zonk t, MonadCheckTerm m) => t -> m t
forall (m :: * -> *). MonadCheckTerm m => Type -> m Type
zonk Type
ty2
    Var -> m ()
forall a. Var -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Var -> m ()) -> Var -> m ()
forall a b. (a -> b) -> a -> b
$ Var
"cannot match type " Var -> Var -> Var
forall a. [a] -> [a] -> [a]
++ Type -> Var
forall a. Show a => a -> Var
show Type
ty1 Var -> Var -> Var
forall a. [a] -> [a] -> [a]
++ Var
" with " Var -> Var -> Var
forall a. [a] -> [a] -> [a]
++ Type -> Var
forall a. Show a => a -> Var
show Type
ty2

-- * Type checking and inference

-- | The type of the integer recursion operator.
intrecType :: Polytype
intrecType :: Polytype
intrecType = [(Var, Constancy)] -> Type -> Polytype
Forall [(Var
"a", Constancy
False)] ((Type
"a" Type -> Type -> Type
:->: Type
"a") Type -> Type -> Type
:->: Type
"a" Type -> Type -> Type
:->: (Type
"a" Type -> Type -> Type
:->: Type
"a") Type -> Type -> Type
:->: Type
TInt Type -> Type -> Type
:->: Type
"a")

class Types t where
    infix 4 !:

    -- | Check that a term has the given type.
    (!:) :: MonadCheckTerm m => Term -> t -> m ()

    -- | Infer a type for the given term.
    (?:) :: MonadCheckTerm m => Term -> m t

instance Types Type where
    Var Var
x !: :: forall (m :: * -> *). MonadCheckTerm m => Term -> Type -> m ()
!: Type
ty = Getting
  (Maybe (Polytype, Constancy))
  Environment
  (Maybe (Polytype, Constancy))
-> m (Maybe (Polytype, Constancy))
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view ((Map Var (Polytype, Constancy)
 -> Const
      (Maybe (Polytype, Constancy)) (Map Var (Polytype, Constancy)))
-> Environment -> Const (Maybe (Polytype, Constancy)) Environment
Lens' Environment (Map Var (Polytype, Constancy))
termCtx((Map Var (Polytype, Constancy)
  -> Const
       (Maybe (Polytype, Constancy)) (Map Var (Polytype, Constancy)))
 -> Environment -> Const (Maybe (Polytype, Constancy)) Environment)
-> ((Maybe (Polytype, Constancy)
     -> Const
          (Maybe (Polytype, Constancy)) (Maybe (Polytype, Constancy)))
    -> Map Var (Polytype, Constancy)
    -> Const
         (Maybe (Polytype, Constancy)) (Map Var (Polytype, Constancy)))
-> Getting
     (Maybe (Polytype, Constancy))
     Environment
     (Maybe (Polytype, Constancy))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Index (Map Var (Polytype, Constancy))
-> Lens'
     (Map Var (Polytype, Constancy))
     (Maybe (IxValue (Map Var (Polytype, Constancy))))
forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
at Var
Index (Map Var (Polytype, Constancy))
x) m (Maybe (Polytype, Constancy))
-> (Maybe (Polytype, Constancy) -> m ()) -> m ()
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Just (Polytype
tyx, Constancy
_) -> (Type
ty !~) (Type -> m ()) -> m Type -> m ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Polytype -> m Type
forall (m :: * -> *). MonadCheckTerm m => Polytype -> m Type
instantiate Polytype
tyx
        Maybe (Polytype, Constancy)
Nothing -> Var -> m ()
forall a. Var -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Var -> m ()) -> Var -> m ()
forall a b. (a -> b) -> a -> b
$ Var
"unbound variable " Var -> Var -> Var
forall a. [a] -> [a] -> [a]
++ Var
x
    Int{} !: Type
ty = Type
ty Type -> Type -> m ()
forall (m :: * -> *). MonadCheckTerm m => Type -> Type -> m ()
!~ Type
TInt
    Plus Term
a Term
b !: Type
ty = do
        Term
a Term -> Type -> m ()
forall t (m :: * -> *).
(Types t, MonadCheckTerm m) =>
Term -> t -> m ()
forall (m :: * -> *). MonadCheckTerm m => Term -> Type -> m ()
!: Type
TInt
        Term
b Term -> Type -> m ()
forall t (m :: * -> *).
(Types t, MonadCheckTerm m) =>
Term -> t -> m ()
forall (m :: * -> *). MonadCheckTerm m => Term -> Type -> m ()
!: Type
TInt
        Type
ty Type -> Type -> m ()
forall (m :: * -> *). MonadCheckTerm m => Type -> Type -> m ()
!~ Type
TInt
    Minus Term
a Term
b !: Type
ty = do
        Term
a Term -> Type -> m ()
forall t (m :: * -> *).
(Types t, MonadCheckTerm m) =>
Term -> t -> m ()
forall (m :: * -> *). MonadCheckTerm m => Term -> Type -> m ()
!: Type
TInt
        Term
b Term -> Type -> m ()
forall t (m :: * -> *).
(Types t, MonadCheckTerm m) =>
Term -> t -> m ()
forall (m :: * -> *). MonadCheckTerm m => Term -> Type -> m ()
!: Type
TInt
        Type
ty Type -> Type -> m ()
forall (m :: * -> *). MonadCheckTerm m => Type -> Type -> m ()
!~ Type
TInt
    Times Term
a Term
b !: Type
ty = do
        Term
a Term -> Type -> m ()
forall t (m :: * -> *).
(Types t, MonadCheckTerm m) =>
Term -> t -> m ()
forall (m :: * -> *). MonadCheckTerm m => Term -> Type -> m ()
!: Type
TInt
        Term
b Term -> Type -> m ()
forall t (m :: * -> *).
(Types t, MonadCheckTerm m) =>
Term -> t -> m ()
forall (m :: * -> *). MonadCheckTerm m => Term -> Type -> m ()
!: Type
TInt
        Type
ty Type -> Type -> m ()
forall (m :: * -> *). MonadCheckTerm m => Type -> Type -> m ()
!~ Type
TInt
    Divide Term
a Term
b !: Type
ty = do
        Term
a Term -> Type -> m ()
forall t (m :: * -> *).
(Types t, MonadCheckTerm m) =>
Term -> t -> m ()
forall (m :: * -> *). MonadCheckTerm m => Term -> Type -> m ()
!: Type
TInt
        Term
b Term -> Type -> m ()
forall t (m :: * -> *).
(Types t, MonadCheckTerm m) =>
Term -> t -> m ()
forall (m :: * -> *). MonadCheckTerm m => Term -> Type -> m ()
!: Type
TInt
        Type
ty Type -> Type -> m ()
forall (m :: * -> *). MonadCheckTerm m => Type -> Type -> m ()
!~ Type
TInt
    Term
IntRec !: Type
ty = (Type
ty !~) (Type -> m ()) -> m Type -> m ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Polytype -> m Type
forall (m :: * -> *). MonadCheckTerm m => Polytype -> m Type
instantiate Polytype
intrecType
    Term
Unit !: Type
ty = Type
ty Type -> Type -> m ()
forall (m :: * -> *). MonadCheckTerm m => Type -> Type -> m ()
!~ Type
One
    Pair Term
a Term
b !: Type
ty = do
        ~[Type
ta, Type
tb] <- Int -> m [Type]
forall {m :: * -> *}.
(MonadState UnificationState m, MonadReader Environment m,
 MonadError Var m) =>
Int -> m [Type]
newMetas Int
2
        Type
ty Type -> Type -> m ()
forall (m :: * -> *). MonadCheckTerm m => Type -> Type -> m ()
!~ Type
ta Type -> Type -> Type
:*: Type
tb
        Term
a Term -> Type -> m ()
forall t (m :: * -> *).
(Types t, MonadCheckTerm m) =>
Term -> t -> m ()
forall (m :: * -> *). MonadCheckTerm m => Term -> Type -> m ()
!: Type
ta
        Term
b Term -> Type -> m ()
forall t (m :: * -> *).
(Types t, MonadCheckTerm m) =>
Term -> t -> m ()
forall (m :: * -> *). MonadCheckTerm m => Term -> Type -> m ()
!: Type
tb
    Fst Term
t !: Type
ty = do
        Type
tb <- m Type
forall {m :: * -> *}.
(MonadState UnificationState m, MonadReader Environment m,
 MonadError Var m) =>
m Type
newMeta
        Term
t Term -> Type -> m ()
forall t (m :: * -> *).
(Types t, MonadCheckTerm m) =>
Term -> t -> m ()
forall (m :: * -> *). MonadCheckTerm m => Term -> Type -> m ()
!: Type
ty Type -> Type -> Type
:*: Type
tb
    Snd Term
t !: Type
ty = do
        Type
ta <- m Type
forall {m :: * -> *}.
(MonadState UnificationState m, MonadReader Environment m,
 MonadError Var m) =>
m Type
newMeta
        Term
t Term -> Type -> m ()
forall t (m :: * -> *).
(Types t, MonadCheckTerm m) =>
Term -> t -> m ()
forall (m :: * -> *). MonadCheckTerm m => Term -> Type -> m ()
!: Type
ta Type -> Type -> Type
:*: Type
ty
    Abort Term
t !: Type
_ = Term
t Term -> Type -> m ()
forall t (m :: * -> *).
(Types t, MonadCheckTerm m) =>
Term -> t -> m ()
forall (m :: * -> *). MonadCheckTerm m => Term -> Type -> m ()
!: Type
Zero
    InL Term
t !: Type
ty = do
        ~[Type
ta, Type
tb] <- Int -> m [Type]
forall {m :: * -> *}.
(MonadState UnificationState m, MonadReader Environment m,
 MonadError Var m) =>
Int -> m [Type]
newMetas Int
2
        Type
ty Type -> Type -> m ()
forall (m :: * -> *). MonadCheckTerm m => Type -> Type -> m ()
!~ Type
ta Type -> Type -> Type
:+: Type
tb
        Term
t Term -> Type -> m ()
forall t (m :: * -> *).
(Types t, MonadCheckTerm m) =>
Term -> t -> m ()
forall (m :: * -> *). MonadCheckTerm m => Term -> Type -> m ()
!: Type
ta
    InR Term
t !: Type
ty = do
        ~[Type
ta, Type
tb] <- Int -> m [Type]
forall {m :: * -> *}.
(MonadState UnificationState m, MonadReader Environment m,
 MonadError Var m) =>
Int -> m [Type]
newMetas Int
2
        Type
ty Type -> Type -> m ()
forall (m :: * -> *). MonadCheckTerm m => Type -> Type -> m ()
!~ Type
ta Type -> Type -> Type
:+: Type
tb
        Term
t Term -> Type -> m ()
forall t (m :: * -> *).
(Types t, MonadCheckTerm m) =>
Term -> t -> m ()
forall (m :: * -> *). MonadCheckTerm m => Term -> Type -> m ()
!: Type
tb
    Case Term
t ~(Abs Var
x1 Term
t1) ~(Abs Var
x2 Term
t2) !: Type
ty = do
        ~[Type
ta, Type
tb] <- Int -> m [Type]
forall {m :: * -> *}.
(MonadState UnificationState m, MonadReader Environment m,
 MonadError Var m) =>
Int -> m [Type]
newMetas Int
2
        Term
t Term -> Type -> m ()
forall t (m :: * -> *).
(Types t, MonadCheckTerm m) =>
Term -> t -> m ()
forall (m :: * -> *). MonadCheckTerm m => Term -> Type -> m ()
!: Type
ta Type -> Type -> Type
:+: Type
tb
        Constancy
constant <- Constancy -> Term -> m Constancy
forall t (m :: * -> *).
(Constant t, MonadCheckTerm m) =>
Constancy -> t -> m Constancy
forall (m :: * -> *).
MonadCheckTerm m =>
Constancy -> Term -> m Constancy
isConstant Constancy
False Term
t
        (Map Var (Polytype, Constancy)
 -> Identity (Map Var (Polytype, Constancy)))
-> Environment -> Identity Environment
Lens' Environment (Map Var (Polytype, Constancy))
termCtx((Map Var (Polytype, Constancy)
  -> Identity (Map Var (Polytype, Constancy)))
 -> Environment -> Identity Environment)
-> ((Maybe (Polytype, Constancy)
     -> Identity (Maybe (Polytype, Constancy)))
    -> Map Var (Polytype, Constancy)
    -> Identity (Map Var (Polytype, Constancy)))
-> (Maybe (Polytype, Constancy)
    -> Identity (Maybe (Polytype, Constancy)))
-> Environment
-> Identity Environment
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Index (Map Var (Polytype, Constancy))
-> Lens'
     (Map Var (Polytype, Constancy))
     (Maybe (IxValue (Map Var (Polytype, Constancy))))
forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
at Var
Index (Map Var (Polytype, Constancy))
x1 ((Maybe (Polytype, Constancy)
  -> Identity (Maybe (Polytype, Constancy)))
 -> Environment -> Identity Environment)
-> (Polytype, Constancy) -> Environment -> Environment
forall s t a b. ASetter s t a (Maybe b) -> b -> s -> t
?~ (Type -> Polytype
Monotype Type
ta, Constancy
constant) (Environment -> Environment) -> m () -> m ()
forall {r} {m :: * -> *} {a}.
MonadReader r m =>
(r -> r) -> m a -> m a
|- Term
t1 Term -> Type -> m ()
forall t (m :: * -> *).
(Types t, MonadCheckTerm m) =>
Term -> t -> m ()
forall (m :: * -> *). MonadCheckTerm m => Term -> Type -> m ()
!: Type
ty
        (Map Var (Polytype, Constancy)
 -> Identity (Map Var (Polytype, Constancy)))
-> Environment -> Identity Environment
Lens' Environment (Map Var (Polytype, Constancy))
termCtx((Map Var (Polytype, Constancy)
  -> Identity (Map Var (Polytype, Constancy)))
 -> Environment -> Identity Environment)
-> ((Maybe (Polytype, Constancy)
     -> Identity (Maybe (Polytype, Constancy)))
    -> Map Var (Polytype, Constancy)
    -> Identity (Map Var (Polytype, Constancy)))
-> (Maybe (Polytype, Constancy)
    -> Identity (Maybe (Polytype, Constancy)))
-> Environment
-> Identity Environment
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Index (Map Var (Polytype, Constancy))
-> Lens'
     (Map Var (Polytype, Constancy))
     (Maybe (IxValue (Map Var (Polytype, Constancy))))
forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
at Var
Index (Map Var (Polytype, Constancy))
x2 ((Maybe (Polytype, Constancy)
  -> Identity (Maybe (Polytype, Constancy)))
 -> Environment -> Identity Environment)
-> (Polytype, Constancy) -> Environment -> Environment
forall s t a b. ASetter s t a (Maybe b) -> b -> s -> t
?~ (Type -> Polytype
Monotype Type
tb, Constancy
constant) (Environment -> Environment) -> m () -> m ()
forall {r} {m :: * -> *} {a}.
MonadReader r m =>
(r -> r) -> m a -> m a
|- Term
t2 Term -> Type -> m ()
forall t (m :: * -> *).
(Types t, MonadCheckTerm m) =>
Term -> t -> m ()
forall (m :: * -> *). MonadCheckTerm m => Term -> Type -> m ()
!: Type
ty
    Abs Var
x Term
t !: Type
ty = do
        ~[Type
ta, Type
tb] <- Int -> m [Type]
forall {m :: * -> *}.
(MonadState UnificationState m, MonadReader Environment m,
 MonadError Var m) =>
Int -> m [Type]
newMetas Int
2
        Type
ty Type -> Type -> m ()
forall (m :: * -> *). MonadCheckTerm m => Type -> Type -> m ()
!~ Type
ta Type -> Type -> Type
:->: Type
tb
        (Map Var (Polytype, Constancy)
 -> Identity (Map Var (Polytype, Constancy)))
-> Environment -> Identity Environment
Lens' Environment (Map Var (Polytype, Constancy))
termCtx((Map Var (Polytype, Constancy)
  -> Identity (Map Var (Polytype, Constancy)))
 -> Environment -> Identity Environment)
-> ((Maybe (Polytype, Constancy)
     -> Identity (Maybe (Polytype, Constancy)))
    -> Map Var (Polytype, Constancy)
    -> Identity (Map Var (Polytype, Constancy)))
-> (Maybe (Polytype, Constancy)
    -> Identity (Maybe (Polytype, Constancy)))
-> Environment
-> Identity Environment
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Index (Map Var (Polytype, Constancy))
-> Lens'
     (Map Var (Polytype, Constancy))
     (Maybe (IxValue (Map Var (Polytype, Constancy))))
forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
at Var
Index (Map Var (Polytype, Constancy))
x ((Maybe (Polytype, Constancy)
  -> Identity (Maybe (Polytype, Constancy)))
 -> Environment -> Identity Environment)
-> (Polytype, Constancy) -> Environment -> Environment
forall s t a b. ASetter s t a (Maybe b) -> b -> s -> t
?~ (Type -> Polytype
Monotype Type
ta, Constancy
False) (Environment -> Environment) -> m () -> m ()
forall {r} {m :: * -> *} {a}.
MonadReader r m =>
(r -> r) -> m a -> m a
|- Term
t Term -> Type -> m ()
forall t (m :: * -> *).
(Types t, MonadCheckTerm m) =>
Term -> t -> m ()
forall (m :: * -> *). MonadCheckTerm m => Term -> Type -> m ()
!: Type
tb
    Term
s :$: Term
t !: Type
ty = do
        Type
ta <- m Type
forall {m :: * -> *}.
(MonadState UnificationState m, MonadReader Environment m,
 MonadError Var m) =>
m Type
newMeta
        Term
s Term -> Type -> m ()
forall t (m :: * -> *).
(Types t, MonadCheckTerm m) =>
Term -> t -> m ()
forall (m :: * -> *). MonadCheckTerm m => Term -> Type -> m ()
!: Type
ta Type -> Type -> Type
:->: Type
ty
        Term
t Term -> Type -> m ()
forall t (m :: * -> *).
(Types t, MonadCheckTerm m) =>
Term -> t -> m ()
forall (m :: * -> *). MonadCheckTerm m => Term -> Type -> m ()
!: Type
ta
    Let Subst
s Term
t !: Type
ty = do
        Map Var (Polytype, Constancy)
e <- Subst
-> (Term -> m (Polytype, Constancy))
-> m (Map Var (Polytype, Constancy))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for Subst
s \Term
t' -> do
            Polytype
ty <- (Term
t' ?:)
            Constancy
constant <- Constancy -> Term -> m Constancy
forall t (m :: * -> *).
(Constant t, MonadCheckTerm m) =>
Constancy -> t -> m Constancy
forall (m :: * -> *).
MonadCheckTerm m =>
Constancy -> Term -> m Constancy
isConstant Constancy
False Term
t'
            pure (Polytype
ty, Constancy
constant)
        (Map Var (Polytype, Constancy)
 -> Identity (Map Var (Polytype, Constancy)))
-> Environment -> Identity Environment
Lens' Environment (Map Var (Polytype, Constancy))
termCtx ((Map Var (Polytype, Constancy)
  -> Identity (Map Var (Polytype, Constancy)))
 -> Environment -> Identity Environment)
-> (Map Var (Polytype, Constancy) -> Map Var (Polytype, Constancy))
-> Environment
-> Environment
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ Map Var (Polytype, Constancy)
-> Map Var (Polytype, Constancy) -> Map Var (Polytype, Constancy)
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map Var (Polytype, Constancy)
e (Environment -> Environment) -> m () -> m ()
forall {r} {m :: * -> *} {a}.
MonadReader r m =>
(r -> r) -> m a -> m a
|- Term
t Term -> Type -> m ()
forall t (m :: * -> *).
(Types t, MonadCheckTerm m) =>
Term -> t -> m ()
forall (m :: * -> *). MonadCheckTerm m => Term -> Type -> m ()
!: Type
ty
    Fold Term
t !: Type
ty = do
        Type
ty <- Type -> m Type
forall t (m :: * -> *). (Zonk t, MonadCheckTerm m) => t -> m t
forall (m :: * -> *). MonadCheckTerm m => Type -> m Type
zonk Type
ty
        case Type
ty of
            TFix Var
x Type
tf -> Term
t Term -> Type -> m ()
forall t (m :: * -> *).
(Types t, MonadCheckTerm m) =>
Term -> t -> m ()
forall (m :: * -> *). MonadCheckTerm m => Term -> Type -> m ()
!: Var -> Type -> Type -> Type
substituteType1 Var
x Type
ty Type
tf
            Type
_ -> Var -> m ()
forall a. Var -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Var -> m ()) -> Var -> m ()
forall a b. (a -> b) -> a -> b
$ Var
"bad type for fold: " Var -> Var -> Var
forall a. [a] -> [a] -> [a]
++ Type -> Var
forall a. Show a => a -> Var
show Type
ty
    Unfold Term
t !: Type
ty = do
        Type
ty' <- Type -> m Type
forall t (m :: * -> *). (Zonk t, MonadCheckTerm m) => t -> m t
forall (m :: * -> *). MonadCheckTerm m => Type -> m Type
zonk (Type -> m Type) -> m Type -> m Type
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Term
t ?:)
        case Type
ty' of
            TFix Var
x Type
tf -> Type
ty Type -> Type -> m ()
forall (m :: * -> *). MonadCheckTerm m => Type -> Type -> m ()
!~ Var -> Type -> Type -> Type
substituteType1 Var
x Type
ty' Type
tf
            Type
_ -> Var -> m ()
forall a. Var -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Var -> m ()) -> Var -> m ()
forall a b. (a -> b) -> a -> b
$ Var
"bad type for unfold: " Var -> Var -> Var
forall a. [a] -> [a] -> [a]
++ Type -> Var
forall a. Show a => a -> Var
show Type
ty'
    Fix ~(Abs Var
x Term
t) !: Type
ty = (Map Var (Polytype, Constancy)
 -> Identity (Map Var (Polytype, Constancy)))
-> Environment -> Identity Environment
Lens' Environment (Map Var (Polytype, Constancy))
termCtx((Map Var (Polytype, Constancy)
  -> Identity (Map Var (Polytype, Constancy)))
 -> Environment -> Identity Environment)
-> ((Maybe (Polytype, Constancy)
     -> Identity (Maybe (Polytype, Constancy)))
    -> Map Var (Polytype, Constancy)
    -> Identity (Map Var (Polytype, Constancy)))
-> (Maybe (Polytype, Constancy)
    -> Identity (Maybe (Polytype, Constancy)))
-> Environment
-> Identity Environment
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Index (Map Var (Polytype, Constancy))
-> Lens'
     (Map Var (Polytype, Constancy))
     (Maybe (IxValue (Map Var (Polytype, Constancy))))
forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
at Var
Index (Map Var (Polytype, Constancy))
x ((Maybe (Polytype, Constancy)
  -> Identity (Maybe (Polytype, Constancy)))
 -> Environment -> Identity Environment)
-> (Polytype, Constancy) -> Environment -> Environment
forall s t a b. ASetter s t a (Maybe b) -> b -> s -> t
?~ (Type -> Polytype
Monotype (Type -> Type
Later Type
ty), Constancy
False) (Environment -> Environment) -> m () -> m ()
forall {r} {m :: * -> *} {a}.
MonadReader r m =>
(r -> r) -> m a -> m a
|- Term
t Term -> Type -> m ()
forall t (m :: * -> *).
(Types t, MonadCheckTerm m) =>
Term -> t -> m ()
forall (m :: * -> *). MonadCheckTerm m => Term -> Type -> m ()
!: Type
ty
    Next Term
t !: Type
ty = do
        Type
ta <- m Type
forall {m :: * -> *}.
(MonadState UnificationState m, MonadReader Environment m,
 MonadError Var m) =>
m Type
newMeta
        Type
ty Type -> Type -> m ()
forall (m :: * -> *). MonadCheckTerm m => Type -> Type -> m ()
!~ Type -> Type
Later Type
ta
        Term
t Term -> Type -> m ()
forall t (m :: * -> *).
(Types t, MonadCheckTerm m) =>
Term -> t -> m ()
forall (m :: * -> *). MonadCheckTerm m => Term -> Type -> m ()
!: Type
ta
    Prev Term
t !: Type
ty = do
        Term
t Term -> Type -> m ()
forall t (m :: * -> *).
(Types t, MonadCheckTerm m) =>
Term -> t -> m ()
forall (m :: * -> *). MonadCheckTerm m => Term -> Type -> m ()
!: Type -> Type
Later Type
ty
        () () -> m Constancy -> m ()
forall a b. a -> m b -> m a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Constancy -> Term -> m Constancy
forall t (m :: * -> *).
(Constant t, MonadCheckTerm m) =>
Constancy -> t -> m Constancy
forall (m :: * -> *).
MonadCheckTerm m =>
Constancy -> Term -> m Constancy
isConstant Constancy
True Term
t
    Term
s :<*>: Term
t !: Type
ty = do
        ~[Type
ta, Type
tb] <- Int -> m [Type]
forall {m :: * -> *}.
(MonadState UnificationState m, MonadReader Environment m,
 MonadError Var m) =>
Int -> m [Type]
newMetas Int
2
        Type
ty Type -> Type -> m ()
forall (m :: * -> *). MonadCheckTerm m => Type -> Type -> m ()
!~ Type -> Type
Later Type
ta
        Term
t Term -> Type -> m ()
forall t (m :: * -> *).
(Types t, MonadCheckTerm m) =>
Term -> t -> m ()
forall (m :: * -> *). MonadCheckTerm m => Term -> Type -> m ()
!: Type -> Type
Later Type
tb
        Term
s Term -> Type -> m ()
forall t (m :: * -> *).
(Types t, MonadCheckTerm m) =>
Term -> t -> m ()
forall (m :: * -> *). MonadCheckTerm m => Term -> Type -> m ()
!: Type -> Type
Later (Type
tb Type -> Type -> Type
:->: Type
ta)
    Box Term
t !: Type
ty = do
        Type
ta <- m Type
forall {m :: * -> *}.
(MonadState UnificationState m, MonadReader Environment m,
 MonadError Var m) =>
m Type
newMeta
        Type
ty Type -> Type -> m ()
forall (m :: * -> *). MonadCheckTerm m => Type -> Type -> m ()
!~ Type -> Type
Constant Type
ta
        Term
t Term -> Type -> m ()
forall t (m :: * -> *).
(Types t, MonadCheckTerm m) =>
Term -> t -> m ()
forall (m :: * -> *). MonadCheckTerm m => Term -> Type -> m ()
!: Type
ta
        () () -> m Constancy -> m ()
forall a b. a -> m b -> m a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Constancy -> Term -> m Constancy
forall t (m :: * -> *).
(Constant t, MonadCheckTerm m) =>
Constancy -> t -> m Constancy
forall (m :: * -> *).
MonadCheckTerm m =>
Constancy -> Term -> m Constancy
isConstant Constancy
True Term
t
    Unbox Term
t !: Type
ty = Term
t Term -> Type -> m ()
forall t (m :: * -> *).
(Types t, MonadCheckTerm m) =>
Term -> t -> m ()
forall (m :: * -> *). MonadCheckTerm m => Term -> Type -> m ()
!: Type -> Type
Constant Type
ty

    ?: :: forall (m :: * -> *). MonadCheckTerm m => Term -> m Type
(?:) Term
t = do
        Type
ty <- m Type
forall {m :: * -> *}.
(MonadState UnificationState m, MonadReader Environment m,
 MonadError Var m) =>
m Type
newMeta
        Term
t Term -> Type -> m ()
forall t (m :: * -> *).
(Types t, MonadCheckTerm m) =>
Term -> t -> m ()
forall (m :: * -> *). MonadCheckTerm m => Term -> Type -> m ()
!: Type
ty
        pure Type
ty

instance Types Polytype where
    Term
t !: :: forall (m :: * -> *). MonadCheckTerm m => Term -> Polytype -> m ()
!: Forall [(Var, Constancy)]
xs Type
ty = ([(Var, Constancy)] -> Identity [(Var, Constancy)])
-> Environment -> Identity Environment
Lens' Environment [(Var, Constancy)]
typeCtx (([(Var, Constancy)] -> Identity [(Var, Constancy)])
 -> Environment -> Identity Environment)
-> ([(Var, Constancy)] -> [(Var, Constancy)])
-> Environment
-> Environment
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ ([(Var, Constancy)]
xs ++) (Environment -> Environment) -> m () -> m ()
forall {r} {m :: * -> *} {a}.
MonadReader r m =>
(r -> r) -> m a -> m a
|- Term
t Term -> Type -> m ()
forall t (m :: * -> *).
(Types t, MonadCheckTerm m) =>
Term -> t -> m ()
forall (m :: * -> *). MonadCheckTerm m => Term -> Type -> m ()
!: Type
ty

    ?: :: forall (m :: * -> *). MonadCheckTerm m => Term -> m Polytype
(?:) = Term -> m Type
forall t (m :: * -> *). (Types t, MonadCheckTerm m) => Term -> m t
forall (m :: * -> *). MonadCheckTerm m => Term -> m Type
(?:) (Term -> m Type) -> (Type -> m Polytype) -> Term -> m Polytype
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Type -> m Polytype
forall (m :: * -> *). MonadCheckTerm m => Type -> m Polytype
generalise

checkTerm :: Term -> t -> m ()
checkTerm Term
t t
ty = StateT UnificationState m () -> Set Var -> m ()
forall {m :: * -> *} {a}.
Monad m =>
StateT UnificationState m a -> Set Var -> m a
runUnification (Term
t Term -> t -> StateT UnificationState m ()
forall t (m :: * -> *).
(Types t, MonadCheckTerm m) =>
Term -> t -> m ()
forall (m :: * -> *). MonadCheckTerm m => Term -> t -> m ()
!: t
ty) (t -> Set Var
forall t. HasTVars t => t -> Set Var
allTVars t
ty)

inferTerm :: Term -> f Polytype
inferTerm Term
t = Polytype -> Polytype
alphaNormalise (Polytype -> Polytype) -> f Polytype -> f Polytype
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT UnificationState f Polytype -> Set Var -> f Polytype
forall {m :: * -> *} {a}.
Monad m =>
StateT UnificationState m a -> Set Var -> m a
runUnification (Term
t ?:) Set Var
forall a. Monoid a => a
mempty