-- editorconfig-checker-disable-file
-- | The internal module of the type checker that defines the actual algorithms,
-- but not the user-facing API.

{-# LANGUAGE ConstraintKinds        #-}
{-# LANGUAGE FlexibleInstances      #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE OverloadedStrings      #-}
{-# LANGUAGE TemplateHaskell        #-}
{-# LANGUAGE TypeApplications       #-}
{-# LANGUAGE TypeOperators          #-}

{-# LANGUAGE StrictData             #-}

module PlutusCore.TypeCheck.Internal
    ( -- export all because a lot are used by the pir-typechecker
      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)
-- Using @transformers@ rather than @mtl@, because the former doesn't impose the 'Monad' constraint
-- on 'local'.
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))

{- Note [Global uniqueness in the type checker]
WARNING: type inference/checking works under the assumption that the global uniqueness condition
is satisfied. The invariant is not checked, enforced or automatically fulfilled. So you must ensure
that the global uniqueness condition is satisfied before calling 'inferTypeM' or 'checkTypeM'.

The invariant is preserved. In future we will enforce the invariant.
-}

{- Note [Typing rules]
We write type rules in the bidirectional style.

[infer| G !- x : a] -- means that the inferred type of 'x' in the context 'G' is 'a'.
'a' is not necessary a varible, e.g. [infer| G !- fun : dom -> cod] is fine too.
It reads as follows: "infer the type of 'fun' in the context 'G', check that it's functional and
bind the 'dom' variable to the domain and the 'cod' variable to the codomain of this type".

Analogously, [infer| G !- t :: k] means that the inferred kind of 't' in the context 'G' is 'k'.
The [infer| G !- x : a] judgement appears in conclusions in the clauses of the 'inferTypeM'
function.

[check| G !- x : a] -- check that the type of 'x' in the context 'G' is 'a'.
Since Plutus Core is a fully elaborated language, this amounts to inferring the type of 'x' and
checking that it's equal to 'a'.

Analogously, [check| G !- t :: k] means "check that the kind of 't' in the context 'G' is 'k'".
The [check| G !- x : a] judgement appears in the conclusion in the sole clause of
the 'checkTypeM' function.

The equality check is denoted as "a ~ b".

We use unified contexts in rules, i.e. a context can carry type variables as well as term variables.

The "NORM a" notation reads as "normalize 'a'".

The "a ~> b" notations reads as "normalize 'a' to 'b'".

Functions that can fail start with either @infer@ or @check@ prefixes,
functions that cannot fail look like this:

    kindOfBuiltinType
    typeOfBuiltinFunction
-}

-- ######################
-- ## Type definitions ##
-- ######################

-- | Mapping from 'Builtin's to their 'Normalized' 'Type's.
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 ()))))

-- | Decides what to do upon encountering a variable whose name doesn't match the name of the
-- variable with the same unique that is currently in the scope. Consider for example this type:
--
--     \(a_0 :: *) (b_0 :: *) -> a_0
--
-- here @b_0@ shadows @a_0@ and so any variable having the @0@th unique within the body of the
-- lambda references @b_0@, but we have @a_0@ there and so there's a name mismatch. Technically,
-- it's not a type error to have a name mismatch, because uniques are the single source of truth,
-- however a name mismatch is deeply suspicious and is likely to be caused by a bug somewhere.
--
-- We perform the same check for term-level variables too.
data HandleNameMismatches
    = DetectNameMismatches  -- ^ Throw upon encountering such a name.
    | IgnoreNameMismatches  -- ^ Ignore it.
    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)

