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

-- 'makeLenses' produces an unused lens.
{-# OPTIONS_GHC -fno-warn-unused-binds #-}

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

module PlutusCore.TypeCheck.Internal
  -- export all because a lot are used by the pir-typechecker
  where

import PlutusCore.Builtin
import PlutusCore.Core
import PlutusCore.Error
import PlutusCore.MkPlc
import PlutusCore.Name
import PlutusCore.Normalize.Internal qualified as Norm
import PlutusCore.Quote
import PlutusCore.Rename
import PlutusPrelude

import Control.Lens
import Control.Monad.Error.Lens
import Control.Monad.Except
import Control.Monad.Reader
import Data.Array
import Universe

{- Note [Global uniqueness]
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 [Notation]
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 looks like this:

    kindOfBuiltinType
    typeOfBuiltinFunction
-}

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

-- | Mapping from 'Builtin's to their 'Type's.
newtype BuiltinTypes uni fun = BuiltinTypes
    -- We need to kind check types of all built-in functions before proceeding to type checking a
    -- program, so when we do that we don't have any normalized types of built-in functions yet
    -- (as normalization has to be preceded by kind/type checking, which is the very thing that
    -- we are up to). And since both kind and type checking run in the same 'TypeCheckM' monad,
    -- we do need to provide a 'BuiltinTypes' argument, even though we know that at kind checking
    -- time no built-in function can be encountered (as those live at the value level, not the type
    -- one). So we could wrap an empty 'Array' with 'BuiltinTypes' but how to construct an empty
    -- array? This works:
    --
    --     listArray (maxBound, minBound) []
    --
    -- but only when 'maxBound' is not equal to 'minBound' (and both exist). Which sucks.
    --
    -- So we use 'Nothing' to say "no builtins". It's sufficient and doesn't complicate anything.
    { BuiltinTypes uni fun
-> Maybe (Array fun (Dupable (Normalized (Type TyName uni ()))))
unBuiltinTypes :: Maybe (Array fun (Dupable (Normalized (Type TyName uni ()))))
    }

type TyVarKinds = UniqueMap TypeUnique (Kind ())
type VarTypes uni = UniqueMap TermUnique (Dupable (Normalized (Type TyName uni ())))

-- | Configuration of the type checker.
newtype TypeCheckConfig uni fun = TypeCheckConfig
    { TypeCheckConfig uni fun -> BuiltinTypes uni fun
_tccBuiltinTypes :: BuiltinTypes uni fun
    }
makeClassy ''TypeCheckConfig

-- | The environment that the type checker runs in.
data TypeCheckEnv uni fun cfg = TypeCheckEnv
    { TypeCheckEnv uni fun cfg -> cfg
_tceTypeCheckConfig :: cfg
    , TypeCheckEnv uni fun cfg -> TyVarKinds
_tceTyVarKinds      :: TyVarKinds
    , TypeCheckEnv uni fun cfg -> VarTypes uni
_tceVarTypes        :: VarTypes uni
    }
makeLenses ''TypeCheckEnv

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

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


-- | Run a 'TypeCheckM' computation by supplying a 'TypeCheckConfig' to it.
runTypeCheckM :: (MonadError err m, MonadQuote m) => cfg -> TypeCheckM uni fun cfg err a -> m a
runTypeCheckM :: cfg -> TypeCheckM uni fun cfg err a -> m a
runTypeCheckM cfg
config TypeCheckM uni fun cfg err a
a =
    Either err a -> m a
forall e (m :: * -> *) a. MonadError e m => Either e a -> m a
liftEither (Either err a -> m a) -> m (Either err a) -> m a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Quote (Either err a) -> m (Either err a)
forall (m :: * -> *) a. MonadQuote m => Quote a -> m a
liftQuote (ExceptT err Quote a -> Quote (Either err a)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT err Quote a -> Quote (Either err a))
-> ExceptT err Quote a -> Quote (Either err a)
forall a b. (a -> b) -> a -> b
$ TypeCheckM uni fun cfg err a
-> TypeCheckEnv uni fun cfg -> ExceptT err Quote a
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT TypeCheckM uni fun cfg err a
a TypeCheckEnv uni fun cfg
forall (uni :: * -> *) fun. TypeCheckEnv uni fun cfg
env) where
        env :: TypeCheckEnv uni fun cfg
env = cfg -> TyVarKinds -> VarTypes uni -> TypeCheckEnv uni fun cfg
forall (uni :: * -> *) fun cfg.
cfg -> TyVarKinds -> VarTypes uni -> TypeCheckEnv uni fun cfg
TypeCheckEnv cfg
config TyVarKinds
forall a. Monoid a => a
mempty VarTypes uni
forall a. Monoid a => a
mempty

-- | Extend the context of a 'TypeCheckM' computation with a kinded variable.
withTyVar :: TyName -> Kind () -> TypeCheckM uni fun cfg err a -> TypeCheckM uni fun cfg err a
withTyVar :: TyName
-> Kind ()
-> TypeCheckM uni fun cfg err a
-> TypeCheckM uni fun cfg err a
withTyVar TyName
name = (TypeCheckEnv uni fun cfg -> TypeCheckEnv uni fun cfg)
-> TypeCheckM uni fun cfg err a -> TypeCheckM uni fun cfg err a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((TypeCheckEnv uni fun cfg -> TypeCheckEnv uni fun cfg)
 -> TypeCheckM uni fun cfg err a -> TypeCheckM uni fun cfg err a)
-> (Kind ()
    -> TypeCheckEnv uni fun cfg -> TypeCheckEnv uni fun cfg)
-> Kind ()
-> TypeCheckM uni fun cfg err a
-> TypeCheckM uni fun cfg err a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ASetter
  (TypeCheckEnv uni fun cfg)
  (TypeCheckEnv uni fun cfg)
  TyVarKinds
  TyVarKinds
-> (TyVarKinds -> TyVarKinds)
-> TypeCheckEnv uni fun cfg
-> TypeCheckEnv uni fun cfg
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter
  (TypeCheckEnv uni fun cfg)
  (TypeCheckEnv uni fun cfg)
  TyVarKinds
  TyVarKinds
forall (uni :: * -> *) fun cfg fun.
Lens
  (TypeCheckEnv uni fun cfg)
  (TypeCheckEnv uni fun cfg)
  TyVarKinds
  TyVarKinds
tceTyVarKinds ((TyVarKinds -> TyVarKinds)
 -> TypeCheckEnv uni fun cfg -> TypeCheckEnv uni fun cfg)
-> (Kind () -> TyVarKinds -> TyVarKinds)
-> Kind ()
-> TypeCheckEnv uni fun cfg
-> TypeCheckEnv uni fun cfg
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyName -> Kind () -> TyVarKinds -> TyVarKinds
forall name unique a.
HasUnique name unique =>
name -> a -> UniqueMap unique a -> UniqueMap unique a
insertByName TyName
name

-- | Look up the type of a built-in function.
lookupBuiltinM
    :: (AsTypeError err term uni fun ann, HasTypeCheckConfig cfg uni fun, Ix fun)
    => ann -> fun -> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
lookupBuiltinM :: ann
-> fun
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
lookupBuiltinM ann
ann fun
fun = do
    BuiltinTypes Maybe (Array fun (Dupable (Normalized (Type TyName uni ()))))
mayArr <- Getting
  (BuiltinTypes uni fun)
  (TypeCheckEnv uni fun cfg)
  (BuiltinTypes uni fun)
-> ReaderT
     (TypeCheckEnv uni fun cfg)
     (ExceptT err Quote)
     (BuiltinTypes uni fun)
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view (Getting
   (BuiltinTypes uni fun)
   (TypeCheckEnv uni fun cfg)
   (BuiltinTypes uni fun)
 -> ReaderT
      (TypeCheckEnv uni fun cfg)
      (ExceptT err Quote)
      (BuiltinTypes uni fun))
-> Getting
     (BuiltinTypes uni fun)
     (TypeCheckEnv uni fun cfg)
     (BuiltinTypes uni fun)
