{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE StrictData #-}
module PlutusCore.TypeCheck.Internal
(
module PlutusCore.TypeCheck.Internal
, MonadNormalizeType
) where
import PlutusCore.Builtin.KnownKind (ToKind, kindOfBuiltinType)
import PlutusCore.Builtin.Result (throwing)
import PlutusCore.Core.Type (Kind (..), Normalized (..), Term (..), Type (..), toPatFuncKind)
import PlutusCore.Error (AsTypeError (_TypeError), ExpectedShapeOr (ExpectedExact, ExpectedShape),
TypeError (FreeTypeVariableE, FreeVariableE, KindMismatch, NameMismatch, TyNameMismatch, TypeMismatch, UnknownBuiltinFunctionE))
import PlutusCore.MkPlc (mkIterTyAppNoAnn, mkIterTyFun, mkTyBuiltinOf)
import PlutusCore.Name.Unique (HasText (theText), Name (Name), Named (Named), TermUnique,
TyName (TyName), TypeUnique, theUnique)
import PlutusCore.Name.UniqueMap (UniqueMap, insertNamed, lookupName)
import PlutusCore.Normalize.Internal (MonadNormalizeType)
import PlutusCore.Normalize.Internal qualified as Norm
import PlutusCore.Quote (MonadQuote (liftQuote), freshTyName)
import PlutusCore.Rename (Dupable, Rename (rename), dupable, liftDupable)
import PlutusPrelude (Lens', lens, over, view, void, zipExact, (<<$>>), (<<*>>), (^.))
import Control.Lens (Ixed (ix), makeClassy, makeLenses, preview, (^?))
import Control.Monad (when)
import Control.Monad.Except (MonadError)
import Control.Monad.Trans.Reader (ReaderT (runReaderT), ask, local)
import Data.Array (Array, Ix)
import Data.Foldable (for_)
import Data.List.Extras (wix)
import Data.Text qualified as Text
import Universe.Core (GEq, Some (Some), SomeTypeIn (SomeTypeIn), ValueOf (ValueOf))
newtype BuiltinTypes uni fun = BuiltinTypes
{ forall (uni :: * -> *) fun.
BuiltinTypes uni fun
-> Array fun (Dupable (Normalized (Type TyName uni ())))
unBuiltinTypes :: Array fun (Dupable (Normalized (Type TyName uni ())))
}
type TyVarKinds = UniqueMap TypeUnique (Named (Kind ()))
type VarTypes uni = UniqueMap TermUnique (Named (Dupable (Normalized (Type TyName uni ()))))
data HandleNameMismatches
= DetectNameMismatches
| IgnoreNameMismatches
deriving stock (Int -> HandleNameMismatches -> ShowS
[HandleNameMismatches] -> ShowS
HandleNameMismatches -> String
(Int -> HandleNameMismatches -> ShowS)
-> (HandleNameMismatches -> String)
-> ([HandleNameMismatches] -> ShowS)
-> Show HandleNameMismatches
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> HandleNameMismatches -> ShowS
showsPrec :: Int -> HandleNameMismatches -> ShowS
$cshow :: HandleNameMismatches -> String
show :: HandleNameMismatches -> String
$cshowList :: [HandleNameMismatches] -> ShowS
showList :: [HandleNameMismatches] -> ShowS
Show, HandleNameMismatches -> HandleNameMismatches -> Bool
(HandleNameMismatches -> HandleNameMismatches -> Bool)
-> (HandleNameMismatches -> HandleNameMismatches -> Bool)
-> Eq HandleNameMismatches
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: HandleNameMismatches -> HandleNameMismatches -> Bool
== :: HandleNameMismatches -> HandleNameMismatches -> Bool
$c/= :: HandleNameMismatches -> HandleNameMismatches -> Bool
/= :: HandleNameMismatches -> HandleNameMismatches -> Bool
Eq)
newtype KindCheckConfig = KindCheckConfig
{ KindCheckConfig -> HandleNameMismatches
_kccHandleNameMismatches :: HandleNameMismatches
}
makeClassy ''KindCheckConfig
data TypeCheckConfig uni fun = TypeCheckConfig
{ forall (uni :: * -> *) fun.
TypeCheckConfig uni fun -> KindCheckConfig
_tccKindCheckConfig :: KindCheckConfig
, forall (uni :: * -> *) fun.
TypeCheckConfig uni fun -> BuiltinTypes uni fun
_tccBuiltinTypes :: BuiltinTypes uni fun
}
class HasKindCheckConfig cfg => HasTypeCheckConfig cfg uni fun | cfg -> uni fun where
typeCheckConfig :: Lens' cfg (TypeCheckConfig uni fun)
tccKindCheckConfig :: Lens' cfg KindCheckConfig
tccKindCheckConfig =
(TypeCheckConfig uni fun -> f (TypeCheckConfig uni fun))
-> cfg -> f cfg
forall cfg (uni :: * -> *) fun.
HasTypeCheckConfig cfg uni fun =>
Lens' cfg (TypeCheckConfig uni fun)
Lens' cfg (TypeCheckConfig uni fun)
typeCheckConfig ((TypeCheckConfig uni fun -> f (TypeCheckConfig uni fun))
-> cfg -> f cfg)
-> ((KindCheckConfig -> f KindCheckConfig)
-> TypeCheckConfig uni fun -> f (TypeCheckConfig uni fun))
-> (KindCheckConfig -> f KindCheckConfig)
-> cfg
-> f cfg
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TypeCheckConfig uni fun -> KindCheckConfig)
-> (TypeCheckConfig uni fun
-> KindCheckConfig -> TypeCheckConfig uni fun)
-> Lens
(TypeCheckConfig uni fun)
(TypeCheckConfig uni fun)
KindCheckConfig
KindCheckConfig
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens TypeCheckConfig uni fun -> KindCheckConfig
forall (uni :: * -> *) fun.
TypeCheckConfig uni fun -> KindCheckConfig
_tccKindCheckConfig (\TypeCheckConfig uni fun
s KindCheckConfig
b -> TypeCheckConfig uni fun
s { _tccKindCheckConfig = b })
tccBuiltinTypes :: Lens' cfg (BuiltinTypes uni fun)
tccBuiltinTypes =
(TypeCheckConfig uni fun -> f (TypeCheckConfig uni fun))
-> cfg -> f cfg
forall cfg (uni :: * -> *) fun.
HasTypeCheckConfig cfg uni fun =>
Lens' cfg (TypeCheckConfig uni fun)
Lens' cfg (TypeCheckConfig uni fun)
typeCheckConfig ((TypeCheckConfig uni fun -> f (TypeCheckConfig uni fun))
-> cfg -> f cfg)
-> ((BuiltinTypes uni fun -> f (BuiltinTypes uni fun))
-> TypeCheckConfig uni fun -> f (TypeCheckConfig uni fun))
-> (BuiltinTypes uni fun -> f (BuiltinTypes uni fun))
-> cfg
-> f cfg
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TypeCheckConfig uni fun -> BuiltinTypes uni fun)
-> (TypeCheckConfig uni fun
-> BuiltinTypes uni fun -> TypeCheckConfig uni fun)
-> Lens
(TypeCheckConfig uni fun)
(TypeCheckConfig uni fun)
(BuiltinTypes uni fun)
(BuiltinTypes uni fun)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens TypeCheckConfig uni fun -> BuiltinTypes uni fun
forall (uni :: * -> *) fun.
TypeCheckConfig uni fun -> BuiltinTypes uni fun
_tccBuiltinTypes (\TypeCheckConfig uni fun
s BuiltinTypes uni fun
b -> TypeCheckConfig uni fun
s { _tccBuiltinTypes = b })
instance HasKindCheckConfig (TypeCheckConfig uni fun) where
kindCheckConfig :: Lens' (TypeCheckConfig uni fun) KindCheckConfig
kindCheckConfig = (KindCheckConfig -> f KindCheckConfig)
-> TypeCheckConfig uni fun -> f (TypeCheckConfig uni fun)
forall cfg (uni :: * -> *) fun.
HasTypeCheckConfig cfg uni fun =>
Lens' cfg KindCheckConfig
Lens' (TypeCheckConfig uni fun) KindCheckConfig
tccKindCheckConfig
instance HasTypeCheckConfig (TypeCheckConfig uni fun) uni fun where
typeCheckConfig :: Lens' (TypeCheckConfig uni fun) (TypeCheckConfig uni fun)
typeCheckConfig = (TypeCheckConfig uni fun -> f (TypeCheckConfig uni fun))
-> TypeCheckConfig uni fun -> f (TypeCheckConfig uni fun)
forall a. a -> a
id
data TypeCheckEnv uni fun cfg = TypeCheckEnv
{ forall (uni :: * -> *) fun cfg. TypeCheckEnv uni fun cfg -> cfg
_tceTypeCheckConfig :: cfg
, forall (uni :: * -> *) fun cfg.
TypeCheckEnv uni fun cfg -> TyVarKinds
_tceTyVarKinds :: TyVarKinds
, forall (uni :: * -> *) fun cfg.
TypeCheckEnv uni fun cfg -> VarTypes uni
_tceVarTypes :: VarTypes uni
}
makeLenses ''TypeCheckEnv
type TypeCheckT uni fun cfg m = ReaderT (TypeCheckEnv uni fun cfg) m
type MonadKindCheck err term uni fun ann m =
( MonadError err m
, AsTypeError err term uni fun ann
, ToKind uni
)
type MonadTypeCheck err term uni fun ann m =
( MonadKindCheck err term uni fun ann m
, Norm.MonadNormalizeType uni m
, GEq uni
, Ix fun
)
type MonadTypeCheckPlc err uni fun ann m =
MonadTypeCheck err (Term TyName Name uni fun ()) uni fun ann m
runTypeCheckM :: cfg -> TypeCheckT uni fun cfg m a -> m a
runTypeCheckM :: forall cfg (uni :: * -> *) fun (m :: * -> *) a.
cfg -> TypeCheckT uni fun cfg m a -> m a
runTypeCheckM cfg
config TypeCheckT uni fun cfg m a
a = TypeCheckT uni fun cfg m a -> TypeCheckEnv uni fun cfg -> m a
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT TypeCheckT uni fun cfg m a
a (TypeCheckEnv uni fun cfg -> m a)
-> TypeCheckEnv uni fun cfg -> m a
forall a b. (a -> b) -> a -> b
$ 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 () -> TypeCheckT uni fun cfg m a -> TypeCheckT uni fun cfg m a
withTyVar :: forall (uni :: * -> *) fun cfg (m :: * -> *) a.
TyName
-> Kind ()
-> TypeCheckT uni fun cfg m a
-> TypeCheckT uni fun cfg m a
withTyVar TyName
name = (TypeCheckEnv uni fun cfg -> TypeCheckEnv uni fun cfg)
-> ReaderT (TypeCheckEnv uni fun cfg) m a
-> ReaderT (TypeCheckEnv uni fun cfg) m a
forall r (m :: * -> *) a.
(r -> r) -> ReaderT r m a -> ReaderT r m a
local ((TypeCheckEnv uni fun cfg -> TypeCheckEnv uni fun cfg)
-> ReaderT (TypeCheckEnv uni fun cfg) m a
-> ReaderT (TypeCheckEnv uni fun cfg) m a)
-> (Kind ()
-> TypeCheckEnv uni fun cfg -> TypeCheckEnv uni fun cfg)
-> Kind ()
-> ReaderT (TypeCheckEnv uni fun cfg) m a
-> ReaderT (TypeCheckEnv uni fun cfg) m 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 (f :: * -> *).
Functor f =>
(TyVarKinds -> f TyVarKinds)
-> TypeCheckEnv uni fun cfg -> f (TypeCheckEnv uni fun cfg)
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.
(HasText name, HasUnique name unique) =>
name
-> a -> UniqueMap unique (Named a) -> UniqueMap unique (Named a)
insertNamed TyName
name
lookupBuiltinM
:: (MonadTypeCheck err term uni fun ann m, HasTypeCheckConfig cfg uni fun)
=> ann -> fun -> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ()))
lookupBuiltinM :: forall err term (uni :: * -> *) fun ann (m :: * -> *) cfg.
(MonadTypeCheck err term uni fun ann m,
HasTypeCheckConfig cfg uni fun) =>
ann
-> fun
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ()))
lookupBuiltinM ann
ann fun
fun = do
BuiltinTypes Array fun (Dupable (Normalized (Type TyName uni ())))
arr <- Getting
(BuiltinTypes uni fun)
(TypeCheckEnv uni fun cfg)
(BuiltinTypes uni fun)
-> ReaderT (TypeCheckEnv uni fun cfg) m (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) m (BuiltinTypes uni fun))
-> Getting
(BuiltinTypes uni fun)
(TypeCheckEnv uni fun cfg)
(BuiltinTypes uni fun)
-> ReaderT (TypeCheckEnv uni fun cfg) m (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 (f :: * -> *).
Functor f =>
(cfg -> f cfg)
-> TypeCheckEnv uni fun cfg -> f (TypeCheckEnv uni fun 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 cfg (uni :: * -> *) fun.
HasTypeCheckConfig cfg uni fun =>
Lens' cfg (BuiltinTypes uni fun)
Lens' cfg (BuiltinTypes uni fun)
tccBuiltinTypes
case 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) Array fun (Dupable (Normalized (Type TyName uni ())))
arr of
Maybe (Dupable (Normalized (Type TyName uni ())))
Nothing -> AReview err (TypeError term uni fun ann)
-> TypeError term uni fun ann
-> TypeCheckT uni fun cfg m (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)
Prism' err (TypeError term uni fun ann)
_TypeError (TypeError term uni fun ann
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ())))
-> TypeError term uni fun ann
-> TypeCheckT uni fun cfg m (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 ()))
-> TypeCheckT uni fun cfg m (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 ())
-> TypeCheckT uni fun cfg m a
-> TypeCheckT uni fun cfg m a
withVar :: forall (uni :: * -> *) fun cfg (m :: * -> *) a.
Name
-> Normalized (Type TyName uni ())
-> TypeCheckT uni fun cfg m a
-> TypeCheckT uni fun cfg m a
withVar Name
name = (TypeCheckEnv uni fun cfg -> TypeCheckEnv uni fun cfg)
-> ReaderT (TypeCheckEnv uni fun cfg) m a
-> ReaderT (TypeCheckEnv uni fun cfg) m a
forall r (m :: * -> *) a.
(r -> r) -> ReaderT r m a -> ReaderT r m a
local ((TypeCheckEnv uni fun cfg -> TypeCheckEnv uni fun cfg)
-> ReaderT (TypeCheckEnv uni fun cfg) m a
-> ReaderT (TypeCheckEnv uni fun cfg) m a)
-> (Normalized (Type TyName uni ())
-> TypeCheckEnv uni fun cfg -> TypeCheckEnv uni fun cfg)
-> Normalized (Type TyName uni ())
-> ReaderT (TypeCheckEnv uni fun cfg) m a
-> ReaderT (TypeCheckEnv uni fun cfg) m 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 (f :: * -> *).
Functor f =>
(VarTypes uni -> f (VarTypes uni))
-> TypeCheckEnv uni fun cfg -> f (TypeCheckEnv uni fun cfg)
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.
(HasText name, HasUnique name unique) =>
name
-> a -> UniqueMap unique (Named a) -> UniqueMap unique (Named a)
insertNamed 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 a. a -> Dupable a
dupable
lookupTyVarM
:: (MonadKindCheck err term uni fun ann m, HasKindCheckConfig cfg)
=> ann -> TyName -> TypeCheckT uni fun cfg m (Kind ())
lookupTyVarM :: forall err term (uni :: * -> *) fun ann (m :: * -> *) cfg.
(MonadKindCheck err term uni fun ann m, HasKindCheckConfig cfg) =>
ann -> TyName -> TypeCheckT uni fun cfg m (Kind ())
lookupTyVarM ann
ann TyName
name = do
TypeCheckEnv uni fun cfg
env <- ReaderT (TypeCheckEnv uni fun cfg) m (TypeCheckEnv uni fun cfg)
forall (m :: * -> *) r. Monad m => ReaderT r m r
ask
let handleNameMismatches :: HandleNameMismatches
handleNameMismatches = TypeCheckEnv uni fun cfg
env TypeCheckEnv uni fun cfg
-> Getting
HandleNameMismatches
(TypeCheckEnv uni fun cfg)
HandleNameMismatches
-> HandleNameMismatches
forall s a. s -> Getting a s a -> a
^. (cfg -> Const HandleNameMismatches cfg)
-> TypeCheckEnv uni fun cfg
-> Const HandleNameMismatches (TypeCheckEnv uni fun cfg)
forall (uni :: * -> *) fun cfg fun cfg (f :: * -> *).
Functor f =>
(cfg -> f cfg)
-> TypeCheckEnv uni fun cfg -> f (TypeCheckEnv uni fun cfg)
tceTypeCheckConfig ((cfg -> Const HandleNameMismatches cfg)
-> TypeCheckEnv uni fun cfg
-> Const HandleNameMismatches (TypeCheckEnv uni fun cfg))
-> ((HandleNameMismatches
-> Const HandleNameMismatches HandleNameMismatches)
-> cfg -> Const HandleNameMismatches cfg)
-> Getting
HandleNameMismatches
(TypeCheckEnv uni fun cfg)
HandleNameMismatches
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (HandleNameMismatches
-> Const HandleNameMismatches HandleNameMismatches)
-> cfg -> Const HandleNameMismatches cfg
forall c. HasKindCheckConfig c => Lens' c HandleNameMismatches
Lens' cfg HandleNameMismatches
kccHandleNameMismatches
case TyName -> TyVarKinds -> Maybe (Named (Kind ()))
forall name unique a.
HasUnique name unique =>
name -> UniqueMap unique a -> Maybe a
lookupName TyName
name (TyVarKinds -> Maybe (Named (Kind ())))
-> TyVarKinds -> Maybe (Named (Kind ()))
forall a b. (a -> b) -> a -> b
$ TypeCheckEnv uni fun cfg -> TyVarKinds
forall (uni :: * -> *) fun cfg.
TypeCheckEnv uni fun cfg -> TyVarKinds
_tceTyVarKinds TypeCheckEnv uni fun cfg
env of
Maybe (Named (Kind ()))
Nothing -> AReview err (TypeError term uni fun ann)
-> TypeError term uni fun ann -> TypeCheckT uni fun cfg m (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)
Prism' err (TypeError term uni fun ann)
_TypeError (TypeError term uni fun ann -> TypeCheckT uni fun cfg m (Kind ()))
-> TypeError term uni fun ann -> TypeCheckT uni fun cfg m (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 (Named Text
nameOrig Kind ()
kind) ->
if HandleNameMismatches
handleNameMismatches HandleNameMismatches -> HandleNameMismatches -> Bool
forall a. Eq a => a -> a -> Bool
== HandleNameMismatches
IgnoreNameMismatches Bool -> Bool -> Bool
|| Getting Text TyName Text -> TyName -> Text
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting Text TyName Text
forall a. HasText a => Lens' a Text
Lens' TyName Text
theText TyName
name Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
nameOrig
then Kind () -> TypeCheckT uni fun cfg m (Kind ())
forall a. a -> ReaderT (TypeCheckEnv uni fun cfg) m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Kind ()
kind
else AReview err (TypeError term uni fun ann)
-> TypeError term uni fun ann -> TypeCheckT uni fun cfg m (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)
Prism' err (TypeError term uni fun ann)
_TypeError (TypeError term uni fun ann -> TypeCheckT uni fun cfg m (Kind ()))
-> TypeError term uni fun ann -> TypeCheckT uni fun cfg m (Kind ())
forall a b. (a -> b) -> a -> b
$
ann -> TyName -> TyName -> TypeError term uni fun ann
forall term (uni :: * -> *) fun ann.
ann -> TyName -> TyName -> TypeError term uni fun ann
TyNameMismatch ann
ann (Name -> TyName
TyName (Name -> TyName) -> (Unique -> Name) -> Unique -> TyName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Unique -> Name
Name Text
nameOrig (Unique -> TyName) -> Unique -> TyName
forall a b. (a -> b) -> a -> b
$ TyName
name TyName -> Getting Unique TyName Unique -> Unique
forall s a. s -> Getting a s a -> a
^. Getting Unique TyName Unique
forall name unique. HasUnique name unique => Lens' name Unique
Lens' TyName Unique
theUnique) TyName
name
lookupVarM
:: (MonadTypeCheck err term uni fun ann m, HasTypeCheckConfig cfg uni fun)
=> ann -> Name -> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ()))
lookupVarM :: forall err term (uni :: * -> *) fun ann (m :: * -> *) cfg.
(MonadTypeCheck err term uni fun ann m,
HasTypeCheckConfig cfg uni fun) =>
ann
-> Name
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ()))
lookupVarM ann
ann Name
name = do
TypeCheckEnv uni fun cfg
env <- ReaderT (TypeCheckEnv uni fun cfg) m (TypeCheckEnv uni fun cfg)
forall (m :: * -> *) r. Monad m => ReaderT r m r
ask
let handleNameMismatches :: HandleNameMismatches
handleNameMismatches =
TypeCheckEnv uni fun cfg
env TypeCheckEnv uni fun cfg
-> Getting
HandleNameMismatches
(TypeCheckEnv uni fun cfg)
HandleNameMismatches
-> HandleNameMismatches
forall s a. s -> Getting a s a -> a
^. (cfg -> Const HandleNameMismatches cfg)
-> TypeCheckEnv uni fun cfg
-> Const HandleNameMismatches (TypeCheckEnv uni fun cfg)
forall (uni :: * -> *) fun cfg fun cfg (f :: * -> *).
Functor f =>
(cfg -> f cfg)
-> TypeCheckEnv uni fun cfg -> f (TypeCheckEnv uni fun cfg)
tceTypeCheckConfig ((cfg -> Const HandleNameMismatches cfg)
-> TypeCheckEnv uni fun cfg
-> Const HandleNameMismatches (TypeCheckEnv uni fun cfg))
-> ((HandleNameMismatches
-> Const HandleNameMismatches HandleNameMismatches)
-> cfg -> Const HandleNameMismatches cfg)
-> Getting
HandleNameMismatches
(TypeCheckEnv uni fun cfg)
HandleNameMismatches
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (KindCheckConfig -> Const HandleNameMismatches KindCheckConfig)
-> cfg -> Const HandleNameMismatches cfg
forall cfg (uni :: * -> *) fun.
HasTypeCheckConfig cfg uni fun =>
Lens' cfg KindCheckConfig
Lens' cfg KindCheckConfig
tccKindCheckConfig ((KindCheckConfig -> Const HandleNameMismatches KindCheckConfig)
-> cfg -> Const HandleNameMismatches cfg)
-> ((HandleNameMismatches
-> Const HandleNameMismatches HandleNameMismatches)
-> KindCheckConfig -> Const HandleNameMismatches KindCheckConfig)
-> (HandleNameMismatches
-> Const HandleNameMismatches HandleNameMismatches)
-> cfg
-> Const HandleNameMismatches cfg
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (HandleNameMismatches
-> Const HandleNameMismatches HandleNameMismatches)
-> KindCheckConfig -> Const HandleNameMismatches KindCheckConfig
forall c. HasKindCheckConfig c => Lens' c HandleNameMismatches
Lens' KindCheckConfig HandleNameMismatches
kccHandleNameMismatches
case Name
-> UniqueMap
TermUnique (Named (Dupable (Normalized (Type TyName uni ()))))
-> Maybe (Named (Dupable (Normalized (Type TyName uni ()))))
forall name unique a.
HasUnique name unique =>
name -> UniqueMap unique a -> Maybe a
lookupName Name
name (UniqueMap
TermUnique (Named (Dupable (Normalized (Type TyName uni ()))))
-> Maybe (Named (Dupable (Normalized (Type TyName uni ())))))
-> UniqueMap
TermUnique (Named (Dupable (Normalized (Type TyName uni ()))))
-> Maybe (Named (Dupable (Normalized (Type TyName uni ()))))
forall a b. (a -> b) -> a -> b
$ TypeCheckEnv uni fun cfg
-> UniqueMap
TermUnique (Named (Dupable (Normalized (Type TyName uni ()))))
forall (uni :: * -> *) fun cfg.
TypeCheckEnv uni fun cfg -> VarTypes uni
_tceVarTypes TypeCheckEnv uni fun cfg
env of
Maybe (Named (Dupable (Normalized (Type TyName uni ()))))
Nothing -> AReview err (TypeError term uni fun ann)
-> TypeError term uni fun ann
-> TypeCheckT uni fun cfg m (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)
Prism' err (TypeError term uni fun ann)
_TypeError (TypeError term uni fun ann
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ())))
-> TypeError term uni fun ann
-> TypeCheckT uni fun cfg m (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 (Named Text
nameOrig Dupable (Normalized (Type TyName uni ()))
ty) ->
if HandleNameMismatches
handleNameMismatches HandleNameMismatches -> HandleNameMismatches -> Bool
forall a. Eq a => a -> a -> Bool
== HandleNameMismatches
IgnoreNameMismatches Bool -> Bool -> Bool
|| Getting Text Name Text -> Name -> Text
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting Text Name Text
forall a. HasText a => Lens' a Text
Lens' Name Text
theText Name
name Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
nameOrig
then Dupable (Normalized (Type TyName uni ()))
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ()))
forall (m :: * -> *) a.
(MonadQuote m, Rename a) =>
Dupable a -> m a
liftDupable Dupable (Normalized (Type TyName uni ()))
ty
else AReview err (TypeError term uni fun ann)
-> TypeError term uni fun ann
-> TypeCheckT uni fun cfg m (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)
Prism' err (TypeError term uni fun ann)
_TypeError (TypeError term uni fun ann
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ())))
-> TypeError term uni fun ann
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ()))
forall a b. (a -> b) -> a -> b
$
ann -> Name -> Name -> TypeError term uni fun ann
forall term (uni :: * -> *) fun ann.
ann -> Name -> Name -> TypeError term uni fun ann
NameMismatch ann
ann (Text -> Unique -> Name
Name Text
nameOrig (Unique -> Name) -> Unique -> Name
forall a b. (a -> b) -> a -> b
$ Name
name Name -> Getting Unique Name Unique -> Unique
forall s a. s -> Getting a s a -> a
^. Getting Unique Name Unique
forall name unique. HasUnique name unique => Lens' name Unique
Lens' Name Unique
theUnique) Name
name
normalizeTypeM
:: MonadNormalizeType uni m
=> Type TyName uni ann
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ann))
normalizeTypeM :: forall (uni :: * -> *) (m :: * -> *) ann fun cfg.
MonadNormalizeType uni m =>
Type TyName uni ann
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ann))
normalizeTypeM Type TyName uni ann
ty = NormalizeTypeT
(ReaderT (TypeCheckEnv uni fun cfg) m)
TyName
uni
ann
(Normalized (Type TyName uni ann))
-> ReaderT
(TypeCheckEnv uni fun cfg) m (Normalized (Type TyName uni ann))
forall (m :: * -> *) tyname (uni :: * -> *) ann a.
NormalizeTypeT m tyname uni ann a -> m a
Norm.runNormalizeTypeT (NormalizeTypeT
(ReaderT (TypeCheckEnv uni fun cfg) m)
TyName
uni
ann
(Normalized (Type TyName uni ann))
-> ReaderT
(TypeCheckEnv uni fun cfg) m (Normalized (Type TyName uni ann)))
-> NormalizeTypeT
(ReaderT (TypeCheckEnv uni fun cfg) m)
TyName
uni
ann
(Normalized (Type TyName uni ann))
-> ReaderT
(TypeCheckEnv uni fun cfg) m (Normalized (Type TyName uni ann))
forall a b. (a -> b) -> a -> b
$ Type TyName uni ann
-> NormalizeTypeT
(ReaderT (TypeCheckEnv uni fun cfg) m)
TyName
uni
ann
(Normalized (Type TyName uni ann))
forall tyname (uni :: * -> *) (m :: * -> *) ann.
(HasUnique tyname TypeUnique, MonadNormalizeType uni m) =>
Type tyname uni ann
-> NormalizeTypeT
m tyname uni ann (Normalized (Type tyname uni ann))
Norm.normalizeTypeM Type TyName uni ann
ty
substNormalizeTypeM
:: MonadNormalizeType uni m
=> Normalized (Type TyName uni ())
-> TyName
-> Type TyName uni ()
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ()))
substNormalizeTypeM :: forall (uni :: * -> *) (m :: * -> *) fun cfg.
MonadNormalizeType uni m =>
Normalized (Type TyName uni ())
-> TyName
-> Type TyName uni ()
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ()))
substNormalizeTypeM Normalized (Type TyName uni ())
ty TyName
name Type TyName uni ()
body = NormalizeTypeT
(ReaderT (TypeCheckEnv uni fun cfg) m)
TyName
uni
()
(Normalized (Type TyName uni ()))
-> ReaderT
(TypeCheckEnv uni fun cfg) m (Normalized (Type TyName uni ()))
forall (m :: * -> *) tyname (uni :: * -> *) ann a.
NormalizeTypeT m tyname uni ann a -> m a
Norm.runNormalizeTypeT (NormalizeTypeT
(ReaderT (TypeCheckEnv uni fun cfg) m)
TyName
uni
()
(Normalized (Type TyName uni ()))
-> ReaderT
(TypeCheckEnv uni fun cfg) m (Normalized (Type TyName uni ())))
-> NormalizeTypeT
(ReaderT (TypeCheckEnv uni fun cfg) m)
TyName
uni
()
(Normalized (Type TyName uni ()))
-> ReaderT
(TypeCheckEnv uni fun cfg) m (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) m)
TyName
uni
()
(Normalized (Type TyName uni ()))
forall tyname (uni :: * -> *) (m :: * -> *) ann.
(HasUnique tyname TypeUnique, MonadNormalizeType uni m) =>
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
:: (MonadKindCheck err term uni fun ann m, HasKindCheckConfig cfg)
=> Type TyName uni ann -> TypeCheckT uni fun cfg m (Kind ())
inferKindM :: forall err term (uni :: * -> *) fun ann (m :: * -> *) cfg.
(MonadKindCheck err term uni fun ann m, HasKindCheckConfig cfg) =>
Type TyName uni ann -> TypeCheckT uni fun cfg m (Kind ())
inferKindM (TyBuiltin ann
_ (SomeTypeIn uni (Esc a)
uni)) =
Kind () -> ReaderT (TypeCheckEnv uni fun cfg) m (Kind ())
forall a. a -> ReaderT (TypeCheckEnv uni fun cfg) m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Kind () -> ReaderT (TypeCheckEnv uni fun cfg) m (Kind ()))
-> Kind () -> ReaderT (TypeCheckEnv uni fun cfg) m (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 -> ReaderT (TypeCheckEnv uni fun cfg) m (Kind ())
forall err term (uni :: * -> *) fun ann (m :: * -> *) cfg.
(MonadKindCheck err term uni fun ann m, HasKindCheckConfig cfg) =>
ann -> TyName -> TypeCheckT uni fun cfg m (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 ()
-> ReaderT (TypeCheckEnv uni fun cfg) m (Kind ())
-> ReaderT (TypeCheckEnv uni fun cfg) m (Kind ())
forall (uni :: * -> *) fun cfg (m :: * -> *) a.
TyName
-> Kind ()
-> TypeCheckT uni fun cfg m a
-> TypeCheckT uni fun cfg m a
withTyVar TyName
n Kind ()
dom_ (ReaderT (TypeCheckEnv uni fun cfg) m (Kind ())
-> ReaderT (TypeCheckEnv uni fun cfg) m (Kind ()))
-> ReaderT (TypeCheckEnv uni fun cfg) m (Kind ())
-> ReaderT (TypeCheckEnv uni fun cfg) m (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 ())
-> ReaderT (TypeCheckEnv uni fun cfg) m (Kind ())
-> ReaderT (TypeCheckEnv uni fun cfg) m (Kind ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type TyName uni ann
-> ReaderT (TypeCheckEnv uni fun cfg) m (Kind ())
forall err term (uni :: * -> *) fun ann (m :: * -> *) cfg.
(MonadKindCheck err term uni fun ann m, HasKindCheckConfig cfg) =>
Type TyName uni ann -> TypeCheckT uni fun cfg m (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
-> ReaderT (TypeCheckEnv uni fun cfg) m (Kind ())
forall err term (uni :: * -> *) fun ann (m :: * -> *) cfg.
(MonadKindCheck err term uni fun ann m, HasKindCheckConfig cfg) =>
Type TyName uni ann -> TypeCheckT uni fun cfg m (Kind ())
inferKindM Type TyName uni ann
fun
case Kind ()
funKind of
KindArrow ()
_ Kind ()
dom Kind ()
cod -> do
ann
-> Type TyName uni ann -> Kind () -> TypeCheckT uni fun cfg m ()
forall err term (uni :: * -> *) fun ann (m :: * -> *) cfg.
(MonadKindCheck err term uni fun ann m, HasKindCheckConfig cfg) =>
ann
-> Type TyName uni ann -> Kind () -> TypeCheckT uni fun cfg m ()
checkKindM ann
ann Type TyName uni ann
arg Kind ()
dom
Kind () -> ReaderT (TypeCheckEnv uni fun cfg) m (Kind ())
forall a. a -> ReaderT (TypeCheckEnv uni fun cfg) m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Kind ()
cod
Kind ()
_ -> do
let expectedKindArrow :: ExpectedShapeOr a
expectedKindArrow = Text -> [Text] -> ExpectedShapeOr a
forall a. Text -> [Text] -> ExpectedShapeOr a
ExpectedShape Text
"fun k l" [Text
"k", Text
"l"]
AReview err (TypeError term uni fun ann)
-> TypeError term uni fun ann
-> ReaderT (TypeCheckEnv uni fun cfg) m (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)
Prism' err (TypeError term uni fun ann)
_TypeError (TypeError term uni fun ann
-> ReaderT (TypeCheckEnv uni fun cfg) m (Kind ()))
-> TypeError term uni fun ann
-> ReaderT (TypeCheckEnv uni fun cfg) m (Kind ())
forall a b. (a -> b) -> a -> b
$ ann
-> Type TyName uni ()
-> ExpectedShapeOr (Kind ())
-> Kind ()
-> TypeError term uni fun ann
forall term (uni :: * -> *) fun ann.
ann
-> Type TyName uni ()
-> ExpectedShapeOr (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) ExpectedShapeOr (Kind ())
forall {a}. ExpectedShapeOr a
expectedKindArrow Kind ()
funKind
inferKindM (TyFun ann
ann Type TyName uni ann
dom Type TyName uni ann
cod) = do
ann
-> Type TyName uni ann -> Kind () -> TypeCheckT uni fun cfg m ()
forall err term (uni :: * -> *) fun ann (m :: * -> *) cfg.
(MonadKindCheck err term uni fun ann m, HasKindCheckConfig cfg) =>
ann
-> Type TyName uni ann -> Kind () -> TypeCheckT uni fun cfg m ()
checkKindM ann
ann Type TyName uni ann
dom (Kind () -> TypeCheckT uni fun cfg m ())
-> Kind () -> TypeCheckT uni fun cfg m ()
forall a b. (a -> b) -> a -> b
$ () -> Kind ()
forall ann. ann -> Kind ann
Type ()
ann
-> Type TyName uni ann -> Kind () -> TypeCheckT uni fun cfg m ()
forall err term (uni :: * -> *) fun ann (m :: * -> *) cfg.
(MonadKindCheck err term uni fun ann m, HasKindCheckConfig cfg) =>
ann
-> Type TyName uni ann -> Kind () -> TypeCheckT uni fun cfg m ()
checkKindM ann
ann Type TyName uni ann
cod (Kind () -> TypeCheckT uni fun cfg m ())
-> Kind () -> TypeCheckT uni fun cfg m ()
forall a b. (a -> b) -> a -> b
$ () -> Kind ()
forall ann. ann -> Kind ann
Type ()
Kind () -> ReaderT (TypeCheckEnv uni fun cfg) m (Kind ())
forall a. a -> ReaderT (TypeCheckEnv uni fun cfg) m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Kind () -> ReaderT (TypeCheckEnv uni fun cfg) m (Kind ()))
-> Kind () -> ReaderT (TypeCheckEnv uni fun cfg) m (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 ()
-> TypeCheckT uni fun cfg m ()
-> TypeCheckT uni fun cfg m ()
forall (uni :: * -> *) fun cfg (m :: * -> *) a.
TyName
-> Kind ()
-> TypeCheckT uni fun cfg m a
-> TypeCheckT uni fun cfg m a
withTyVar TyName
n (Kind ann -> Kind ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Kind ann
k) (TypeCheckT uni fun cfg m () -> TypeCheckT uni fun cfg m ())
-> TypeCheckT uni fun cfg m () -> TypeCheckT uni fun cfg m ()
forall a b. (a -> b) -> a -> b
$ ann
-> Type TyName uni ann -> Kind () -> TypeCheckT uni fun cfg m ()
forall err term (uni :: * -> *) fun ann (m :: * -> *) cfg.
(MonadKindCheck err term uni fun ann m, HasKindCheckConfig cfg) =>
ann
-> Type TyName uni ann -> Kind () -> TypeCheckT uni fun cfg m ()
checkKindM ann
ann Type TyName uni ann
body (() -> Kind ()
forall ann. ann -> Kind ann
Type ())
Kind () -> ReaderT (TypeCheckEnv uni fun cfg) m (Kind ())
forall a. a -> ReaderT (TypeCheckEnv uni fun cfg) m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Kind () -> ReaderT (TypeCheckEnv uni fun cfg) m (Kind ()))
-> Kind () -> ReaderT (TypeCheckEnv uni fun cfg) m (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
-> ReaderT (TypeCheckEnv uni fun cfg) m (Kind ())
forall err term (uni :: * -> *) fun ann (m :: * -> *) cfg.
(MonadKindCheck err term uni fun ann m, HasKindCheckConfig cfg) =>
Type TyName uni ann -> TypeCheckT uni fun cfg m (Kind ())
inferKindM Type TyName uni ann
arg
ann
-> Type TyName uni ann -> Kind () -> TypeCheckT uni fun cfg m ()
forall err term (uni :: * -> *) fun ann (m :: * -> *) cfg.
(MonadKindCheck err term uni fun ann m, HasKindCheckConfig cfg) =>
ann
-> Type TyName uni ann -> Kind () -> TypeCheckT uni fun cfg m ()
checkKindM ann
ann Type TyName uni ann
pat (Kind () -> TypeCheckT uni fun cfg m ())
-> Kind () -> TypeCheckT uni fun cfg m ()
forall a b. (a -> b) -> a -> b
$ Kind () -> Kind ()
toPatFuncKind Kind ()
k
Kind () -> ReaderT (TypeCheckEnv uni fun cfg) m (Kind ())
forall a. a -> ReaderT (TypeCheckEnv uni fun cfg) m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Kind () -> ReaderT (TypeCheckEnv uni fun cfg) m (Kind ()))
-> Kind () -> ReaderT (TypeCheckEnv uni fun cfg) m (Kind ())
forall a b. (a -> b) -> a -> b
$ () -> Kind ()
forall ann. ann -> Kind ann
Type ()
inferKindM (TySOP ann
ann [[Type TyName uni ann]]
tyls) = do
[[Type TyName uni ann]]
-> ([Type TyName uni ann] -> TypeCheckT uni fun cfg m ())
-> TypeCheckT uni fun cfg m ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ [[Type TyName uni ann]]
tyls (([Type TyName uni ann] -> TypeCheckT uni fun cfg m ())
-> TypeCheckT uni fun cfg m ())
-> ([Type TyName uni ann] -> TypeCheckT uni fun cfg m ())
-> TypeCheckT uni fun cfg m ()
forall a b. (a -> b) -> a -> b
$ \[Type TyName uni ann]
tyl -> [Type TyName uni ann]
-> (Type TyName uni ann -> TypeCheckT uni fun cfg m ())
-> TypeCheckT uni fun cfg m ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ [Type TyName uni ann]
tyl ((Type TyName uni ann -> TypeCheckT uni fun cfg m ())
-> TypeCheckT uni fun cfg m ())
-> (Type TyName uni ann -> TypeCheckT uni fun cfg m ())
-> TypeCheckT uni fun cfg m ()
forall a b. (a -> b) -> a -> b
$ \Type TyName uni ann
ty -> ann
-> Type TyName uni ann -> Kind () -> TypeCheckT uni fun cfg m ()
forall err term (uni :: * -> *) fun ann (m :: * -> *) cfg.
(MonadKindCheck err term uni fun ann m, HasKindCheckConfig cfg) =>
ann
-> Type TyName uni ann -> Kind () -> TypeCheckT uni fun cfg m ()
checkKindM ann
ann Type TyName uni ann
ty (() -> Kind ()
forall ann. ann -> Kind ann
Type ())
Kind () -> ReaderT (TypeCheckEnv uni fun cfg) m (Kind ())
forall a. a -> ReaderT (TypeCheckEnv uni fun cfg) m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Kind () -> ReaderT (TypeCheckEnv uni fun cfg) m (Kind ()))
-> Kind () -> ReaderT (TypeCheckEnv uni fun cfg) m (Kind ())
forall a b. (a -> b) -> a -> b
$ () -> Kind ()
forall ann. ann -> Kind ann
Type ()
checkKindM
:: (MonadKindCheck err term uni fun ann m, HasKindCheckConfig cfg)
=> ann -> Type TyName uni ann -> Kind () -> TypeCheckT uni fun cfg m ()
checkKindM :: forall err term (uni :: * -> *) fun ann (m :: * -> *) cfg.
(MonadKindCheck err term uni fun ann m, HasKindCheckConfig cfg) =>
ann
-> Type TyName uni ann -> Kind () -> TypeCheckT uni fun cfg m ()
checkKindM ann
ann Type TyName uni ann
ty Kind ()
k = do
Kind ()
tyK <- Type TyName uni ann -> TypeCheckT uni fun cfg m (Kind ())
forall err term (uni :: * -> *) fun ann (m :: * -> *) cfg.
(MonadKindCheck err term uni fun ann m, HasKindCheckConfig cfg) =>
Type TyName uni ann -> TypeCheckT uni fun cfg m (Kind ())
inferKindM Type TyName uni ann
ty
Bool -> TypeCheckT uni fun cfg m () -> TypeCheckT uni fun cfg m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Kind ()
tyK Kind () -> Kind () -> Bool
forall a. Eq a => a -> a -> Bool
/= Kind ()
k) (TypeCheckT uni fun cfg m () -> TypeCheckT uni fun cfg m ())
-> TypeCheckT uni fun cfg m () -> TypeCheckT uni fun cfg m ()
forall a b. (a -> b) -> a -> b
$ AReview err (TypeError term uni fun ann)
-> TypeError term uni fun ann -> TypeCheckT uni fun cfg m ()
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)
Prism' err (TypeError term uni fun ann)
_TypeError (ann
-> Type TyName uni ()
-> ExpectedShapeOr (Kind ())
-> Kind ()
-> TypeError term uni fun ann
forall term (uni :: * -> *) fun ann.
ann
-> Type TyName uni ()
-> ExpectedShapeOr (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 () -> ExpectedShapeOr (Kind ())
forall a. a -> ExpectedShapeOr a
ExpectedExact Kind ()
k) Kind ()
tyK)
unfoldIFixOf
:: MonadNormalizeType uni m
=> Normalized (Type TyName uni ())
-> Normalized (Type TyName uni ())
-> Kind ()
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ()))
unfoldIFixOf :: forall (uni :: * -> *) (m :: * -> *) fun cfg.
MonadNormalizeType uni m =>
Normalized (Type TyName uni ())
-> Normalized (Type TyName uni ())
-> Kind ()
-> TypeCheckT uni fun cfg m (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) m TyName
forall a. Quote a -> ReaderT (TypeCheckEnv uni fun cfg) m a
forall (m :: * -> *) a. MonadQuote m => Quote a -> m a
liftQuote (Quote TyName -> ReaderT (TypeCheckEnv uni fun cfg) m TyName)
-> Quote TyName -> ReaderT (TypeCheckEnv uni fun cfg) m 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) m (Type TyName uni ())
forall a (m :: * -> *). (Rename a, MonadQuote m) => a -> m a
forall (m :: * -> *).
MonadQuote m =>
Type TyName uni () -> m (Type TyName uni ())
rename Type TyName uni ()
vPat
Type TyName uni ()
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ()))
forall (uni :: * -> *) (m :: * -> *) ann fun cfg.
MonadNormalizeType uni m =>
Type TyName uni ann
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ann))
normalizeTypeM (Type TyName uni ()
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ())))
-> Type TyName uni ()
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ()))
forall a b. (a -> b) -> a -> b
$
Type TyName uni () -> [Type TyName uni ()] -> Type TyName uni ()
forall tyname (uni :: * -> *).
Type tyname uni () -> [Type tyname uni ()] -> Type tyname uni ()
mkIterTyAppNoAnn 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
:: (MonadTypeCheckPlc err uni fun ann m, HasTypeCheckConfig cfg uni fun)
=> Term TyName Name uni fun ann -> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ()))
inferTypeM :: forall err (uni :: * -> *) fun ann (m :: * -> *) cfg.
(MonadTypeCheckPlc err uni fun ann m,
HasTypeCheckConfig cfg uni fun) =>
Term TyName Name uni fun ann
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ()))
inferTypeM (Constant ann
_ (Some (ValueOf uni (Esc a)
uni a
_))) =
Type TyName uni ()
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ()))
forall (uni :: * -> *) (m :: * -> *) ann fun cfg.
MonadNormalizeType uni m =>
Type TyName uni ann
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ann))
normalizeTypeM (Type TyName uni ()
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ())))
-> Type TyName uni ()
-> TypeCheckT uni fun cfg m (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
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ()))
forall err term (uni :: * -> *) fun ann (m :: * -> *) cfg.
(MonadTypeCheck err term uni fun ann m,
HasTypeCheckConfig cfg uni fun) =>
ann
-> fun
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ()))
lookupBuiltinM ann
ann fun
fun
inferTypeM (Var ann
ann Name
name) =
ann
-> Name
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ()))
forall err term (uni :: * -> *) fun ann (m :: * -> *) cfg.
(MonadTypeCheck err term uni fun ann m,
HasTypeCheckConfig cfg uni fun) =>
ann
-> Name
-> TypeCheckT uni fun cfg m (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 () -> TypeCheckT uni fun cfg m ()
forall err term (uni :: * -> *) fun ann (m :: * -> *) cfg.
(MonadKindCheck err term uni fun ann m, HasKindCheckConfig cfg) =>
ann
-> Type TyName uni ann -> Kind () -> TypeCheckT uni fun cfg m ()
checkKindM ann
ann Type TyName uni ann
dom (Kind () -> TypeCheckT uni fun cfg m ())
-> Kind () -> TypeCheckT uni fun cfg m ()
forall a b. (a -> b) -> a -> b
$ () -> Kind ()
forall ann. ann -> Kind ann
Type ()
Normalized (Type TyName uni ())
vDom <- Type TyName uni ()
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ()))
forall (uni :: * -> *) (m :: * -> *) ann fun cfg.
MonadNormalizeType uni m =>
Type TyName uni ann
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ann))
normalizeTypeM (Type TyName uni ()
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ())))
-> Type TyName uni ()
-> TypeCheckT uni fun cfg m (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 ())
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ()))
-> ReaderT
(TypeCheckEnv uni fun cfg)
m
(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 ())
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ()))
forall a. a -> ReaderT (TypeCheckEnv uni fun cfg) m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Normalized (Type TyName uni ())
vDom ReaderT
(TypeCheckEnv uni fun cfg)
m
(Normalized (Type TyName uni () -> Type TyName uni ()))
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ()))
-> TypeCheckT uni fun cfg m (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 ())
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ()))
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ()))
forall (uni :: * -> *) fun cfg (m :: * -> *) a.
Name
-> Normalized (Type TyName uni ())
-> TypeCheckT uni fun cfg m a
-> TypeCheckT uni fun cfg m a
withVar Name
n Normalized (Type TyName uni ())
vDom (Term TyName Name uni fun ann
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ()))
forall err (uni :: * -> *) fun ann (m :: * -> *) cfg.
(MonadTypeCheckPlc err uni fun ann m,
HasTypeCheckConfig cfg uni fun) =>
Term TyName Name uni fun ann
-> TypeCheckT uni fun cfg m (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 ())
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ()))
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ()))
forall (f1 :: * -> *) (f2 :: * -> *) a b.
(Functor f1, Functor f2) =>
(a -> b) -> f1 (f2 a) -> f1 (f2 b)
<<$>> TyName
-> Kind ()
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ()))
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ()))
forall (uni :: * -> *) fun cfg (m :: * -> *) a.
TyName
-> Kind ()
-> TypeCheckT uni fun cfg m a
-> TypeCheckT uni fun cfg m a
withTyVar TyName
n Kind ()
nK_ (Term TyName Name uni fun ann
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ()))
forall err (uni :: * -> *) fun ann (m :: * -> *) cfg.
(MonadTypeCheckPlc err uni fun ann m,
HasTypeCheckConfig cfg uni fun) =>
Term TyName Name uni fun ann
-> TypeCheckT uni fun cfg m (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
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ()))
forall err (uni :: * -> *) fun ann (m :: * -> *) cfg.
(MonadTypeCheckPlc err uni fun ann m,
HasTypeCheckConfig cfg uni fun) =>
Term TyName Name uni fun ann
-> TypeCheckT uni fun cfg m (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 ())
-> TypeCheckT uni fun cfg m ()
forall err (uni :: * -> *) fun ann (m :: * -> *) cfg.
(MonadTypeCheckPlc err uni fun ann m,
HasTypeCheckConfig cfg uni fun) =>
ann
-> Term TyName Name uni fun ann
-> Normalized (Type TyName uni ())
-> TypeCheckT uni fun cfg m ()
checkTypeM ann
ann Term TyName Name uni fun ann
arg (Normalized (Type TyName uni ()) -> TypeCheckT uni fun cfg m ())
-> Normalized (Type TyName uni ()) -> TypeCheckT uni fun cfg m ()
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 ())
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ()))
forall a. a -> ReaderT (TypeCheckEnv uni fun cfg) m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Normalized (Type TyName uni ())
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ())))
-> Normalized (Type TyName uni ())
-> TypeCheckT uni fun cfg m (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 ()
_ -> do
let expectedTyFun :: ExpectedShapeOr a
expectedTyFun = Text -> [Text] -> ExpectedShapeOr a
forall a. Text -> [Text] -> ExpectedShapeOr a
ExpectedShape Text
"fun k l" [Text
"k", Text
"l"]
AReview err (TypeError (Term TyName Name uni fun ()) uni fun ann)
-> TypeError (Term TyName Name uni fun ()) uni fun ann
-> TypeCheckT uni fun cfg m (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)
Prism' err (TypeError (Term TyName Name uni fun ()) uni fun ann)
_TypeError (ann
-> Term TyName Name uni fun ()
-> ExpectedShapeOr (Type TyName uni ())
-> Normalized (Type TyName uni ())
-> TypeError (Term TyName Name uni fun ()) uni fun ann
forall term (uni :: * -> *) fun ann.
ann
-> term
-> ExpectedShapeOr (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) ExpectedShapeOr (Type TyName uni ())
forall {a}. ExpectedShapeOr a
expectedTyFun 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
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ()))
forall err (uni :: * -> *) fun ann (m :: * -> *) cfg.
(MonadTypeCheckPlc err uni fun ann m,
HasTypeCheckConfig cfg uni fun) =>
Term TyName Name uni fun ann
-> TypeCheckT uni fun cfg m (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 () -> TypeCheckT uni fun cfg m ()
forall err term (uni :: * -> *) fun ann (m :: * -> *) cfg.
(MonadKindCheck err term uni fun ann m, HasKindCheckConfig cfg) =>
ann
-> Type TyName uni ann -> Kind () -> TypeCheckT uni fun cfg m ()
checkKindM ann
ann Type TyName uni ann
ty Kind ()
nK
Normalized (Type TyName uni ())
vTy <- Type TyName uni ()
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ()))
forall (uni :: * -> *) (m :: * -> *) ann fun cfg.
MonadNormalizeType uni m =>
Type TyName uni ann
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ann))
normalizeTypeM (Type TyName uni ()
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ())))
-> Type TyName uni ()
-> TypeCheckT uni fun cfg m (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 ()
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ()))
forall (uni :: * -> *) (m :: * -> *) fun cfg.
MonadNormalizeType uni m =>
Normalized (Type TyName uni ())
-> TyName
-> Type TyName uni ()
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ()))
substNormalizeTypeM Normalized (Type TyName uni ())
vTy TyName
n Type TyName uni ()
vCod
Type TyName uni ()
_ -> do
let expectedTyForall :: ExpectedShapeOr a
expectedTyForall = Text -> [Text] -> ExpectedShapeOr a
forall a. Text -> [Text] -> ExpectedShapeOr a
ExpectedShape Text
"all a kind body" [Text
"a", Text
"kind", Text
"body"]
AReview err (TypeError (Term TyName Name uni fun ()) uni fun ann)
-> TypeError (Term TyName Name uni fun ()) uni fun ann
-> TypeCheckT uni fun cfg m (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)
Prism' err (TypeError (Term TyName Name uni fun ()) uni fun ann)
_TypeError (ann
-> Term TyName Name uni fun ()
-> ExpectedShapeOr (Type TyName uni ())
-> Normalized (Type TyName uni ())
-> TypeError (Term TyName Name uni fun ()) uni fun ann
forall term (uni :: * -> *) fun ann.
ann
-> term
-> ExpectedShapeOr (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) ExpectedShapeOr (Type TyName uni ())
forall {a}. ExpectedShapeOr a
expectedTyForall 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 -> TypeCheckT uni fun cfg m (Kind ())
forall err term (uni :: * -> *) fun ann (m :: * -> *) cfg.
(MonadKindCheck err term uni fun ann m, HasKindCheckConfig cfg) =>
Type TyName uni ann -> TypeCheckT uni fun cfg m (Kind ())
inferKindM Type TyName uni ann
arg
ann
-> Type TyName uni ann -> Kind () -> TypeCheckT uni fun cfg m ()
forall err term (uni :: * -> *) fun ann (m :: * -> *) cfg.
(MonadKindCheck err term uni fun ann m, HasKindCheckConfig cfg) =>
ann
-> Type TyName uni ann -> Kind () -> TypeCheckT uni fun cfg m ()
checkKindM ann
ann Type TyName uni ann
pat (Kind () -> TypeCheckT uni fun cfg m ())
-> Kind () -> TypeCheckT uni fun cfg m ()
forall a b. (a -> b) -> a -> b
$ Kind () -> Kind ()
toPatFuncKind Kind ()
k
Normalized (Type TyName uni ())
vPat <- Type TyName uni ()
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ()))
forall (uni :: * -> *) (m :: * -> *) ann fun cfg.
MonadNormalizeType uni m =>
Type TyName uni ann
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ann))
normalizeTypeM (Type TyName uni ()
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ())))
-> Type TyName uni ()
-> TypeCheckT uni fun cfg m (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 ()
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ()))
forall (uni :: * -> *) (m :: * -> *) ann fun cfg.
MonadNormalizeType uni m =>
Type TyName uni ann
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ann))
normalizeTypeM (Type TyName uni ()
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ())))
-> Type TyName uni ()
-> TypeCheckT uni fun cfg m (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 ())
-> TypeCheckT uni fun cfg m ()
forall err (uni :: * -> *) fun ann (m :: * -> *) cfg.
(MonadTypeCheckPlc err uni fun ann m,
HasTypeCheckConfig cfg uni fun) =>
ann
-> Term TyName Name uni fun ann
-> Normalized (Type TyName uni ())
-> TypeCheckT uni fun cfg m ()
checkTypeM ann
ann Term TyName Name uni fun ann
term (Normalized (Type TyName uni ()) -> TypeCheckT uni fun cfg m ())
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ()))
-> TypeCheckT uni fun cfg m ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Normalized (Type TyName uni ())
-> Normalized (Type TyName uni ())
-> Kind ()
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ()))
forall (uni :: * -> *) (m :: * -> *) fun cfg.
MonadNormalizeType uni m =>
Normalized (Type TyName uni ())
-> Normalized (Type TyName uni ())
-> Kind ()
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ()))
unfoldIFixOf Normalized (Type TyName uni ())
vPat Normalized (Type TyName uni ())
vArg Kind ()
k
Normalized (Type TyName uni ())
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ()))
forall a. a -> ReaderT (TypeCheckEnv uni fun cfg) m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Normalized (Type TyName uni ())
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ())))
-> Normalized (Type TyName uni ())
-> TypeCheckT uni fun cfg m (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 a b. Normalized (a -> b) -> Normalized a -> Normalized b
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
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ()))
forall err (uni :: * -> *) fun ann (m :: * -> *) cfg.
(MonadTypeCheckPlc err uni fun ann m,
HasTypeCheckConfig cfg uni fun) =>
Term TyName Name uni fun ann
-> TypeCheckT uni fun cfg m (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 -> TypeCheckT uni fun cfg m (Kind ())
forall err term (uni :: * -> *) fun ann (m :: * -> *) cfg.
(MonadKindCheck err term uni fun ann m, HasKindCheckConfig cfg) =>
Type TyName uni ann -> TypeCheckT uni fun cfg m (Kind ())
inferKindM (Type TyName uni ann -> TypeCheckT uni fun cfg m (Kind ()))
-> Type TyName uni ann -> TypeCheckT uni fun cfg m (Kind ())
forall a b. (a -> b) -> a -> b
$ ann
ann ann -> Type TyName uni () -> Type TyName uni ann
forall a b. a -> Type TyName uni b -> Type TyName uni a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Type TyName uni ()
vArg
Normalized (Type TyName uni ())
-> Normalized (Type TyName uni ())
-> Kind ()
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ()))
forall (uni :: * -> *) (m :: * -> *) fun cfg.
MonadNormalizeType uni m =>
Normalized (Type TyName uni ())
-> Normalized (Type TyName uni ())
-> Kind ()
-> TypeCheckT uni fun cfg m (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 ()
_ -> do
let expectedTyIFix :: ExpectedShapeOr a
expectedTyIFix = Text -> [Text] -> ExpectedShapeOr a
forall a. Text -> [Text] -> ExpectedShapeOr a
ExpectedShape Text
"ifix pat arg" [Text
"pat", Text
"arg"]
AReview err (TypeError (Term TyName Name uni fun ()) uni fun ann)
-> TypeError (Term TyName Name uni fun ()) uni fun ann
-> TypeCheckT uni fun cfg m (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)
Prism' err (TypeError (Term TyName Name uni fun ()) uni fun ann)
_TypeError (ann
-> Term TyName Name uni fun ()
-> ExpectedShapeOr (Type TyName uni ())
-> Normalized (Type TyName uni ())
-> TypeError (Term TyName Name uni fun ()) uni fun ann
forall term (uni :: * -> *) fun ann.
ann
-> term
-> ExpectedShapeOr (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) ExpectedShapeOr (Type TyName uni ())
forall {a}. ExpectedShapeOr a
expectedTyIFix Normalized (Type TyName uni ())
vTermTy)
inferTypeM (Error ann
ann Type TyName uni ann
ty) = do
ann
-> Type TyName uni ann -> Kind () -> TypeCheckT uni fun cfg m ()
forall err term (uni :: * -> *) fun ann (m :: * -> *) cfg.
(MonadKindCheck err term uni fun ann m, HasKindCheckConfig cfg) =>
ann
-> Type TyName uni ann -> Kind () -> TypeCheckT uni fun cfg m ()
checkKindM ann
ann Type TyName uni ann
ty (Kind () -> TypeCheckT uni fun cfg m ())
-> Kind () -> TypeCheckT uni fun cfg m ()
forall a b. (a -> b) -> a -> b
$ () -> Kind ()
forall ann. ann -> Kind ann
Type ()
Type TyName uni ()
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ()))
forall (uni :: * -> *) (m :: * -> *) ann fun cfg.
MonadNormalizeType uni m =>
Type TyName uni ann
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ann))
normalizeTypeM (Type TyName uni ()
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ())))
-> Type TyName uni ()
-> TypeCheckT uni fun cfg m (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
inferTypeM t :: Term TyName Name uni fun ann
t@(Constr ann
ann Type TyName uni ann
resTy Word64
i [Term TyName Name uni fun ann]
args) = do
Normalized (Type TyName uni ())
vResTy <- Type TyName uni ()
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ()))
forall (uni :: * -> *) (m :: * -> *) ann fun cfg.
MonadNormalizeType uni m =>
Type TyName uni ann
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ann))
normalizeTypeM (Type TyName uni ()
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ())))
-> Type TyName uni ()
-> TypeCheckT uni fun cfg m (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
resTy
let
prodPrefix :: [Text]
prodPrefix = (Integer -> Text) -> [Integer] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map (\Integer
j -> Text
"prod_" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
Text.pack (Integer -> String
forall a. Show a => a -> String
show Integer
j)) [Integer
0 .. Word64 -> Integer
forall a. Integral a => a -> Integer
toInteger Word64
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1]
fields :: [Text]
fields = (Int -> Text) -> [Int] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map (\Int
k -> Text
"field_" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
Text.pack (Int -> String
forall a. Show a => a -> String
show Int
k)) [Int
0 .. [Term TyName Name uni fun ann] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term TyName Name uni fun ann]
args Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]
prod_i :: Text
prod_i = Text
"[" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text -> [Text] -> Text
Text.intercalate Text
" " [Text]
fields Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"]"
shape :: Text
shape = Text
"sop " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> (Text -> Text) -> [Text] -> Text
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" ") [Text]
prodPrefix Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
prod_i Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" ..."
vars :: [Text]
vars = [Text]
prodPrefix [Text] -> [Text] -> [Text]
forall a. [a] -> [a] -> [a]
++ [Text]
fields
expectedSop :: ExpectedShapeOr a
expectedSop = Text -> [Text] -> ExpectedShapeOr a
forall a. Text -> [Text] -> ExpectedShapeOr a
ExpectedShape Text
shape [Text]
vars
case Normalized (Type TyName uni ()) -> Type TyName uni ()
forall a. Normalized a -> a
unNormalized Normalized (Type TyName uni ())
vResTy of
TySOP ()
_ [[Type TyName uni ()]]
vSTys -> case [[Type TyName uni ()]]
vSTys [[Type TyName uni ()]]
-> Getting
(First [Type TyName uni ()])
[[Type TyName uni ()]]
[Type TyName uni ()]
-> Maybe [Type TyName uni ()]
forall s a. s -> Getting (First a) s a -> Maybe a
^? Word64 -> Traversal' [[Type TyName uni ()]] [Type TyName uni ()]
forall a. Word64 -> Traversal' [a] a
wix Word64
i of
Just [Type TyName uni ()]
pTys -> case [Term TyName Name uni fun ann]
-> [Type TyName uni ()]
-> Maybe [(Term TyName Name uni fun ann, Type TyName uni ())]
forall a b. [a] -> [b] -> Maybe [(a, b)]
zipExact [Term TyName Name uni fun ann]
args [Type TyName uni ()]
pTys of
Just [(Term TyName Name uni fun ann, Type TyName uni ())]
ps -> [(Term TyName Name uni fun ann, Type TyName uni ())]
-> ((Term TyName Name uni fun ann, Type TyName uni ())
-> TypeCheckT uni fun cfg m ())
-> TypeCheckT uni fun cfg m ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ [(Term TyName Name uni fun ann, Type TyName uni ())]
ps (((Term TyName Name uni fun ann, Type TyName uni ())
-> TypeCheckT uni fun cfg m ())
-> TypeCheckT uni fun cfg m ())
-> ((Term TyName Name uni fun ann, Type TyName uni ())
-> TypeCheckT uni fun cfg m ())
-> TypeCheckT uni fun cfg m ()
forall a b. (a -> b) -> a -> b
$ \(Term TyName Name uni fun ann
arg, Type TyName uni ()
pTy) -> ann
-> Term TyName Name uni fun ann
-> Normalized (Type TyName uni ())
-> TypeCheckT uni fun cfg m ()
forall err (uni :: * -> *) fun ann (m :: * -> *) cfg.
(MonadTypeCheckPlc err uni fun ann m,
HasTypeCheckConfig cfg uni fun) =>
ann
-> Term TyName Name uni fun ann
-> Normalized (Type TyName uni ())
-> TypeCheckT uni fun cfg m ()
checkTypeM ann
ann Term TyName Name uni fun ann
arg (Type TyName uni () -> Normalized (Type TyName uni ())
forall a. a -> Normalized a
Normalized Type TyName uni ()
pTy)
Maybe [(Term TyName Name uni fun ann, Type TyName uni ())]
Nothing -> AReview err (TypeError (Term TyName Name uni fun ()) uni fun ann)
-> TypeError (Term TyName Name uni fun ()) uni fun ann
-> TypeCheckT uni fun cfg m ()
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)
Prism' err (TypeError (Term TyName Name uni fun ()) uni fun ann)
_TypeError (ann
-> Term TyName Name uni fun ()
-> ExpectedShapeOr (Type TyName uni ())
-> Normalized (Type TyName uni ())
-> TypeError (Term TyName Name uni fun ()) uni fun ann
forall term (uni :: * -> *) fun ann.
ann
-> term
-> ExpectedShapeOr (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
t) ExpectedShapeOr (Type TyName uni ())
forall {a}. ExpectedShapeOr a
expectedSop Normalized (Type TyName uni ())
vResTy)
Maybe [Type TyName uni ()]
Nothing -> AReview err (TypeError (Term TyName Name uni fun ()) uni fun ann)
-> TypeError (Term TyName Name uni fun ()) uni fun ann
-> TypeCheckT uni fun cfg m ()
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)
Prism' err (TypeError (Term TyName Name uni fun ()) uni fun ann)
_TypeError (ann
-> Term TyName Name uni fun ()
-> ExpectedShapeOr (Type TyName uni ())
-> Normalized (Type TyName uni ())
-> TypeError (Term TyName Name uni fun ()) uni fun ann
forall term (uni :: * -> *) fun ann.
ann
-> term
-> ExpectedShapeOr (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
t) ExpectedShapeOr (Type TyName uni ())
forall {a}. ExpectedShapeOr a
expectedSop Normalized (Type TyName uni ())
vResTy)
Type TyName uni ()
_ -> AReview err (TypeError (Term TyName Name uni fun ()) uni fun ann)
-> TypeError (Term TyName Name uni fun ()) uni fun ann
-> TypeCheckT uni fun cfg m ()
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)
Prism' err (TypeError (Term TyName Name uni fun ()) uni fun ann)
_TypeError (ann
-> Term TyName Name uni fun ()
-> ExpectedShapeOr (Type TyName uni ())
-> Normalized (Type TyName uni ())
-> TypeError (Term TyName Name uni fun ()) uni fun ann
forall term (uni :: * -> *) fun ann.
ann
-> term
-> ExpectedShapeOr (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
t) ExpectedShapeOr (Type TyName uni ())
forall {a}. ExpectedShapeOr a
expectedSop Normalized (Type TyName uni ())
vResTy)
Normalized (Type TyName uni ())
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ()))
forall a. a -> ReaderT (TypeCheckEnv uni fun cfg) m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Normalized (Type TyName uni ())
vResTy
inferTypeM (Case ann
ann Type TyName uni ann
resTy Term TyName Name uni fun ann
scrut [Term TyName Name uni fun ann]
cases) = do
Normalized (Type TyName uni ())
vResTy <- Type TyName uni ()
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ()))
forall (uni :: * -> *) (m :: * -> *) ann fun cfg.
MonadNormalizeType uni m =>
Type TyName uni ann
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ann))
normalizeTypeM (Type TyName uni ()
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ())))
-> Type TyName uni ()
-> TypeCheckT uni fun cfg m (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
resTy
Normalized (Type TyName uni ())
vScrutTy <- Term TyName Name uni fun ann
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ()))
forall err (uni :: * -> *) fun ann (m :: * -> *) cfg.
(MonadTypeCheckPlc err uni fun ann m,
HasTypeCheckConfig cfg uni fun) =>
Term TyName Name uni fun ann
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ()))
inferTypeM Term TyName Name uni fun ann
scrut
let prods :: [Text]
prods = (Int -> Text) -> [Int] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map (\Int
j -> Text
"prod_" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
Text.pack (Int -> String
forall a. Show a => a -> String
show Int
j)) [Int
0 .. [Term TyName Name uni fun ann] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term TyName Name uni fun ann]
cases Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]
expectedSop :: ExpectedShapeOr a
expectedSop = Text -> [Text] -> ExpectedShapeOr a
forall a. Text -> [Text] -> ExpectedShapeOr a
ExpectedShape (Text -> [Text] -> Text
Text.intercalate Text
" " ([Text] -> Text) -> [Text] -> Text
forall a b. (a -> b) -> a -> b
$ Text
"sop" Text -> [Text] -> [Text]
forall a. a -> [a] -> [a]
: [Text]
prods) [Text]
prods
case Normalized (Type TyName uni ()) -> Type TyName uni ()
forall a. Normalized a -> a
unNormalized Normalized (Type TyName uni ())
vScrutTy of
TySOP ()
_ [[Type TyName uni ()]]
sTys -> case [Term TyName Name uni fun ann]
-> [[Type TyName uni ()]]
-> Maybe [(Term TyName Name uni fun ann, [Type TyName uni ()])]
forall a b. [a] -> [b] -> Maybe [(a, b)]
zipExact [Term TyName Name uni fun ann]
cases [[Type TyName uni ()]]
sTys of
Just [(Term TyName Name uni fun ann, [Type TyName uni ()])]
casesAndArgTypes -> [(Term TyName Name uni fun ann, [Type TyName uni ()])]
-> ((Term TyName Name uni fun ann, [Type TyName uni ()])
-> TypeCheckT uni fun cfg m ())
-> TypeCheckT uni fun cfg m ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ [(Term TyName Name uni fun ann, [Type TyName uni ()])]
casesAndArgTypes (((Term TyName Name uni fun ann, [Type TyName uni ()])
-> TypeCheckT uni fun cfg m ())
-> TypeCheckT uni fun cfg m ())
-> ((Term TyName Name uni fun ann, [Type TyName uni ()])
-> TypeCheckT uni fun cfg m ())
-> TypeCheckT uni fun cfg m ()
forall a b. (a -> b) -> a -> b
$ \(Term TyName Name uni fun ann
c, [Type TyName uni ()]
argTypes) ->
ann
-> Term TyName Name uni fun ann
-> Normalized (Type TyName uni ())
-> TypeCheckT uni fun cfg m ()
forall err (uni :: * -> *) fun ann (m :: * -> *) cfg.
(MonadTypeCheckPlc err uni fun ann m,
HasTypeCheckConfig cfg uni fun) =>
ann
-> Term TyName Name uni fun ann
-> Normalized (Type TyName uni ())
-> TypeCheckT uni fun cfg m ()
checkTypeM ann
ann Term TyName Name uni fun ann
c (Type TyName uni () -> Normalized (Type TyName uni ())
forall a. a -> Normalized a
Normalized (Type TyName uni () -> Normalized (Type TyName uni ()))
-> Type TyName uni () -> 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
mkIterTyFun () [Type TyName uni ()]
argTypes (Normalized (Type TyName uni ()) -> Type TyName uni ()
forall a. Normalized a -> a
unNormalized Normalized (Type TyName uni ())
vResTy))
Maybe [(Term TyName Name uni fun ann, [Type TyName uni ()])]
Nothing -> AReview err (TypeError (Term TyName Name uni fun ()) uni fun ann)
-> TypeError (Term TyName Name uni fun ()) uni fun ann
-> TypeCheckT uni fun cfg m ()
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)
Prism' err (TypeError (Term TyName Name uni fun ()) uni fun ann)
_TypeError (ann
-> Term TyName Name uni fun ()
-> ExpectedShapeOr (Type TyName uni ())
-> Normalized (Type TyName uni ())
-> TypeError (Term TyName Name uni fun ()) uni fun ann
forall term (uni :: * -> *) fun ann.
ann
-> term
-> ExpectedShapeOr (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
scrut) ExpectedShapeOr (Type TyName uni ())
forall {a}. ExpectedShapeOr a
expectedSop Normalized (Type TyName uni ())
vScrutTy)
Type TyName uni ()
_ -> AReview err (TypeError (Term TyName Name uni fun ()) uni fun ann)
-> TypeError (Term TyName Name uni fun ()) uni fun ann
-> TypeCheckT uni fun cfg m ()
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)
Prism' err (TypeError (Term TyName Name uni fun ()) uni fun ann)
_TypeError (ann
-> Term TyName Name uni fun ()
-> ExpectedShapeOr (Type TyName uni ())
-> Normalized (Type TyName uni ())
-> TypeError (Term TyName Name uni fun ()) uni fun ann
forall term (uni :: * -> *) fun ann.
ann
-> term
-> ExpectedShapeOr (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
scrut) ExpectedShapeOr (Type TyName uni ())
forall {a}. ExpectedShapeOr a
expectedSop Normalized (Type TyName uni ())
vScrutTy)
Normalized (Type TyName uni ())
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ()))
forall a. a -> ReaderT (TypeCheckEnv uni fun cfg) m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Normalized (Type TyName uni ())
vResTy
checkTypeM
:: (MonadTypeCheckPlc err uni fun ann m, HasTypeCheckConfig cfg uni fun)
=> ann
-> Term TyName Name uni fun ann
-> Normalized (Type TyName uni ())
-> TypeCheckT uni fun cfg m ()
checkTypeM :: forall err (uni :: * -> *) fun ann (m :: * -> *) cfg.
(MonadTypeCheckPlc err uni fun ann m,
HasTypeCheckConfig cfg uni fun) =>
ann
-> Term TyName Name uni fun ann
-> Normalized (Type TyName uni ())
-> TypeCheckT uni fun cfg m ()
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
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ()))
forall err (uni :: * -> *) fun ann (m :: * -> *) cfg.
(MonadTypeCheckPlc err uni fun ann m,
HasTypeCheckConfig cfg uni fun) =>
Term TyName Name uni fun ann
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ()))
inferTypeM Term TyName Name uni fun ann
term
Bool -> TypeCheckT uni fun cfg m () -> TypeCheckT uni fun cfg m ()
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) (TypeCheckT uni fun cfg m () -> TypeCheckT uni fun cfg m ())
-> TypeCheckT uni fun cfg m () -> TypeCheckT uni fun cfg m ()
forall a b. (a -> b) -> a -> b
$ do
let expectedVTy :: ExpectedShapeOr (Type TyName uni ())
expectedVTy = Type TyName uni () -> ExpectedShapeOr (Type TyName uni ())
forall a. a -> ExpectedShapeOr a
ExpectedExact (Type TyName uni () -> ExpectedShapeOr (Type TyName uni ()))
-> Type TyName uni () -> ExpectedShapeOr (Type TyName uni ())
forall a b. (a -> b) -> a -> b
$ Normalized (Type TyName uni ()) -> Type TyName uni ()
forall a. Normalized a -> a
unNormalized Normalized (Type TyName uni ())
vTy
AReview err (TypeError (Term TyName Name uni fun ()) uni fun ann)
-> TypeError (Term TyName Name uni fun ()) uni fun ann
-> TypeCheckT uni fun cfg m ()
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)
Prism' err (TypeError (Term TyName Name uni fun ()) uni fun ann)
_TypeError (TypeError (Term TyName Name uni fun ()) uni fun ann
-> TypeCheckT uni fun cfg m ())
-> TypeError (Term TyName Name uni fun ()) uni fun ann
-> TypeCheckT uni fun cfg m ()
forall a b. (a -> b) -> a -> b
$ ann
-> Term TyName Name uni fun ()
-> ExpectedShapeOr (Type TyName uni ())
-> Normalized (Type TyName uni ())
-> TypeError (Term TyName Name uni fun ()) uni fun ann
forall term (uni :: * -> *) fun ann.
ann
-> term
-> ExpectedShapeOr (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) ExpectedShapeOr (Type TyName uni ())
expectedVTy Normalized (Type TyName uni ())
vTermTy