{- Note [Alignment of kind and type checker configs]
Kind checking is performed as a part of type checking meaning we always need a kind checking config
whenever a type checking one is required. There are three ways we can align the two sorts of config:

1. store them separately and require the caller to provide both
2. put the type checking config into the kind checking config
3. put the kind checking config into the type checking config

1 is straightforward, but makes the caller provide one config for kind checking and two configs for
type checking, which is inconsistent boilerplate and so it's not really a good option.

2 is better: it makes the caller provide only one config: the type checking config stored in the
kind checking config. However that makes the type signatures unwieldy:

    KindCheckConfig (TypeCheckConfig uni fun) => <...>

plus it's kinda weird to put the type checking config inside the kind checking one.

3 is what we choose. It makes the caller only worry about the type checking config when doing type
checking, hence no syntactical or semantical overhead, plus it makes the type signatures symmetric:

    (MonadKindCheck err term uni fun ann m, HasKindCheckConfig cfg) => <...>

vs

    (MonadTypeCheck err term uni fun ann m, HasTypeCheckConfig cfg uni fun) => <...>

This approach does require a bit of boilerplate at the definition site (see 'HasTypeCheckConfig'),
but it's not much and it doesn't proliferate into user space unlike with the other approaches.
-}

-- | Configuration of the kind checker.
newtype KindCheckConfig = KindCheckConfig
    { KindCheckConfig -> HandleNameMismatches
_kccHandleNameMismatches :: HandleNameMismatches
    }
makeClassy ''KindCheckConfig

-- | Configuration of the type checker.
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
    }

-- | We want 'HasKindCheckConfig' to be a superclass of 'HasTypeCheckConfig' for being able to
-- seamlessly call the kind checker from the type checker, hence we're rolling out our own
-- 'makeClassy' here just to add the constraint.
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

-- | The environment that the type checker runs in.
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

-- | The type checking monad that the type checker runs in.
-- In contains a 'TypeCheckEnv' and allows to throw 'TypeError's.
type TypeCheckT uni fun cfg m = ReaderT (TypeCheckEnv uni fun cfg) m

-- | The constraints that are required for kind checking.
type MonadKindCheck err term uni fun ann m =
    ( MonadError err m                  -- Kind/type checking can fail
    , AsTypeError err term uni fun ann  -- with a 'TypeError'.
    , ToKind uni                        -- For getting the kind of a built-in type.
    )

-- | The general constraints that are required for type checking a Plutus AST.
type MonadTypeCheck err term uni fun ann m =
    ( MonadKindCheck err term uni fun ann m  -- Kind checking is run during type checking
                                             -- (this includes the constraint for throwing errors).
    , Norm.MonadNormalizeType uni m          -- Type lambdas open up type computation.
    , GEq uni                                -- For checking equality of built-in types.
    , Ix fun                                 -- For indexing into the precomputed array of types of
                                             -- built-in functions.
    )

-- | The constraints that are required for type checking Plutus Core.
type MonadTypeCheckPlc err uni fun ann m =
    MonadTypeCheck err (Term TyName Name uni fun ()) uni fun ann m

-- #########################
-- ## Auxiliary functions ##
-- #########################

-- | Run a 'TypeCheckM' computation by supplying a 'TypeCheckConfig' to it.
--
-- Used for both type and kind checking, because we need to do kind checking during type checking
-- and so it makes sense to keep a single monad. However type checking requires a 'TypeCheckConfig',
-- while kind checking doesn't, hence we keep the kind checker fully polymorphic over the type of
-- config, so that the kinder checker can be run with an empty config (such as @()@) and access to
-- a 'TypeCheckConfig' is not needed.
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

-- | Extend the context of a 'TypeCheckM' computation with a kinded variable.
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

-- | Look up the type of a built-in function.
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
    -- Believe it or not, but 'Data.Array' doesn't seem to expose any way of indexing into an array
    -- safely.
    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

-- | Extend the context of a 'TypeCheckM' computation with a typed variable.
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

-- | Look up a type variable in the current context.
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

-- | Look up a term variable in the current context.
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

-- ########################
-- ## Type normalization ##
-- ########################

-- | Normalize a 'Type'.
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

-- | Substitute a type for a variable in a type and normalize the result.
substNormalizeTypeM
    :: MonadNormalizeType uni m
    => Normalized (Type TyName uni ())  -- ^ @ty@
    -> TyName                           -- ^ @name@
    -> Type TyName uni ()               -- ^ @body@
    -> 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