-> ReaderT
     (TypeCheckEnv uni fun cfg)
     (ExceptT err Quote)
     (BuiltinTypes uni fun)
forall a b. (a -> b) -> a -> b
$ (cfg -> Const (BuiltinTypes uni fun) cfg)
-> TypeCheckEnv uni fun cfg
-> Const (BuiltinTypes uni fun) (TypeCheckEnv uni fun cfg)
forall (uni :: * -> *) fun cfg fun cfg.
Lens (TypeCheckEnv uni fun cfg) (TypeCheckEnv uni fun cfg) cfg cfg
tceTypeCheckConfig ((cfg -> Const (BuiltinTypes uni fun) cfg)
 -> TypeCheckEnv uni fun cfg
 -> Const (BuiltinTypes uni fun) (TypeCheckEnv uni fun cfg))
-> ((BuiltinTypes uni fun
     -> Const (BuiltinTypes uni fun) (BuiltinTypes uni fun))
    -> cfg -> Const (BuiltinTypes uni fun) cfg)
-> Getting
     (BuiltinTypes uni fun)
     (TypeCheckEnv uni fun cfg)
     (BuiltinTypes uni fun)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (BuiltinTypes uni fun
 -> Const (BuiltinTypes uni fun) (BuiltinTypes uni fun))
-> cfg -> Const (BuiltinTypes uni fun) cfg
forall c (uni :: * -> *) fun.
HasTypeCheckConfig c uni fun =>
Lens' c (BuiltinTypes uni fun)
tccBuiltinTypes
    case Maybe (Array fun (Dupable (Normalized (Type TyName uni ()))))
mayArr Maybe (Array fun (Dupable (Normalized (Type TyName uni ()))))
-> (Array fun (Dupable (Normalized (Type TyName uni ())))
    -> Maybe (Dupable (Normalized (Type TyName uni ()))))
-> Maybe (Dupable (Normalized (Type TyName uni ())))
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Getting
  (First (Dupable (Normalized (Type TyName uni ()))))
  (Array fun (Dupable (Normalized (Type TyName uni ()))))
  (Dupable (Normalized (Type TyName uni ())))
-> Array fun (Dupable (Normalized (Type TyName uni ())))
-> Maybe (Dupable (Normalized (Type TyName uni ())))
forall s (m :: * -> *) a.
MonadReader s m =>
Getting (First a) s a -> m (Maybe a)
preview (Index (Array fun (Dupable (Normalized (Type TyName uni ()))))
-> Traversal'
     (Array fun (Dupable (Normalized (Type TyName uni ()))))
     (IxValue (Array fun (Dupable (Normalized (Type TyName uni ())))))
forall m. Ixed m => Index m -> Traversal' m (IxValue m)
ix fun
Index (Array fun (Dupable (Normalized (Type TyName uni ()))))
fun) of
        Maybe (Dupable (Normalized (Type TyName uni ())))
Nothing -> AReview err (TypeError term uni fun ann)
-> TypeError term uni fun ann
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall e (m :: * -> *) t x.
MonadError e m =>
AReview e t -> t -> m x
throwing AReview err (TypeError term uni fun ann)
forall r term (uni :: * -> *) fun ann.
AsTypeError r term uni fun ann =>
Prism' r (TypeError term uni fun ann)
_TypeError (TypeError term uni fun ann
 -> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ())))
-> TypeError term uni fun ann
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall a b. (a -> b) -> a -> b
$ ann -> fun -> TypeError term uni fun ann
forall term (uni :: * -> *) fun ann.
ann -> fun -> TypeError term uni fun ann
UnknownBuiltinFunctionE ann
ann fun
fun
        Just Dupable (Normalized (Type TyName uni ()))
ty -> Dupable (Normalized (Type TyName uni ()))
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall (m :: * -> *) a.
(MonadQuote m, Rename a) =>
Dupable a -> m a
liftDupable Dupable (Normalized (Type TyName uni ()))
ty

-- | Extend the context of a 'TypeCheckM' computation with a typed variable.
withVar :: Name -> Normalized (Type TyName uni ()) -> TypeCheckM uni fun cfg err a -> TypeCheckM uni fun cfg err a
withVar :: Name
-> Normalized (Type TyName uni ())
-> TypeCheckM uni fun cfg err a
-> TypeCheckM uni fun cfg err a
withVar Name
name = (TypeCheckEnv uni fun cfg -> TypeCheckEnv uni fun cfg)
-> TypeCheckM uni fun cfg err a -> TypeCheckM uni fun cfg err a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((TypeCheckEnv uni fun cfg -> TypeCheckEnv uni fun cfg)
 -> TypeCheckM uni fun cfg err a -> TypeCheckM uni fun cfg err a)
-> (Normalized (Type TyName uni ())
    -> TypeCheckEnv uni fun cfg -> TypeCheckEnv uni fun cfg)
-> Normalized (Type TyName uni ())
-> TypeCheckM uni fun cfg err a
-> TypeCheckM uni fun cfg err a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ASetter
  (TypeCheckEnv uni fun cfg)
  (TypeCheckEnv uni fun cfg)
  (VarTypes uni)
  (VarTypes uni)
-> (VarTypes uni -> VarTypes uni)
-> TypeCheckEnv uni fun cfg
-> TypeCheckEnv uni fun cfg
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter
  (TypeCheckEnv uni fun cfg)
  (TypeCheckEnv uni fun cfg)
  (VarTypes uni)
  (VarTypes uni)
forall (uni :: * -> *) fun cfg (uni :: * -> *) fun.
Lens
  (TypeCheckEnv uni fun cfg)
  (TypeCheckEnv uni fun cfg)
  (VarTypes uni)
  (VarTypes uni)
tceVarTypes ((VarTypes uni -> VarTypes uni)
 -> TypeCheckEnv uni fun cfg -> TypeCheckEnv uni fun cfg)
-> (Normalized (Type TyName uni ())
    -> VarTypes uni -> VarTypes uni)
-> Normalized (Type TyName uni ())
-> TypeCheckEnv uni fun cfg
-> TypeCheckEnv uni fun cfg
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name
-> Dupable (Normalized (Type TyName uni ()))
-> VarTypes uni
-> VarTypes uni
forall name unique a.
HasUnique name unique =>
name -> a -> UniqueMap unique a -> UniqueMap unique a
insertByName Name
name (Dupable (Normalized (Type TyName uni ()))
 -> VarTypes uni -> VarTypes uni)
-> (Normalized (Type TyName uni ())
    -> Dupable (Normalized (Type TyName uni ())))
-> Normalized (Type TyName uni ())
-> VarTypes uni
-> VarTypes uni
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Normalized (Type TyName uni ())
-> Dupable (Normalized (Type TyName uni ()))
forall (f :: * -> *) a. Applicative f => a -> f a
pure

-- | Look up a type variable in the current context.
lookupTyVarM
    :: (AsTypeError err term uni fun ann)
    => ann -> TyName -> TypeCheckM uni fun cfg err (Kind ())
lookupTyVarM :: ann -> TyName -> TypeCheckM uni fun cfg err (Kind ())
lookupTyVarM ann
ann TyName
name = do
    Maybe (Kind ())
mayKind <- (TypeCheckEnv uni fun cfg -> Maybe (Kind ()))
-> ReaderT
     (TypeCheckEnv uni fun cfg) (ExceptT err Quote) (Maybe (Kind ()))
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ((TypeCheckEnv uni fun cfg -> Maybe (Kind ()))
 -> ReaderT
      (TypeCheckEnv uni fun cfg) (ExceptT err Quote) (Maybe (Kind ())))
-> (TypeCheckEnv uni fun cfg -> Maybe (Kind ()))
-> ReaderT
     (TypeCheckEnv uni fun cfg) (ExceptT err Quote) (Maybe (Kind ()))
