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

{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE LambdaCase         #-}
{-# LANGUAGE OverloadedStrings  #-}
{-# LANGUAGE RankNTypes         #-}
{-# LANGUAGE TypeOperators      #-}
module PlutusIR.TypeCheck.Internal
    ( BuiltinTypes (..)
    , TypeCheckConfig (..)
    , TypeCheckM
    , tccBuiltinTypes
    , PirTCConfig (..)
    , AllowEscape (..)
    , inferTypeM
    , checkTypeM
    , runTypeCheckM
    ) where


import Control.Monad.Error.Lens
import Control.Monad.Except
import Control.Monad.Reader
import Data.Foldable
import Data.Ix
import PlutusCore (ToKind, typeAnn)
import PlutusCore.Error as PLC
import PlutusCore.Quote
import PlutusCore.Rename as PLC
import PlutusIR
import PlutusIR.Compiler.Datatype
import PlutusIR.Compiler.Provenance
import PlutusIR.Compiler.Types
import PlutusIR.Error
import PlutusIR.Transform.Rename ()
import PlutusPrelude

-- we mirror inferTypeM, checkTypeM of plc-tc and extend it for plutus-ir terms
import PlutusCore.TypeCheck.Internal hiding (checkTypeM, inferTypeM, runTypeCheckM)
import PlutusIR.MkPir qualified as PIR

import Universe

{- Note [PLC Typechecker code reuse]
For PIR kind-checking, we reuse `checkKindM`, `inferKindM` directly from the PLC typechecker.
For PIR type-checking, we port the `checkTypeM` and `inferTypeM` from PLC typechecker.
The port is a direct copy, except for the modifications of `Term` to `PIR.Term`
and error type signatures and `throwError` to accomodate for the new pir type-errors.
These modifications are currently necesessary since PIR.Term ADT /= PLC.Term ADT.
We then extend this ported `PIR.inferTypeM` with cases for inferring type of LetRec and LetNonRec.

See Note [Notation] of PlutusCore.TypeCheck.Internal for the notation of inference rules, which appear in the comments.
-}

{- Note [PIR vs Paper Syntax Difference]
Link to the paper: <https://hydra.iohk.io/job/Cardano/plutus/linux.papers.unraveling-recursion/latest/download-by-type/doc-pdf/unraveling-recursion>
FIR's syntax requires that the data-constructor is annotated with a *list of its argument types* (domain),
instead of requiring a single valid type T (usually in the form `dataconstr : arg1 -> arg2 ->... argn`)
The codomain is also left out of the syntax and implied to be of the type `[TypeCons tyarg1 tyarg2 ... tyargn]`
(what would be expected for a non-GADT). Finally, the leading "forall type-parameters" are implicit (since they are consider in scope).

PIR's syntax requires that a full (valid) type is written for the data-constructor, using the syntax for types
(the forall type-parameters remains implicit). This means that the codomain has to be be explicitly given in PIR.
To make sure that the PIR-user has written down the expected non-GADT type we do an extra codomainCheck.
This codomainCheck will have to be relaxed if/when PIR introduces GADTs.
More importantly, since the type for the PIR data-constructor can be any syntax-valid type,
the PIR user may have placed inside there a non-normalized type there. Currently, the PIR typechecker will
assume the types of all data-constructors are prior normalized *before* type-checking, otherwise
the PIR typechecking and PIR compilation will fail.
See NOTE [Normalization of data-constructors' types] at PlutusIR.Compiler.Datatype
-}

{- Note [PIR vs Paper Escaping Types Difference]
Link to the paper: <https://hydra.iohk.io/job/Cardano/plutus/linux.papers.unraveling-recursion/latest/download-by-type/doc-pdf/unraveling-recursion>
In FIR paper's Fig.6, T-Let and T-LetRec rules dictate that: Gamma !- inTerm :: * for two reasons:
1. check (locally) that the kind of the in-term's inferred type is indeed *
2. ensure that the inferred type does not escaping its scope (hence Gamma)

This is in general true for the PIR implementation as well, except in the special
case when a Type is inferred for the top-level expression (`program`-level).
In contrast to (2), we allow such a "top-level" type to escape its scope;
the reasoning is that PIR programs with toplevel escaping types would behave correctly when they are translated down to PLC.
Even in the case where we let the type variables escape, (1) must still hold:
the kind of the escaping type should still be star. Unfortunately, in order to check that we'd have to use the variables
which are no longer in scope. So we skip the rule (Gamma !- inTermTopLevel :: *) in case of top-level inferred types.

The implementation has a user-configurable flag to let the typechecker know if the current term under examination
is at the program's "top-level" position, and thus allow its type to escape. The flag is automatically set to no-type-escape
when typechecking inside a let termbind's rhs term.
-}

-- | a shorthand for our pir-specialized tc functions
type PirTCEnv uni fun e a = TypeCheckM uni fun (PirTCConfig uni fun) e a

-- ###########################
-- ## Port of Type checking ##
-- ##########################
--  Taken from `PlutusCore.Typecheck.Internal`

-- See the [Global uniqueness] and [Type rules] notes.
-- | Check a 'Term' against a 'NormalizedType'.
checkTypeM
    :: (GEq uni, Ix fun, AsTypeErrorExt e uni ann, AsTypeError e (Term TyName Name uni fun ()) uni fun ann, ToKind uni, HasUniApply uni)
    => ann -> Term TyName Name uni fun ann -> Normalized (Type TyName uni ()) -> PirTCEnv uni fun e ()
-- [infer| G !- term : vTermTy]    vTermTy ~ vTy
-- ---------------------------------------------
-- [check| G !- term : vTy]
checkTypeM :: ann
-> Term TyName Name uni fun ann
-> Normalized (Type TyName uni ())
-> PirTCEnv uni fun e ()
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
-> PirTCEnv uni fun e (Normalized (Type TyName uni ()))
forall (uni :: * -> *) fun ann e.
(GEq uni, Ix fun,
 AsTypeError e (Term TyName Name uni fun ()) uni fun ann,
 ToKind uni, HasUniApply uni, AsTypeErrorExt e uni ann) =>
Term TyName Name uni fun ann
-> PirTCEnv uni fun e (Normalized (Type TyName uni ()))
inferTypeM Term TyName Name uni fun ann
term
    Bool -> PirTCEnv uni fun e () -> PirTCEnv uni fun e ()
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) (PirTCEnv uni fun e () -> PirTCEnv uni fun e ())
-> PirTCEnv uni fun e () -> PirTCEnv uni fun e ()
forall a b. (a -> b) -> a -> b
$ AReview e (TypeError (Term TyName Name uni fun ()) uni fun ann)
-> TypeError (Term TyName Name uni fun ()) uni fun ann
-> PirTCEnv uni fun e ()
forall e (m :: * -> *) t x.
MonadError e m =>
AReview e t -> t -> m x
throwing AReview e (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)

-- See the [Global uniqueness] and [Type rules] notes.
-- | Synthesize the type of a term, returning a normalized type.
inferTypeM
    :: forall uni fun ann e. (GEq uni, Ix fun, AsTypeError e (Term TyName Name uni fun ()) uni fun ann, ToKind uni, HasUniApply uni, AsTypeErrorExt e uni ann)
    => Term TyName Name uni fun ann -> PirTCEnv uni fun e (Normalized (Type TyName uni ()))
-- c : vTy
-- -------------------------
-- [infer| G !- con c : vTy]
inferTypeM :: Term TyName Name uni fun ann
-> PirTCEnv uni fun e (Normalized (Type TyName uni ()))
inferTypeM (Constant ann
_ (Some (ValueOf uni (Esc a)
uni a
_))) =
    -- See Note [Normalization of built-in types].
    Type TyName uni ()
-> PirTCEnv uni fun e (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 ()
 -> PirTCEnv uni fun e (Normalized (Type TyName uni ())))
-> Type TyName uni ()
-> PirTCEnv uni fun e (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
PIR.mkTyBuiltinOf () uni (Esc a)
uni

-- [infer| G !- bi : vTy]
-- ------------------------------
-- [infer| G !- builtin bi : vTy]
inferTypeM (Builtin ann
ann fun
bn)         =
    ann -> fun -> PirTCEnv uni fun e (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
bn

-- [infer| G !- v : ty]    ty ~> vTy
-- ---------------------------------
-- [infer| G !- var v : vTy]
inferTypeM (Var ann
ann Name
name)           =
    ann -> Name -> PirTCEnv uni fun e (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 (PirTCConfig uni fun) e ()
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 (PirTCConfig uni fun) e ())
-> Kind () -> TypeCheckM uni fun (PirTCConfig uni fun) e ()
forall a b. (a -> b) -> a -> b
$ () -> Kind ()
forall ann. ann -> Kind ann
Type ()
    Normalized (Type TyName uni ())
vDom <- Type TyName uni ()
-> PirTCEnv uni fun e (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 ()
 -> PirTCEnv uni fun e (Normalized (Type TyName uni ())))
-> Type TyName uni ()
-> PirTCEnv uni fun e (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 ())
-> PirTCEnv uni fun e (Normalized (Type TyName uni ()))
-> ReaderT
     (TypeCheckEnv uni fun (PirTCConfig uni fun))
     (ExceptT e 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 ())
-> PirTCEnv uni fun e (Normalized (Type TyName uni ()))
forall (f :: * -> *) a. Applicative f => a -> f a
pure Normalized (Type TyName uni ())
vDom ReaderT
  (TypeCheckEnv uni fun (PirTCConfig uni fun))
  (ExceptT e Quote)
  (Normalized (Type TyName uni () -> Type TyName uni ()))
-> PirTCEnv uni fun e (Normalized (Type TyName uni ()))
-> PirTCEnv uni fun e (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 ())
-> PirTCEnv uni fun e (Normalized (Type TyName uni ()))
-> PirTCEnv uni fun e (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
-> PirTCEnv uni fun e (Normalized (Type TyName uni ()))
forall (uni :: * -> *) fun ann e.
(GEq uni, Ix fun,
 AsTypeError e (Term TyName Name uni fun ()) uni fun ann,
 ToKind uni, HasUniApply uni, AsTypeErrorExt e uni ann) =>
Term TyName Name uni fun ann
-> PirTCEnv uni fun e (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 ())
-> PirTCEnv uni fun e (Normalized (Type TyName uni ()))
-> PirTCEnv uni fun e (Normalized (Type TyName uni ()))
forall (f1 :: * -> *) (f2 :: * -> *) a b.
(Functor f1, Functor f2) =>
(a -> b) -> f1 (f2 a) -> f1 (f2 b)
<<$>> TyName
-> Kind ()
-> PirTCEnv uni fun e (Normalized (Type TyName uni ()))
-> PirTCEnv uni fun e (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
-> PirTCEnv uni fun e (Normalized (Type TyName uni ()))
forall (uni :: * -> *) fun ann e.
(GEq uni, Ix fun,
 AsTypeError e (Term TyName Name uni fun ()) uni fun ann,
 ToKind uni, HasUniApply uni, AsTypeErrorExt e uni ann) =>
Term TyName Name uni fun ann
-> PirTCEnv uni fun e (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
-> PirTCEnv uni fun e (Normalized (Type TyName uni ()))
forall (uni :: * -> *) fun ann e.
(GEq uni, Ix fun,
 AsTypeError e (Term TyName Name uni fun ()) uni fun ann,
 ToKind uni, HasUniApply uni, AsTypeErrorExt e uni ann) =>
Term TyName Name uni fun ann
-> PirTCEnv uni fun e (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 (PirTCConfig uni fun) e ()
forall (uni :: * -> *) fun e ann.
(GEq uni, Ix fun, AsTypeErrorExt e uni ann,
 AsTypeError e (Term TyName Name uni fun ()) uni fun ann,
 ToKind uni, HasUniApply uni) =>
ann
-> Term TyName Name uni fun ann
-> Normalized (Type TyName uni ())
-> PirTCEnv uni fun e ()
checkTypeM ann
ann Term TyName Name uni fun ann
arg (Normalized (Type TyName uni ())
 -> TypeCheckM uni fun (PirTCConfig uni fun) e ())
-> Normalized (Type TyName uni ())
-> TypeCheckM uni fun (PirTCConfig uni fun) e ()
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 ())
-> PirTCEnv uni fun e (Normalized (Type TyName uni ()))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Normalized (Type TyName uni ())
 -> PirTCEnv uni fun e (Normalized (Type TyName uni ())))
-> Normalized (Type TyName uni ())
-> PirTCEnv uni fun e (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 e (TypeError (Term TyName Name uni fun ()) uni fun ann)
-> TypeError (Term TyName Name uni fun ()) uni fun ann
-> PirTCEnv uni fun e (Normalized (Type TyName uni ()))
forall e (m :: * -> *) t x.
MonadError e m =>
AReview e t -> t -> m x
throwing AReview e (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
-> PirTCEnv uni fun e (Normalized (Type TyName uni ()))
forall (uni :: * -> *) fun ann e.
(GEq uni, Ix fun,
 AsTypeError e (Term TyName Name uni fun ()) uni fun ann,
 ToKind uni, HasUniApply uni, AsTypeErrorExt e uni ann) =>
Term TyName Name uni fun ann
-> PirTCEnv uni fun e (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 (PirTCConfig uni fun) e ()
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 ()
-> PirTCEnv uni fun e (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 ()
 -> PirTCEnv uni fun e (Normalized (Type TyName uni ())))
-> Type TyName uni ()
-> PirTCEnv uni fun e (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 ()
-> PirTCEnv uni fun e (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 e (TypeError (Term TyName Name uni fun ()) uni fun ann)
-> TypeError (Term TyName Name uni fun ()) uni fun ann
-> PirTCEnv uni fun e (Normalized (Type TyName uni ()))
forall e (m :: * -> *) t x.
MonadError e m =>
AReview e t -> t -> m x
throwing AReview e (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 (PirTCConfig uni fun) e (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 (PirTCConfig uni fun) e ()
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 ()
-> PirTCEnv uni fun e (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 ()
 -> PirTCEnv uni fun e (Normalized (Type TyName uni ())))
-> Type TyName uni ()
-> PirTCEnv uni fun e (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 ()
-> PirTCEnv uni fun e (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 ()
 -> PirTCEnv uni fun e (Normalized (Type TyName uni ())))
-> Type TyName uni ()
-> PirTCEnv uni fun e (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 (PirTCConfig uni fun) e ()
forall (uni :: * -> *) fun e ann.
(GEq uni, Ix fun, AsTypeErrorExt e uni ann,
 AsTypeError e (Term TyName Name uni fun ()) uni fun ann,
 ToKind uni, HasUniApply uni) =>
ann
-> Term TyName Name uni fun ann
-> Normalized (Type TyName uni ())
-> PirTCEnv uni fun e ()
checkTypeM ann
ann Term TyName Name uni fun ann
term (Normalized (Type TyName uni ())
 -> TypeCheckM uni fun (PirTCConfig uni fun) e ())
-> PirTCEnv uni fun e (Normalized (Type TyName uni ()))
-> TypeCheckM uni fun (PirTCConfig uni fun) e ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Normalized (Type TyName uni ())
-> Normalized (Type TyName uni ())
-> Kind ()
-> PirTCEnv uni fun e (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 ())
-> PirTCEnv uni fun e (Normalized (Type TyName uni ()))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Normalized (Type TyName uni ())
 -> PirTCEnv uni fun e (Normalized (Type TyName uni ())))
-> Normalized (Type TyName uni ())
-> PirTCEnv uni fun e (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
-> PirTCEnv uni fun e (Normalized (Type TyName uni ()))
forall (uni :: * -> *) fun ann e.
(GEq uni, Ix fun,
 AsTypeError e (Term TyName Name uni fun ()) uni fun ann,
 ToKind uni, HasUniApply uni, AsTypeErrorExt e uni ann) =>
Term TyName Name uni fun ann
-> PirTCEnv uni fun e (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 (PirTCConfig uni fun) e (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 (PirTCConfig uni fun) e (Kind ()))
-> Type TyName uni ann
-> TypeCheckM uni fun (PirTCConfig uni fun) e (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 ()
-> PirTCEnv uni fun e (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 e (TypeError (Term TyName Name uni fun ()) uni fun ann)
-> TypeError (Term TyName Name uni fun ()) uni fun ann
-> PirTCEnv uni fun e (Normalized (Type TyName uni ()))
forall e (m :: * -> *) t x.
MonadError e m =>
AReview e t -> t -> m x
throwing AReview e (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 (PirTCConfig uni fun) e ()
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 (PirTCConfig uni fun) e ())
-> Kind () -> TypeCheckM uni fun (PirTCConfig uni fun) e ()
forall a b. (a -> b) -> a -> b
$ () -> Kind ()
forall ann. ann -> Kind ann
Type ()
    Type TyName uni ()
-> PirTCEnv uni fun e (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 ()
 -> PirTCEnv uni fun e (Normalized (Type TyName uni ())))
-> Type TyName uni ()
-> PirTCEnv uni fun e (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
-- ##############
-- ## Port end ##
-- ##############

-- Note on symbols:  '=>' means implies

{-
checkKindFromBinding(G,b) checkTypeFromBinding(G,b)
!null(bs) => [infer| G,withVarsOfBinding(b),withTyVarsOfBinding(b) !- (let nonrec {bs} in inT) : ty]
null(bs) => [infer| G,withVarsOfBinding(b),withTyVarsOfBinding(b) !- inT : ty]
ty ~> vTy
-------------------------------------------------
[infer| G !- (let nonrec {b ; bs} in inT) : vTy]
-}
inferTypeM (Let ann
ann r :: Recursivity
r@Recursivity
NonRec NonEmpty (Binding TyName Name uni fun ann)
bs Term TyName Name uni fun ann
inTerm) = do
    -- Check each binding individually, then if ok, introduce its new type/vars to the (linearly) next let or inTerm
    Normalized (Type TyName uni ())
ty <- (Binding TyName Name uni fun ann
 -> PirTCEnv uni fun e (Normalized (Type TyName uni ()))
 -> PirTCEnv uni fun e (Normalized (Type TyName uni ())))
-> PirTCEnv uni fun e (Normalized (Type TyName uni ()))
-> NonEmpty (Binding TyName Name uni fun ann)
-> PirTCEnv uni fun e (Normalized (Type TyName uni ()))
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Binding TyName Name uni fun ann
-> PirTCEnv uni fun e (Normalized (Type TyName uni ()))
-> PirTCEnv uni fun e (Normalized (Type TyName uni ()))
forall res.
Binding TyName Name uni fun ann
-> PirTCEnv uni fun e res -> PirTCEnv uni fun e res
checkBindingThenScope (Term TyName Name uni fun ann
-> PirTCEnv uni fun e (Normalized (Type TyName uni ()))
forall (uni :: * -> *) fun ann e.
(GEq uni, Ix fun,
 AsTypeError e (Term TyName Name uni fun ()) uni fun ann,
 ToKind uni, HasUniApply uni, AsTypeErrorExt e uni ann) =>
Term TyName Name uni fun ann
-> PirTCEnv uni fun e (Normalized (Type TyName uni ()))
inferTypeM Term TyName Name uni fun ann
inTerm) NonEmpty (Binding TyName Name uni fun ann)
bs
    -- check the in-term's inferred type has kind * (except at toplevel)
    ann
-> Normalized (Type TyName uni ())
-> TypeCheckM uni fun (PirTCConfig uni fun) e ()
forall e term (uni :: * -> *) fun ann b.
(AsTypeError e term uni fun ann, ToKind uni) =>
ann -> Normalized (Type TyName uni b) -> PirTCEnv uni fun e ()
checkStarInferred ann
ann Normalized (Type TyName uni ())
ty
    Normalized (Type TyName uni ())
-> PirTCEnv uni fun e (Normalized (Type TyName uni ()))
forall (f :: * -> *) a. Applicative f => a -> f a
pure Normalized (Type TyName uni ())
ty
 where
   checkBindingThenScope :: Binding TyName Name uni fun ann -> PirTCEnv uni fun e res -> PirTCEnv uni fun e res
   checkBindingThenScope :: Binding TyName Name uni fun ann
-> PirTCEnv uni fun e res -> PirTCEnv uni fun e res
checkBindingThenScope Binding TyName Name uni fun ann
b PirTCEnv uni fun e res
acc = do
       -- check that the kinds of the declared types are correct
       Binding TyName Name uni fun ann
-> TypeCheckM uni fun (PirTCConfig uni fun) e ()
forall e (uni :: * -> *) fun ann.
(AsTypeError e (Term TyName Name uni fun ()) uni fun ann,
 ToKind uni) =>
Binding TyName Name uni fun ann -> PirTCEnv uni fun e ()
checkKindFromBinding Binding TyName Name uni fun ann
b
       -- check that the types of declared terms are correct
       Recursivity
-> Binding TyName Name uni fun ann
-> TypeCheckM uni fun (PirTCConfig uni fun) e ()
forall e (uni :: * -> *) fun a.
(GEq uni, Ix fun,
 AsTypeError e (Term TyName Name uni fun ()) uni fun a, ToKind uni,
 HasUniApply uni, AsTypeErrorExt e uni a) =>
Recursivity
-> Binding TyName Name uni fun a -> PirTCEnv uni fun e ()
checkTypeFromBinding Recursivity
r Binding TyName Name uni fun ann
b
       -- add new *normalized* termvariables to env
       -- Note that the order of adding typesVSkinds here does not matter
       Binding TyName Name uni fun ann
-> PirTCEnv uni fun e res -> PirTCEnv uni fun e res
forall name (uni :: * -> *) fun ann c e res.
Binding TyName name uni fun ann
-> TypeCheckM uni fun c e res -> TypeCheckM uni fun c e res
withTyVarsOfBinding Binding TyName Name uni fun ann
b (PirTCEnv uni fun e res -> PirTCEnv uni fun e res)
-> PirTCEnv uni fun e res -> PirTCEnv uni fun e res
forall a b. (a -> b) -> a -> b
$
           Recursivity
-> Binding TyName Name uni fun ann
-> PirTCEnv uni fun e res
-> PirTCEnv uni fun e res
forall (uni :: * -> *) fun c e a res.
HasUniApply uni =>
Recursivity
-> Binding TyName Name uni fun a
-> TypeCheckM uni fun c e res
-> TypeCheckM uni fun c e res
withVarsOfBinding Recursivity
r Binding TyName Name uni fun ann
b PirTCEnv uni fun e res
acc

{-
G'=G,withTyVarsOfBindings(bs)
forall b in bs. checkKindFromBinding(G', b)
G''=G',withVarsOfBindings(bs)
forall b in bs. checkTypeFromBinding(G'', b)
[infer| G'' !- inT : ty] ty ~> vTy
-------------------------------------------------
[infer| G !- (let rec bs in inT) : vTy]
-}
inferTypeM (Let ann
ann r :: Recursivity
r@Recursivity
Rec NonEmpty (Binding TyName Name uni fun ann)
bs Term TyName Name uni fun ann
inTerm) = do
    Normalized (Type TyName uni ())
ty <- NonEmpty (Binding TyName Name uni fun ann)
-> PirTCEnv uni fun e (Normalized (Type TyName uni ()))
-> PirTCEnv uni fun e (Normalized (Type TyName uni ()))
forall (f :: * -> *) name (uni :: * -> *) fun ann c e res.
Foldable f =>
f (Binding TyName name uni fun ann)
-> TypeCheckM uni fun c e res -> TypeCheckM uni fun c e res
withTyVarsOfBindings NonEmpty (Binding TyName Name uni fun ann)
bs (PirTCEnv uni fun e (Normalized (Type TyName uni ()))
 -> PirTCEnv uni fun e (Normalized (Type TyName uni ())))
-> PirTCEnv uni fun e (Normalized (Type TyName uni ()))
-> PirTCEnv uni fun e (Normalized (Type TyName uni ()))
forall a b. (a -> b) -> a -> b
$ do
       -- check that the kinds of the declared types *over all bindings* are correct
       -- Note that, compared to NonRec, we need the newtyvars in scope to do kindchecking
       NonEmpty (Binding TyName Name uni fun ann)
-> (Binding TyName Name uni fun ann
    -> TypeCheckM uni fun (PirTCConfig uni fun) e ())
-> TypeCheckM uni fun (PirTCConfig uni fun) e ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ NonEmpty (Binding TyName Name uni fun ann)
bs Binding TyName Name uni fun ann
-> TypeCheckM uni fun (PirTCConfig uni fun) e ()
forall e (uni :: * -> *) fun ann.
(AsTypeError e (Term TyName Name uni fun ()) uni fun ann,
 ToKind uni) =>
Binding TyName Name uni fun ann -> PirTCEnv uni fun e ()
checkKindFromBinding
       Recursivity
-> NonEmpty (Binding TyName Name uni fun ann)
-> PirTCEnv uni fun e (Normalized (Type TyName uni ()))
-> PirTCEnv uni fun e (Normalized (Type TyName uni ()))
forall (t :: * -> *) (uni :: * -> *) fun a c e res.
(Foldable t, HasUniApply uni) =>
Recursivity
-> t (Binding TyName Name uni fun a)
-> TypeCheckM uni fun c e res
-> TypeCheckM uni fun c e res
withVarsOfBindings Recursivity
r NonEmpty (Binding TyName Name uni fun ann)
bs (PirTCEnv uni fun e (Normalized (Type TyName uni ()))
 -> PirTCEnv uni fun e (Normalized (Type TyName uni ())))
-> PirTCEnv uni fun e (Normalized (Type TyName uni ()))
-> PirTCEnv uni fun e (Normalized (Type TyName uni ()))
forall a b. (a -> b) -> a -> b
$ do
              -- check that the types of declared terms are correct
              -- Note that, compared to NonRec, we need the newtyvars+newvars in scope to do typechecking
              NonEmpty (Binding TyName Name uni fun ann)
-> (Binding TyName Name uni fun ann
    -> TypeCheckM uni fun (PirTCConfig uni fun) e ())
-> TypeCheckM uni fun (PirTCConfig uni fun) e ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ NonEmpty (Binding TyName Name uni fun ann)
bs ((Binding TyName Name uni fun ann
  -> TypeCheckM uni fun (PirTCConfig uni fun) e ())
 -> TypeCheckM uni fun (PirTCConfig uni fun) e ())
-> (Binding TyName Name uni fun ann
    -> TypeCheckM uni fun (PirTCConfig uni fun) e ())
-> TypeCheckM uni fun (PirTCConfig uni fun) e ()
forall a b. (a -> b) -> a -> b
$ Recursivity
-> Binding TyName Name uni fun ann
-> TypeCheckM uni fun (PirTCConfig uni fun) e ()
forall e (uni :: * -> *) fun a.
(GEq uni, Ix fun,
 AsTypeError e (Term TyName Name uni fun ()) uni fun a, ToKind uni,
 HasUniApply uni, AsTypeErrorExt e uni a) =>
Recursivity
-> Binding TyName Name uni fun a -> PirTCEnv uni fun e ()
checkTypeFromBinding Recursivity
r
              Term TyName Name uni fun ann
-> PirTCEnv uni fun e (Normalized (Type TyName uni ()))
forall (uni :: * -> *) fun ann e.
(GEq uni, Ix fun,
 AsTypeError e (Term TyName Name uni fun ()) uni fun ann,
 ToKind uni, HasUniApply uni, AsTypeErrorExt e uni ann) =>
Term TyName Name uni fun ann
-> PirTCEnv uni fun e (Normalized (Type TyName uni ()))
inferTypeM Term TyName Name uni fun ann
inTerm
    -- check the in-term's inferred type has kind * (except at toplevel)
    ann
-> Normalized (Type TyName uni ())
-> TypeCheckM uni fun (PirTCConfig uni fun) e ()
forall e term (uni :: * -> *) fun ann b.
(AsTypeError e term uni fun ann, ToKind uni) =>
ann -> Normalized (Type TyName uni b) -> PirTCEnv uni fun e ()
checkStarInferred ann
ann Normalized (Type TyName uni ())
ty
    Normalized (Type TyName uni ())
-> PirTCEnv uni fun e (Normalized (Type TyName uni ()))
forall (f :: * -> *) a. Applicative f => a -> f a
pure Normalized (Type TyName uni ())
ty

{-| This checks that a newly-introduced type variable is correctly kinded.

(b is ty::K = rhs) => [check| G !- rhs :: K]
(b is term (X::T) => [check| G !- T :: *])
(b is data (X::K) tyarg1::K1 ... tyargN::KN  = _) => [check| G, X::K, tyarg1::K1...tyargN::KN !- [X tyarg1 ... tyargN] :: *]
--------------------------------------------------------------------------------------
checkKindFromBinding(G,b)
-}
checkKindFromBinding :: forall e uni fun ann.
                   (AsTypeError e (Term TyName Name uni fun ()) uni fun ann, ToKind uni)
                 => Binding TyName Name uni fun ann
                 -> PirTCEnv uni fun e ()
checkKindFromBinding :: Binding TyName Name uni fun ann -> PirTCEnv uni fun e ()
checkKindFromBinding = \case
    -- For a type binding, correct means that the the RHS is indeed kinded by the declared kind.
    TypeBind ann
_ (TyVarDecl ann
ann TyName
_ Kind ann
k) Type TyName uni ann
rhs ->
        ann -> Type TyName uni ann -> Kind () -> PirTCEnv uni fun e ()
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
rhs (Kind () -> PirTCEnv uni fun e ())
-> Kind () -> PirTCEnv uni fun e ()
forall a b. (a -> b) -> a -> b
$ Kind ann -> Kind ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Kind ann
k
    -- For a term binding, correct means that the declared type has kind *.
    TermBind ann
_ Strictness
_ (VarDecl ann
_ Name
_ Type TyName uni ann
ty) Term TyName Name uni fun ann
_ ->
        ann -> Type TyName uni ann -> Kind () -> PirTCEnv uni fun e ()
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 (Type TyName uni ann -> ann
forall tyname (uni :: * -> *) ann. Type tyname uni ann -> ann
typeAnn Type TyName uni ann
ty) Type TyName uni ann
ty (Kind () -> PirTCEnv uni fun e ())
-> Kind () -> PirTCEnv uni fun e ()
forall a b. (a -> b) -> a -> b
$ () -> Kind ()
forall ann. ann -> Kind ann
Type ()
    -- For a datatype binding, correct means that the type constructor has kind * when fully-applied to its type arguments.
    DatatypeBind ann
_ dt :: Datatype TyName Name uni fun ann
dt@(Datatype ann
ann TyVarDecl TyName ann
tycon [TyVarDecl TyName ann]
tyargs Name
_ [VarDecl TyName Name uni fun ann]
vdecls) ->
        -- tycon+tyargs must be in scope during kindchecking
        [TyVarDecl TyName ann]
-> PirTCEnv uni fun e () -> PirTCEnv uni fun e ()
forall ann (uni :: * -> *) fun c e a.
[TyVarDecl TyName ann]
-> TypeCheckM uni fun c e a -> TypeCheckM uni fun c e a
withTyVarDecls (TyVarDecl TyName ann
tyconTyVarDecl TyName ann
-> [TyVarDecl TyName ann] -> [TyVarDecl TyName ann]
forall a. a -> [a] -> [a]
:[TyVarDecl TyName ann]
tyargs) (PirTCEnv uni fun e () -> PirTCEnv uni fun e ())
-> PirTCEnv uni fun e () -> PirTCEnv uni fun e ()
forall a b. (a -> b) -> a -> b
$ do
          -- the fully-applied type-constructor must be *-kinded
          ann -> Type TyName uni ann -> Kind () -> PirTCEnv uni fun e ()
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
appliedTyCon (Kind () -> PirTCEnv uni fun e ())
-> Kind () -> PirTCEnv uni fun e ()
forall a b. (a -> b) -> a -> b
$ () -> Kind ()
forall ann. ann -> Kind ann
Type ()
          -- the types of all the data-constructors must be *-kinded
          [Type TyName uni ann]
-> (Type TyName uni ann -> PirTCEnv uni fun e ())
-> PirTCEnv uni fun e ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ (VarDecl TyName Name uni fun ann -> Type TyName uni ann
forall tyname name (uni :: * -> *) k (fun :: k) ann.
VarDecl tyname name uni fun ann -> Type tyname uni ann
_varDeclType (VarDecl TyName Name uni fun ann -> Type TyName uni ann)
-> [VarDecl TyName Name uni fun ann] -> [Type TyName uni ann]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [VarDecl TyName Name uni fun ann]
vdecls) ((Type TyName uni ann -> PirTCEnv uni fun e ())
 -> PirTCEnv uni fun e ())
-> (Type TyName uni ann -> PirTCEnv uni fun e ())
-> PirTCEnv uni fun e ()
forall a b. (a -> b) -> a -> b
$
               ann -> Type TyName uni ann -> Kind () -> PirTCEnv uni fun e ()
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 -> Kind () -> PirTCEnv uni fun e ())
-> Kind () -> Type TyName uni ann -> PirTCEnv uni fun e ()
forall a b c. (a -> b -> c) -> b -> a -> c
`flip` () -> Kind ()
forall ann. ann -> Kind ann
Type ()
     where
       Type TyName uni ann
appliedTyCon :: Type TyName uni ann = ann -> Datatype TyName Name uni fun ann -> Type TyName uni ann
forall a (uni :: * -> *) fun.
a -> Datatype TyName Name uni fun a -> Type TyName uni a
mkDatatypeValueType ann
ann Datatype TyName Name uni fun ann
dt


{- | This checks that a newly-introduced variable has declared the *right type* for its term
(rhs term in case of termbind or implicit constructor term in case of dataconstructor).

(b is t:ty = _) => [check| G !- t : nTy]  ty ~> vTy
---------------------------------------------------
checkTypeFromBinding(G,b)
-}
checkTypeFromBinding :: forall e uni fun a. (GEq uni, Ix fun, AsTypeError e (Term TyName Name uni fun ()) uni fun a, ToKind uni, HasUniApply uni, AsTypeErrorExt e uni a)
                 => Recursivity -> Binding TyName Name uni fun a -> PirTCEnv uni fun e ()
checkTypeFromBinding :: Recursivity
-> Binding TyName Name uni fun a -> PirTCEnv uni fun e ()
checkTypeFromBinding Recursivity
recurs = \case
    TypeBind{} -> () -> PirTCEnv uni fun e ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure () -- no types to check
    TermBind a
_ Strictness
_ (VarDecl a
ann Name
_ Type TyName uni a
ty) Term TyName Name uni fun a
rhs ->
        -- See Note [PIR vs Paper Escaping Types Difference]
        PirTCEnv uni fun e () -> PirTCEnv uni fun e ()
forall (uni :: * -> *) fun e a.
PirTCEnv uni fun e a -> PirTCEnv uni fun e a
withNoEscapingTypes (a
-> Term TyName Name uni fun a
-> Normalized (Type TyName uni ())
-> PirTCEnv uni fun e ()
forall (uni :: * -> *) fun e ann.
(GEq uni, Ix fun, AsTypeErrorExt e uni ann,
 AsTypeError e (Term TyName Name uni fun ()) uni fun ann,
 ToKind uni, HasUniApply uni) =>
ann
-> Term TyName Name uni fun ann
-> Normalized (Type TyName uni ())
-> PirTCEnv uni fun e ()
checkTypeM a
ann Term TyName Name uni fun a
rhs (Normalized (Type TyName uni ()) -> PirTCEnv uni fun e ())
-> (Normalized (Type TyName uni a)
    -> Normalized (Type TyName uni ()))
-> Normalized (Type TyName uni a)
-> PirTCEnv uni fun e ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type TyName uni a -> Type TyName uni ())
-> Normalized (Type TyName uni a)
-> Normalized (Type TyName uni ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Type TyName uni a -> Type TyName uni ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Normalized (Type TyName uni a) -> PirTCEnv uni fun e ())
-> ReaderT
     (TypeCheckEnv uni fun (PirTCConfig uni fun))
     (ExceptT e Quote)
     (Normalized (Type TyName uni a))
-> PirTCEnv uni fun e ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Type TyName uni a
-> ReaderT
     (TypeCheckEnv uni fun (PirTCConfig uni fun))
     (ExceptT e Quote)
     (Normalized (Type TyName uni a))
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 a
ty)
    DatatypeBind a
_ dt :: Datatype TyName Name uni fun a
dt@(Datatype a
ann TyVarDecl TyName a
_ [TyVarDecl TyName a]
tyargs Name
_ [VarDecl TyName Name uni fun a]
constrs) ->
        [Type TyName uni a]
-> (Type TyName uni a -> PirTCEnv uni fun e ())
-> PirTCEnv uni fun e ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ (VarDecl TyName Name uni fun a -> Type TyName uni a
forall tyname name (uni :: * -> *) k (fun :: k) ann.
VarDecl tyname name uni fun ann -> Type tyname uni ann
_varDeclType (VarDecl TyName Name uni fun a -> Type TyName uni a)
-> [VarDecl TyName Name uni fun a] -> [Type TyName uni a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [VarDecl TyName Name uni fun a]
constrs) ((Type TyName uni a -> PirTCEnv uni fun e ())
 -> PirTCEnv uni fun e ())
-> (Type TyName uni a -> PirTCEnv uni fun e ())
-> PirTCEnv uni fun e ()
forall a b. (a -> b) -> a -> b
$
            \ Type TyName uni a
ty -> Type TyName uni a -> PirTCEnv uni fun e ()
checkConRes Type TyName uni a
ty PirTCEnv uni fun e ()
-> PirTCEnv uni fun e () -> PirTCEnv uni fun e ()
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Type TyName uni a -> PirTCEnv uni fun e ()
checkNonRecScope Type TyName uni a
ty
      where
       Type TyName uni a
appliedTyCon :: Type TyName uni a = a -> Datatype TyName Name uni fun a -> Type TyName uni a
forall a (uni :: * -> *) fun.
a -> Datatype TyName Name uni fun a -> Type TyName uni a
mkDatatypeValueType a
ann Datatype TyName Name uni fun a
dt
       checkConRes :: Type TyName uni a -> PirTCEnv uni fun e ()
       checkConRes :: Type TyName uni a -> PirTCEnv uni fun e ()
checkConRes Type TyName uni a
ty =
           -- We earlier checked that datacons' type is *-kinded (using checkKindBinding), but this is not enough:
           -- we must also check that its result type is EXACTLY `[[TypeCon tyarg1] ... tyargn]` (ignoring annotations)
           Bool -> PirTCEnv uni fun e () -> PirTCEnv uni fun e ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Type TyName uni a -> Type TyName uni ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Type TyName uni a -> Type TyName uni a
forall tyname (uni :: * -> *) a.
Type tyname uni a -> Type tyname uni a
funResultType Type TyName uni a
ty) Type TyName uni () -> Type TyName uni () -> Bool
forall a. Eq a => a -> a -> Bool
/= Type TyName uni a -> Type TyName uni ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Type TyName uni a
appliedTyCon) (PirTCEnv uni fun e () -> PirTCEnv uni fun e ())
-> (TypeErrorExt uni a -> PirTCEnv uni fun e ())
-> TypeErrorExt uni a
-> PirTCEnv uni fun e ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
               AReview e (TypeErrorExt uni a)
-> TypeErrorExt uni a -> PirTCEnv uni fun e ()
forall e (m :: * -> *) t x.
MonadError e m =>
AReview e t -> t -> m x
throwing AReview e (TypeErrorExt uni a)
forall r (uni :: * -> *) ann.
AsTypeErrorExt r uni ann =>
Prism' r (TypeErrorExt uni ann)
_TypeErrorExt (TypeErrorExt uni a -> PirTCEnv uni fun e ())
-> TypeErrorExt uni a -> PirTCEnv uni fun e ()
forall a b. (a -> b) -> a -> b
$ a -> Type TyName uni a -> TypeErrorExt uni a
forall (uni :: * -> *) ann.
ann -> Type TyName uni ann -> TypeErrorExt uni ann
MalformedDataConstrResType a
ann Type TyName uni a
appliedTyCon

       -- if nonrec binding, make sure that type-constructor is not part of the data-constructor's argument types.
       checkNonRecScope :: Type TyName uni a -> PirTCEnv uni fun e ()
       checkNonRecScope :: Type TyName uni a -> PirTCEnv uni fun e ()
checkNonRecScope Type TyName uni a
ty = case Recursivity
recurs of
           Recursivity
Rec -> () -> PirTCEnv uni fun e ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
           Recursivity
NonRec ->
               -- now we make sure that dataconstructor is not self-recursive, i.e. funargs don't contain tycon
               [TyVarDecl TyName a]
-> PirTCEnv uni fun e () -> PirTCEnv uni fun e ()
forall ann (uni :: * -> *) fun c e a.
[TyVarDecl TyName ann]
-> TypeCheckM uni fun c e a -> TypeCheckM uni fun c e a
withTyVarDecls [TyVarDecl TyName a]
tyargs (PirTCEnv uni fun e () -> PirTCEnv uni fun e ())
-> PirTCEnv uni fun e () -> PirTCEnv uni fun e ()
forall a b. (a -> b) -> a -> b
$ -- tycon not in scope here
                      -- OPTIMIZE: we use inferKind for scope-checking, but a simple ADT-traversal would suffice
                      [Type TyName uni a]
-> (Type TyName uni a
    -> ReaderT
         (TypeCheckEnv uni fun (PirTCConfig uni fun))
         (ExceptT e Quote)
         (Kind ()))
-> PirTCEnv uni fun e ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ (Type TyName uni a -> [Type TyName uni a]
forall tyname (uni :: * -> *) a.
Type tyname uni a -> [Type tyname uni a]
funTyArgs Type TyName uni a
ty) Type TyName uni a
-> ReaderT
     (TypeCheckEnv uni fun (PirTCConfig uni fun))
     (ExceptT e Quote)
     (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

-- | Check that the in-Term's inferred type of a Let has kind *.
-- Skip this check at the top-level, to allow top-level types to escape; see Note [PIR vs Paper Escaping Types Difference].
checkStarInferred :: (AsTypeError e term uni fun ann, ToKind uni)
                  => ann -> Normalized (Type TyName uni b) -> PirTCEnv uni fun e ()
checkStarInferred :: ann -> Normalized (Type TyName uni b) -> PirTCEnv uni fun e ()
checkStarInferred ann
ann Normalized (Type TyName uni b)
t = do
    AllowEscape
allowEscape <- Getting
  AllowEscape
  (TypeCheckEnv uni fun (PirTCConfig uni fun))
  AllowEscape
-> ReaderT
     (TypeCheckEnv uni fun (PirTCConfig uni fun))
     (ExceptT e Quote)
     AllowEscape
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view (Getting
   AllowEscape
   (TypeCheckEnv uni fun (PirTCConfig uni fun))
   AllowEscape
 -> ReaderT
      (TypeCheckEnv uni fun (PirTCConfig uni fun))
      (ExceptT e Quote)
      AllowEscape)
-> Getting
     AllowEscape
     (TypeCheckEnv uni fun (PirTCConfig uni fun))
     AllowEscape
-> ReaderT
     (TypeCheckEnv uni fun (PirTCConfig uni fun))
     (ExceptT e Quote)
     AllowEscape
forall a b. (a -> b) -> a -> b
$ (PirTCConfig uni fun -> Const AllowEscape (PirTCConfig uni fun))
-> TypeCheckEnv uni fun (PirTCConfig uni fun)
-> Const AllowEscape (TypeCheckEnv uni fun (PirTCConfig uni fun))
forall (uni :: * -> *) fun cfg fun2 cfg2.
Lens
  (TypeCheckEnv uni fun cfg) (TypeCheckEnv uni fun2 cfg2) cfg cfg2
tceTypeCheckConfig ((PirTCConfig uni fun -> Const AllowEscape (PirTCConfig uni fun))
 -> TypeCheckEnv uni fun (PirTCConfig uni fun)
 -> Const AllowEscape (TypeCheckEnv uni fun (PirTCConfig uni fun)))
-> ((AllowEscape -> Const AllowEscape AllowEscape)
    -> PirTCConfig uni fun -> Const AllowEscape (PirTCConfig uni fun))
-> Getting
     AllowEscape
     (TypeCheckEnv uni fun (PirTCConfig uni fun))
     AllowEscape
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (AllowEscape -> Const AllowEscape AllowEscape)
-> PirTCConfig uni fun -> Const AllowEscape (PirTCConfig uni fun)
forall (uni :: * -> *) fun. Lens' (PirTCConfig uni fun) AllowEscape
pirConfigAllowEscape
    case AllowEscape
allowEscape of
        AllowEscape
NoEscape  -> ann -> Type TyName uni ann -> Kind () -> PirTCEnv uni fun e ()
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 (ann
ann ann -> Type TyName uni b -> Type TyName uni ann
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Normalized (Type TyName uni b) -> Type TyName uni b
forall a. Normalized a -> a
unNormalized Normalized (Type TyName uni b)
t) (Kind () -> PirTCEnv uni fun e ())
-> Kind () -> PirTCEnv uni fun e ()
forall a b. (a -> b) -> a -> b
$ () -> Kind ()
forall ann. ann -> Kind ann
Type ()
        -- NOTE: we completely skip the check in case of toplevel because we would need an *final, extended Gamma environment*
        -- to run the kind-check in, but we cannot easily get that since we are using a Reader for environments and not State
        AllowEscape
YesEscape -> () -> PirTCEnv uni fun e ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()


-- | Changes the flag in nested-lets so to disallow returning a type outside of the type's scope
withNoEscapingTypes :: PirTCEnv uni fun e a -> PirTCEnv uni fun e a
withNoEscapingTypes :: PirTCEnv uni fun e a -> PirTCEnv uni fun e a
withNoEscapingTypes = (TypeCheckEnv uni fun (PirTCConfig uni fun)
 -> TypeCheckEnv uni fun (PirTCConfig uni fun))
-> PirTCEnv uni fun e a -> PirTCEnv uni fun e a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((TypeCheckEnv uni fun (PirTCConfig uni fun)
  -> TypeCheckEnv uni fun (PirTCConfig uni fun))
 -> PirTCEnv uni fun e a -> PirTCEnv uni fun e a)
-> (TypeCheckEnv uni fun (PirTCConfig uni fun)
    -> TypeCheckEnv uni fun (PirTCConfig uni fun))
-> PirTCEnv uni fun e a
-> PirTCEnv uni fun e a
forall a b. (a -> b) -> a -> b
$ ASetter
  (TypeCheckEnv uni fun (PirTCConfig uni fun))
  (TypeCheckEnv uni fun (PirTCConfig uni fun))
  AllowEscape
  AllowEscape
-> AllowEscape
-> TypeCheckEnv uni fun (PirTCConfig uni fun)
-> TypeCheckEnv uni fun (PirTCConfig uni fun)
forall s t a b. ASetter s t a b -> b -> s -> t
set ((PirTCConfig uni fun -> Identity (PirTCConfig uni fun))
-> TypeCheckEnv uni fun (PirTCConfig uni fun)
-> Identity (TypeCheckEnv uni fun (PirTCConfig uni fun))
forall (uni :: * -> *) fun cfg fun2 cfg2.
Lens
  (TypeCheckEnv uni fun cfg) (TypeCheckEnv uni fun2 cfg2) cfg cfg2
tceTypeCheckConfig((PirTCConfig uni fun -> Identity (PirTCConfig uni fun))
 -> TypeCheckEnv uni fun (PirTCConfig uni fun)
 -> Identity (TypeCheckEnv uni fun (PirTCConfig uni fun)))
-> ((AllowEscape -> Identity AllowEscape)
    -> PirTCConfig uni fun -> Identity (PirTCConfig uni fun))
-> ASetter
     (TypeCheckEnv uni fun (PirTCConfig uni fun))
     (TypeCheckEnv uni fun (PirTCConfig uni fun))
     AllowEscape
     AllowEscape
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(AllowEscape -> Identity AllowEscape)
-> PirTCConfig uni fun -> Identity (PirTCConfig uni fun)
forall (uni :: * -> *) fun. Lens' (PirTCConfig uni fun) AllowEscape
pirConfigAllowEscape) AllowEscape
NoEscape

-- | Run a 'TypeCheckM' computation by supplying a 'TypeCheckConfig' to it.
-- Differs from its PLC version in that is passes an extra env flag 'YesEscape'.
runTypeCheckM :: (MonadError e m, MonadQuote m)
              => PirTCConfig uni fun -> PirTCEnv uni fun e a -> m a
runTypeCheckM :: PirTCConfig uni fun -> PirTCEnv uni fun e a -> m a
runTypeCheckM PirTCConfig uni fun
config PirTCEnv uni fun e a
a =
    Either e a -> m a
forall e (m :: * -> *) a. MonadError e m => Either e a -> m a
liftEither (Either e a -> m a) -> m (Either e a) -> m a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Quote (Either e a) -> m (Either e a)
forall (m :: * -> *) a. MonadQuote m => Quote a -> m a
liftQuote (ExceptT e Quote a -> Quote (Either e a)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT e Quote a -> Quote (Either e a))
-> ExceptT e Quote a -> Quote (Either e a)
forall a b. (a -> b) -> a -> b
$ PirTCEnv uni fun e a
-> TypeCheckEnv uni fun (PirTCConfig uni fun) -> ExceptT e Quote a
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT PirTCEnv uni fun e a
a TypeCheckEnv uni fun (PirTCConfig uni fun)
forall (uni :: * -> *) fun.
TypeCheckEnv uni fun (PirTCConfig uni fun)
env) where
        env :: TypeCheckEnv uni fun (PirTCConfig uni fun)
env = PirTCConfig uni fun
-> TyVarKinds
-> VarTypes uni
-> TypeCheckEnv uni fun (PirTCConfig uni fun)
forall (uni :: * -> *) fun cfg.
cfg -> TyVarKinds -> VarTypes uni -> TypeCheckEnv uni fun cfg
TypeCheckEnv PirTCConfig uni fun
config TyVarKinds
forall a. Monoid a => a
mempty VarTypes uni
forall a. Monoid a => a
mempty

-- Helpers
----------

-- | For a single binding, generate the newly-introduce term-variables' types,
-- normalize them, rename them and add them into scope.
-- Newly-declared term variables are: variables of termbinds, constructors, destructor
-- Note: Assumes that the input is globally-unique and preserves global-uniqueness
-- Note to self: actually passing here recursivity is unnecessary, but we do it for sake of compiler/datatype.hs api
withVarsOfBinding :: forall uni fun c e a res. HasUniApply uni =>
                    Recursivity -> Binding TyName Name uni fun a
                  -> TypeCheckM uni fun c e res -> TypeCheckM uni fun c e res
withVarsOfBinding :: Recursivity
-> Binding TyName Name uni fun a
-> TypeCheckM uni fun c e res
-> TypeCheckM uni fun c e res
withVarsOfBinding Recursivity
_ TypeBind{} TypeCheckM uni fun c e res
k = TypeCheckM uni fun c e res
k
withVarsOfBinding Recursivity
_ (TermBind a
_ Strictness
_ VarDecl TyName Name uni fun a
vdecl Term TyName Name uni fun a
_) TypeCheckM uni fun c e res
k = do
    Normalized (Type TyName uni a)
vTy <- Type TyName uni a
-> TypeCheckM uni fun c e (Normalized (Type TyName uni a))
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 a
 -> TypeCheckM uni fun c e (Normalized (Type TyName uni a)))
-> Type TyName uni a
-> TypeCheckM uni fun c e (Normalized (Type TyName uni a))
forall a b. (a -> b) -> a -> b
$ VarDecl TyName Name uni fun a -> Type TyName uni a
forall tyname name (uni :: * -> *) k (fun :: k) ann.
VarDecl tyname name uni fun ann -> Type tyname uni ann
_varDeclType VarDecl TyName Name uni fun a
vdecl
    -- no need to rename here
    Name
-> Normalized (Type TyName uni ())
-> TypeCheckM uni fun c e res
-> TypeCheckM uni fun c e res
forall (uni :: * -> *) fun cfg err a.
Name
-> Normalized (Type TyName uni ())
-> TypeCheckM uni fun cfg err a
-> TypeCheckM uni fun cfg err a
withVar (VarDecl TyName Name uni fun a -> Name
forall tyname name (uni :: * -> *) k (fun :: k) ann.
VarDecl tyname name uni fun ann -> name
_varDeclName VarDecl TyName Name uni fun a
vdecl) (Type TyName uni a -> Type TyName uni ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Type TyName uni a -> Type TyName uni ())
-> Normalized (Type TyName uni a)
-> Normalized (Type TyName uni ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Normalized (Type TyName uni a)
vTy) TypeCheckM uni fun c e res
k
withVarsOfBinding Recursivity
r (DatatypeBind a
_ Datatype TyName Name uni fun a
dt) TypeCheckM uni fun c e res
k = do
    -- generate all the definitions
    (Def (TyVarDecl TyName (Provenance a)) (PLCRecType uni fun a)
_tyconstrDef, [Def
   (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a)]
constrDefs, Def
  (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a)
destrDef) <- Recursivity
-> Datatype TyName Name uni fun (Provenance a)
-> ReaderT
     (TypeCheckEnv uni fun c)
     (ExceptT e Quote)
     (Def (TyVarDecl TyName (Provenance a)) (PLCRecType uni fun a),
      [Def
         (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a)],
      Def
        (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a))
forall (m :: * -> *) (uni :: * -> *) fun a.
MonadQuote m =>
Recursivity
-> Datatype TyName Name uni fun (Provenance a)
-> m (Def (TyVarDecl TyName (Provenance a)) (PLCRecType uni fun a),
      [Def
         (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a)],
      Def
        (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a))
compileDatatypeDefs Recursivity
r (Datatype TyName Name uni fun a
-> Datatype TyName Name uni fun (Provenance a)
forall (f :: * -> *) a. Functor f => f a -> f (Provenance a)
original Datatype TyName Name uni fun a
dt)
    -- ignore the generated rhs terms of constructors/destructor
    let structorDecls :: [VarDecl TyName Name uni fun (Provenance a)]
structorDecls = Def
  (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a)
-> VarDecl TyName Name uni fun (Provenance a)
forall var val. Def var val -> var
PIR.defVar (Def
   (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a)
 -> VarDecl TyName Name uni fun (Provenance a))
-> [Def
      (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a)]
-> [VarDecl TyName Name uni fun (Provenance a)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Def
  (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a)
destrDefDef
  (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a)
-> [Def
      (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a)]
-> [Def
      (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a)]
forall a. a -> [a] -> [a]
:[Def
   (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a)]
constrDefs
    -- normalize, then rename, then only introduce the vardecl to scope
    (VarDecl TyName Name uni fun (Provenance a)
 -> TypeCheckM uni fun c e res -> TypeCheckM uni fun c e res)
-> TypeCheckM uni fun c e res
-> [VarDecl TyName Name uni fun (Provenance a)]
-> TypeCheckM uni fun c e res
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr VarDecl TyName Name uni fun (Provenance a)
-> TypeCheckM uni fun c e res -> TypeCheckM uni fun c e res
normRenameScope TypeCheckM uni fun c e res
k [VarDecl TyName Name uni fun (Provenance a)]
structorDecls
    where
      normRenameScope :: VarDecl TyName Name uni fun (Provenance a)
                      -> TypeCheckM uni fun c e res -> TypeCheckM uni fun c e res
      normRenameScope :: VarDecl TyName Name uni fun (Provenance a)
-> TypeCheckM uni fun c e res -> TypeCheckM uni fun c e res
normRenameScope VarDecl TyName Name uni fun (Provenance a)
v TypeCheckM uni fun c e res
acc = do
          Normalized (Type TyName uni (Provenance a))
normRenamedTy <- Normalized (Type TyName uni (Provenance a))
-> ReaderT
     (TypeCheckEnv uni fun c)
     (ExceptT e Quote)
     (Normalized (Type TyName uni (Provenance a)))
forall a (m :: * -> *). (Rename a, MonadQuote m) => a -> m a
rename (Normalized (Type TyName uni (Provenance a))
 -> ReaderT
      (TypeCheckEnv uni fun c)
      (ExceptT e Quote)
      (Normalized (Type TyName uni (Provenance a))))
-> ReaderT
     (TypeCheckEnv uni fun c)
     (ExceptT e Quote)
     (Normalized (Type TyName uni (Provenance a)))
-> ReaderT
     (TypeCheckEnv uni fun c)
     (ExceptT e Quote)
     (Normalized (Type TyName uni (Provenance a)))
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Type TyName uni (Provenance a)
-> ReaderT
     (TypeCheckEnv uni fun c)
     (ExceptT e Quote)
     (Normalized (Type TyName uni (Provenance a)))
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 (Provenance a)
 -> ReaderT
      (TypeCheckEnv uni fun c)
      (ExceptT e Quote)
      (Normalized (Type TyName uni (Provenance a))))
-> Type TyName uni (Provenance a)
-> ReaderT
     (TypeCheckEnv uni fun c)
     (ExceptT e Quote)
     (Normalized (Type TyName uni (Provenance a)))
forall a b. (a -> b) -> a -> b
$ VarDecl TyName Name uni fun (Provenance a)
-> Type TyName uni (Provenance a)
forall tyname name (uni :: * -> *) k (fun :: k) ann.
VarDecl tyname name uni fun ann -> Type tyname uni ann
_varDeclType VarDecl TyName Name uni fun (Provenance a)
v)
          Name
-> Normalized (Type TyName uni ())
-> TypeCheckM uni fun c e res
-> TypeCheckM uni fun c e res
forall (uni :: * -> *) fun cfg err a.
Name
-> Normalized (Type TyName uni ())
-> TypeCheckM uni fun cfg err a
-> TypeCheckM uni fun cfg err a
withVar (VarDecl TyName Name uni fun (Provenance a) -> Name
forall tyname name (uni :: * -> *) k (fun :: k) ann.
VarDecl tyname name uni fun ann -> name
_varDeclName VarDecl TyName Name uni fun (Provenance a)
v) (Type TyName uni (Provenance a) -> Type TyName uni ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Type TyName uni (Provenance a) -> Type TyName uni ())
-> Normalized (Type TyName uni (Provenance a))
-> Normalized (Type TyName uni ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Normalized (Type TyName uni (Provenance a))
normRenamedTy) TypeCheckM uni fun c e res
acc


withVarsOfBindings :: (Foldable t, HasUniApply uni) => Recursivity -> t (Binding TyName Name uni fun a)
                   -> TypeCheckM uni fun c e res -> TypeCheckM uni fun c e res
withVarsOfBindings :: Recursivity
-> t (Binding TyName Name uni fun a)
-> TypeCheckM uni fun c e res
-> TypeCheckM uni fun c e res
withVarsOfBindings Recursivity
r t (Binding TyName Name uni fun a)
bs TypeCheckM uni fun c e res
k = (Binding TyName Name uni fun a
 -> TypeCheckM uni fun c e res -> TypeCheckM uni fun c e res)
-> TypeCheckM uni fun c e res
-> t (Binding TyName Name uni fun a)
-> TypeCheckM uni fun c e res
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Recursivity
-> Binding TyName Name uni fun a
-> TypeCheckM uni fun c e res
-> TypeCheckM uni fun c e res
forall (uni :: * -> *) fun c e a res.
HasUniApply uni =>
Recursivity
-> Binding TyName Name uni fun a
-> TypeCheckM uni fun c e res
-> TypeCheckM uni fun c e res
withVarsOfBinding Recursivity
r) TypeCheckM uni fun c e res
k t (Binding TyName Name uni fun a)
bs

-- | Scope a typechecking computation with the given binding's newly-introducing type (if there is one)
withTyVarsOfBinding :: Binding TyName name uni fun ann -> TypeCheckM uni fun c e res -> TypeCheckM uni fun c e res
withTyVarsOfBinding :: Binding TyName name uni fun ann
-> TypeCheckM uni fun c e res -> TypeCheckM uni fun c e res
withTyVarsOfBinding = \case
       TypeBind ann
_ TyVarDecl TyName ann
tvdecl Type TyName uni ann
_                      -> [TyVarDecl TyName ann]
-> TypeCheckM uni fun c e res -> TypeCheckM uni fun c e res
forall ann (uni :: * -> *) fun c e a.
[TyVarDecl TyName ann]
-> TypeCheckM uni fun c e a -> TypeCheckM uni fun c e a
withTyVarDecls [TyVarDecl TyName ann
tvdecl]
       DatatypeBind ann
_ (Datatype ann
_ TyVarDecl TyName ann
tvdecl [TyVarDecl TyName ann]
_ name
_ [VarDecl TyName name uni fun ann]
_) -> [TyVarDecl TyName ann]
-> TypeCheckM uni fun c e res -> TypeCheckM uni fun c e res
forall ann (uni :: * -> *) fun c e a.
[TyVarDecl TyName ann]
-> TypeCheckM uni fun c e a -> TypeCheckM uni fun c e a
withTyVarDecls [TyVarDecl TyName ann
tvdecl]
       TermBind{}                               -> TypeCheckM uni fun c e res -> TypeCheckM uni fun c e res
forall a. a -> a
id -- no type to introduce

-- | Extend the typecheck reader environment with the kinds of the newly-introduced type variables of a binding.
withTyVarsOfBindings :: Foldable f => f (Binding TyName name uni fun ann) -> TypeCheckM uni fun c e res -> TypeCheckM uni fun c e res
withTyVarsOfBindings :: f (Binding TyName name uni fun ann)
-> TypeCheckM uni fun c e res -> TypeCheckM uni fun c e res
withTyVarsOfBindings = (TypeCheckM uni fun c e res
 -> f (Binding TyName name uni fun ann)
 -> TypeCheckM uni fun c e res)
-> f (Binding TyName name uni fun ann)
-> TypeCheckM uni fun c e res
-> TypeCheckM uni fun c e res
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((TypeCheckM uni fun c e res
  -> f (Binding TyName name uni fun ann)
  -> TypeCheckM uni fun c e res)
 -> f (Binding TyName name uni fun ann)
 -> TypeCheckM uni fun c e res
 -> TypeCheckM uni fun c e res)
-> (TypeCheckM uni fun c e res
    -> f (Binding TyName name uni fun ann)
    -> TypeCheckM uni fun c e res)
-> f (Binding TyName name uni fun ann)
-> TypeCheckM uni fun c e res
-> TypeCheckM uni fun c e res
forall a b. (a -> b) -> a -> b
$ (Binding TyName name uni fun ann
 -> TypeCheckM uni fun c e res -> TypeCheckM uni fun c e res)
-> TypeCheckM uni fun c e res
-> f (Binding TyName name uni fun ann)
-> TypeCheckM uni fun c e res
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Binding TyName name uni fun ann
-> TypeCheckM uni fun c e res -> TypeCheckM uni fun c e res
forall name (uni :: * -> *) fun ann c e res.
Binding TyName name uni fun ann
-> TypeCheckM uni fun c e res -> TypeCheckM uni fun c e res
withTyVarsOfBinding

-- | Helper to add type variables into a computation's environment.
withTyVarDecls :: [TyVarDecl TyName ann] -> TypeCheckM uni fun c e a -> TypeCheckM uni fun c e a
withTyVarDecls :: [TyVarDecl TyName ann]
-> TypeCheckM uni fun c e a -> TypeCheckM uni fun c e a
withTyVarDecls = (TypeCheckM uni fun c e a
 -> [TyVarDecl TyName ann] -> TypeCheckM uni fun c e a)
-> [TyVarDecl TyName ann]
-> TypeCheckM uni fun c e a
-> TypeCheckM uni fun c e a
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((TypeCheckM uni fun c e a
  -> [TyVarDecl TyName ann] -> TypeCheckM uni fun c e a)
 -> [TyVarDecl TyName ann]
 -> TypeCheckM uni fun c e a
 -> TypeCheckM uni fun c e a)
-> ((TyVarDecl TyName ann
     -> TypeCheckM uni fun c e a -> TypeCheckM uni fun c e a)
    -> TypeCheckM uni fun c e a
    -> [TyVarDecl TyName ann]
    -> TypeCheckM uni fun c e a)
-> (TyVarDecl TyName ann
    -> TypeCheckM uni fun c e a -> TypeCheckM uni fun c e a)
-> [TyVarDecl TyName ann]
-> TypeCheckM uni fun c e a
-> TypeCheckM uni fun c e a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TyVarDecl TyName ann
 -> TypeCheckM uni fun c e a -> TypeCheckM uni fun c e a)
-> TypeCheckM uni fun c e a
-> [TyVarDecl TyName ann]
-> TypeCheckM uni fun c e a
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((TyVarDecl TyName ann
  -> TypeCheckM uni fun c e a -> TypeCheckM uni fun c e a)
 -> [TyVarDecl TyName ann]
 -> TypeCheckM uni fun c e a
 -> TypeCheckM uni fun c e a)
-> (TyVarDecl TyName ann
    -> TypeCheckM uni fun c e a -> TypeCheckM uni fun c e a)
-> [TyVarDecl TyName ann]
-> TypeCheckM uni fun c e a
-> TypeCheckM uni fun c e a
forall a b. (a -> b) -> a -> b
$ \(TyVarDecl ann
_ TyName
n Kind ann
k) -> TyName
-> Kind () -> TypeCheckM uni fun c e a -> TypeCheckM uni fun c e a
forall (uni :: * -> *) fun cfg err a.
TyName
-> Kind ()
-> TypeCheckM uni fun cfg err a
-> TypeCheckM uni fun cfg err a
withTyVar TyName
n (Kind () -> TypeCheckM uni fun c e a -> TypeCheckM uni fun c e a)
-> Kind () -> TypeCheckM uni fun c e a -> TypeCheckM uni fun c e a
forall a b. (a -> b) -> a -> b
$ Kind ann -> Kind ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Kind ann
k