-- ###################
-- ## Kind checking ##
-- ###################

-- | Infer the kind of a type.
inferKindM
    :: (MonadKindCheck err term uni fun ann m, HasKindCheckConfig cfg)
    => Type TyName uni ann -> TypeCheckT uni fun cfg m (Kind ())

-- b :: k
-- ------------------------
-- [infer| G !- con b :: k]
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

-- [infer| G !- v :: k]
-- ------------------------
-- [infer| G !- var v :: k]
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

-- [infer| G , n :: dom !- body :: cod]
-- -------------------------------------------------
-- [infer| G !- (\(n :: dom) -> body) :: dom -> cod]
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

-- [infer| G !- fun :: dom -> cod]    [check| G !- arg :: dom]
-- -----------------------------------------------------------
-- [infer| G !- fun arg :: cod]
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

-- [check| G !- a :: *]    [check| G !- b :: *]
-- --------------------------------------------
-- [infer| G !- a -> b :: *]
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 ()

-- [check| G , n :: k !- body :: *]
-- ---------------------------------------
-- [infer| G !- (all (n :: k). body) :: *]
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 ()


-- [infer| G !- arg :: k]    [check| G !- pat :: (k -> *) -> k -> *]
-- -----------------------------------------------------------------
-- [infer| G !- ifix pat arg :: *]
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 ()

-- s_0 = [p_0_0 ... p_0_m]   [check| G !- p_0_0 :: *] ... [check| G !- p_0_m :: *]
-- ...
-- s_n = [p_n_0 ... p_n_m]   [check| G !- p_n_0 :: *] ... [check| G !- p_n_m :: *]
-- -------------------------------------------------------------------------------
-- [infer| G !- sop s_0 ... s_n :: *]
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 ()

-- | Check a 'Type' against a 'Kind'.
checkKindM
    :: (MonadKindCheck err term uni fun ann m, HasKindCheckConfig cfg)
    => ann -> Type TyName uni ann -> Kind () -> TypeCheckT uni fun cfg m ()

-- [infer| G !- ty : tyK]    tyK ~ k
-- ---------------------------------
-- [check| G !- ty : k]
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)

-- ###################
-- ## Type checking ##
-- ###################

-- | @unfoldIFixOf pat arg k = NORM (vPat (\(a :: k) -> ifix vPat a) arg)@
unfoldIFixOf
    :: MonadNormalizeType uni m
    => Normalized (Type TyName uni ())  -- ^ @vPat@
    -> Normalized (Type TyName uni ())  -- ^ @vArg@
    -> Kind ()                          -- ^ @k@
    -> 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"
    -- We need to rename @vPat@, otherwise it would be used twice below, which would break global
    -- uniqueness. Alternatively, we could use 'normalizeType' instead of 'normalizeTypeM' as the
    -- former performs renaming before doing normalization, but renaming the entire type implicitly
    -- would be less efficient than renaming a subpart of the type explicitly.
    --
    -- Note however that breaking global uniqueness here most likely would not result in buggy
    -- behavior, see https://github.com/IntersectMBO/plutus/pull/2219#issuecomment-672815272
    -- But breaking global uniqueness is a bad idea regardless.
    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
            ]

-- See Note [Global uniqueness in the type checker].
-- See Note [Typing rules].
-- | Synthesize the type of a term, returning a normalized type.
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 ()))

-- c : vTy
-- -------------------------
-- [infer| G !- con c : vTy]
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
_))) =
    -- See Note [Normalization of built-in types].
    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

-- [infer| G !- bi : vTy]
-- ------------------------------
-- [infer| G !- builtin bi : vTy]
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

-- [infer| G !- v : ty]    ty ~> vTy
-- ---------------------------------
-- [infer| G !- var v : vTy]
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