forall a b. (a -> b) -> a -> b
$ TyName -> TyVarKinds -> Maybe (Kind ())
forall name unique a.
HasUnique name unique =>
name -> UniqueMap unique a -> Maybe a
lookupName TyName
name (TyVarKinds -> Maybe (Kind ()))
-> (TypeCheckEnv uni fun cfg -> TyVarKinds)
-> TypeCheckEnv uni fun cfg
-> Maybe (Kind ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeCheckEnv uni fun cfg -> TyVarKinds
forall (uni :: * -> *) fun cfg.
TypeCheckEnv uni fun cfg -> TyVarKinds
_tceTyVarKinds
    case Maybe (Kind ())
mayKind of
        Maybe (Kind ())
Nothing   -> AReview err (TypeError term uni fun ann)
-> TypeError term uni fun ann
-> TypeCheckM uni fun cfg err (Kind ())
forall e (m :: * -> *) t x.
MonadError e m =>
AReview e t -> t -> m x
throwing AReview err (TypeError term uni fun ann)
forall r term (uni :: * -> *) fun ann.
AsTypeError r term uni fun ann =>
Prism' r (TypeError term uni fun ann)
_TypeError (TypeError term uni fun ann
 -> TypeCheckM uni fun cfg err (Kind ()))
-> TypeError term uni fun ann
-> TypeCheckM uni fun cfg err (Kind ())
forall a b. (a -> b) -> a -> b
$ ann -> TyName -> TypeError term uni fun ann
forall term (uni :: * -> *) fun ann.
ann -> TyName -> TypeError term uni fun ann
FreeTypeVariableE ann
ann TyName
name
        Just Kind ()
kind -> Kind () -> TypeCheckM uni fun cfg err (Kind ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure Kind ()
kind

-- | Look up a term variable in the current context.
lookupVarM
    :: AsTypeError err term uni fun ann
    => ann -> Name -> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
lookupVarM :: ann
-> Name
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
lookupVarM ann
ann Name
name = do
    Maybe (Dupable (Normalized (Type TyName uni ())))
mayTy <- (TypeCheckEnv uni fun cfg
 -> Maybe (Dupable (Normalized (Type TyName uni ()))))
-> ReaderT
     (TypeCheckEnv uni fun cfg)
     (ExceptT err Quote)
     (Maybe (Dupable (Normalized (Type TyName uni ()))))
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ((TypeCheckEnv uni fun cfg
  -> Maybe (Dupable (Normalized (Type TyName uni ()))))
 -> ReaderT
      (TypeCheckEnv uni fun cfg)
      (ExceptT err Quote)
      (Maybe (Dupable (Normalized (Type TyName uni ())))))
-> (TypeCheckEnv uni fun cfg
    -> Maybe (Dupable (Normalized (Type TyName uni ()))))
-> ReaderT
     (TypeCheckEnv uni fun cfg)
     (ExceptT err Quote)
     (Maybe (Dupable (Normalized (Type TyName uni ()))))
forall a b. (a -> b) -> a -> b
$ Name
-> UniqueMap TermUnique (Dupable (Normalized (Type TyName uni ())))
-> Maybe (Dupable (Normalized (Type TyName uni ())))
forall name unique a.
HasUnique name unique =>
name -> UniqueMap unique a -> Maybe a
lookupName Name
name (UniqueMap TermUnique (Dupable (Normalized (Type TyName uni ())))
 -> Maybe (Dupable (Normalized (Type TyName uni ()))))
-> (TypeCheckEnv uni fun cfg
    -> UniqueMap
         TermUnique (Dupable (Normalized (Type TyName uni ()))))
-> TypeCheckEnv uni fun cfg
-> Maybe (Dupable (Normalized (Type TyName uni ())))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeCheckEnv uni fun cfg
-> UniqueMap TermUnique (Dupable (Normalized (Type TyName uni ())))
forall (uni :: * -> *) fun cfg.
TypeCheckEnv uni fun cfg -> VarTypes uni
_tceVarTypes
    case Maybe (Dupable (Normalized (Type TyName uni ())))
mayTy of
        Maybe (Dupable (Normalized (Type TyName uni ())))
Nothing -> AReview err (TypeError term uni fun ann)
-> TypeError term uni fun ann
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall e (m :: * -> *) t x.
MonadError e m =>
AReview e t -> t -> m x
throwing AReview err (TypeError term uni fun ann)
forall r term (uni :: * -> *) fun ann.
AsTypeError r term uni fun ann =>
Prism' r (TypeError term uni fun ann)
_TypeError (TypeError term uni fun ann
 -> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ())))
-> TypeError term uni fun ann
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall a b. (a -> b) -> a -> b
$ ann -> Name -> TypeError term uni fun ann
forall term (uni :: * -> *) fun ann.
ann -> Name -> TypeError term uni fun ann
FreeVariableE ann
ann Name
name
        Just Dupable (Normalized (Type TyName uni ()))
ty -> Dupable (Normalized (Type TyName uni ()))
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall (m :: * -> *) a.
(MonadQuote m, Rename a) =>
Dupable a -> m a
liftDupable Dupable (Normalized (Type TyName uni ()))
ty

-- #############
-- ## Dummies ##
-- #############

dummyUnique :: Unique
dummyUnique :: Unique
dummyUnique = Int -> Unique
Unique Int
0

dummyTyName :: TyName
dummyTyName :: TyName
dummyTyName = Name -> TyName
TyName (Text -> Unique -> Name
Name Text
"*" Unique
dummyUnique)

dummyKind :: Kind ()
dummyKind :: Kind ()
dummyKind = () -> Kind ()
forall ann. ann -> Kind ann
Type ()

dummyType :: Type TyName uni ()
dummyType :: Type TyName uni ()
dummyType = () -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
dummyTyName

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

-- | Normalize a 'Type'.
normalizeTypeM
    :: HasUniApply uni
    => Type TyName uni ann
    -> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ann))
normalizeTypeM :: Type TyName uni ann
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ann))
normalizeTypeM Type TyName uni ann
ty = NormalizeTypeT
  (ReaderT (TypeCheckEnv uni fun cfg) (ExceptT err Quote))
  TyName
  uni
  ann
  (Normalized (Type TyName uni ann))
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ann))
forall (m :: * -> *) tyname (uni :: * -> *) ann a.
NormalizeTypeT m tyname uni ann a -> m a
Norm.runNormalizeTypeM (NormalizeTypeT
   (ReaderT (TypeCheckEnv uni fun cfg) (ExceptT err Quote))
   TyName
   uni
   ann
   (Normalized (Type TyName uni ann))
 -> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ann)))
-> NormalizeTypeT
     (ReaderT (TypeCheckEnv uni fun cfg) (ExceptT err Quote))
     TyName
     uni
     ann
     (Normalized (Type TyName uni ann))
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ann))
forall a b. (a -> b) -> a -> b
$ Type TyName uni ann
-> NormalizeTypeT
     (ReaderT (TypeCheckEnv uni fun cfg) (ExceptT err Quote))
     TyName
     uni
     ann
     (Normalized (Type TyName uni ann))
forall tyname (m :: * -> *) (uni :: * -> *) ann.
(HasUnique tyname TypeUnique, MonadQuote m, HasUniApply uni) =>
Type tyname uni ann
-> NormalizeTypeT
     m tyname uni ann (Normalized (Type tyname uni ann))
Norm.normalizeTypeM Type TyName uni ann
ty

-- | Substitute a type for a variable in a type and normalize the result.
substNormalizeTypeM
    :: HasUniApply uni
    => Normalized (Type TyName uni ())  -- ^ @ty@
    -> TyName                           -- ^ @name@
    -> Type TyName uni ()               -- ^ @body@
    -> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
