{-# OPTIONS_GHC -fno-warn-unused-binds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
module PlutusCore.TypeCheck.Internal
where
import PlutusCore.Builtin
import PlutusCore.Core
import PlutusCore.Error
import PlutusCore.MkPlc
import PlutusCore.Name
import PlutusCore.Normalize.Internal qualified as Norm
import PlutusCore.Quote
import PlutusCore.Rename
import PlutusPrelude
import Control.Lens
import Control.Monad.Error.Lens
import Control.Monad.Except
import Control.Monad.Reader
import Data.Array
import Universe
newtype BuiltinTypes uni fun = BuiltinTypes
{ BuiltinTypes uni fun
-> Maybe (Array fun (Dupable (Normalized (Type TyName uni ()))))
unBuiltinTypes :: Maybe (Array fun (Dupable (Normalized (Type TyName uni ()))))
}
type TyVarKinds = UniqueMap TypeUnique (Kind ())
type VarTypes uni = UniqueMap TermUnique (Dupable (Normalized (Type TyName uni ())))
newtype TypeCheckConfig uni fun = TypeCheckConfig
{ TypeCheckConfig uni fun -> BuiltinTypes uni fun
_tccBuiltinTypes :: BuiltinTypes uni fun
}
makeClassy ''TypeCheckConfig
data TypeCheckEnv uni fun cfg = TypeCheckEnv
{ TypeCheckEnv uni fun cfg -> cfg
_tceTypeCheckConfig :: cfg
, TypeCheckEnv uni fun cfg -> TyVarKinds
_tceTyVarKinds :: TyVarKinds
, TypeCheckEnv uni fun cfg -> VarTypes uni
_tceVarTypes :: VarTypes uni
}
makeLenses ''TypeCheckEnv
type TypeCheckM uni fun cfg err = ReaderT (TypeCheckEnv uni fun cfg) (ExceptT err Quote)
runTypeCheckM :: (MonadError err m, MonadQuote m) => cfg -> TypeCheckM uni fun cfg err a -> m a
runTypeCheckM :: cfg -> TypeCheckM uni fun cfg err a -> m a
runTypeCheckM cfg
config TypeCheckM uni fun cfg err a
a =
Either err a -> m a
forall e (m :: * -> *) a. MonadError e m => Either e a -> m a
liftEither (Either err a -> m a) -> m (Either err a) -> m a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Quote (Either err a) -> m (Either err a)
forall (m :: * -> *) a. MonadQuote m => Quote a -> m a
liftQuote (ExceptT err Quote a -> Quote (Either err a)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT err Quote a -> Quote (Either err a))
-> ExceptT err Quote a -> Quote (Either err a)
forall a b. (a -> b) -> a -> b
$ TypeCheckM uni fun cfg err a
-> TypeCheckEnv uni fun cfg -> ExceptT err Quote a
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT TypeCheckM uni fun cfg err a
a TypeCheckEnv uni fun cfg
forall (uni :: * -> *) fun. TypeCheckEnv uni fun cfg
env) where
env :: TypeCheckEnv uni fun cfg
env = cfg -> TyVarKinds -> VarTypes uni -> TypeCheckEnv uni fun cfg
forall (uni :: * -> *) fun cfg.
cfg -> TyVarKinds -> VarTypes uni -> TypeCheckEnv uni fun cfg
TypeCheckEnv cfg
config TyVarKinds
forall a. Monoid a => a
mempty VarTypes uni
forall a. Monoid a => a
mempty
withTyVar :: TyName -> Kind () -> TypeCheckM uni fun cfg err a -> TypeCheckM uni fun cfg err a
withTyVar :: TyName
-> Kind ()
-> TypeCheckM uni fun cfg err a
-> TypeCheckM uni fun cfg err a
withTyVar TyName
name = (TypeCheckEnv uni fun cfg -> TypeCheckEnv uni fun cfg)
-> TypeCheckM uni fun cfg err a -> TypeCheckM uni fun cfg err a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((TypeCheckEnv uni fun cfg -> TypeCheckEnv uni fun cfg)
-> TypeCheckM uni fun cfg err a -> TypeCheckM uni fun cfg err a)
-> (Kind ()
-> TypeCheckEnv uni fun cfg -> TypeCheckEnv uni fun cfg)
-> Kind ()
-> TypeCheckM uni fun cfg err a
-> TypeCheckM uni fun cfg err a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ASetter
(TypeCheckEnv uni fun cfg)
(TypeCheckEnv uni fun cfg)
TyVarKinds
TyVarKinds
-> (TyVarKinds -> TyVarKinds)
-> TypeCheckEnv uni fun cfg
-> TypeCheckEnv uni fun cfg
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter
(TypeCheckEnv uni fun cfg)
(TypeCheckEnv uni fun cfg)
TyVarKinds
TyVarKinds
forall (uni :: * -> *) fun cfg fun.
Lens
(TypeCheckEnv uni fun cfg)
(TypeCheckEnv uni fun cfg)
TyVarKinds
TyVarKinds
tceTyVarKinds ((TyVarKinds -> TyVarKinds)
-> TypeCheckEnv uni fun cfg -> TypeCheckEnv uni fun cfg)
-> (Kind () -> TyVarKinds -> TyVarKinds)
-> Kind ()
-> TypeCheckEnv uni fun cfg
-> TypeCheckEnv uni fun cfg
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyName -> Kind () -> TyVarKinds -> TyVarKinds
forall name unique a.
HasUnique name unique =>
name -> a -> UniqueMap unique a -> UniqueMap unique a
insertByName TyName
name
lookupBuiltinM
:: (AsTypeError err term uni fun ann, HasTypeCheckConfig cfg uni fun, Ix fun)
=> ann -> fun -> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
lookupBuiltinM :: ann
-> fun
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
lookupBuiltinM ann
ann fun
fun = do
BuiltinTypes Maybe (Array fun (Dupable (Normalized (Type TyName uni ()))))
mayArr <- Getting
(BuiltinTypes uni fun)
(TypeCheckEnv uni fun cfg)
(BuiltinTypes uni fun)
-> ReaderT
(TypeCheckEnv uni fun cfg)
(ExceptT err Quote)
(BuiltinTypes uni fun)
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view (Getting
(BuiltinTypes uni fun)
(TypeCheckEnv uni fun cfg)
(BuiltinTypes uni fun)
-> ReaderT
(TypeCheckEnv uni fun cfg)
(ExceptT err Quote)
(BuiltinTypes uni fun))
-> Getting
(BuiltinTypes uni fun)
(TypeCheckEnv uni fun cfg)
(BuiltinTypes uni fun)
-> ReaderT
(TypeCheckEnv uni fun cfg)
(ExceptT err Quote)
(BuiltinTypes uni fun)
forall a b. (a -> b) -> a -> b
$ (cfg -> Const (BuiltinTypes uni fun) cfg)
-> TypeCheckEnv uni fun cfg
-> Const (BuiltinTypes uni fun) (TypeCheckEnv uni fun cfg)
forall (uni :: * -> *) fun cfg fun cfg.
Lens (TypeCheckEnv uni fun cfg) (TypeCheckEnv uni fun cfg) cfg cfg
tceTypeCheckConfig ((cfg -> Const (BuiltinTypes uni fun) cfg)
-> TypeCheckEnv uni fun cfg
-> Const (BuiltinTypes uni fun) (TypeCheckEnv uni fun cfg))
-> ((BuiltinTypes uni fun
-> Const (BuiltinTypes uni fun) (BuiltinTypes uni fun))
-> cfg -> Const (BuiltinTypes uni fun) cfg)
-> Getting
(BuiltinTypes uni fun)
(TypeCheckEnv uni fun cfg)
(BuiltinTypes uni fun)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (BuiltinTypes uni fun
-> Const (BuiltinTypes uni fun) (BuiltinTypes uni fun))
-> cfg -> Const (BuiltinTypes uni fun) cfg
forall c (uni :: * -> *) fun.
HasTypeCheckConfig c uni fun =>
Lens' c (BuiltinTypes uni fun)
tccBuiltinTypes
case Maybe (Array fun (Dupable (Normalized (Type TyName uni ()))))
mayArr Maybe (Array fun (Dupable (Normalized (Type TyName uni ()))))
-> (Array fun (Dupable (Normalized (Type TyName uni ())))
-> Maybe (Dupable (Normalized (Type TyName uni ()))))
-> Maybe (Dupable (Normalized (Type TyName uni ())))
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Getting
(First (Dupable (Normalized (Type TyName uni ()))))
(Array fun (Dupable (Normalized (Type TyName uni ()))))
(Dupable (Normalized (Type TyName uni ())))
-> Array fun (Dupable (Normalized (Type TyName uni ())))
-> Maybe (Dupable (Normalized (Type TyName uni ())))
forall s (m :: * -> *) a.
MonadReader s m =>
Getting (First a) s a -> m (Maybe a)
preview (Index (Array fun (Dupable (Normalized (Type TyName uni ()))))
-> Traversal'
(Array fun (Dupable (Normalized (Type TyName uni ()))))
(IxValue (Array fun (Dupable (Normalized (Type TyName uni ())))))
forall m. Ixed m => Index m -> Traversal' m (IxValue m)
ix fun
Index (Array fun (Dupable (Normalized (Type TyName uni ()))))
fun) of
Maybe (Dupable (Normalized (Type TyName uni ())))
Nothing -> AReview err (TypeError term uni fun ann)
-> TypeError term uni fun ann
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall e (m :: * -> *) t x.
MonadError e m =>
AReview e t -> t -> m x
throwing AReview err (TypeError term uni fun ann)
forall r term (uni :: * -> *) fun ann.
AsTypeError r term uni fun ann =>
Prism' r (TypeError term uni fun ann)
_TypeError (TypeError term uni fun ann
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ())))
-> TypeError term uni fun ann
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall a b. (a -> b) -> a -> b
$ ann -> fun -> TypeError term uni fun ann
forall term (uni :: * -> *) fun ann.
ann -> fun -> TypeError term uni fun ann
UnknownBuiltinFunctionE ann
ann fun
fun
Just Dupable (Normalized (Type TyName uni ()))
ty -> Dupable (Normalized (Type TyName uni ()))
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall (m :: * -> *) a.
(MonadQuote m, Rename a) =>
Dupable a -> m a
liftDupable Dupable (Normalized (Type TyName uni ()))
ty
withVar :: Name -> Normalized (Type TyName uni ()) -> TypeCheckM uni fun cfg err a -> TypeCheckM uni fun cfg err a
withVar :: Name
-> Normalized (Type TyName uni ())
-> TypeCheckM uni fun cfg err a
-> TypeCheckM uni fun cfg err a
withVar Name
name = (TypeCheckEnv uni fun cfg -> TypeCheckEnv uni fun cfg)
-> TypeCheckM uni fun cfg err a -> TypeCheckM uni fun cfg err a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((TypeCheckEnv uni fun cfg -> TypeCheckEnv uni fun cfg)
-> TypeCheckM uni fun cfg err a -> TypeCheckM uni fun cfg err a)
-> (Normalized (Type TyName uni ())
-> TypeCheckEnv uni fun cfg -> TypeCheckEnv uni fun cfg)
-> Normalized (Type TyName uni ())
-> TypeCheckM uni fun cfg err a
-> TypeCheckM uni fun cfg err a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ASetter
(TypeCheckEnv uni fun cfg)
(TypeCheckEnv uni fun cfg)
(VarTypes uni)
(VarTypes uni)
-> (VarTypes uni -> VarTypes uni)
-> TypeCheckEnv uni fun cfg
-> TypeCheckEnv uni fun cfg
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter
(TypeCheckEnv uni fun cfg)
(TypeCheckEnv uni fun cfg)
(VarTypes uni)
(VarTypes uni)
forall (uni :: * -> *) fun cfg (uni :: * -> *) fun.
Lens
(TypeCheckEnv uni fun cfg)
(TypeCheckEnv uni fun cfg)
(VarTypes uni)
(VarTypes uni)
tceVarTypes ((VarTypes uni -> VarTypes uni)
-> TypeCheckEnv uni fun cfg -> TypeCheckEnv uni fun cfg)
-> (Normalized (Type TyName uni ())
-> VarTypes uni -> VarTypes uni)
-> Normalized (Type TyName uni ())
-> TypeCheckEnv uni fun cfg
-> TypeCheckEnv uni fun cfg
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name
-> Dupable (Normalized (Type TyName uni ()))
-> VarTypes uni
-> VarTypes uni
forall name unique a.
HasUnique name unique =>
name -> a -> UniqueMap unique a -> UniqueMap unique a
insertByName Name
name (Dupable (Normalized (Type TyName uni ()))
-> VarTypes uni -> VarTypes uni)
-> (Normalized (Type TyName uni ())
-> Dupable (Normalized (Type TyName uni ())))
-> Normalized (Type TyName uni ())
-> VarTypes uni
-> VarTypes uni
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Normalized (Type TyName uni ())
-> Dupable (Normalized (Type TyName uni ()))
forall (f :: * -> *) a. Applicative f => a -> f a
pure
lookupTyVarM
:: (AsTypeError err term uni fun ann)
=> ann -> TyName -> TypeCheckM uni fun cfg err (Kind ())
lookupTyVarM :: ann -> TyName -> TypeCheckM uni fun cfg err (Kind ())
lookupTyVarM ann
ann TyName
name = do
Maybe (Kind ())
mayKind <- (TypeCheckEnv uni fun cfg -> Maybe (Kind ()))
-> ReaderT
(TypeCheckEnv uni fun cfg) (ExceptT err Quote) (Maybe (Kind ()))
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ((TypeCheckEnv uni fun cfg -> Maybe (Kind ()))
-> ReaderT
(TypeCheckEnv uni fun cfg) (ExceptT err Quote) (Maybe (Kind ())))
-> (TypeCheckEnv uni fun cfg -> Maybe (Kind ()))
-> ReaderT
(TypeCheckEnv uni fun cfg) (ExceptT err Quote) (Maybe (Kind ()))
forall a b. (a -> b) -> a -> b
$ TyName -> TyVarKinds -> Maybe (Kind ())
forall name unique a.
HasUnique name unique =>
name -> UniqueMap unique a -> Maybe a
lookupName TyName
name (TyVarKinds -> Maybe (Kind ()))
-> (TypeCheckEnv uni fun cfg -> TyVarKinds)
-> TypeCheckEnv uni fun cfg
-> Maybe (Kind ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeCheckEnv uni fun cfg -> TyVarKinds
forall (uni :: * -> *) fun cfg.
TypeCheckEnv uni fun cfg -> TyVarKinds
_tceTyVarKinds
case Maybe (Kind ())
mayKind of
Maybe (Kind ())
Nothing -> AReview err (TypeError term uni fun ann)
-> TypeError term uni fun ann
-> TypeCheckM uni fun cfg err (Kind ())
forall e (m :: * -> *) t x.
MonadError e m =>
AReview e t -> t -> m x
throwing AReview err (TypeError term uni fun ann)
forall r term (uni :: * -> *) fun ann.
AsTypeError r term uni fun ann =>
Prism' r (TypeError term uni fun ann)
_TypeError (TypeError term uni fun ann
-> TypeCheckM uni fun cfg err (Kind ()))
-> TypeError term uni fun ann
-> TypeCheckM uni fun cfg err (Kind ())
forall a b. (a -> b) -> a -> b
$ ann -> TyName -> TypeError term uni fun ann
forall term (uni :: * -> *) fun ann.
ann -> TyName -> TypeError term uni fun ann
FreeTypeVariableE ann
ann TyName
name
Just Kind ()
kind -> Kind () -> TypeCheckM uni fun cfg err (Kind ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure Kind ()
kind
lookupVarM
:: AsTypeError err term uni fun ann
=> ann -> Name -> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
lookupVarM :: ann
-> Name
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
lookupVarM ann
ann Name
name = do
Maybe (Dupable (Normalized (Type TyName uni ())))
mayTy <- (TypeCheckEnv uni fun cfg
-> Maybe (Dupable (Normalized (Type TyName uni ()))))
-> ReaderT
(TypeCheckEnv uni fun cfg)
(ExceptT err Quote)
(Maybe (Dupable (Normalized (Type TyName uni ()))))
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ((TypeCheckEnv uni fun cfg
-> Maybe (Dupable (Normalized (Type TyName uni ()))))
-> ReaderT
(TypeCheckEnv uni fun cfg)
(ExceptT err Quote)
(Maybe (Dupable (Normalized (Type TyName uni ())))))
-> (TypeCheckEnv uni fun cfg
-> Maybe (Dupable (Normalized (Type TyName uni ()))))
-> ReaderT
(TypeCheckEnv uni fun cfg)
(ExceptT err Quote)
(Maybe (Dupable (Normalized (Type TyName uni ()))))
forall a b. (a -> b) -> a -> b
$ Name
-> UniqueMap TermUnique (Dupable (Normalized (Type TyName uni ())))
-> Maybe (Dupable (Normalized (Type TyName uni ())))
forall name unique a.
HasUnique name unique =>
name -> UniqueMap unique a -> Maybe a
lookupName Name
name (UniqueMap TermUnique (Dupable (Normalized (Type TyName uni ())))
-> Maybe (Dupable (Normalized (Type TyName uni ()))))
-> (TypeCheckEnv uni fun cfg
-> UniqueMap
TermUnique (Dupable (Normalized (Type TyName uni ()))))
-> TypeCheckEnv uni fun cfg
-> Maybe (Dupable (Normalized (Type TyName uni ())))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeCheckEnv uni fun cfg
-> UniqueMap TermUnique (Dupable (Normalized (Type TyName uni ())))
forall (uni :: * -> *) fun cfg.
TypeCheckEnv uni fun cfg -> VarTypes uni
_tceVarTypes
case Maybe (Dupable (Normalized (Type TyName uni ())))
mayTy of
Maybe (Dupable (Normalized (Type TyName uni ())))
Nothing -> AReview err (TypeError term uni fun ann)
-> TypeError term uni fun ann
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall e (m :: * -> *) t x.
MonadError e m =>
AReview e t -> t -> m x
throwing AReview err (TypeError term uni fun ann)
forall r term (uni :: * -> *) fun ann.
AsTypeError r term uni fun ann =>
Prism' r (TypeError term uni fun ann)
_TypeError (TypeError term uni fun ann
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ())))
-> TypeError term uni fun ann
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall a b. (a -> b) -> a -> b
$ ann -> Name -> TypeError term uni fun ann
forall term (uni :: * -> *) fun ann.
ann -> Name -> TypeError term uni fun ann
FreeVariableE ann
ann Name
name
Just Dupable (Normalized (Type TyName uni ()))
ty -> Dupable (Normalized (Type TyName uni ()))
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall (m :: * -> *) a.
(MonadQuote m, Rename a) =>
Dupable a -> m a
liftDupable Dupable (Normalized (Type TyName uni ()))
ty
dummyUnique :: Unique
dummyUnique :: Unique
dummyUnique = Int -> Unique
Unique Int
0
dummyTyName :: TyName
dummyTyName :: TyName
dummyTyName = Name -> TyName
TyName (Text -> Unique -> Name
Name Text
"*" Unique
dummyUnique)
dummyKind :: Kind ()
dummyKind :: Kind ()
dummyKind = () -> Kind ()
forall ann. ann -> Kind ann
Type ()
dummyType :: Type TyName uni ()
dummyType :: Type TyName uni ()
dummyType = () -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
dummyTyName
normalizeTypeM
:: HasUniApply uni
=> Type TyName uni ann
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ann))
normalizeTypeM :: Type TyName uni ann
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ann))
normalizeTypeM Type TyName uni ann
ty = NormalizeTypeT
(ReaderT (TypeCheckEnv uni fun cfg) (ExceptT err Quote))
TyName
uni
ann
(Normalized (Type TyName uni ann))
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ann))
forall (m :: * -> *) tyname (uni :: * -> *) ann a.
NormalizeTypeT m tyname uni ann a -> m a
Norm.runNormalizeTypeM (NormalizeTypeT
(ReaderT (TypeCheckEnv uni fun cfg) (ExceptT err Quote))
TyName
uni
ann
(Normalized (Type TyName uni ann))
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ann)))
-> NormalizeTypeT
(ReaderT (TypeCheckEnv uni fun cfg) (ExceptT err Quote))
TyName
uni
ann
(Normalized (Type TyName uni ann))
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ann))
forall a b. (a -> b) -> a -> b
$ Type TyName uni ann
-> NormalizeTypeT
(ReaderT (TypeCheckEnv uni fun cfg) (ExceptT err Quote))
TyName
uni
ann
(Normalized (Type TyName uni ann))
forall tyname (m :: * -> *) (uni :: * -> *) ann.
(HasUnique tyname TypeUnique, MonadQuote m, HasUniApply uni) =>
Type tyname uni ann
-> NormalizeTypeT
m tyname uni ann (Normalized (Type tyname uni ann))
Norm.normalizeTypeM Type TyName uni ann
ty
substNormalizeTypeM
:: HasUniApply uni
=> Normalized (Type TyName uni ())
-> TyName
-> Type TyName uni ()
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
substNormalizeTypeM :: Normalized (Type TyName uni ())
-> TyName
-> Type TyName uni ()
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
substNormalizeTypeM Normalized (Type TyName uni ())
ty TyName
name Type TyName uni ()
body = NormalizeTypeT
(ReaderT (TypeCheckEnv uni fun cfg) (ExceptT err Quote))
TyName
uni
()
(Normalized (Type TyName uni ()))
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall (m :: * -> *) tyname (uni :: * -> *) ann a.
NormalizeTypeT m tyname uni ann a -> m a
Norm.runNormalizeTypeM (NormalizeTypeT
(ReaderT (TypeCheckEnv uni fun cfg) (ExceptT err Quote))
TyName
uni
()
(Normalized (Type TyName uni ()))
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ())))
-> NormalizeTypeT
(ReaderT (TypeCheckEnv uni fun cfg) (ExceptT err Quote))
TyName
uni
()
(Normalized (Type TyName uni ()))
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall a b. (a -> b) -> a -> b
$ Normalized (Type TyName uni ())
-> TyName
-> Type TyName uni ()
-> NormalizeTypeT
(ReaderT (TypeCheckEnv uni fun cfg) (ExceptT err Quote))
TyName
uni
()
(Normalized (Type TyName uni ()))
forall tyname (m :: * -> *) (uni :: * -> *) ann.
(HasUnique tyname TypeUnique, MonadQuote m, HasUniApply uni) =>
Normalized (Type tyname uni ann)
-> tyname
-> Type tyname uni ann
-> NormalizeTypeT
m tyname uni ann (Normalized (Type tyname uni ann))
Norm.substNormalizeTypeM Normalized (Type TyName uni ())
ty TyName
name Type TyName uni ()
body
inferKindM
:: (AsTypeError err term uni fun ann, ToKind uni)
=> Type TyName uni ann -> TypeCheckM uni fun cfg err (Kind ())
inferKindM :: Type TyName uni ann -> TypeCheckM uni fun cfg err (Kind ())
inferKindM (TyBuiltin ann
_ (SomeTypeIn uni (Esc a)
uni)) =
Kind () -> TypeCheckM uni fun cfg err (Kind ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Kind () -> TypeCheckM uni fun cfg err (Kind ()))
-> Kind () -> TypeCheckM uni fun cfg err (Kind ())
forall a b. (a -> b) -> a -> b
$ uni (Esc a) -> Kind ()
forall k (uni :: * -> *) (a :: k).
ToKind uni =>
uni (Esc a) -> Kind ()
kindOfBuiltinType uni (Esc a)
uni
inferKindM (TyVar ann
ann TyName
v) =
ann -> TyName -> TypeCheckM uni fun cfg err (Kind ())
forall err term (uni :: * -> *) fun ann cfg.
AsTypeError err term uni fun ann =>
ann -> TyName -> TypeCheckM uni fun cfg err (Kind ())
lookupTyVarM ann
ann TyName
v
inferKindM (TyLam ann
_ TyName
n Kind ann
dom Type TyName uni ann
body) = do
let dom_ :: Kind ()
dom_ = Kind ann -> Kind ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Kind ann
dom
TyName
-> Kind ()
-> TypeCheckM uni fun cfg err (Kind ())
-> TypeCheckM uni fun cfg err (Kind ())
forall (uni :: * -> *) fun cfg err a.
TyName
-> Kind ()
-> TypeCheckM uni fun cfg err a
-> TypeCheckM uni fun cfg err a
withTyVar TyName
n Kind ()
dom_ (TypeCheckM uni fun cfg err (Kind ())
-> TypeCheckM uni fun cfg err (Kind ()))
-> TypeCheckM uni fun cfg err (Kind ())
-> TypeCheckM uni fun cfg err (Kind ())
forall a b. (a -> b) -> a -> b
$ () -> Kind () -> Kind () -> Kind ()
forall ann. ann -> Kind ann -> Kind ann -> Kind ann
KindArrow () Kind ()
dom_ (Kind () -> Kind ())
-> TypeCheckM uni fun cfg err (Kind ())
-> TypeCheckM uni fun cfg err (Kind ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type TyName uni ann -> TypeCheckM uni fun cfg err (Kind ())
forall err term (uni :: * -> *) fun ann cfg.
(AsTypeError err term uni fun ann, ToKind uni) =>
Type TyName uni ann -> TypeCheckM uni fun cfg err (Kind ())
inferKindM Type TyName uni ann
body
inferKindM (TyApp ann
ann Type TyName uni ann
fun Type TyName uni ann
arg) = do
Kind ()
funKind <- Type TyName uni ann -> TypeCheckM uni fun cfg err (Kind ())
forall err term (uni :: * -> *) fun ann cfg.
(AsTypeError err term uni fun ann, ToKind uni) =>
Type TyName uni ann -> TypeCheckM uni fun cfg err (Kind ())
inferKindM Type TyName uni ann
fun
case Kind ()
funKind of
KindArrow ()
_ Kind ()
dom Kind ()
cod -> do
ann
-> Type TyName uni ann -> Kind () -> TypeCheckM uni fun cfg err ()
forall err term (uni :: * -> *) fun ann cfg.
(AsTypeError err term uni fun ann, ToKind uni) =>
ann
-> Type TyName uni ann -> Kind () -> TypeCheckM uni fun cfg err ()
checkKindM ann
ann Type TyName uni ann
arg Kind ()
dom
Kind () -> TypeCheckM uni fun cfg err (Kind ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure Kind ()
cod
Kind ()
_ -> AReview err (TypeError term uni fun ann)
-> TypeError term uni fun ann
-> TypeCheckM uni fun cfg err (Kind ())
forall e (m :: * -> *) t x.
MonadError e m =>
AReview e t -> t -> m x
throwing AReview err (TypeError term uni fun ann)
forall r term (uni :: * -> *) fun ann.
AsTypeError r term uni fun ann =>
Prism' r (TypeError term uni fun ann)
_TypeError (TypeError term uni fun ann
-> TypeCheckM uni fun cfg err (Kind ()))
-> TypeError term uni fun ann
-> TypeCheckM uni fun cfg err (Kind ())
forall a b. (a -> b) -> a -> b
$ ann
-> Type TyName uni ()
-> Kind ()
-> Kind ()
-> TypeError term uni fun ann
forall term (uni :: * -> *) fun ann.
ann
-> Type TyName uni ()
-> Kind ()
-> Kind ()
-> TypeError term uni fun ann
KindMismatch ann
ann (Type TyName uni ann -> Type TyName uni ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Type TyName uni ann
fun) (() -> Kind () -> Kind () -> Kind ()
forall ann. ann -> Kind ann -> Kind ann -> Kind ann
KindArrow () Kind ()
dummyKind Kind ()
dummyKind) Kind ()
funKind
inferKindM (TyFun ann
ann Type TyName uni ann
dom Type TyName uni ann
cod) = do
ann
-> Type TyName uni ann -> Kind () -> TypeCheckM uni fun cfg err ()
forall err term (uni :: * -> *) fun ann cfg.
(AsTypeError err term uni fun ann, ToKind uni) =>
ann
-> Type TyName uni ann -> Kind () -> TypeCheckM uni fun cfg err ()
checkKindM ann
ann Type TyName uni ann
dom (Kind () -> TypeCheckM uni fun cfg err ())
-> Kind () -> TypeCheckM uni fun cfg err ()
forall a b. (a -> b) -> a -> b
$ () -> Kind ()
forall ann. ann -> Kind ann
Type ()
ann
-> Type TyName uni ann -> Kind () -> TypeCheckM uni fun cfg err ()
forall err term (uni :: * -> *) fun ann cfg.
(AsTypeError err term uni fun ann, ToKind uni) =>
ann
-> Type TyName uni ann -> Kind () -> TypeCheckM uni fun cfg err ()
checkKindM ann
ann Type TyName uni ann
cod (Kind () -> TypeCheckM uni fun cfg err ())
-> Kind () -> TypeCheckM uni fun cfg err ()
forall a b. (a -> b) -> a -> b
$ () -> Kind ()
forall ann. ann -> Kind ann
Type ()
Kind () -> TypeCheckM uni fun cfg err (Kind ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Kind () -> TypeCheckM uni fun cfg err (Kind ()))
-> Kind () -> TypeCheckM uni fun cfg err (Kind ())
forall a b. (a -> b) -> a -> b
$ () -> Kind ()
forall ann. ann -> Kind ann
Type ()
inferKindM (TyForall ann
ann TyName
n Kind ann
k Type TyName uni ann
body) = do
TyName
-> Kind ()
-> TypeCheckM uni fun cfg err ()
-> TypeCheckM uni fun cfg err ()
forall (uni :: * -> *) fun cfg err a.
TyName
-> Kind ()
-> TypeCheckM uni fun cfg err a
-> TypeCheckM uni fun cfg err a
withTyVar TyName
n (Kind ann -> Kind ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Kind ann
k) (TypeCheckM uni fun cfg err () -> TypeCheckM uni fun cfg err ())
-> TypeCheckM uni fun cfg err () -> TypeCheckM uni fun cfg err ()
forall a b. (a -> b) -> a -> b
$ ann
-> Type TyName uni ann -> Kind () -> TypeCheckM uni fun cfg err ()
forall err term (uni :: * -> *) fun ann cfg.
(AsTypeError err term uni fun ann, ToKind uni) =>
ann
-> Type TyName uni ann -> Kind () -> TypeCheckM uni fun cfg err ()
checkKindM ann
ann Type TyName uni ann
body (() -> Kind ()
forall ann. ann -> Kind ann
Type ())
Kind () -> TypeCheckM uni fun cfg err (Kind ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Kind () -> TypeCheckM uni fun cfg err (Kind ()))
-> Kind () -> TypeCheckM uni fun cfg err (Kind ())
forall a b. (a -> b) -> a -> b
$ () -> Kind ()
forall ann. ann -> Kind ann
Type ()
inferKindM (TyIFix ann
ann Type TyName uni ann
pat Type TyName uni ann
arg) = do
Kind ()
k <- Type TyName uni ann -> TypeCheckM uni fun cfg err (Kind ())
forall err term (uni :: * -> *) fun ann cfg.
(AsTypeError err term uni fun ann, ToKind uni) =>
Type TyName uni ann -> TypeCheckM uni fun cfg err (Kind ())
inferKindM Type TyName uni ann
arg
ann
-> Type TyName uni ann -> Kind () -> TypeCheckM uni fun cfg err ()
forall err term (uni :: * -> *) fun ann cfg.
(AsTypeError err term uni fun ann, ToKind uni) =>
ann
-> Type TyName uni ann -> Kind () -> TypeCheckM uni fun cfg err ()
checkKindOfPatternFunctorM ann
ann Type TyName uni ann
pat Kind ()
k
Kind () -> TypeCheckM uni fun cfg err (Kind ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Kind () -> TypeCheckM uni fun cfg err (Kind ()))
-> Kind () -> TypeCheckM uni fun cfg err (Kind ())
forall a b. (a -> b) -> a -> b
$ () -> Kind ()
forall ann. ann -> Kind ann
Type ()
checkKindM
:: (AsTypeError err term uni fun ann, ToKind uni)
=> ann -> Type TyName uni ann -> Kind () -> TypeCheckM uni fun cfg err ()
checkKindM :: ann
-> Type TyName uni ann -> Kind () -> TypeCheckM uni fun cfg err ()
checkKindM ann
ann Type TyName uni ann
ty Kind ()
k = do
Kind ()
tyK <- Type TyName uni ann -> TypeCheckM uni fun cfg err (Kind ())
forall err term (uni :: * -> *) fun ann cfg.
(AsTypeError err term uni fun ann, ToKind uni) =>
Type TyName uni ann -> TypeCheckM uni fun cfg err (Kind ())
inferKindM Type TyName uni ann
ty
Bool
-> TypeCheckM uni fun cfg err () -> TypeCheckM uni fun cfg err ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Kind ()
tyK Kind () -> Kind () -> Bool
forall a. Eq a => a -> a -> Bool
/= Kind ()
k) (TypeCheckM uni fun cfg err () -> TypeCheckM uni fun cfg err ())
-> TypeCheckM uni fun cfg err () -> TypeCheckM uni fun cfg err ()
forall a b. (a -> b) -> a -> b
$ AReview err (TypeError term uni fun ann)
-> TypeError term uni fun ann -> TypeCheckM uni fun cfg err ()
forall e (m :: * -> *) t x.
MonadError e m =>
AReview e t -> t -> m x
throwing AReview err (TypeError term uni fun ann)
forall r term (uni :: * -> *) fun ann.
AsTypeError r term uni fun ann =>
Prism' r (TypeError term uni fun ann)
_TypeError (ann
-> Type TyName uni ()
-> Kind ()
-> Kind ()
-> TypeError term uni fun ann
forall term (uni :: * -> *) fun ann.
ann
-> Type TyName uni ()
-> Kind ()
-> Kind ()
-> TypeError term uni fun ann
KindMismatch ann
ann (Type TyName uni ann -> Type TyName uni ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Type TyName uni ann
ty) Kind ()
k Kind ()
tyK)
checkKindOfPatternFunctorM
:: (AsTypeError err term uni fun ann, ToKind uni)
=> ann
-> Type TyName uni ann
-> Kind ()
-> TypeCheckM uni fun cfg err ()
checkKindOfPatternFunctorM :: ann
-> Type TyName uni ann -> Kind () -> TypeCheckM uni fun cfg err ()
checkKindOfPatternFunctorM ann
ann Type TyName uni ann
pat Kind ()
k =
ann
-> Type TyName uni ann -> Kind () -> TypeCheckM uni fun cfg err ()
forall err term (uni :: * -> *) fun ann cfg.
(AsTypeError err term uni fun ann, ToKind uni) =>
ann
-> Type TyName uni ann -> Kind () -> TypeCheckM uni fun cfg err ()
checkKindM ann
ann Type TyName uni ann
pat (Kind () -> TypeCheckM uni fun cfg err ())
-> Kind () -> TypeCheckM uni fun cfg err ()
forall a b. (a -> b) -> a -> b
$ () -> Kind () -> Kind () -> Kind ()
forall ann. ann -> Kind ann -> Kind ann -> Kind ann
KindArrow () (() -> Kind () -> Kind () -> Kind ()
forall ann. ann -> Kind ann -> Kind ann -> Kind ann
KindArrow () Kind ()
k (() -> Kind ()
forall ann. ann -> Kind ann
Type ())) (() -> Kind () -> Kind () -> Kind ()
forall ann. ann -> Kind ann -> Kind ann -> Kind ann
KindArrow () Kind ()
k (() -> Kind ()
forall ann. ann -> Kind ann
Type ()))
unfoldIFixOf
:: HasUniApply uni
=> Normalized (Type TyName uni ())
-> Normalized (Type TyName uni ())
-> Kind ()
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
unfoldIFixOf :: Normalized (Type TyName uni ())
-> Normalized (Type TyName uni ())
-> Kind ()
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
unfoldIFixOf Normalized (Type TyName uni ())
pat Normalized (Type TyName uni ())
arg Kind ()
k = do
let vPat :: Type TyName uni ()
vPat = Normalized (Type TyName uni ()) -> Type TyName uni ()
forall a. Normalized a -> a
unNormalized Normalized (Type TyName uni ())
pat
vArg :: Type TyName uni ()
vArg = Normalized (Type TyName uni ()) -> Type TyName uni ()
forall a. Normalized a -> a
unNormalized Normalized (Type TyName uni ())
arg
TyName
a <- Quote TyName
-> ReaderT (TypeCheckEnv uni fun cfg) (ExceptT err Quote) TyName
forall (m :: * -> *) a. MonadQuote m => Quote a -> m a
liftQuote (Quote TyName
-> ReaderT (TypeCheckEnv uni fun cfg) (ExceptT err Quote) TyName)
-> Quote TyName
-> ReaderT (TypeCheckEnv uni fun cfg) (ExceptT err Quote) TyName
forall a b. (a -> b) -> a -> b
$ Text -> Quote TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"a"
Type TyName uni ()
vPat' <- Type TyName uni ()
-> ReaderT
(TypeCheckEnv uni fun cfg) (ExceptT err Quote) (Type TyName uni ())
forall a (m :: * -> *). (Rename a, MonadQuote m) => a -> m a
rename Type TyName uni ()
vPat
Type TyName uni ()
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall (uni :: * -> *) ann fun cfg err.
HasUniApply uni =>
Type TyName uni ann
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ann))
normalizeTypeM (Type TyName uni ()
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ())))
-> Type TyName uni ()
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall a b. (a -> b) -> a -> b
$
()
-> Type TyName uni () -> [Type TyName uni ()] -> Type TyName uni ()
forall ann tyname (uni :: * -> *).
ann
-> Type tyname uni ann
-> [Type tyname uni ann]
-> Type tyname uni ann
mkIterTyApp () Type TyName uni ()
vPat'
[ () -> TyName -> Kind () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyLam () TyName
a Kind ()
k (Type TyName uni () -> Type TyName uni ())
-> (Type TyName uni () -> Type TyName uni ())
-> Type TyName uni ()
-> Type TyName uni ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyIFix () Type TyName uni ()
vPat (Type TyName uni () -> Type TyName uni ())
-> Type TyName uni () -> Type TyName uni ()
forall a b. (a -> b) -> a -> b
$ () -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a
, Type TyName uni ()
vArg
]
inferTypeM
:: ( AsTypeError err (Term TyName Name uni fun ()) uni fun ann, ToKind uni, HasUniApply uni
, HasTypeCheckConfig cfg uni fun, GEq uni, Ix fun
)
=> Term TyName Name uni fun ann -> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
inferTypeM :: Term TyName Name uni fun ann
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
inferTypeM (Constant ann
_ (Some (ValueOf uni (Esc a)
uni a
_))) =
Type TyName uni ()
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall (uni :: * -> *) ann fun cfg err.
HasUniApply uni =>
Type TyName uni ann
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ann))
normalizeTypeM (Type TyName uni ()
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ())))
-> Type TyName uni ()
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall a b. (a -> b) -> a -> b
$ () -> uni (Esc a) -> Type TyName uni ()
forall k (a :: k) (uni :: * -> *) tyname ann.
ann -> uni (Esc a) -> Type tyname uni ann
mkTyBuiltinOf () uni (Esc a)
uni
inferTypeM (Builtin ann
ann fun
fun) =
ann
-> fun
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall err term (uni :: * -> *) fun ann cfg.
(AsTypeError err term uni fun ann, HasTypeCheckConfig cfg uni fun,
Ix fun) =>
ann
-> fun
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
lookupBuiltinM ann
ann fun
fun
inferTypeM (Var ann
ann Name
name) =
ann
-> Name
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall err term (uni :: * -> *) fun ann cfg.
AsTypeError err term uni fun ann =>
ann
-> Name
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
lookupVarM ann
ann Name
name
inferTypeM (LamAbs ann
ann Name
n Type TyName uni ann
dom Term TyName Name uni fun ann
body) = do
ann
-> Type TyName uni ann -> Kind () -> TypeCheckM uni fun cfg err ()
forall err term (uni :: * -> *) fun ann cfg.
(AsTypeError err term uni fun ann, ToKind uni) =>
ann
-> Type TyName uni ann -> Kind () -> TypeCheckM uni fun cfg err ()
checkKindM ann
ann Type TyName uni ann
dom (Kind () -> TypeCheckM uni fun cfg err ())
-> Kind () -> TypeCheckM uni fun cfg err ()
forall a b. (a -> b) -> a -> b
$ () -> Kind ()
forall ann. ann -> Kind ann
Type ()
Normalized (Type TyName uni ())
vDom <- Type TyName uni ()
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall (uni :: * -> *) ann fun cfg err.
HasUniApply uni =>
Type TyName uni ann
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ann))
normalizeTypeM (Type TyName uni ()
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ())))
-> Type TyName uni ()
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall a b. (a -> b) -> a -> b
$ Type TyName uni ann -> Type TyName uni ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Type TyName uni ann
dom
()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () (Type TyName uni () -> Type TyName uni () -> Type TyName uni ())
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
-> ReaderT
(TypeCheckEnv uni fun cfg)
(ExceptT err Quote)
(Normalized (Type TyName uni () -> Type TyName uni ()))
forall (f1 :: * -> *) (f2 :: * -> *) a b.
(Functor f1, Functor f2) =>
(a -> b) -> f1 (f2 a) -> f1 (f2 b)
<<$>> Normalized (Type TyName uni ())
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall (f :: * -> *) a. Applicative f => a -> f a
pure Normalized (Type TyName uni ())
vDom ReaderT
(TypeCheckEnv uni fun cfg)
(ExceptT err Quote)
(Normalized (Type TyName uni () -> Type TyName uni ()))
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall (f1 :: * -> *) (f2 :: * -> *) a b.
(Applicative f1, Applicative f2) =>
f1 (f2 (a -> b)) -> f1 (f2 a) -> f1 (f2 b)
<<*>> Name
-> Normalized (Type TyName uni ())
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall (uni :: * -> *) fun cfg err a.
Name
-> Normalized (Type TyName uni ())
-> TypeCheckM uni fun cfg err a
-> TypeCheckM uni fun cfg err a
withVar Name
n Normalized (Type TyName uni ())
vDom (Term TyName Name uni fun ann
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall err (uni :: * -> *) fun ann cfg.
(AsTypeError err (Term TyName Name uni fun ()) uni fun ann,
ToKind uni, HasUniApply uni, HasTypeCheckConfig cfg uni fun,
GEq uni, Ix fun) =>
Term TyName Name uni fun ann
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
inferTypeM Term TyName Name uni fun ann
body)
inferTypeM (TyAbs ann
_ TyName
n Kind ann
nK Term TyName Name uni fun ann
body) = do
let nK_ :: Kind ()
nK_ = Kind ann -> Kind ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Kind ann
nK
() -> TyName -> Kind () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyForall () TyName
n Kind ()
nK_ (Type TyName uni () -> Type TyName uni ())
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall (f1 :: * -> *) (f2 :: * -> *) a b.
(Functor f1, Functor f2) =>
(a -> b) -> f1 (f2 a) -> f1 (f2 b)
<<$>> TyName
-> Kind ()
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall (uni :: * -> *) fun cfg err a.
TyName
-> Kind ()
-> TypeCheckM uni fun cfg err a
-> TypeCheckM uni fun cfg err a
withTyVar TyName
n Kind ()
nK_ (Term TyName Name uni fun ann
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall err (uni :: * -> *) fun ann cfg.
(AsTypeError err (Term TyName Name uni fun ()) uni fun ann,
ToKind uni, HasUniApply uni, HasTypeCheckConfig cfg uni fun,
GEq uni, Ix fun) =>
Term TyName Name uni fun ann
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
inferTypeM Term TyName Name uni fun ann
body)
inferTypeM (Apply ann
ann Term TyName Name uni fun ann
fun Term TyName Name uni fun ann
arg) = do
Normalized (Type TyName uni ())
vFunTy <- Term TyName Name uni fun ann
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall err (uni :: * -> *) fun ann cfg.
(AsTypeError err (Term TyName Name uni fun ()) uni fun ann,
ToKind uni, HasUniApply uni, HasTypeCheckConfig cfg uni fun,
GEq uni, Ix fun) =>
Term TyName Name uni fun ann
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
inferTypeM Term TyName Name uni fun ann
fun
case Normalized (Type TyName uni ()) -> Type TyName uni ()
forall a. Normalized a -> a
unNormalized Normalized (Type TyName uni ())
vFunTy of
TyFun ()
_ Type TyName uni ()
vDom Type TyName uni ()
vCod -> do
ann
-> Term TyName Name uni fun ann
-> Normalized (Type TyName uni ())
-> TypeCheckM uni fun cfg err ()
forall err (uni :: * -> *) fun ann cfg.
(AsTypeError err (Term TyName Name uni fun ()) uni fun ann,
ToKind uni, HasUniApply uni, HasTypeCheckConfig cfg uni fun,
GEq uni, Ix fun) =>
ann
-> Term TyName Name uni fun ann
-> Normalized (Type TyName uni ())
-> TypeCheckM uni fun cfg err ()
checkTypeM ann
ann Term TyName Name uni fun ann
arg (Normalized (Type TyName uni ()) -> TypeCheckM uni fun cfg err ())
-> Normalized (Type TyName uni ()) -> TypeCheckM uni fun cfg err ()
forall a b. (a -> b) -> a -> b
$ Type TyName uni () -> Normalized (Type TyName uni ())
forall a. a -> Normalized a
Normalized Type TyName uni ()
vDom
Normalized (Type TyName uni ())
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Normalized (Type TyName uni ())
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ())))
-> Normalized (Type TyName uni ())
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall a b. (a -> b) -> a -> b
$ Type TyName uni () -> Normalized (Type TyName uni ())
forall a. a -> Normalized a
Normalized Type TyName uni ()
vCod
Type TyName uni ()
_ -> AReview err (TypeError (Term TyName Name uni fun ()) uni fun ann)
-> TypeError (Term TyName Name uni fun ()) uni fun ann
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall e (m :: * -> *) t x.
MonadError e m =>
AReview e t -> t -> m x
throwing AReview err (TypeError (Term TyName Name uni fun ()) uni fun ann)
forall r term (uni :: * -> *) fun ann.
AsTypeError r term uni fun ann =>
Prism' r (TypeError term uni fun ann)
_TypeError (ann
-> Term TyName Name uni fun ()
-> Type TyName uni ()
-> Normalized (Type TyName uni ())
-> TypeError (Term TyName Name uni fun ()) uni fun ann
forall term (uni :: * -> *) fun ann.
ann
-> term
-> Type TyName uni ()
-> Normalized (Type TyName uni ())
-> TypeError term uni fun ann
TypeMismatch ann
ann (Term TyName Name uni fun ann -> Term TyName Name uni fun ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Term TyName Name uni fun ann
fun) (()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
dummyType Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
dummyType) Normalized (Type TyName uni ())
vFunTy)
inferTypeM (TyInst ann
ann Term TyName Name uni fun ann
body Type TyName uni ann
ty) = do
Normalized (Type TyName uni ())
vBodyTy <- Term TyName Name uni fun ann
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall err (uni :: * -> *) fun ann cfg.
(AsTypeError err (Term TyName Name uni fun ()) uni fun ann,
ToKind uni, HasUniApply uni, HasTypeCheckConfig cfg uni fun,
GEq uni, Ix fun) =>
Term TyName Name uni fun ann
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
inferTypeM Term TyName Name uni fun ann
body
case Normalized (Type TyName uni ()) -> Type TyName uni ()
forall a. Normalized a -> a
unNormalized Normalized (Type TyName uni ())
vBodyTy of
TyForall ()
_ TyName
n Kind ()
nK Type TyName uni ()
vCod -> do
ann
-> Type TyName uni ann -> Kind () -> TypeCheckM uni fun cfg err ()
forall err term (uni :: * -> *) fun ann cfg.
(AsTypeError err term uni fun ann, ToKind uni) =>
ann
-> Type TyName uni ann -> Kind () -> TypeCheckM uni fun cfg err ()
checkKindM ann
ann Type TyName uni ann
ty Kind ()
nK
Normalized (Type TyName uni ())
vTy <- Type TyName uni ()
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall (uni :: * -> *) ann fun cfg err.
HasUniApply uni =>
Type TyName uni ann
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ann))
normalizeTypeM (Type TyName uni ()
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ())))
-> Type TyName uni ()
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall a b. (a -> b) -> a -> b
$ Type TyName uni ann -> Type TyName uni ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Type TyName uni ann
ty
Normalized (Type TyName uni ())
-> TyName
-> Type TyName uni ()
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall (uni :: * -> *) fun cfg err.
HasUniApply uni =>
Normalized (Type TyName uni ())
-> TyName
-> Type TyName uni ()
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
substNormalizeTypeM Normalized (Type TyName uni ())
vTy TyName
n Type TyName uni ()
vCod
Type TyName uni ()
_ -> AReview err (TypeError (Term TyName Name uni fun ()) uni fun ann)
-> TypeError (Term TyName Name uni fun ()) uni fun ann
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall e (m :: * -> *) t x.
MonadError e m =>
AReview e t -> t -> m x
throwing AReview err (TypeError (Term TyName Name uni fun ()) uni fun ann)
forall r term (uni :: * -> *) fun ann.
AsTypeError r term uni fun ann =>
Prism' r (TypeError term uni fun ann)
_TypeError (ann
-> Term TyName Name uni fun ()
-> Type TyName uni ()
-> Normalized (Type TyName uni ())
-> TypeError (Term TyName Name uni fun ()) uni fun ann
forall term (uni :: * -> *) fun ann.
ann
-> term
-> Type TyName uni ()
-> Normalized (Type TyName uni ())
-> TypeError term uni fun ann
TypeMismatch ann
ann (Term TyName Name uni fun ann -> Term TyName Name uni fun ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Term TyName Name uni fun ann
body) (() -> TyName -> Kind () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyForall () TyName
dummyTyName Kind ()
dummyKind Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
dummyType) Normalized (Type TyName uni ())
vBodyTy)
inferTypeM (IWrap ann
ann Type TyName uni ann
pat Type TyName uni ann
arg Term TyName Name uni fun ann
term) = do
Kind ()
k <- Type TyName uni ann -> TypeCheckM uni fun cfg err (Kind ())
forall err term (uni :: * -> *) fun ann cfg.
(AsTypeError err term uni fun ann, ToKind uni) =>
Type TyName uni ann -> TypeCheckM uni fun cfg err (Kind ())
inferKindM Type TyName uni ann
arg
ann
-> Type TyName uni ann -> Kind () -> TypeCheckM uni fun cfg err ()
forall err term (uni :: * -> *) fun ann cfg.
(AsTypeError err term uni fun ann, ToKind uni) =>
ann
-> Type TyName uni ann -> Kind () -> TypeCheckM uni fun cfg err ()
checkKindOfPatternFunctorM ann
ann Type TyName uni ann
pat Kind ()
k
Normalized (Type TyName uni ())
vPat <- Type TyName uni ()
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall (uni :: * -> *) ann fun cfg err.
HasUniApply uni =>
Type TyName uni ann
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ann))
normalizeTypeM (Type TyName uni ()
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ())))
-> Type TyName uni ()
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall a b. (a -> b) -> a -> b
$ Type TyName uni ann -> Type TyName uni ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Type TyName uni ann
pat
Normalized (Type TyName uni ())
vArg <- Type TyName uni ()
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall (uni :: * -> *) ann fun cfg err.
HasUniApply uni =>
Type TyName uni ann
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ann))
normalizeTypeM (Type TyName uni ()
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ())))
-> Type TyName uni ()
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall a b. (a -> b) -> a -> b
$ Type TyName uni ann -> Type TyName uni ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Type TyName uni ann
arg
ann
-> Term TyName Name uni fun ann
-> Normalized (Type TyName uni ())
-> TypeCheckM uni fun cfg err ()
forall err (uni :: * -> *) fun ann cfg.
(AsTypeError err (Term TyName Name uni fun ()) uni fun ann,
ToKind uni, HasUniApply uni, HasTypeCheckConfig cfg uni fun,
GEq uni, Ix fun) =>
ann
-> Term TyName Name uni fun ann
-> Normalized (Type TyName uni ())
-> TypeCheckM uni fun cfg err ()
checkTypeM ann
ann Term TyName Name uni fun ann
term (Normalized (Type TyName uni ()) -> TypeCheckM uni fun cfg err ())
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
-> TypeCheckM uni fun cfg err ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Normalized (Type TyName uni ())
-> Normalized (Type TyName uni ())
-> Kind ()
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall (uni :: * -> *) fun cfg err.
HasUniApply uni =>
Normalized (Type TyName uni ())
-> Normalized (Type TyName uni ())
-> Kind ()
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
unfoldIFixOf Normalized (Type TyName uni ())
vPat Normalized (Type TyName uni ())
vArg Kind ()
k
Normalized (Type TyName uni ())
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Normalized (Type TyName uni ())
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ())))
-> Normalized (Type TyName uni ())
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall a b. (a -> b) -> a -> b
$ ()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyIFix () (Type TyName uni () -> Type TyName uni () -> Type TyName uni ())
-> Normalized (Type TyName uni ())
-> Normalized (Type TyName uni () -> Type TyName uni ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Normalized (Type TyName uni ())
vPat Normalized (Type TyName uni () -> Type TyName uni ())
-> Normalized (Type TyName uni ())
-> Normalized (Type TyName uni ())
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Normalized (Type TyName uni ())
vArg
inferTypeM (Unwrap ann
ann Term TyName Name uni fun ann
term) = do
Normalized (Type TyName uni ())
vTermTy <- Term TyName Name uni fun ann
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall err (uni :: * -> *) fun ann cfg.
(AsTypeError err (Term TyName Name uni fun ()) uni fun ann,
ToKind uni, HasUniApply uni, HasTypeCheckConfig cfg uni fun,
GEq uni, Ix fun) =>
Term TyName Name uni fun ann
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
inferTypeM Term TyName Name uni fun ann
term
case Normalized (Type TyName uni ()) -> Type TyName uni ()
forall a. Normalized a -> a
unNormalized Normalized (Type TyName uni ())
vTermTy of
TyIFix ()
_ Type TyName uni ()
vPat Type TyName uni ()
vArg -> do
Kind ()
k <- Type TyName uni ann -> TypeCheckM uni fun cfg err (Kind ())
forall err term (uni :: * -> *) fun ann cfg.
(AsTypeError err term uni fun ann, ToKind uni) =>
Type TyName uni ann -> TypeCheckM uni fun cfg err (Kind ())
inferKindM (Type TyName uni ann -> TypeCheckM uni fun cfg err (Kind ()))
-> Type TyName uni ann -> TypeCheckM uni fun cfg err (Kind ())
forall a b. (a -> b) -> a -> b
$ ann
ann ann -> Type TyName uni () -> Type TyName uni ann
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Type TyName uni ()
vArg
Normalized (Type TyName uni ())
-> Normalized (Type TyName uni ())
-> Kind ()
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall (uni :: * -> *) fun cfg err.
HasUniApply uni =>
Normalized (Type TyName uni ())
-> Normalized (Type TyName uni ())
-> Kind ()
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
unfoldIFixOf (Type TyName uni () -> Normalized (Type TyName uni ())
forall a. a -> Normalized a
Normalized Type TyName uni ()
vPat) (Type TyName uni () -> Normalized (Type TyName uni ())
forall a. a -> Normalized a
Normalized Type TyName uni ()
vArg) Kind ()
k
Type TyName uni ()
_ -> AReview err (TypeError (Term TyName Name uni fun ()) uni fun ann)
-> TypeError (Term TyName Name uni fun ()) uni fun ann
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall e (m :: * -> *) t x.
MonadError e m =>
AReview e t -> t -> m x
throwing AReview err (TypeError (Term TyName Name uni fun ()) uni fun ann)
forall r term (uni :: * -> *) fun ann.
AsTypeError r term uni fun ann =>
Prism' r (TypeError term uni fun ann)
_TypeError (ann
-> Term TyName Name uni fun ()
-> Type TyName uni ()
-> Normalized (Type TyName uni ())
-> TypeError (Term TyName Name uni fun ()) uni fun ann
forall term (uni :: * -> *) fun ann.
ann
-> term
-> Type TyName uni ()
-> Normalized (Type TyName uni ())
-> TypeError term uni fun ann
TypeMismatch ann
ann (Term TyName Name uni fun ann -> Term TyName Name uni fun ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Term TyName Name uni fun ann
term) (()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyIFix () Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
dummyType Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
dummyType) Normalized (Type TyName uni ())
vTermTy)
inferTypeM (Error ann
ann Type TyName uni ann
ty) = do
ann
-> Type TyName uni ann -> Kind () -> TypeCheckM uni fun cfg err ()
forall err term (uni :: * -> *) fun ann cfg.
(AsTypeError err term uni fun ann, ToKind uni) =>
ann
-> Type TyName uni ann -> Kind () -> TypeCheckM uni fun cfg err ()
checkKindM ann
ann Type TyName uni ann
ty (Kind () -> TypeCheckM uni fun cfg err ())
-> Kind () -> TypeCheckM uni fun cfg err ()
forall a b. (a -> b) -> a -> b
$ () -> Kind ()
forall ann. ann -> Kind ann
Type ()
Type TyName uni ()
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall (uni :: * -> *) ann fun cfg err.
HasUniApply uni =>
Type TyName uni ann
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ann))
normalizeTypeM (Type TyName uni ()
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ())))
-> Type TyName uni ()
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall a b. (a -> b) -> a -> b
$ Type TyName uni ann -> Type TyName uni ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Type TyName uni ann
ty
checkTypeM
:: ( AsTypeError err (Term TyName Name uni fun ()) uni fun ann, ToKind uni, HasUniApply uni
, HasTypeCheckConfig cfg uni fun, GEq uni, Ix fun
)
=> ann
-> Term TyName Name uni fun ann
-> Normalized (Type TyName uni ())
-> TypeCheckM uni fun cfg err ()
checkTypeM :: ann
-> Term TyName Name uni fun ann
-> Normalized (Type TyName uni ())
-> TypeCheckM uni fun cfg err ()
checkTypeM ann
ann Term TyName Name uni fun ann
term Normalized (Type TyName uni ())
vTy = do
Normalized (Type TyName uni ())
vTermTy <- Term TyName Name uni fun ann
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall err (uni :: * -> *) fun ann cfg.
(AsTypeError err (Term TyName Name uni fun ()) uni fun ann,
ToKind uni, HasUniApply uni, HasTypeCheckConfig cfg uni fun,
GEq uni, Ix fun) =>
Term TyName Name uni fun ann
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
inferTypeM Term TyName Name uni fun ann
term
Bool
-> TypeCheckM uni fun cfg err () -> TypeCheckM uni fun cfg err ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Normalized (Type TyName uni ())
vTermTy Normalized (Type TyName uni ())
-> Normalized (Type TyName uni ()) -> Bool
forall a. Eq a => a -> a -> Bool
/= Normalized (Type TyName uni ())
vTy) (TypeCheckM uni fun cfg err () -> TypeCheckM uni fun cfg err ())
-> TypeCheckM uni fun cfg err () -> TypeCheckM uni fun cfg err ()
forall a b. (a -> b) -> a -> b
$ AReview err (TypeError (Term TyName Name uni fun ()) uni fun ann)
-> TypeError (Term TyName Name uni fun ()) uni fun ann
-> TypeCheckM uni fun cfg err ()
forall e (m :: * -> *) t x.
MonadError e m =>
AReview e t -> t -> m x
throwing AReview err (TypeError (Term TyName Name uni fun ()) uni fun ann)
forall r term (uni :: * -> *) fun ann.
AsTypeError r term uni fun ann =>
Prism' r (TypeError term uni fun ann)
_TypeError (ann
-> Term TyName Name uni fun ()
-> Type TyName uni ()
-> Normalized (Type TyName uni ())
-> TypeError (Term TyName Name uni fun ()) uni fun ann
forall term (uni :: * -> *) fun ann.
ann
-> term
-> Type TyName uni ()
-> Normalized (Type TyName uni ())
-> TypeError term uni fun ann
TypeMismatch ann
ann (Term TyName Name uni fun ann -> Term TyName Name uni fun ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Term TyName Name uni fun ann
term) (Normalized (Type TyName uni ()) -> Type TyName uni ()
forall a. Normalized a -> a
unNormalized Normalized (Type TyName uni ())
vTermTy) Normalized (Type TyName uni ())
vTy)