-- [check| G !- dom :: *]    dom ~> vDom    [infer| G , n : dom !- body : vCod]
-- ----------------------------------------------------------------------------
-- [infer| G !- lam n dom body : vDom -> vCod]
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)

-- [infer| G , n :: nK !- body : vBodyTy]
-- ---------------------------------------------------
-- [infer| G !- abs n nK body : all (n :: nK) vBodyTy]
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)

-- [infer| G !- fun : vDom -> vCod]    [check| G !- arg : vDom]
-- ------------------------------------------------------------
-- [infer| G !- fun arg : vCod]
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
            -- Subparts of a normalized type, so normalized.
            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)

-- [infer| G !- body : all (n :: nK) vCod]    [check| G !- ty :: tyK]    ty ~> vTy
-- -------------------------------------------------------------------------------
-- [infer| G !- body {ty} : NORM ([vTy / n] vCod)]
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)

-- [infer| G !- arg :: k]    [check| G !- pat :: (k -> *) -> k -> *]    pat ~> vPat    arg ~> vArg
-- [check| G !- term : NORM (vPat (\(a :: k) -> ifix vPat a) vArg)]
-- -----------------------------------------------------------------------------------------------
-- [infer| G !- iwrap pat arg term : ifix vPat vArg]
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

-- [infer| G !- term : ifix vPat vArg]    [infer| G !- vArg :: k]
-- -----------------------------------------------------------------------
-- [infer| G !- unwrap term : NORM (vPat (\(a :: k) -> ifix vPat a) 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
            -- Subparts of a normalized type, so normalized.
            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)

-- [check| G !- ty :: *]    ty ~> vTy
-- ----------------------------------
-- [infer| G !- error ty : vTy]
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

-- resTy ~> vResTy     vResTy = sop s_0 ... s_i ... s_n
-- s_i = [p_i_0 ... p_i_m]   [check| G !- t_0 : p_i_0] ... [check| G !- t_m : p_i_m]
-- ---------------------------------------------------------------------------------
-- [infer| G !- constr resTy i t_0 ... t_m : vResTy]
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

    -- We don't know exactly what to expect, we only know what the i-th sum should look like, so we
    -- assert that we should have some types in the sum up to there, and then the known product type.
    let -- 'toInteger' is necessary, because @i@ is a @Word64@ and therefore @i - 1@ would be
        -- @maxBound :: Word64@ for @i = 0@ if we didn't have 'toInteger'.
        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
                -- pTy is a sub-part of a normalized type, so normalized
                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)
                -- the number of args does not match the number of types in the i'th SOP
                -- alternative
                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)
            -- result type does not contain an i'th sum alternative
            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)
        -- result type is not a SOP type
        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

-- resTy ~> vResTy   [infer| G !- scrut : sop s_0 ... s_n]
-- s_0 = [p_0_0 ... p_0_m]   [check| G !- c_0 : p_0_0 -> ... -> p_0_m -> vResTy]
-- ...
-- s_n = [p_n_0 ... p_n_m]   [check| G !- c_n : p_n_0 -> ... -> p_n_m -> vResTy]
-- -----------------------------------------------------------------------------
-- [infer| G !- case resTy scrut c_0 ... c_n : 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

    -- We don't know exactly what to expect, we only know that it should
    -- be a SOP with the right number of sum alternatives
    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) ->
                -- made of sub-parts of a normalized type, so normalized
                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))
            -- scrutinee does not have a SOP type with the right number of alternatives
            -- for the number of cases
            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)
        -- scrutinee does not have a SOP type at all
        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)

    -- If we got through all that, then every case type is correct, including that
    -- they all result in vResTy, so we can safely conclude that that is the type of the
    -- whole expression.
    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

-- See Note [Global uniqueness in the type checker].
-- See Note [Typing rules].
-- | Check a 'Term' against a 'NormalizedType'.
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 ()

-- [infer| G !- term : vTermTy]    vTermTy ~ vTy
-- ---------------------------------------------
-- [check| G !- term : vTy]
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