substNormalizeTypeM :: Normalized (Type TyName uni ())
-> TyName
-> Type TyName uni ()
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
substNormalizeTypeM Normalized (Type TyName uni ())
ty TyName
name Type TyName uni ()
body = NormalizeTypeT
  (ReaderT (TypeCheckEnv uni fun cfg) (ExceptT err Quote))
  TyName
  uni
  ()
  (Normalized (Type TyName uni ()))
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall (m :: * -> *) tyname (uni :: * -> *) ann a.
NormalizeTypeT m tyname uni ann a -> m a
Norm.runNormalizeTypeM (NormalizeTypeT
   (ReaderT (TypeCheckEnv uni fun cfg) (ExceptT err Quote))
   TyName
   uni
   ()
   (Normalized (Type TyName uni ()))
 -> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ())))
-> NormalizeTypeT
     (ReaderT (TypeCheckEnv uni fun cfg) (ExceptT err Quote))
     TyName
     uni
     ()
     (Normalized (Type TyName uni ()))
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall a b. (a -> b) -> a -> b
$ Normalized (Type TyName uni ())
-> TyName
-> Type TyName uni ()
-> NormalizeTypeT
     (ReaderT (TypeCheckEnv uni fun cfg) (ExceptT err Quote))
     TyName
     uni
     ()
     (Normalized (Type TyName uni ()))
forall tyname (m :: * -> *) (uni :: * -> *) ann.
(HasUnique tyname TypeUnique, MonadQuote m, HasUniApply uni) =>
Normalized (Type tyname uni ann)
-> tyname
-> Type tyname uni ann
-> NormalizeTypeT
     m tyname uni ann (Normalized (Type tyname uni ann))
Norm.substNormalizeTypeM Normalized (Type TyName uni ())
ty TyName
name Type TyName uni ()
body

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

-- | Infer the kind of a type.
inferKindM
    :: (AsTypeError err term uni fun ann, ToKind uni)
    => Type TyName uni ann -> TypeCheckM uni fun cfg err (Kind ())

-- b :: k
-- ------------------------
-- [infer| G !- con b :: k]
inferKindM :: Type TyName uni ann -> TypeCheckM uni fun cfg err (Kind ())
inferKindM (TyBuiltin ann
_ (SomeTypeIn uni (Esc a)
uni)) =
    Kind () -> TypeCheckM uni fun cfg err (Kind ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Kind () -> TypeCheckM uni fun cfg err (Kind ()))
-> Kind () -> TypeCheckM uni fun cfg err (Kind ())
forall a b. (a -> b) -> a -> b
$ uni (Esc a) -> Kind ()
forall k (uni :: * -> *) (a :: k).
ToKind uni =>
uni (Esc a) -> Kind ()
kindOfBuiltinType uni (Esc a)
uni

-- [infer| G !- v :: k]
-- ------------------------
-- [infer| G !- var v :: k]
inferKindM (TyVar ann
ann TyName
v)           =
    ann -> TyName -> TypeCheckM uni fun cfg err (Kind ())
forall err term (uni :: * -> *) fun ann cfg.
AsTypeError err term uni fun ann =>
ann -> TyName -> TypeCheckM uni fun cfg err (Kind ())
lookupTyVarM ann
ann TyName
v

-- [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 ()
-> TypeCheckM uni fun cfg err (Kind ())
-> TypeCheckM uni fun cfg err (Kind ())
forall (uni :: * -> *) fun cfg err a.
TyName
-> Kind ()
-> TypeCheckM uni fun cfg err a
-> TypeCheckM uni fun cfg err a
withTyVar TyName
n Kind ()
dom_ (TypeCheckM uni fun cfg err (Kind ())
 -> TypeCheckM uni fun cfg err (Kind ()))
-> TypeCheckM uni fun cfg err (Kind ())
-> TypeCheckM uni fun cfg err (Kind ())
forall a b. (a -> b) -> a -> b
$ () -> Kind () -> Kind () -> Kind ()
forall ann. ann -> Kind ann -> Kind ann -> Kind ann
KindArrow () Kind ()
dom_ (Kind () -> Kind ())
-> TypeCheckM uni fun cfg err (Kind ())
-> TypeCheckM uni fun cfg err (Kind ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type TyName uni ann -> TypeCheckM uni fun cfg err (Kind ())
forall err term (uni :: * -> *) fun ann cfg.
(AsTypeError err term uni fun ann, ToKind uni) =>
Type TyName uni ann -> TypeCheckM uni fun cfg err (Kind ())
inferKindM Type TyName uni ann
body

-- [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 -> TypeCheckM uni fun cfg err (Kind ())
forall err term (uni :: * -> *) fun ann cfg.
(AsTypeError err term uni fun ann, ToKind uni) =>
Type TyName uni ann -> TypeCheckM uni fun cfg err (Kind ())
inferKindM Type TyName uni ann
fun
    case Kind ()
funKind of
        KindArrow ()
_ Kind ()
dom Kind ()
cod -> do
            ann
-> Type TyName uni ann -> Kind () -> TypeCheckM uni fun cfg err ()
forall err term (uni :: * -> *) fun ann cfg.
(AsTypeError err term uni fun ann, ToKind uni) =>
ann
-> Type TyName uni ann -> Kind () -> TypeCheckM uni fun cfg err ()
checkKindM ann
ann Type TyName uni ann
arg Kind ()
dom
            Kind () -> TypeCheckM uni fun cfg err (Kind ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure Kind ()
cod
        Kind ()
_ -> AReview err (TypeError term uni fun ann)
-> TypeError term uni fun ann
-> TypeCheckM uni fun cfg err (Kind ())
forall e (m :: * -> *) t x.
MonadError e m =>
AReview e t -> t -> m x
throwing AReview err (TypeError term uni fun ann)
forall r term (uni :: * -> *) fun ann.
AsTypeError r term uni fun ann =>
Prism' r (TypeError term uni fun ann)
_TypeError (TypeError term uni fun ann
 -> TypeCheckM uni fun cfg err (Kind ()))
-> TypeError term uni fun ann
-> TypeCheckM uni fun cfg err (Kind ())
forall a b. (a -> b) -> a -> b
$ ann
-> Type TyName uni ()
-> Kind ()
-> Kind ()
-> TypeError term uni fun ann
forall term (uni :: * -> *) fun ann.
ann
-> Type TyName uni ()
-> Kind ()
-> Kind ()
-> TypeError term uni fun ann
KindMismatch ann
ann (Type TyName uni ann -> Type TyName uni ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Type TyName uni ann
fun) (() -> Kind () -> Kind () -> Kind ()
forall ann. ann -> Kind ann -> Kind ann -> Kind ann
KindArrow () Kind ()
dummyKind Kind ()
dummyKind) Kind ()
funKind

-- [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 () -> TypeCheckM uni fun cfg err ()
forall err term (uni :: * -> *) fun ann cfg.
(AsTypeError err term uni fun ann, ToKind uni) =>
ann
-> Type TyName uni ann -> Kind () -> TypeCheckM uni fun cfg err ()
checkKindM ann
ann Type TyName uni ann
dom (Kind () -> TypeCheckM uni fun cfg err ())
-> Kind () -> TypeCheckM uni fun cfg err ()
forall a b. (a -> b) -> a -> b
$ () -> Kind ()
forall ann. ann -> Kind ann
Type ()
    ann
-> Type TyName uni ann -> Kind () -> TypeCheckM uni fun cfg err ()
forall err term (uni :: * -> *) fun ann cfg.
(AsTypeError err term uni fun ann, ToKind uni) =>
ann
-> Type TyName uni ann -> Kind () -> TypeCheckM uni fun cfg err ()
checkKindM ann
ann Type TyName uni ann
cod (Kind () -> TypeCheckM uni fun cfg err ())
-> Kind () -> TypeCheckM uni fun cfg err ()
forall a b. (a -> b) -> a -> b
$ () -> Kind ()
forall ann. ann -> Kind ann
Type ()
    Kind () -> TypeCheckM uni fun cfg err (Kind ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Kind () -> TypeCheckM uni fun cfg err (Kind ()))
-> Kind () -> TypeCheckM uni fun cfg err (Kind ())
forall a b. (a -> b) -> a -> b
$ () -> Kind ()
forall ann. ann -> Kind ann
Type ()

-- [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 ()
-> TypeCheckM uni fun cfg err ()
-> TypeCheckM uni fun cfg err ()
forall (uni :: * -> *) fun cfg err a.
TyName
-> Kind ()
-> TypeCheckM uni fun cfg err a
-> TypeCheckM uni fun cfg err a
withTyVar TyName
n (Kind ann -> Kind ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Kind ann
k) (TypeCheckM uni fun cfg err () -> TypeCheckM uni fun cfg err ())
-> TypeCheckM uni fun cfg err () -> TypeCheckM uni fun cfg err ()
forall a b. (a -> b) -> a -> b
$ ann
-> Type TyName uni ann -> Kind () -> TypeCheckM uni fun cfg err ()
forall err term (uni :: * -> *) fun ann cfg.
(AsTypeError err term uni fun ann, ToKind uni) =>
ann
-> Type TyName uni ann -> Kind () -> TypeCheckM uni fun cfg err ()
checkKindM ann
ann Type TyName uni ann
body (() -> Kind ()
forall ann. ann -> Kind ann
Type ())
    Kind () -> TypeCheckM uni fun cfg err (Kind ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Kind () -> TypeCheckM uni fun cfg err (Kind ()))
-> Kind () -> TypeCheckM uni fun cfg err (Kind ())
forall a b. (a -> b) -> a -> b
$ () -> Kind ()
forall ann. ann -> Kind ann
Type ()

-- [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 -> TypeCheckM uni fun cfg err (Kind ())
forall err term (uni :: * -> *) fun ann cfg.
(AsTypeError err term uni fun ann, ToKind uni) =>
Type TyName uni ann -> TypeCheckM uni fun cfg err (Kind ())
inferKindM Type TyName uni ann
arg
    ann
-> Type TyName uni ann -> Kind () -> TypeCheckM uni fun cfg err ()
forall err term (uni :: * -> *) fun ann cfg.
(AsTypeError err term uni fun ann, ToKind uni) =>
ann
-> Type TyName uni ann -> Kind () -> TypeCheckM uni fun cfg err ()
checkKindOfPatternFunctorM ann
ann Type TyName uni ann
pat Kind ()
k
    Kind () -> TypeCheckM uni fun cfg err (Kind ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Kind () -> TypeCheckM uni fun cfg err (Kind ()))
-> Kind () -> TypeCheckM uni fun cfg err (Kind ())
forall a b. (a -> b) -> a -> b
$ () -> Kind ()
forall ann. ann -> Kind ann
Type ()

-- | Check a 'Type' against a 'Kind'.
checkKindM
    :: (AsTypeError err term uni fun ann, ToKind uni)
    => ann -> Type TyName uni ann -> Kind () -> TypeCheckM uni fun cfg err ()

-- [infer| G !- ty : tyK]    tyK ~ k
-- ---------------------------------
-- [check| G !- ty : k]
checkKindM :: ann
-> Type TyName uni ann -> Kind () -> TypeCheckM uni fun cfg err ()
checkKindM ann
ann Type TyName uni ann
ty Kind ()
k = do
    Kind ()
tyK <- Type TyName uni ann -> TypeCheckM uni fun cfg err (Kind ())
forall err term (uni :: * -> *) fun ann cfg.
(AsTypeError err term uni fun ann, ToKind uni) =>
Type TyName uni ann -> TypeCheckM uni fun cfg err (Kind ())
inferKindM Type TyName uni ann
ty
    Bool
-> TypeCheckM uni fun cfg err () -> TypeCheckM uni fun cfg err ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Kind ()
tyK Kind () -> Kind () -> Bool
forall a. Eq a => a -> a -> Bool
/= Kind ()
k) (TypeCheckM uni fun cfg err () -> TypeCheckM uni fun cfg err ())
-> TypeCheckM uni fun cfg err () -> TypeCheckM uni fun cfg err ()
forall a b. (a -> b) -> a -> b
$ AReview err (TypeError term uni fun ann)
-> TypeError term uni fun ann -> TypeCheckM uni fun cfg err ()
forall e (m :: * -> *) t x.
MonadError e m =>
AReview e t -> t -> m x
throwing AReview err (TypeError term uni fun ann)
forall r term (uni :: * -> *) fun ann.
AsTypeError r term uni fun ann =>
Prism' r (TypeError term uni fun ann)
_TypeError (ann
-> Type TyName uni ()
-> Kind ()
-> Kind ()
-> TypeError term uni fun ann
forall term (uni :: * -> *) fun ann.
ann
-> Type TyName uni ()
-> Kind ()
-> Kind ()
-> TypeError term uni fun ann
KindMismatch ann
ann (Type TyName uni ann -> Type TyName uni ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Type TyName uni ann
ty) Kind ()
k Kind ()
tyK)

-- | Check that the kind of a pattern functor is @(k -> *) -> k -> *@.
checkKindOfPatternFunctorM
    :: (AsTypeError err term uni fun ann, ToKind uni)
    => ann
    -> Type TyName uni ann  -- ^ A pattern functor.
    -> Kind ()              -- ^ @k@.
    -> TypeCheckM uni fun cfg err ()
checkKindOfPatternFunctorM :: ann
-> Type TyName uni ann -> Kind () -> TypeCheckM uni fun cfg err ()
checkKindOfPatternFunctorM ann
ann Type TyName uni ann
pat Kind ()
k =
    ann
-> Type TyName uni ann -> Kind () -> TypeCheckM uni fun cfg err ()
forall err term (uni :: * -> *) fun ann cfg.
(AsTypeError err term uni fun ann, ToKind uni) =>
ann
-> Type TyName uni ann -> Kind () -> TypeCheckM uni fun cfg err ()
checkKindM ann
ann Type TyName uni ann
pat (Kind () -> TypeCheckM uni fun cfg err ())
-> Kind () -> TypeCheckM uni fun cfg err ()
forall a b. (a -> b) -> a -> b
$ () -> Kind () -> Kind () -> Kind ()
forall ann. ann -> Kind ann -> Kind ann -> Kind ann
KindArrow () (() -> Kind () -> Kind () -> Kind ()
forall ann. ann -> Kind ann -> Kind ann -> Kind ann
KindArrow () Kind ()
k (() -> Kind ()
forall ann. ann -> Kind ann
Type ())) (() -> Kind () -> Kind () -> Kind ()
forall ann. ann -> Kind ann -> Kind ann -> Kind ann
KindArrow () Kind ()
k (() -> Kind ()
forall ann. ann -> Kind ann
Type ()))

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

-- | @unfoldIFixOf pat arg k = NORM (vPat (\(a :: k) -> ifix vPat a) arg)@
unfoldIFixOf
    :: HasUniApply uni
    => Normalized (Type TyName uni ())  -- ^ @vPat@
    -> Normalized (Type TyName uni ())  -- ^ @vArg@
    -> Kind ()                          -- ^ @k@
    -> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
unfoldIFixOf :: Normalized (Type TyName uni ())
-> Normalized (Type TyName uni ())
-> Kind ()
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
unfoldIFixOf Normalized (Type TyName uni ())
pat Normalized (Type TyName uni ())
arg Kind ()
k = do
    let vPat :: Type TyName uni ()
vPat = Normalized (Type TyName uni ()) -> Type TyName uni ()
forall a. Normalized a -> a
unNormalized Normalized (Type TyName uni ())
pat
        vArg :: Type TyName uni ()
vArg = Normalized (Type TyName uni ()) -> Type TyName uni ()
forall a. Normalized a -> a
unNormalized Normalized (Type TyName uni ())
arg
    TyName
a <- Quote TyName
-> ReaderT (TypeCheckEnv uni fun cfg) (ExceptT err Quote) TyName
forall (m :: * -> *) a. MonadQuote m => Quote a -> m a
liftQuote (Quote TyName
 -> ReaderT (TypeCheckEnv uni fun cfg) (ExceptT err Quote) TyName)
-> Quote TyName
-> ReaderT (TypeCheckEnv uni fun cfg) (ExceptT err Quote) TyName
forall a b. (a -> b) -> a -> b
$ Text -> Quote TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"a"
    -- 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/input-output-hk/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) (ExceptT err Quote) (Type TyName uni ())
forall a (m :: * -> *). (Rename a, MonadQuote m) => a -> m a
rename Type TyName uni ()
vPat
    Type TyName uni ()
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall (uni :: * -> *) ann fun cfg err.
HasUniApply uni =>
Type TyName uni ann
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ann))
normalizeTypeM (Type TyName uni ()
 -> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ())))
-> Type TyName uni ()
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall a b. (a -> b) -> a -> b
$
        ()
-> Type TyName uni () -> [Type TyName uni ()] -> Type TyName uni ()
forall ann tyname (uni :: * -> *).
ann
-> Type tyname uni ann
-> [Type tyname uni ann]
-> Type tyname uni ann
mkIterTyApp () Type TyName uni ()
vPat'
            [ () -> TyName -> Kind () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyLam () TyName
a Kind ()
k (Type TyName uni () -> Type TyName uni ())
-> (Type TyName uni () -> Type TyName uni ())
-> Type TyName uni ()
-> Type TyName uni ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyIFix () Type TyName uni ()
vPat (Type TyName uni () -> Type TyName uni ())
-> Type TyName uni () -> Type TyName uni ()
forall a b. (a -> b) -> a -> b
$ () -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a
            , Type TyName uni ()
vArg
            ]

-- See the [Global uniqueness] and [Type rules] notes.
-- | Synthesize the type of a term, returning a normalized type.
inferTypeM
    :: ( AsTypeError err (Term TyName Name uni fun ()) uni fun ann, ToKind uni, HasUniApply uni
       , HasTypeCheckConfig cfg uni fun, GEq uni, Ix fun
       )
    => Term TyName Name uni fun ann -> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))

-- c : vTy
-- -------------------------
-- [infer| G !- con c : vTy]
inferTypeM :: Term TyName Name uni fun ann
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
inferTypeM (Constant ann
_ (Some (ValueOf uni (Esc a)
uni a
_))) =
    -- See Note [Normalization of built-in types].
    Type TyName uni ()
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall (uni :: * -> *) ann fun cfg err.
HasUniApply uni =>
Type TyName uni ann
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ann))
normalizeTypeM (Type TyName uni ()
 -> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ())))
-> Type TyName uni ()
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall a b. (a -> b) -> a -> b
$ () -> uni (Esc a) -> Type TyName uni ()
forall k (a :: k) (uni :: * -> *) tyname ann.
ann -> uni (Esc a) -> Type tyname uni ann
mkTyBuiltinOf () uni (Esc a)
uni

-- [infer| G !- bi : vTy]
-- ------------------------------
-- [infer| G !- builtin bi : vTy]
inferTypeM (Builtin ann
ann fun
fun) =
    ann
-> fun
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall err term (uni :: * -> *) fun ann cfg.
(AsTypeError err term uni fun ann, HasTypeCheckConfig cfg uni fun,
 Ix fun) =>
ann
-> fun
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
lookupBuiltinM ann
ann fun
fun

-- [infer| G !- v : ty]    ty ~> vTy
-- ---------------------------------
-- [infer| G !- var v : vTy]
inferTypeM (Var ann
ann Name
name) =
    ann
-> Name
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall err term (uni :: * -> *) fun ann cfg.
AsTypeError err term uni fun ann =>
ann
-> Name
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
lookupVarM ann
ann Name
name

-- [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 () -> TypeCheckM uni fun cfg err ()
forall err term (uni :: * -> *) fun ann cfg.
(AsTypeError err term uni fun ann, ToKind uni) =>
ann
-> Type TyName uni ann -> Kind () -> TypeCheckM uni fun cfg err ()
checkKindM ann
ann Type TyName uni ann
dom (Kind () -> TypeCheckM uni fun cfg err ())
-> Kind () -> TypeCheckM uni fun cfg err ()
forall a b. (a -> b) -> a -> b
$ () -> Kind ()
forall ann. ann -> Kind ann
Type ()
    Normalized (Type TyName uni ())
vDom <- Type TyName uni ()
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall (uni :: * -> *) ann fun cfg err.
HasUniApply uni =>
Type TyName uni ann
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ann))
normalizeTypeM (Type TyName uni ()
 -> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ())))
-> Type TyName uni ()
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall a b. (a -> b) -> a -> b
$ Type TyName uni ann -> Type TyName uni ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Type TyName uni ann
dom
    ()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () (Type TyName uni () -> Type TyName uni () -> Type TyName uni ())
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
-> ReaderT
     (TypeCheckEnv uni fun cfg)
     (ExceptT err Quote)
     (Normalized (Type TyName uni () -> Type TyName uni ()))
forall (f1 :: * -> *) (f2 :: * -> *) a b.
(Functor f1, Functor f2) =>
(a -> b) -> f1 (f2 a) -> f1 (f2 b)
<<$>> Normalized (Type TyName uni ())
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall (f :: * -> *) a. Applicative f => a -> f a
pure Normalized (Type TyName uni ())
vDom ReaderT
  (TypeCheckEnv uni fun cfg)
  (ExceptT err Quote)
  (Normalized (Type TyName uni () -> Type TyName uni ()))
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall (f1 :: * -> *) (f2 :: * -> *) a b.
(Applicative f1, Applicative f2) =>
f1 (f2 (a -> b)) -> f1 (f2 a) -> f1 (f2 b)
<<*>> Name
-> Normalized (Type TyName uni ())
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall (uni :: * -> *) fun cfg err a.
Name
-> Normalized (Type TyName uni ())
-> TypeCheckM uni fun cfg err a
-> TypeCheckM uni fun cfg err a
withVar Name
n Normalized (Type TyName uni ())
vDom (Term TyName Name uni fun ann
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall err (uni :: * -> *) fun ann cfg.
(AsTypeError err (Term TyName Name uni fun ()) uni fun ann,
 ToKind uni, HasUniApply uni, HasTypeCheckConfig cfg uni fun,
 GEq uni, Ix fun) =>
Term TyName Name uni fun ann
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
inferTypeM Term TyName Name uni fun ann
body)

-- [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 ())
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall (f1 :: * -> *) (f2 :: * -> *) a b.
(Functor f1, Functor f2) =>
(a -> b) -> f1 (f2 a) -> f1 (f2 b)
<<$>> TyName
-> Kind ()
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall (uni :: * -> *) fun cfg err a.
TyName
-> Kind ()
-> TypeCheckM uni fun cfg err a
-> TypeCheckM uni fun cfg err a
withTyVar TyName
n Kind ()
nK_ (Term TyName Name uni fun ann
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall err (uni :: * -> *) fun ann cfg.
(AsTypeError err (Term TyName Name uni fun ()) uni fun ann,
 ToKind uni, HasUniApply uni, HasTypeCheckConfig cfg uni fun,
 GEq uni, Ix fun) =>
Term TyName Name uni fun ann
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
inferTypeM Term TyName Name uni fun ann
body)

-- [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
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall err (uni :: * -> *) fun ann cfg.
(AsTypeError err (Term TyName Name uni fun ()) uni fun ann,
 ToKind uni, HasUniApply uni, HasTypeCheckConfig cfg uni fun,
 GEq uni, Ix fun) =>
Term TyName Name uni fun ann
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
inferTypeM Term TyName Name uni fun ann
fun
    case Normalized (Type TyName uni ()) -> Type TyName uni ()
forall a. Normalized a -> a
unNormalized Normalized (Type TyName uni ())
vFunTy of
        TyFun ()
_ Type TyName uni ()
vDom Type TyName uni ()
vCod -> do
            -- Subparts of a normalized type, so normalized.
            ann
-> Term TyName Name uni fun ann
-> Normalized (Type TyName uni ())
-> TypeCheckM uni fun cfg err ()
forall err (uni :: * -> *) fun ann cfg.
(AsTypeError err (Term TyName Name uni fun ()) uni fun ann,
 ToKind uni, HasUniApply uni, HasTypeCheckConfig cfg uni fun,
 GEq uni, Ix fun) =>
ann
-> Term TyName Name uni fun ann
-> Normalized (Type TyName uni ())
-> TypeCheckM uni fun cfg err ()
checkTypeM ann
ann Term TyName Name uni fun ann
arg (Normalized (Type TyName uni ()) -> TypeCheckM uni fun cfg err ())
-> Normalized (Type TyName uni ()) -> TypeCheckM uni fun cfg err ()
forall a b. (a -> b) -> a -> b
$ Type TyName uni () -> Normalized (Type TyName uni ())
forall a. a -> Normalized a
Normalized Type TyName uni ()
vDom
            Normalized (Type TyName uni ())
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Normalized (Type TyName uni ())
 -> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ())))
-> Normalized (Type TyName uni ())
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall a b. (a -> b) -> a -> b
$ Type TyName uni () -> Normalized (Type TyName uni ())
forall a. a -> Normalized a
Normalized Type TyName uni ()
vCod
        Type TyName uni ()
_ -> AReview err (TypeError (Term TyName Name uni fun ()) uni fun ann)
-> TypeError (Term TyName Name uni fun ()) uni fun ann
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall e (m :: * -> *) t x.
MonadError e m =>
AReview e t -> t -> m x
throwing AReview err (TypeError (Term TyName Name uni fun ()) uni fun ann)
forall r term (uni :: * -> *) fun ann.
AsTypeError r term uni fun ann =>
Prism' r (TypeError term uni fun ann)
_TypeError (ann
-> Term TyName Name uni fun ()
-> Type TyName uni ()
-> Normalized (Type TyName uni ())
-> TypeError (Term TyName Name uni fun ()) uni fun ann
forall term (uni :: * -> *) fun ann.
ann
-> term
-> Type TyName uni ()
-> Normalized (Type TyName uni ())
-> TypeError term uni fun ann
TypeMismatch ann
ann (Term TyName Name uni fun ann -> Term TyName Name uni fun ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Term TyName Name uni fun ann
fun) (()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
dummyType Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
dummyType) Normalized (Type TyName uni ())
vFunTy)

-- [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
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall err (uni :: * -> *) fun ann cfg.
(AsTypeError err (Term TyName Name uni fun ()) uni fun ann,
 ToKind uni, HasUniApply uni, HasTypeCheckConfig cfg uni fun,
 GEq uni, Ix fun) =>
Term TyName Name uni fun ann
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
inferTypeM Term TyName Name uni fun ann
body
    case Normalized (Type TyName uni ()) -> Type TyName uni ()
forall a. Normalized a -> a
unNormalized Normalized (Type TyName uni ())
vBodyTy of
        TyForall ()
_ TyName
n Kind ()
nK Type TyName uni ()
vCod -> do
            ann
-> Type TyName uni ann -> Kind () -> TypeCheckM uni fun cfg err ()
forall err term (uni :: * -> *) fun ann cfg.
(AsTypeError err term uni fun ann, ToKind uni) =>
ann
-> Type TyName uni ann -> Kind () -> TypeCheckM uni fun cfg err ()
checkKindM ann
ann Type TyName uni ann
ty Kind ()
nK
            Normalized (Type TyName uni ())
vTy <- Type TyName uni ()
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall (uni :: * -> *) ann fun cfg err.
HasUniApply uni =>
Type TyName uni ann
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ann))
normalizeTypeM (Type TyName uni ()
 -> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ())))
-> Type TyName uni ()
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall a b. (a -> b) -> a -> b
$ Type TyName uni ann -> Type TyName uni ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Type TyName uni ann
ty
            Normalized (Type TyName uni ())
-> TyName
-> Type TyName uni ()
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall (uni :: * -> *) fun cfg err.
HasUniApply uni =>
Normalized (Type TyName uni ())
-> TyName
-> Type TyName uni ()
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
substNormalizeTypeM Normalized (Type TyName uni ())
vTy TyName
n Type TyName uni ()
vCod
        Type TyName uni ()
_ -> AReview err (TypeError (Term TyName Name uni fun ()) uni fun ann)
-> TypeError (Term TyName Name uni fun ()) uni fun ann
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall e (m :: * -> *) t x.
MonadError e m =>
AReview e t -> t -> m x
throwing AReview err (TypeError (Term TyName Name uni fun ()) uni fun ann)
forall r term (uni :: * -> *) fun ann.
AsTypeError r term uni fun ann =>
Prism' r (TypeError term uni fun ann)
_TypeError (ann
-> Term TyName Name uni fun ()
-> Type TyName uni ()
-> Normalized (Type TyName uni ())
-> TypeError (Term TyName Name uni fun ()) uni fun ann
forall term (uni :: * -> *) fun ann.
ann
-> term
-> Type TyName uni ()
-> Normalized (Type TyName uni ())
-> TypeError term uni fun ann
TypeMismatch ann
ann (Term TyName Name uni fun ann -> Term TyName Name uni fun ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Term TyName Name uni fun ann
body) (() -> TyName -> Kind () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyForall () TyName
dummyTyName Kind ()
dummyKind Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
dummyType) Normalized (Type TyName uni ())
vBodyTy)

-- [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 -> TypeCheckM uni fun cfg err (Kind ())
forall err term (uni :: * -> *) fun ann cfg.
(AsTypeError err term uni fun ann, ToKind uni) =>
Type TyName uni ann -> TypeCheckM uni fun cfg err (Kind ())
inferKindM Type TyName uni ann
arg
    ann
-> Type TyName uni ann -> Kind () -> TypeCheckM uni fun cfg err ()
forall err term (uni :: * -> *) fun ann cfg.
(AsTypeError err term uni fun ann, ToKind uni) =>
ann
-> Type TyName uni ann -> Kind () -> TypeCheckM uni fun cfg err ()
checkKindOfPatternFunctorM ann
ann Type TyName uni ann
pat Kind ()
k
    Normalized (Type TyName uni ())
vPat <- Type TyName uni ()
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall (uni :: * -> *) ann fun cfg err.
HasUniApply uni =>
Type TyName uni ann
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ann))
normalizeTypeM (Type TyName uni ()
 -> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ())))
-> Type TyName uni ()
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall a b. (a -> b) -> a -> b
$ Type TyName uni ann -> Type TyName uni ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Type TyName uni ann
pat
    Normalized (Type TyName uni ())
vArg <- Type TyName uni ()
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall (uni :: * -> *) ann fun cfg err.
HasUniApply uni =>
Type TyName uni ann
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ann))
normalizeTypeM (Type TyName uni ()
 -> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ())))
-> Type TyName uni ()
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall a b. (a -> b) -> a -> b
$ Type TyName uni ann -> Type TyName uni ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Type TyName uni ann
arg
    ann
-> Term TyName Name uni fun ann
-> Normalized (Type TyName uni ())
-> TypeCheckM uni fun cfg err ()
forall err (uni :: * -> *) fun ann cfg.
(AsTypeError err (Term TyName Name uni fun ()) uni fun ann,
 ToKind uni, HasUniApply uni, HasTypeCheckConfig cfg uni fun,
 GEq uni, Ix fun) =>
ann
-> Term TyName Name uni fun ann
-> Normalized (Type TyName uni ())
-> TypeCheckM uni fun cfg err ()
checkTypeM ann
ann Term TyName Name uni fun ann
term (Normalized (Type TyName uni ()) -> TypeCheckM uni fun cfg err ())
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
-> TypeCheckM uni fun cfg err ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Normalized (Type TyName uni ())
-> Normalized (Type TyName uni ())
-> Kind ()
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall (uni :: * -> *) fun cfg err.
HasUniApply uni =>
Normalized (Type TyName uni ())
-> Normalized (Type TyName uni ())
-> Kind ()
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
unfoldIFixOf Normalized (Type TyName uni ())
vPat Normalized (Type TyName uni ())
vArg Kind ()
k
    Normalized (Type TyName uni ())
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Normalized (Type TyName uni ())
 -> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ())))
-> Normalized (Type TyName uni ())
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall a b. (a -> b) -> a -> b
$ ()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyIFix () (Type TyName uni () -> Type TyName uni () -> Type TyName uni ())
-> Normalized (Type TyName uni ())
-> Normalized (Type TyName uni () -> Type TyName uni ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Normalized (Type TyName uni ())
vPat Normalized (Type TyName uni () -> Type TyName uni ())
-> Normalized (Type TyName uni ())
-> Normalized (Type TyName uni ())
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Normalized (Type TyName uni ())
vArg

-- [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
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall err (uni :: * -> *) fun ann cfg.
(AsTypeError err (Term TyName Name uni fun ()) uni fun ann,
 ToKind uni, HasUniApply uni, HasTypeCheckConfig cfg uni fun,
 GEq uni, Ix fun) =>
Term TyName Name uni fun ann
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
inferTypeM Term TyName Name uni fun ann
term
    case Normalized (Type TyName uni ()) -> Type TyName uni ()
forall a. Normalized a -> a
unNormalized Normalized (Type TyName uni ())
vTermTy of
        TyIFix ()
_ Type TyName uni ()
vPat Type TyName uni ()
vArg -> do
            Kind ()
k <- Type TyName uni ann -> TypeCheckM uni fun cfg err (Kind ())
forall err term (uni :: * -> *) fun ann cfg.
(AsTypeError err term uni fun ann, ToKind uni) =>
Type TyName uni ann -> TypeCheckM uni fun cfg err (Kind ())
inferKindM (Type TyName uni ann -> TypeCheckM uni fun cfg err (Kind ()))
-> Type TyName uni ann -> TypeCheckM uni fun cfg err (Kind ())
forall a b. (a -> b) -> a -> b
$ ann
ann ann -> Type TyName uni () -> Type TyName uni ann
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Type TyName uni ()
vArg
            -- Subparts of a normalized type, so normalized.
            Normalized (Type TyName uni ())
-> Normalized (Type TyName uni ())
-> Kind ()
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall (uni :: * -> *) fun cfg err.
HasUniApply uni =>
Normalized (Type TyName uni ())
-> Normalized (Type TyName uni ())
-> Kind ()
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
unfoldIFixOf (Type TyName uni () -> Normalized (Type TyName uni ())
forall a. a -> Normalized a
Normalized Type TyName uni ()
vPat) (Type TyName uni () -> Normalized (Type TyName uni ())
forall a. a -> Normalized a
Normalized Type TyName uni ()
vArg) Kind ()
k
        Type TyName uni ()
_                  -> AReview err (TypeError (Term TyName Name uni fun ()) uni fun ann)
-> TypeError (Term TyName Name uni fun ()) uni fun ann
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall e (m :: * -> *) t x.
MonadError e m =>
AReview e t -> t -> m x
throwing AReview err (TypeError (Term TyName Name uni fun ()) uni fun ann)
forall r term (uni :: * -> *) fun ann.
AsTypeError r term uni fun ann =>
Prism' r (TypeError term uni fun ann)
_TypeError (ann
-> Term TyName Name uni fun ()
-> Type TyName uni ()
-> Normalized (Type TyName uni ())
-> TypeError (Term TyName Name uni fun ()) uni fun ann
forall term (uni :: * -> *) fun ann.
ann
-> term
-> Type TyName uni ()
-> Normalized (Type TyName uni ())
-> TypeError term uni fun ann
TypeMismatch ann
ann (Term TyName Name uni fun ann -> Term TyName Name uni fun ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Term TyName Name uni fun ann
term) (()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyIFix () Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
dummyType Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
dummyType) Normalized (Type TyName uni ())
vTermTy)

-- [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 () -> TypeCheckM uni fun cfg err ()
forall err term (uni :: * -> *) fun ann cfg.
(AsTypeError err term uni fun ann, ToKind uni) =>
ann
-> Type TyName uni ann -> Kind () -> TypeCheckM uni fun cfg err ()
checkKindM ann
ann Type TyName uni ann
ty (Kind () -> TypeCheckM uni fun cfg err ())
-> Kind () -> TypeCheckM uni fun cfg err ()
forall a b. (a -> b) -> a -> b
$ () -> Kind ()
forall ann. ann -> Kind ann
Type ()
    Type TyName uni ()
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall (uni :: * -> *) ann fun cfg err.
HasUniApply uni =>
Type TyName uni ann
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ann))
normalizeTypeM (Type TyName uni ()
 -> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ())))
-> Type TyName uni ()
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall a b. (a -> b) -> a -> b
$ Type TyName uni ann -> Type TyName uni ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Type TyName uni ann
ty

-- See the [Global uniqueness] and [Type rules] notes.
-- | Check a 'Term' against a 'NormalizedType'.
checkTypeM
    :: ( AsTypeError err (Term TyName Name uni fun ()) uni fun ann, ToKind uni, HasUniApply uni
       , HasTypeCheckConfig cfg uni fun, GEq uni, Ix fun
       )
    => ann
    -> Term TyName Name uni fun ann
    -> Normalized (Type TyName uni ())
    -> TypeCheckM uni fun cfg err ()

-- [infer| G !- term : vTermTy]    vTermTy ~ vTy
-- ---------------------------------------------
-- [check| G !- term : vTy]
checkTypeM :: ann
-> Term TyName Name uni fun ann
-> Normalized (Type TyName uni ())
-> TypeCheckM uni fun cfg err ()
checkTypeM ann
ann Term TyName Name uni fun ann
term Normalized (Type TyName uni ())
vTy = do
    Normalized (Type TyName uni ())
vTermTy <- Term TyName Name uni fun ann
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
forall err (uni :: * -> *) fun ann cfg.
(AsTypeError err (Term TyName Name uni fun ()) uni fun ann,
 ToKind uni, HasUniApply uni, HasTypeCheckConfig cfg uni fun,
 GEq uni, Ix fun) =>
Term TyName Name uni fun ann
-> TypeCheckM uni fun cfg err (Normalized (Type TyName uni ()))
inferTypeM Term TyName Name uni fun ann
term
    Bool
-> TypeCheckM uni fun cfg err () -> TypeCheckM uni fun cfg err ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Normalized (Type TyName uni ())
vTermTy Normalized (Type TyName uni ())
-> Normalized (Type TyName uni ()) -> Bool
forall a. Eq a => a -> a -> Bool
/= Normalized (Type TyName uni ())
vTy) (TypeCheckM uni fun cfg err () -> TypeCheckM uni fun cfg err ())
-> TypeCheckM uni fun cfg err () -> TypeCheckM uni fun cfg err ()
forall a b. (a -> b) -> a -> b
$ AReview err (TypeError (Term TyName Name uni fun ()) uni fun ann)
-> TypeError (Term TyName Name uni fun ()) uni fun ann
-> TypeCheckM uni fun cfg err ()
forall e (m :: * -> *) t x.
MonadError e m =>
AReview e t -> t -> m x
throwing AReview err (TypeError (Term TyName Name uni fun ()) uni fun ann)
forall r term (uni :: * -> *) fun ann.
AsTypeError r term uni fun ann =>
Prism' r (TypeError term uni fun ann)
_TypeError (ann
-> Term TyName Name uni fun ()
-> Type TyName uni ()
-> Normalized (Type TyName uni ())
-> TypeError (Term TyName Name uni fun ()) uni fun ann
forall term (uni :: * -> *) fun ann.
ann
-> term
-> Type TyName uni ()
-> Normalized (Type TyName uni ())
-> TypeError term uni fun ann
TypeMismatch ann
ann (Term TyName Name uni fun ann -> Term TyName Name uni fun ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Term TyName Name uni fun ann
term) (Normalized (Type TyName uni ()) -> Type TyName uni ()
forall a. Normalized a -> a
unNormalized Normalized (Type TyName uni ())
vTermTy) Normalized (Type TyName uni ())
vTy)