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

{-# LANGUAGE ConstraintKinds    #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE LambdaCase         #-}
{-# LANGUAGE OverloadedStrings  #-}
{-# LANGUAGE RankNTypes         #-}
module PlutusIR.TypeCheck.Internal
    ( BuiltinTypes (..)
    , TypeCheckConfig (..)
    , TypeCheckT
    , MonadKindCheck
    , MonadTypeCheck
    , MonadTypeCheckPir
    , tccBuiltinTypes
    , PirTCConfig (..)
    , AllowEscape (..)
    , inferTypeM
    , checkTypeM
    , runTypeCheckM
    ) where


import PlutusPrelude

import PlutusIR
import PlutusIR.Compiler.Datatype
import PlutusIR.Compiler.Provenance
import PlutusIR.Compiler.Types
import PlutusIR.Error
import PlutusIR.MkPir qualified as PIR
import PlutusIR.Transform.Rename ()

import PlutusCore (toPatFuncKind, tyVarDeclName, typeAnn)
import PlutusCore.Core qualified as PLC
import PlutusCore.Error as PLC
import PlutusCore.MkPlc (mkIterTyFun)
-- we mirror inferTypeM, checkTypeM of plc-tc and extend it for plutus-ir terms
import PlutusCore.TypeCheck.Internal hiding (checkTypeM, inferTypeM, runTypeCheckM)

import Control.Monad (when)
import Control.Monad.Error.Lens
import Data.Text qualified as Text
-- Using @transformers@ rather than @mtl@, because the former doesn't impose the 'Monad' constraint
-- on 'local'.
import Control.Lens ((^?))
import Control.Monad.Trans.Reader
import Data.Foldable
import Data.List.Extras (wix)
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 accommodate for the new pir type-errors.
These modifications are currently necessary 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 [Typing rules] 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 m = TypeCheckT uni fun (PirTCConfig uni fun) m

-- | The constraints that are required for type checking Plutus IR.
type MonadTypeCheckPir err uni fun ann m =
    ( MonadTypeCheck err (Term TyName Name uni fun ()) uni fun ann m
    , AsTypeErrorExt err uni ann  -- Plutus IR has additional type errors, see 'TypeErrorExt'.
    )

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

-- See Note [Global uniqueness in the type checker].
-- See Note [Typing rules].
-- | Check a 'Term' against a 'NormalizedType'.
checkTypeM
    :: MonadTypeCheckPir err uni fun ann m
    => ann
    -> Term TyName Name uni fun ann
    -> Normalized (Type TyName uni ())
    -> PirTCEnv uni fun m ()

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

-- See Note [Global uniqueness in the type checker].
-- See Note [Typing rules].
-- | Synthesize the type of a term, returning a normalized type.
inferTypeM
    :: forall err m uni fun ann.
       MonadTypeCheckPir err uni fun ann m
    => Term TyName Name uni fun ann -> PirTCEnv uni fun m (Normalized (Type TyName uni ()))
-- c : vTy
-- -------------------------
-- [infer| G !- con c : vTy]
inferTypeM :: forall err (m :: * -> *) (uni :: * -> *) fun ann.
MonadTypeCheckPir err uni fun ann m =>
Term TyName Name uni fun ann
-> PirTCEnv uni fun m (Normalized (Type TyName uni ()))
inferTypeM (Constant ann
_ (Some (ValueOf uni (Esc a)
uni a
_))) =
    -- See Note [Normalization of built-in types].
    Type TyName uni ()
-> TypeCheckT
     uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ()))
forall (uni :: * -> *) (m :: * -> *) ann fun cfg.
MonadNormalizeType uni m =>
Type TyName uni ann
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ann))
normalizeTypeM (Type TyName uni ()
 -> TypeCheckT
      uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ())))
-> Type TyName uni ()
-> TypeCheckT
     uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ()))
forall a b. (a -> b) -> a -> b
$ () -> uni (Esc a) -> Type TyName uni ()
forall k (a :: k) (uni :: * -> *) tyname ann.
ann -> uni (Esc a) -> Type tyname uni ann
PIR.mkTyBuiltinOf () uni (Esc a)
uni

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

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

-- [check| G !- dom :: *]    dom ~> vDom    [infer| G , n : dom !- body : vCod]
-- ----------------------------------------------------------------------------
-- [infer| G !- lam n dom body : vDom -> vCod]
inferTypeM (LamAbs ann
ann Name
n Type TyName uni ann
dom Term TyName Name uni fun ann
body)  = do
    ann
-> Type TyName uni ann
-> Kind ()
-> TypeCheckT uni fun (PirTCConfig uni fun) m ()
forall err term (uni :: * -> *) fun ann (m :: * -> *) cfg.
(MonadKindCheck err term uni fun ann m, HasKindCheckConfig cfg) =>
ann
-> Type TyName uni ann -> Kind () -> TypeCheckT uni fun cfg m ()
checkKindM ann
ann Type TyName uni ann
dom (Kind () -> TypeCheckT uni fun (PirTCConfig uni fun) m ())
-> Kind () -> TypeCheckT uni fun (PirTCConfig uni fun) m ()
forall a b. (a -> b) -> a -> b
$ () -> Kind ()
forall ann. ann -> Kind ann
Type ()
    Normalized (Type TyName uni ())
vDom <- Type TyName uni ()
-> TypeCheckT
     uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ()))
forall (uni :: * -> *) (m :: * -> *) ann fun cfg.
MonadNormalizeType uni m =>
Type TyName uni ann
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ann))
normalizeTypeM (Type TyName uni ()
 -> TypeCheckT
      uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ())))
-> Type TyName uni ()
-> TypeCheckT
     uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ()))
forall a b. (a -> b) -> a -> b
$ Type TyName uni ann -> Type TyName uni ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Type TyName uni ann
dom
    ()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () (Type TyName uni () -> Type TyName uni () -> Type TyName uni ())
-> TypeCheckT
     uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ()))
-> ReaderT
     (TypeCheckEnv uni fun (PirTCConfig uni fun))
     m
     (Normalized (Type TyName uni () -> Type TyName uni ()))
forall (f1 :: * -> *) (f2 :: * -> *) a b.
(Functor f1, Functor f2) =>
(a -> b) -> f1 (f2 a) -> f1 (f2 b)
<<$>> Normalized (Type TyName uni ())
-> TypeCheckT
     uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ()))
forall a.
a -> ReaderT (TypeCheckEnv uni fun (PirTCConfig uni fun)) m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Normalized (Type TyName uni ())
vDom ReaderT
  (TypeCheckEnv uni fun (PirTCConfig uni fun))
  m
  (Normalized (Type TyName uni () -> Type TyName uni ()))
-> TypeCheckT
     uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ()))
-> TypeCheckT
     uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ()))
forall (f1 :: * -> *) (f2 :: * -> *) a b.
(Applicative f1, Applicative f2) =>
f1 (f2 (a -> b)) -> f1 (f2 a) -> f1 (f2 b)
<<*>> Name
-> Normalized (Type TyName uni ())
-> TypeCheckT
     uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ()))
-> TypeCheckT
     uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ()))
forall (uni :: * -> *) fun cfg (m :: * -> *) a.
Name
-> Normalized (Type TyName uni ())
-> TypeCheckT uni fun cfg m a
-> TypeCheckT uni fun cfg m a
withVar Name
n Normalized (Type TyName uni ())
vDom (Term TyName Name uni fun ann
-> TypeCheckT
     uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ()))
forall err (m :: * -> *) (uni :: * -> *) fun ann.
MonadTypeCheckPir err uni fun ann m =>
Term TyName Name uni fun ann
-> PirTCEnv uni fun m (Normalized (Type TyName uni ()))
inferTypeM Term TyName Name uni fun ann
body)

-- [infer| G , n :: nK !- body : vBodyTy]
-- ---------------------------------------------------
-- [infer| G !- abs n nK body : all (n :: nK) vBodyTy]
inferTypeM (TyAbs ann
_ TyName
n Kind ann
nK Term TyName Name uni fun ann
body)      = do
    let nK_ :: Kind ()
nK_ = Kind ann -> Kind ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Kind ann
nK
    () -> TyName -> Kind () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyForall () TyName
n Kind ()
nK_ (Type TyName uni () -> Type TyName uni ())
-> TypeCheckT
     uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ()))
-> TypeCheckT
     uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ()))
forall (f1 :: * -> *) (f2 :: * -> *) a b.
(Functor f1, Functor f2) =>
(a -> b) -> f1 (f2 a) -> f1 (f2 b)
<<$>> TyName
-> Kind ()
-> TypeCheckT
     uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ()))
-> TypeCheckT
     uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ()))
forall (uni :: * -> *) fun cfg (m :: * -> *) a.
TyName
-> Kind ()
-> TypeCheckT uni fun cfg m a
-> TypeCheckT uni fun cfg m a
withTyVar TyName
n Kind ()
nK_ (Term TyName Name uni fun ann
-> TypeCheckT
     uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ()))
forall err (m :: * -> *) (uni :: * -> *) fun ann.
MonadTypeCheckPir err uni fun ann m =>
Term TyName Name uni fun ann
-> PirTCEnv uni fun m (Normalized (Type TyName uni ()))
inferTypeM Term TyName Name uni fun ann
body)

-- [infer| G !- fun : vDom -> vCod]    [check| G !- arg : vDom]
-- ------------------------------------------------------------
-- [infer| G !- fun arg : vCod]
inferTypeM (Apply ann
ann Term TyName Name uni fun ann
fun Term TyName Name uni fun ann
arg)      = do
    Normalized (Type TyName uni ())
vFunTy <- Term TyName Name uni fun ann
-> TypeCheckT
     uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ()))
forall err (m :: * -> *) (uni :: * -> *) fun ann.
MonadTypeCheckPir err uni fun ann m =>
Term TyName Name uni fun ann
-> PirTCEnv uni fun m (Normalized (Type TyName uni ()))
inferTypeM Term TyName Name uni fun ann
fun
    case Normalized (Type TyName uni ()) -> Type TyName uni ()
forall a. Normalized a -> a
unNormalized Normalized (Type TyName uni ())
vFunTy of
        TyFun ()
_ Type TyName uni ()
vDom Type TyName uni ()
vCod -> do
            -- Subparts of a normalized type, so normalized.
            ann
-> Term TyName Name uni fun ann
-> Normalized (Type TyName uni ())
-> TypeCheckT uni fun (PirTCConfig uni fun) m ()
forall err (uni :: * -> *) fun ann (m :: * -> *).
MonadTypeCheckPir err uni fun ann m =>
ann
-> Term TyName Name uni fun ann
-> Normalized (Type TyName uni ())
-> PirTCEnv uni fun m ()
checkTypeM ann
ann Term TyName Name uni fun ann
arg (Normalized (Type TyName uni ())
 -> TypeCheckT uni fun (PirTCConfig uni fun) m ())
-> Normalized (Type TyName uni ())
-> TypeCheckT uni fun (PirTCConfig uni fun) m ()
forall a b. (a -> b) -> a -> b
$ Type TyName uni () -> Normalized (Type TyName uni ())
forall a. a -> Normalized a
Normalized Type TyName uni ()
vDom
            Normalized (Type TyName uni ())
-> TypeCheckT
     uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ()))
forall a.
a -> ReaderT (TypeCheckEnv uni fun (PirTCConfig uni fun)) m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Normalized (Type TyName uni ())
 -> TypeCheckT
      uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ())))
-> Normalized (Type TyName uni ())
-> TypeCheckT
     uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ()))
forall a b. (a -> b) -> a -> b
$ Type TyName uni () -> Normalized (Type TyName uni ())
forall a. a -> Normalized a
Normalized Type TyName uni ()
vCod
        Type TyName uni ()
_ -> do
            let expectedTyFun :: ExpectedShapeOr a
expectedTyFun = Text -> [Text] -> ExpectedShapeOr a
forall a. Text -> [Text] -> ExpectedShapeOr a
ExpectedShape Text
"fun k l" [Text
"k", Text
"l"]
            AReview err (TypeError (Term TyName Name uni fun ()) uni fun ann)
-> TypeError (Term TyName Name uni fun ()) uni fun ann
-> TypeCheckT
     uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ()))
forall e (m :: * -> *) t x.
MonadError e m =>
AReview e t -> t -> m x
throwing AReview err (TypeError (Term TyName Name uni fun ()) uni fun ann)
forall r term (uni :: * -> *) fun ann.
AsTypeError r term uni fun ann =>
Prism' r (TypeError term uni fun ann)
Prism' err (TypeError (Term TyName Name uni fun ()) uni fun ann)
_TypeError (TypeError (Term TyName Name uni fun ()) uni fun ann
 -> TypeCheckT
      uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ())))
-> TypeError (Term TyName Name uni fun ()) uni fun ann
-> TypeCheckT
     uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ()))
forall a b. (a -> b) -> a -> b
$ ann
-> Term TyName Name uni fun ()
-> ExpectedShapeOr (Type TyName uni ())
-> Normalized (Type TyName uni ())
-> TypeError (Term TyName Name uni fun ()) uni fun ann
forall term (uni :: * -> *) fun ann.
ann
-> term
-> ExpectedShapeOr (Type TyName uni ())
-> Normalized (Type TyName uni ())
-> TypeError term uni fun ann
TypeMismatch ann
ann (Term TyName Name uni fun ann -> Term TyName Name uni fun ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Term TyName Name uni fun ann
fun) ExpectedShapeOr (Type TyName uni ())
forall {a}. ExpectedShapeOr a
expectedTyFun Normalized (Type TyName uni ())
vFunTy

-- [infer| G !- body : all (n :: nK) vCod]    [check| G !- ty :: tyK]    ty ~> vTy
-- -------------------------------------------------------------------------------
-- [infer| G !- body {ty} : NORM ([vTy / n] vCod)]
inferTypeM (TyInst ann
ann Term TyName Name uni fun ann
body Type TyName uni ann
ty)     = do
    Normalized (Type TyName uni ())
vBodyTy <- Term TyName Name uni fun ann
-> TypeCheckT
     uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ()))
forall err (m :: * -> *) (uni :: * -> *) fun ann.
MonadTypeCheckPir err uni fun ann m =>
Term TyName Name uni fun ann
-> PirTCEnv uni fun m (Normalized (Type TyName uni ()))
inferTypeM Term TyName Name uni fun ann
body
    case Normalized (Type TyName uni ()) -> Type TyName uni ()
forall a. Normalized a -> a
unNormalized Normalized (Type TyName uni ())
vBodyTy of
        TyForall ()
_ TyName
n Kind ()
nK Type TyName uni ()
vCod -> do
            ann
-> Type TyName uni ann
-> Kind ()
-> TypeCheckT uni fun (PirTCConfig uni fun) m ()
forall err term (uni :: * -> *) fun ann (m :: * -> *) cfg.
(MonadKindCheck err term uni fun ann m, HasKindCheckConfig cfg) =>
ann
-> Type TyName uni ann -> Kind () -> TypeCheckT uni fun cfg m ()
checkKindM ann
ann Type TyName uni ann
ty Kind ()
nK
            Normalized (Type TyName uni ())
vTy <- Type TyName uni ()
-> TypeCheckT
     uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ()))
forall (uni :: * -> *) (m :: * -> *) ann fun cfg.
MonadNormalizeType uni m =>
Type TyName uni ann
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ann))
normalizeTypeM (Type TyName uni ()
 -> TypeCheckT
      uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ())))
-> Type TyName uni ()
-> TypeCheckT
     uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ()))
forall a b. (a -> b) -> a -> b
$ Type TyName uni ann -> Type TyName uni ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Type TyName uni ann
ty
            Normalized (Type TyName uni ())
-> TyName
-> Type TyName uni ()
-> TypeCheckT
     uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ()))
forall (uni :: * -> *) (m :: * -> *) fun cfg.
MonadNormalizeType uni m =>
Normalized (Type TyName uni ())
-> TyName
-> Type TyName uni ()
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ()))
substNormalizeTypeM Normalized (Type TyName uni ())
vTy TyName
n Type TyName uni ()
vCod
        Type TyName uni ()
_ -> do
            let expectedTyForall :: ExpectedShapeOr a
expectedTyForall = Text -> [Text] -> ExpectedShapeOr a
forall a. Text -> [Text] -> ExpectedShapeOr a
ExpectedShape Text
"all a kind body" [Text
"a", Text
"kind", Text
"body"]
            AReview err (TypeError (Term TyName Name uni fun ()) uni fun ann)
-> TypeError (Term TyName Name uni fun ()) uni fun ann
-> TypeCheckT
     uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ()))
forall e (m :: * -> *) t x.
MonadError e m =>
AReview e t -> t -> m x
throwing AReview err (TypeError (Term TyName Name uni fun ()) uni fun ann)
forall r term (uni :: * -> *) fun ann.
AsTypeError r term uni fun ann =>
Prism' r (TypeError term uni fun ann)
Prism' err (TypeError (Term TyName Name uni fun ()) uni fun ann)
_TypeError (ann
-> Term TyName Name uni fun ()
-> ExpectedShapeOr (Type TyName uni ())
-> Normalized (Type TyName uni ())
-> TypeError (Term TyName Name uni fun ()) uni fun ann
forall term (uni :: * -> *) fun ann.
ann
-> term
-> ExpectedShapeOr (Type TyName uni ())
-> Normalized (Type TyName uni ())
-> TypeError term uni fun ann
TypeMismatch ann
ann (Term TyName Name uni fun ann -> Term TyName Name uni fun ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Term TyName Name uni fun ann
body) ExpectedShapeOr (Type TyName uni ())
forall {a}. ExpectedShapeOr a
expectedTyForall Normalized (Type TyName uni ())
vBodyTy)

-- [infer| G !- arg :: k]    [check| G !- pat :: (k -> *) -> k -> *]    pat ~> vPat    arg ~> vArg
-- [check| G !- term : NORM (vPat (\(a :: k) -> ifix vPat a) vArg)]
-- -----------------------------------------------------------------------------------------------
-- [infer| G !- iwrap pat arg term : ifix vPat vArg]
inferTypeM (IWrap ann
ann Type TyName uni ann
pat Type TyName uni ann
arg Term TyName Name uni fun ann
term) = do
    Kind ()
k <- Type TyName uni ann
-> TypeCheckT uni fun (PirTCConfig uni fun) m (Kind ())
forall err term (uni :: * -> *) fun ann (m :: * -> *) cfg.
(MonadKindCheck err term uni fun ann m, HasKindCheckConfig cfg) =>
Type TyName uni ann -> TypeCheckT uni fun cfg m (Kind ())
inferKindM Type TyName uni ann
arg
    ann
-> Type TyName uni ann
-> Kind ()
-> TypeCheckT uni fun (PirTCConfig uni fun) m ()
forall err term (uni :: * -> *) fun ann (m :: * -> *) cfg.
(MonadKindCheck err term uni fun ann m, HasKindCheckConfig cfg) =>
ann
-> Type TyName uni ann -> Kind () -> TypeCheckT uni fun cfg m ()
checkKindM ann
ann Type TyName uni ann
pat (Kind () -> TypeCheckT uni fun (PirTCConfig uni fun) m ())
-> Kind () -> TypeCheckT uni fun (PirTCConfig uni fun) m ()
forall a b. (a -> b) -> a -> b
$ Kind () -> Kind ()
toPatFuncKind Kind ()
k
    Normalized (Type TyName uni ())
vPat <- Type TyName uni ()
-> TypeCheckT
     uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ()))
forall (uni :: * -> *) (m :: * -> *) ann fun cfg.
MonadNormalizeType uni m =>
Type TyName uni ann
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ann))
normalizeTypeM (Type TyName uni ()
 -> TypeCheckT
      uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ())))
-> Type TyName uni ()
-> TypeCheckT
     uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ()))
forall a b. (a -> b) -> a -> b
$ Type TyName uni ann -> Type TyName uni ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Type TyName uni ann
pat
    Normalized (Type TyName uni ())
vArg <- Type TyName uni ()
-> TypeCheckT
     uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ()))
forall (uni :: * -> *) (m :: * -> *) ann fun cfg.
MonadNormalizeType uni m =>
Type TyName uni ann
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ann))
normalizeTypeM (Type TyName uni ()
 -> TypeCheckT
      uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ())))
-> Type TyName uni ()
-> TypeCheckT
     uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ()))
forall a b. (a -> b) -> a -> b
$ Type TyName uni ann -> Type TyName uni ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Type TyName uni ann
arg
    ann
-> Term TyName Name uni fun ann
-> Normalized (Type TyName uni ())
-> TypeCheckT uni fun (PirTCConfig uni fun) m ()
forall err (uni :: * -> *) fun ann (m :: * -> *).
MonadTypeCheckPir err uni fun ann m =>
ann
-> Term TyName Name uni fun ann
-> Normalized (Type TyName uni ())
-> PirTCEnv uni fun m ()
checkTypeM ann
ann Term TyName Name uni fun ann
term (Normalized (Type TyName uni ())
 -> TypeCheckT uni fun (PirTCConfig uni fun) m ())
-> TypeCheckT
     uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ()))
-> TypeCheckT uni fun (PirTCConfig uni fun) m ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Normalized (Type TyName uni ())
-> Normalized (Type TyName uni ())
-> Kind ()
-> TypeCheckT
     uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ()))
forall (uni :: * -> *) (m :: * -> *) fun cfg.
MonadNormalizeType uni m =>
Normalized (Type TyName uni ())
-> Normalized (Type TyName uni ())
-> Kind ()
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ()))
unfoldIFixOf Normalized (Type TyName uni ())
vPat Normalized (Type TyName uni ())
vArg Kind ()
k
    Normalized (Type TyName uni ())
-> TypeCheckT
     uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ()))
forall a.
a -> ReaderT (TypeCheckEnv uni fun (PirTCConfig uni fun)) m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Normalized (Type TyName uni ())
 -> TypeCheckT
      uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ())))
-> Normalized (Type TyName uni ())
-> TypeCheckT
     uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ()))
forall a b. (a -> b) -> a -> b
$ ()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyIFix () (Type TyName uni () -> Type TyName uni () -> Type TyName uni ())
-> Normalized (Type TyName uni ())
-> Normalized (Type TyName uni () -> Type TyName uni ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Normalized (Type TyName uni ())
vPat Normalized (Type TyName uni () -> Type TyName uni ())
-> Normalized (Type TyName uni ())
-> Normalized (Type TyName uni ())
forall a b. Normalized (a -> b) -> Normalized a -> Normalized b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Normalized (Type TyName uni ())
vArg

-- [infer| G !- term : ifix vPat vArg]    [infer| G !- vArg :: k]
-- -----------------------------------------------------------------------
-- [infer| G !- unwrap term : NORM (vPat (\(a :: k) -> ifix vPat a) vArg)]
inferTypeM (Unwrap ann
ann Term TyName Name uni fun ann
term)        = do
    Normalized (Type TyName uni ())
vTermTy <- Term TyName Name uni fun ann
-> TypeCheckT
     uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ()))
forall err (m :: * -> *) (uni :: * -> *) fun ann.
MonadTypeCheckPir err uni fun ann m =>
Term TyName Name uni fun ann
-> PirTCEnv uni fun m (Normalized (Type TyName uni ()))
inferTypeM Term TyName Name uni fun ann
term
    case Normalized (Type TyName uni ()) -> Type TyName uni ()
forall a. Normalized a -> a
unNormalized Normalized (Type TyName uni ())
vTermTy of
        TyIFix ()
_ Type TyName uni ()
vPat Type TyName uni ()
vArg -> do
            Kind ()
k <- Type TyName uni ann
-> TypeCheckT uni fun (PirTCConfig uni fun) m (Kind ())
forall err term (uni :: * -> *) fun ann (m :: * -> *) cfg.
(MonadKindCheck err term uni fun ann m, HasKindCheckConfig cfg) =>
Type TyName uni ann -> TypeCheckT uni fun cfg m (Kind ())
inferKindM (Type TyName uni ann
 -> TypeCheckT uni fun (PirTCConfig uni fun) m (Kind ()))
-> Type TyName uni ann
-> TypeCheckT uni fun (PirTCConfig uni fun) m (Kind ())
forall a b. (a -> b) -> a -> b
$ ann
ann ann -> Type TyName uni () -> Type TyName uni ann
forall a b. a -> Type TyName uni b -> Type TyName uni a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Type TyName uni ()
vArg
            -- Subparts of a normalized type, so normalized.
            Normalized (Type TyName uni ())
-> Normalized (Type TyName uni ())
-> Kind ()
-> TypeCheckT
     uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ()))
forall (uni :: * -> *) (m :: * -> *) fun cfg.
MonadNormalizeType uni m =>
Normalized (Type TyName uni ())
-> Normalized (Type TyName uni ())
-> Kind ()
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ()))
unfoldIFixOf (Type TyName uni () -> Normalized (Type TyName uni ())
forall a. a -> Normalized a
Normalized Type TyName uni ()
vPat) (Type TyName uni () -> Normalized (Type TyName uni ())
forall a. a -> Normalized a
Normalized Type TyName uni ()
vArg) Kind ()
k
        Type TyName uni ()
_                  -> do
            let expectedTyIFix :: ExpectedShapeOr a
expectedTyIFix = Text -> [Text] -> ExpectedShapeOr a
forall a. Text -> [Text] -> ExpectedShapeOr a
ExpectedShape Text
"ifix pat arg" [Text
"pat", Text
"arg"]
            AReview err (TypeError (Term TyName Name uni fun ()) uni fun ann)
-> TypeError (Term TyName Name uni fun ()) uni fun ann
-> TypeCheckT
     uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ()))
forall e (m :: * -> *) t x.
MonadError e m =>
AReview e t -> t -> m x
throwing AReview err (TypeError (Term TyName Name uni fun ()) uni fun ann)
forall r term (uni :: * -> *) fun ann.
AsTypeError r term uni fun ann =>
Prism' r (TypeError term uni fun ann)
Prism' err (TypeError (Term TyName Name uni fun ()) uni fun ann)
_TypeError (ann
-> Term TyName Name uni fun ()
-> ExpectedShapeOr (Type TyName uni ())
-> Normalized (Type TyName uni ())
-> TypeError (Term TyName Name uni fun ()) uni fun ann
forall term (uni :: * -> *) fun ann.
ann
-> term
-> ExpectedShapeOr (Type TyName uni ())
-> Normalized (Type TyName uni ())
-> TypeError term uni fun ann
TypeMismatch ann
ann (Term TyName Name uni fun ann -> Term TyName Name uni fun ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Term TyName Name uni fun ann
term) ExpectedShapeOr (Type TyName uni ())
forall {a}. ExpectedShapeOr a
expectedTyIFix Normalized (Type TyName uni ())
vTermTy)

-- [check| G !- ty :: *]    ty ~> vTy
-- ----------------------------------
-- [infer| G !- error ty : vTy]
inferTypeM (Error ann
ann Type TyName uni ann
ty)           = do
    ann
-> Type TyName uni ann
-> Kind ()
-> TypeCheckT uni fun (PirTCConfig uni fun) m ()
forall err term (uni :: * -> *) fun ann (m :: * -> *) cfg.
(MonadKindCheck err term uni fun ann m, HasKindCheckConfig cfg) =>
ann
-> Type TyName uni ann -> Kind () -> TypeCheckT uni fun cfg m ()
checkKindM ann
ann Type TyName uni ann
ty (Kind () -> TypeCheckT uni fun (PirTCConfig uni fun) m ())
-> Kind () -> TypeCheckT uni fun (PirTCConfig uni fun) m ()
forall a b. (a -> b) -> a -> b
$ () -> Kind ()
forall ann. ann -> Kind ann
Type ()
    Type TyName uni ()
-> TypeCheckT
     uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ()))
forall (uni :: * -> *) (m :: * -> *) ann fun cfg.
MonadNormalizeType uni m =>
Type TyName uni ann
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ann))
normalizeTypeM (Type TyName uni ()
 -> TypeCheckT
      uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ())))
-> Type TyName uni ()
-> TypeCheckT
     uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ()))
forall a b. (a -> b) -> a -> b
$ Type TyName uni ann -> Type TyName uni ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Type TyName uni ann
ty

-- resTy ~> vResTy     vResTy = sop s_0 ... s_i ... s_n
-- s_i = [p_i_0 ... p_i_m]   [check| G !- t_0 : p_i_0] ... [check| G !- t_m : p_i_m]
-- ---------------------------------------------------------------------------------
-- [infer| G !- constr resTy i t_0 ... t_m : vResTy]
inferTypeM t :: Term TyName Name uni fun ann
t@(Constr ann
ann Type TyName uni ann
resTy Word64
i [Term TyName Name uni fun ann]
args) = do
    Normalized (Type TyName uni ())
vResTy <- Type TyName uni ()
-> TypeCheckT
     uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ()))
forall (uni :: * -> *) (m :: * -> *) ann fun cfg.
MonadNormalizeType uni m =>
Type TyName uni ann
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ann))
normalizeTypeM (Type TyName uni ()
 -> TypeCheckT
      uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ())))
-> Type TyName uni ()
-> TypeCheckT
     uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ()))
forall a b. (a -> b) -> a -> b
$ Type TyName uni ann -> Type TyName uni ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Type TyName uni ann
resTy

    -- We don't know exactly what to expect, we only know what the i-th sum should look like, so we
    -- assert that we should have some types in the sum up to there, and then the known product type.
    let prodPrefix :: [Text]
prodPrefix  = (Word64 -> Text) -> [Word64] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map (\Word64
j -> Text
"prod_" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
Text.pack (Word64 -> String
forall a. Show a => a -> String
show Word64
j)) [Word64
0 .. Word64
i Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
- Word64
1]
        fields :: [Text]
fields      = (Int -> Text) -> [Int] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map (\Int
k -> Text
"field_" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
Text.pack (Int -> String
forall a. Show a => a -> String
show Int
k)) [Int
0 .. [Term TyName Name uni fun ann] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term TyName Name uni fun ann]
args Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]
        prod_i :: Text
prod_i      = Text
"[" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text -> [Text] -> Text
Text.intercalate Text
" " [Text]
fields Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"]"
        shape :: Text
shape       = Text
"sop " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> (Text -> Text) -> [Text] -> Text
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" ") [Text]
prodPrefix Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
prod_i Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" ... prod_n"
        vars :: [Text]
vars        = [Text]
prodPrefix [Text] -> [Text] -> [Text]
forall a. [a] -> [a] -> [a]
++ [Text]
fields [Text] -> [Text] -> [Text]
forall a. [a] -> [a] -> [a]
++ [Text
"prod_n"]
        expectedSop :: ExpectedShapeOr a
expectedSop = Text -> [Text] -> ExpectedShapeOr a
forall a. Text -> [Text] -> ExpectedShapeOr a
ExpectedShape Text
shape [Text]
vars
    case Normalized (Type TyName uni ()) -> Type TyName uni ()
forall a. Normalized a -> a
unNormalized Normalized (Type TyName uni ())
vResTy of
        TySOP ()
_ [[Type TyName uni ()]]
vSTys -> case [[Type TyName uni ()]]
vSTys [[Type TyName uni ()]]
-> Getting
     (First [Type TyName uni ()])
     [[Type TyName uni ()]]
     [Type TyName uni ()]
-> Maybe [Type TyName uni ()]
forall s a. s -> Getting (First a) s a -> Maybe a
^? Word64 -> Traversal' [[Type TyName uni ()]] [Type TyName uni ()]
forall a. Word64 -> Traversal' [a] a
wix Word64
i of
            Just [Type TyName uni ()]
pTys -> case [Term TyName Name uni fun ann]
-> [Type TyName uni ()]
-> Maybe [(Term TyName Name uni fun ann, Type TyName uni ())]
forall a b. [a] -> [b] -> Maybe [(a, b)]
zipExact [Term TyName Name uni fun ann]
args [Type TyName uni ()]
pTys of
                -- pTy is a sub-part of a normalized type, so normalized
                Just [(Term TyName Name uni fun ann, Type TyName uni ())]
ps -> [(Term TyName Name uni fun ann, Type TyName uni ())]
-> ((Term TyName Name uni fun ann, Type TyName uni ())
    -> TypeCheckT uni fun (PirTCConfig uni fun) m ())
-> TypeCheckT uni fun (PirTCConfig uni fun) m ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ [(Term TyName Name uni fun ann, Type TyName uni ())]
ps (((Term TyName Name uni fun ann, Type TyName uni ())
  -> TypeCheckT uni fun (PirTCConfig uni fun) m ())
 -> TypeCheckT uni fun (PirTCConfig uni fun) m ())
-> ((Term TyName Name uni fun ann, Type TyName uni ())
    -> TypeCheckT uni fun (PirTCConfig uni fun) m ())
-> TypeCheckT uni fun (PirTCConfig uni fun) m ()
forall a b. (a -> b) -> a -> b
$ \(Term TyName Name uni fun ann
arg, Type TyName uni ()
pTy) -> ann
-> Term TyName Name uni fun ann
-> Normalized (Type TyName uni ())
-> TypeCheckT uni fun (PirTCConfig uni fun) m ()
forall err (uni :: * -> *) fun ann (m :: * -> *).
MonadTypeCheckPir err uni fun ann m =>
ann
-> Term TyName Name uni fun ann
-> Normalized (Type TyName uni ())
-> PirTCEnv uni fun m ()
checkTypeM ann
ann Term TyName Name uni fun ann
arg (Type TyName uni () -> Normalized (Type TyName uni ())
forall a. a -> Normalized a
Normalized Type TyName uni ()
pTy)
                -- the number of args does not match the number of types in the i'th SOP
                -- alternative
                Maybe [(Term TyName Name uni fun ann, Type TyName uni ())]
Nothing -> AReview err (TypeError (Term TyName Name uni fun ()) uni fun ann)
-> TypeError (Term TyName Name uni fun ()) uni fun ann
-> TypeCheckT uni fun (PirTCConfig uni fun) m ()
forall e (m :: * -> *) t x.
MonadError e m =>
AReview e t -> t -> m x
throwing AReview err (TypeError (Term TyName Name uni fun ()) uni fun ann)
forall r term (uni :: * -> *) fun ann.
AsTypeError r term uni fun ann =>
Prism' r (TypeError term uni fun ann)
Prism' err (TypeError (Term TyName Name uni fun ()) uni fun ann)
_TypeError (ann
-> Term TyName Name uni fun ()
-> ExpectedShapeOr (Type TyName uni ())
-> Normalized (Type TyName uni ())
-> TypeError (Term TyName Name uni fun ()) uni fun ann
forall term (uni :: * -> *) fun ann.
ann
-> term
-> ExpectedShapeOr (Type TyName uni ())
-> Normalized (Type TyName uni ())
-> TypeError term uni fun ann
TypeMismatch ann
ann (Term TyName Name uni fun ann -> Term TyName Name uni fun ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Term TyName Name uni fun ann
t) ExpectedShapeOr (Type TyName uni ())
forall {a}. ExpectedShapeOr a
expectedSop Normalized (Type TyName uni ())
vResTy)
            -- result type does not contain an i'th sum alternative
            Maybe [Type TyName uni ()]
Nothing -> AReview err (TypeError (Term TyName Name uni fun ()) uni fun ann)
-> TypeError (Term TyName Name uni fun ()) uni fun ann
-> TypeCheckT uni fun (PirTCConfig uni fun) m ()
forall e (m :: * -> *) t x.
MonadError e m =>
AReview e t -> t -> m x
throwing AReview err (TypeError (Term TyName Name uni fun ()) uni fun ann)
forall r term (uni :: * -> *) fun ann.
AsTypeError r term uni fun ann =>
Prism' r (TypeError term uni fun ann)
Prism' err (TypeError (Term TyName Name uni fun ()) uni fun ann)
_TypeError (ann
-> Term TyName Name uni fun ()
-> ExpectedShapeOr (Type TyName uni ())
-> Normalized (Type TyName uni ())
-> TypeError (Term TyName Name uni fun ()) uni fun ann
forall term (uni :: * -> *) fun ann.
ann
-> term
-> ExpectedShapeOr (Type TyName uni ())
-> Normalized (Type TyName uni ())
-> TypeError term uni fun ann
TypeMismatch ann
ann (Term TyName Name uni fun ann -> Term TyName Name uni fun ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Term TyName Name uni fun ann
t) ExpectedShapeOr (Type TyName uni ())
forall {a}. ExpectedShapeOr a
expectedSop Normalized (Type TyName uni ())
vResTy)
        -- result type is not a SOP type
        Type TyName uni ()
_ -> AReview err (TypeError (Term TyName Name uni fun ()) uni fun ann)
-> TypeError (Term TyName Name uni fun ()) uni fun ann
-> TypeCheckT uni fun (PirTCConfig uni fun) m ()
forall e (m :: * -> *) t x.
MonadError e m =>
AReview e t -> t -> m x
throwing AReview err (TypeError (Term TyName Name uni fun ()) uni fun ann)
forall r term (uni :: * -> *) fun ann.
AsTypeError r term uni fun ann =>
Prism' r (TypeError term uni fun ann)
Prism' err (TypeError (Term TyName Name uni fun ()) uni fun ann)
_TypeError (ann
-> Term TyName Name uni fun ()
-> ExpectedShapeOr (Type TyName uni ())
-> Normalized (Type TyName uni ())
-> TypeError (Term TyName Name uni fun ()) uni fun ann
forall term (uni :: * -> *) fun ann.
ann
-> term
-> ExpectedShapeOr (Type TyName uni ())
-> Normalized (Type TyName uni ())
-> TypeError term uni fun ann
TypeMismatch ann
ann (Term TyName Name uni fun ann -> Term TyName Name uni fun ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Term TyName Name uni fun ann
t) ExpectedShapeOr (Type TyName uni ())
forall {a}. ExpectedShapeOr a
expectedSop Normalized (Type TyName uni ())
vResTy)

    Normalized (Type TyName uni ())
-> TypeCheckT
     uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ()))
forall a.
a -> ReaderT (TypeCheckEnv uni fun (PirTCConfig uni fun)) m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Normalized (Type TyName uni ())
vResTy

-- resTy ~> vResTy   [infer| G !- scrut : sop s_0 ... s_n]
-- s_0 = [p_0_0 ... p_0_m]   [check| G !- c_0 : p_0_0 -> ... -> p_0_m -> vResTy]
-- ...
-- s_n = [p_n_0 ... p_n_m]   [check| G !- c_n : p_n_0 -> ... -> p_n_m -> vResTy]
-- -----------------------------------------------------------------------------
-- [infer| G !- case resTy scrut c_0 ... c_n : vResTy]
inferTypeM (Case ann
ann Type TyName uni ann
resTy Term TyName Name uni fun ann
scrut [Term TyName Name uni fun ann]
cases) = do
    Normalized (Type TyName uni ())
vResTy <- Type TyName uni ()
-> TypeCheckT
     uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ()))
forall (uni :: * -> *) (m :: * -> *) ann fun cfg.
MonadNormalizeType uni m =>
Type TyName uni ann
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ann))
normalizeTypeM (Type TyName uni ()
 -> TypeCheckT
      uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ())))
-> Type TyName uni ()
-> TypeCheckT
     uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ()))
forall a b. (a -> b) -> a -> b
$ Type TyName uni ann -> Type TyName uni ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Type TyName uni ann
resTy
    Normalized (Type TyName uni ())
vScrutTy <- Term TyName Name uni fun ann
-> TypeCheckT
     uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ()))
forall err (m :: * -> *) (uni :: * -> *) fun ann.
MonadTypeCheckPir err uni fun ann m =>
Term TyName Name uni fun ann
-> PirTCEnv uni fun m (Normalized (Type TyName uni ()))
inferTypeM Term TyName Name uni fun ann
scrut

    -- We don't know exactly what to expect, we only know that it should
    -- be a SOP with the right number of sum alternatives
    let prods :: [Text]
prods = (Int -> Text) -> [Int] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map (\Int
j -> Text
"prod_" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
Text.pack (Int -> String
forall a. Show a => a -> String
show Int
j)) [Int
0 .. [Term TyName Name uni fun ann] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term TyName Name uni fun ann]
cases Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]
        expectedSop :: ExpectedShapeOr a
expectedSop = Text -> [Text] -> ExpectedShapeOr a
forall a. Text -> [Text] -> ExpectedShapeOr a
ExpectedShape (Text -> [Text] -> Text
Text.intercalate Text
" " ([Text] -> Text) -> [Text] -> Text
forall a b. (a -> b) -> a -> b
$ Text
"sop" Text -> [Text] -> [Text]
forall a. a -> [a] -> [a]
: [Text]
prods) [Text]
prods
    case Normalized (Type TyName uni ()) -> Type TyName uni ()
forall a. Normalized a -> a
unNormalized Normalized (Type TyName uni ())
vScrutTy of
        TySOP ()
_ [[Type TyName uni ()]]
sTys -> case [Term TyName Name uni fun ann]
-> [[Type TyName uni ()]]
-> Maybe [(Term TyName Name uni fun ann, [Type TyName uni ()])]
forall a b. [a] -> [b] -> Maybe [(a, b)]
zipExact [Term TyName Name uni fun ann]
cases [[Type TyName uni ()]]
sTys of
            Just [(Term TyName Name uni fun ann, [Type TyName uni ()])]
casesAndArgTypes -> [(Term TyName Name uni fun ann, [Type TyName uni ()])]
-> ((Term TyName Name uni fun ann, [Type TyName uni ()])
    -> TypeCheckT uni fun (PirTCConfig uni fun) m ())
-> TypeCheckT uni fun (PirTCConfig uni fun) m ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ [(Term TyName Name uni fun ann, [Type TyName uni ()])]
casesAndArgTypes (((Term TyName Name uni fun ann, [Type TyName uni ()])
  -> TypeCheckT uni fun (PirTCConfig uni fun) m ())
 -> TypeCheckT uni fun (PirTCConfig uni fun) m ())
-> ((Term TyName Name uni fun ann, [Type TyName uni ()])
    -> TypeCheckT uni fun (PirTCConfig uni fun) m ())
-> TypeCheckT uni fun (PirTCConfig uni fun) m ()
forall a b. (a -> b) -> a -> b
$ \(Term TyName Name uni fun ann
c, [Type TyName uni ()]
argTypes) ->
                -- made of sub-parts of a normalized type, so normalized
                ann
-> Term TyName Name uni fun ann
-> Normalized (Type TyName uni ())
-> TypeCheckT uni fun (PirTCConfig uni fun) m ()
forall err (uni :: * -> *) fun ann (m :: * -> *).
MonadTypeCheckPir err uni fun ann m =>
ann
-> Term TyName Name uni fun ann
-> Normalized (Type TyName uni ())
-> PirTCEnv uni fun m ()
checkTypeM ann
ann Term TyName Name uni fun ann
c (Type TyName uni () -> Normalized (Type TyName uni ())
forall a. a -> Normalized a
Normalized (Type TyName uni () -> Normalized (Type TyName uni ()))
-> Type TyName uni () -> Normalized (Type TyName uni ())
forall a b. (a -> b) -> a -> b
$ ()
-> [Type TyName uni ()] -> Type TyName uni () -> Type TyName uni ()
forall ann tyname (uni :: * -> *).
ann
-> [Type tyname uni ann]
-> Type tyname uni ann
-> Type tyname uni ann
mkIterTyFun () [Type TyName uni ()]
argTypes (Normalized (Type TyName uni ()) -> Type TyName uni ()
forall a. Normalized a -> a
unNormalized Normalized (Type TyName uni ())
vResTy))
            -- scrutinee does not have a SOP type with the right number of alternatives
            -- for the number of cases
            Maybe [(Term TyName Name uni fun ann, [Type TyName uni ()])]
Nothing -> AReview err (TypeError (Term TyName Name uni fun ()) uni fun ann)
-> TypeError (Term TyName Name uni fun ()) uni fun ann
-> TypeCheckT uni fun (PirTCConfig uni fun) m ()
forall e (m :: * -> *) t x.
MonadError e m =>
AReview e t -> t -> m x
throwing AReview err (TypeError (Term TyName Name uni fun ()) uni fun ann)
forall r term (uni :: * -> *) fun ann.
AsTypeError r term uni fun ann =>
Prism' r (TypeError term uni fun ann)
Prism' err (TypeError (Term TyName Name uni fun ()) uni fun ann)
_TypeError (ann
-> Term TyName Name uni fun ()
-> ExpectedShapeOr (Type TyName uni ())
-> Normalized (Type TyName uni ())
-> TypeError (Term TyName Name uni fun ()) uni fun ann
forall term (uni :: * -> *) fun ann.
ann
-> term
-> ExpectedShapeOr (Type TyName uni ())
-> Normalized (Type TyName uni ())
-> TypeError term uni fun ann
TypeMismatch ann
ann (Term TyName Name uni fun ann -> Term TyName Name uni fun ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Term TyName Name uni fun ann
scrut) ExpectedShapeOr (Type TyName uni ())
forall {a}. ExpectedShapeOr a
expectedSop Normalized (Type TyName uni ())
vScrutTy)
        -- scrutinee does not have a SOP type at all
        Type TyName uni ()
_ -> AReview err (TypeError (Term TyName Name uni fun ()) uni fun ann)
-> TypeError (Term TyName Name uni fun ()) uni fun ann
-> TypeCheckT uni fun (PirTCConfig uni fun) m ()
forall e (m :: * -> *) t x.
MonadError e m =>
AReview e t -> t -> m x
throwing AReview err (TypeError (Term TyName Name uni fun ()) uni fun ann)
forall r term (uni :: * -> *) fun ann.
AsTypeError r term uni fun ann =>
Prism' r (TypeError term uni fun ann)
Prism' err (TypeError (Term TyName Name uni fun ()) uni fun ann)
_TypeError (ann
-> Term TyName Name uni fun ()
-> ExpectedShapeOr (Type TyName uni ())
-> Normalized (Type TyName uni ())
-> TypeError (Term TyName Name uni fun ()) uni fun ann
forall term (uni :: * -> *) fun ann.
ann
-> term
-> ExpectedShapeOr (Type TyName uni ())
-> Normalized (Type TyName uni ())
-> TypeError term uni fun ann
TypeMismatch ann
ann (Term TyName Name uni fun ann -> Term TyName Name uni fun ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Term TyName Name uni fun ann
scrut) ExpectedShapeOr (Type TyName uni ())
forall {a}. ExpectedShapeOr a
expectedSop Normalized (Type TyName uni ())
vScrutTy)

    -- If we got through all that, then every case type is correct, including that
    -- they all result in vResTy, so we can safely conclude that that is the type of the
    -- whole expression.
    Normalized (Type TyName uni ())
-> TypeCheckT
     uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ()))
forall a.
a -> ReaderT (TypeCheckEnv uni fun (PirTCConfig uni fun)) m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Normalized (Type TyName uni ())
vResTy
-- ##############
-- ## 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 <- NonEmpty (Binding TyName Name uni fun ann)
-> Normalized (Type TyName uni ())
-> TypeCheckT
     uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ()))
forall (uni :: * -> *) (m :: * -> *) fun ann.
MonadNormalizeType uni m =>
NonEmpty (Binding TyName Name uni fun ann)
-> Normalized (Type TyName uni ())
-> PirTCEnv uni fun m (Normalized (Type TyName uni ()))
substTypeBinds NonEmpty (Binding TyName Name uni fun ann)
bs (Normalized (Type TyName uni ())
 -> TypeCheckT
      uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ())))
-> TypeCheckT
     uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ()))
-> TypeCheckT
     uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ()))
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Binding TyName Name uni fun ann
 -> TypeCheckT
      uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ()))
 -> TypeCheckT
      uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ())))
-> TypeCheckT
     uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ()))
-> NonEmpty (Binding TyName Name uni fun ann)
-> TypeCheckT
     uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ()))
forall a b. (a -> b -> b) -> b -> NonEmpty a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Binding TyName Name uni fun ann
-> TypeCheckT
     uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ()))
-> TypeCheckT
     uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ()))
forall a.
Binding TyName Name uni fun ann
-> PirTCEnv uni fun m a -> PirTCEnv uni fun m a
checkBindingThenScope (Term TyName Name uni fun ann
-> TypeCheckT
     uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ()))
forall err (m :: * -> *) (uni :: * -> *) fun ann.
MonadTypeCheckPir err uni fun ann m =>
Term TyName Name uni fun ann
-> PirTCEnv uni fun m (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 ())
-> TypeCheckT uni fun (PirTCConfig uni fun) m ()
forall err (uni :: * -> *) fun ann (m :: * -> *).
MonadKindCheck err (Term TyName Name uni fun ()) uni fun ann m =>
ann -> Normalized (Type TyName uni ()) -> PirTCEnv uni fun m ()
checkStarInferred ann
ann Normalized (Type TyName uni ())
ty
    Normalized (Type TyName uni ())
-> TypeCheckT
     uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ()))
forall a.
a -> ReaderT (TypeCheckEnv uni fun (PirTCConfig uni fun)) m a
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 m a -> PirTCEnv uni fun m a
    checkBindingThenScope :: forall a.
Binding TyName Name uni fun ann
-> PirTCEnv uni fun m a -> PirTCEnv uni fun m a
checkBindingThenScope Binding TyName Name uni fun ann
b PirTCEnv uni fun m a
acc = do
        -- check that the kinds of the declared types are correct
        Binding TyName Name uni fun ann
-> TypeCheckT uni fun (PirTCConfig uni fun) m ()
forall err (m :: * -> *) (uni :: * -> *) fun ann.
MonadKindCheck err (Term TyName Name uni fun ()) uni fun ann m =>
Binding TyName Name uni fun ann -> PirTCEnv uni fun m ()
checkKindFromBinding Binding TyName Name uni fun ann
b
        -- check that the types of declared terms are correct
        Recursivity
-> Binding TyName Name uni fun ann
-> TypeCheckT uni fun (PirTCConfig uni fun) m ()
forall err (m :: * -> *) (uni :: * -> *) fun ann.
MonadTypeCheckPir err uni fun ann m =>
Recursivity
-> Binding TyName Name uni fun ann -> PirTCEnv uni fun m ()
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 m a -> PirTCEnv uni fun m a
forall name (uni :: * -> *) fun ann cfg (m :: * -> *) a.
Binding TyName name uni fun ann
-> TypeCheckT uni fun cfg m a -> TypeCheckT uni fun cfg m a
withTyVarsOfBinding Binding TyName Name uni fun ann
b (PirTCEnv uni fun m a -> PirTCEnv uni fun m a)
-> PirTCEnv uni fun m a -> PirTCEnv uni fun m a
forall a b. (a -> b) -> a -> b
$
            Recursivity
-> Binding TyName Name uni fun ann
-> PirTCEnv uni fun m a
-> PirTCEnv uni fun m a
forall (uni :: * -> *) fun cfg ann (m :: * -> *) a.
MonadNormalizeType uni m =>
Recursivity
-> Binding TyName Name uni fun ann
-> TypeCheckT uni fun cfg m a
-> TypeCheckT uni fun cfg m a
withVarsOfBinding Recursivity
r Binding TyName Name uni fun ann
b PirTCEnv uni fun m a
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)
-> TypeCheckT
     uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ()))
-> TypeCheckT
     uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ()))
forall (f :: * -> *) name (uni :: * -> *) fun ann cfg (m :: * -> *)
       a.
Foldable f =>
f (Binding TyName name uni fun ann)
-> TypeCheckT uni fun cfg m a -> TypeCheckT uni fun cfg m a
withTyVarsOfBindings NonEmpty (Binding TyName Name uni fun ann)
bs (TypeCheckT
   uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ()))
 -> TypeCheckT
      uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ())))
-> TypeCheckT
     uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ()))
-> TypeCheckT
     uni fun (PirTCConfig uni fun) m (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
    -> TypeCheckT uni fun (PirTCConfig uni fun) m ())
-> TypeCheckT uni fun (PirTCConfig uni fun) m ()
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
-> TypeCheckT uni fun (PirTCConfig uni fun) m ()
forall err (m :: * -> *) (uni :: * -> *) fun ann.
MonadKindCheck err (Term TyName Name uni fun ()) uni fun ann m =>
Binding TyName Name uni fun ann -> PirTCEnv uni fun m ()
checkKindFromBinding
        Normalized (Type TyName uni ())
ty <- Recursivity
-> NonEmpty (Binding TyName Name uni fun ann)
-> TypeCheckT
     uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ()))
-> TypeCheckT
     uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ()))
forall (uni :: * -> *) (m :: * -> *) (t :: * -> *) fun ann cfg a.
(MonadNormalizeType uni m, Foldable t) =>
Recursivity
-> t (Binding TyName Name uni fun ann)
-> TypeCheckT uni fun cfg m a
-> TypeCheckT uni fun cfg m a
withVarsOfBindings Recursivity
r NonEmpty (Binding TyName Name uni fun ann)
bs (TypeCheckT
   uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ()))
 -> TypeCheckT
      uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ())))
-> TypeCheckT
     uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ()))
-> TypeCheckT
     uni fun (PirTCConfig uni fun) m (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
    -> TypeCheckT uni fun (PirTCConfig uni fun) m ())
-> TypeCheckT uni fun (PirTCConfig uni fun) m ()
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
  -> TypeCheckT uni fun (PirTCConfig uni fun) m ())
 -> TypeCheckT uni fun (PirTCConfig uni fun) m ())
-> (Binding TyName Name uni fun ann
    -> TypeCheckT uni fun (PirTCConfig uni fun) m ())
-> TypeCheckT uni fun (PirTCConfig uni fun) m ()
forall a b. (a -> b) -> a -> b
$ Recursivity
-> Binding TyName Name uni fun ann
-> TypeCheckT uni fun (PirTCConfig uni fun) m ()
forall err (m :: * -> *) (uni :: * -> *) fun ann.
MonadTypeCheckPir err uni fun ann m =>
Recursivity
-> Binding TyName Name uni fun ann -> PirTCEnv uni fun m ()
checkTypeFromBinding Recursivity
r
              Term TyName Name uni fun ann
-> TypeCheckT
     uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ()))
forall err (m :: * -> *) (uni :: * -> *) fun ann.
MonadTypeCheckPir err uni fun ann m =>
Term TyName Name uni fun ann
-> PirTCEnv uni fun m (Normalized (Type TyName uni ()))
inferTypeM Term TyName Name uni fun ann
inTerm
        NonEmpty (Binding TyName Name uni fun ann)
-> Normalized (Type TyName uni ())
-> TypeCheckT
     uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ()))
forall (uni :: * -> *) (m :: * -> *) fun ann.
MonadNormalizeType uni m =>
NonEmpty (Binding TyName Name uni fun ann)
-> Normalized (Type TyName uni ())
-> PirTCEnv uni fun m (Normalized (Type TyName uni ()))
substTypeBinds NonEmpty (Binding TyName Name uni fun ann)
bs Normalized (Type TyName uni ())
ty
    -- check the in-term's inferred type has kind * (except at toplevel)
    ann
-> Normalized (Type TyName uni ())
-> TypeCheckT uni fun (PirTCConfig uni fun) m ()
forall err (uni :: * -> *) fun ann (m :: * -> *).
MonadKindCheck err (Term TyName Name uni fun ()) uni fun ann m =>
ann -> Normalized (Type TyName uni ()) -> PirTCEnv uni fun m ()
checkStarInferred ann
ann Normalized (Type TyName uni ())
ty
    Normalized (Type TyName uni ())
-> TypeCheckT
     uni fun (PirTCConfig uni fun) m (Normalized (Type TyName uni ()))
forall a.
a -> ReaderT (TypeCheckEnv uni fun (PirTCConfig uni fun)) m a
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 err m uni fun ann.
       MonadKindCheck err (Term TyName Name uni fun ()) uni fun ann m
    => Binding TyName Name uni fun ann
    -> PirTCEnv uni fun m ()
checkKindFromBinding :: forall err (m :: * -> *) (uni :: * -> *) fun ann.
MonadKindCheck err (Term TyName Name uni fun ()) uni fun ann m =>
Binding TyName Name uni fun ann -> PirTCEnv uni fun m ()
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 m ()
forall err term (uni :: * -> *) fun ann (m :: * -> *) cfg.
(MonadKindCheck err term uni fun ann m, HasKindCheckConfig cfg) =>
ann
-> Type TyName uni ann -> Kind () -> TypeCheckT uni fun cfg m ()
checkKindM ann
ann Type TyName uni ann
rhs (Kind () -> PirTCEnv uni fun m ())
-> Kind () -> PirTCEnv uni fun m ()
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 m ()
forall err term (uni :: * -> *) fun ann (m :: * -> *) cfg.
(MonadKindCheck err term uni fun ann m, HasKindCheckConfig cfg) =>
ann
-> Type TyName uni ann -> Kind () -> TypeCheckT uni fun cfg m ()
checkKindM (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 m ())
-> Kind () -> PirTCEnv uni fun m ()
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 ann
dt@(Datatype ann
ann TyVarDecl TyName ann
tycon [TyVarDecl TyName ann]
tyargs Name
_ [VarDecl TyName Name uni ann]
vdecls) ->
        -- tycon+tyargs must be in scope during kindchecking
        [TyVarDecl TyName ann]
-> PirTCEnv uni fun m () -> PirTCEnv uni fun m ()
forall ann (uni :: * -> *) fun cfg (m :: * -> *) a.
[TyVarDecl TyName ann]
-> TypeCheckT uni fun cfg m a -> TypeCheckT uni fun cfg m 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 m () -> PirTCEnv uni fun m ())
-> PirTCEnv uni fun m () -> PirTCEnv uni fun m ()
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 m ()
forall err term (uni :: * -> *) fun ann (m :: * -> *) cfg.
(MonadKindCheck err term uni fun ann m, HasKindCheckConfig cfg) =>
ann
-> Type TyName uni ann -> Kind () -> TypeCheckT uni fun cfg m ()
checkKindM ann
ann Type TyName uni ann
appliedTyCon (Kind () -> PirTCEnv uni fun m ())
-> Kind () -> PirTCEnv uni fun m ()
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 m ())
-> PirTCEnv uni fun m ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ (VarDecl TyName Name uni ann -> Type TyName uni ann
forall tyname name (uni :: * -> *) ann.
VarDecl tyname name uni ann -> Type tyname uni ann
_varDeclType (VarDecl TyName Name uni ann -> Type TyName uni ann)
-> [VarDecl TyName Name uni ann] -> [Type TyName uni ann]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [VarDecl TyName Name uni ann]
vdecls) ((Type TyName uni ann -> PirTCEnv uni fun m ())
 -> PirTCEnv uni fun m ())
-> (Type TyName uni ann -> PirTCEnv uni fun m ())
-> PirTCEnv uni fun m ()
forall a b. (a -> b) -> a -> b
$
               ann -> Type TyName uni ann -> Kind () -> PirTCEnv uni fun m ()
forall err term (uni :: * -> *) fun ann (m :: * -> *) cfg.
(MonadKindCheck err term uni fun ann m, HasKindCheckConfig cfg) =>
ann
-> Type TyName uni ann -> Kind () -> TypeCheckT uni fun cfg m ()
checkKindM ann
ann (Type TyName uni ann -> Kind () -> PirTCEnv uni fun m ())
-> Kind () -> Type TyName uni ann -> PirTCEnv uni fun m ()
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 ann -> Type TyName uni ann
forall a (uni :: * -> *).
a -> Datatype TyName Name uni a -> Type TyName uni a
mkDatatypeValueType ann
ann Datatype TyName Name uni 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 err m uni fun ann.
       MonadTypeCheckPir err uni fun ann m
    => Recursivity -> Binding TyName Name uni fun ann -> PirTCEnv uni fun m ()
checkTypeFromBinding :: forall err (m :: * -> *) (uni :: * -> *) fun ann.
MonadTypeCheckPir err uni fun ann m =>
Recursivity
-> Binding TyName Name uni fun ann -> PirTCEnv uni fun m ()
checkTypeFromBinding Recursivity
recurs = \case
    TypeBind{} -> () -> PirTCEnv uni fun m ()
forall a.
a -> ReaderT (TypeCheckEnv uni fun (PirTCConfig uni fun)) m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure () -- no types to check
    TermBind ann
_ Strictness
_ (VarDecl ann
ann Name
_ Type TyName uni ann
ty) Term TyName Name uni fun ann
rhs ->
        -- See Note [PIR vs Paper Escaping Types Difference]
        PirTCEnv uni fun m () -> PirTCEnv uni fun m ()
forall (uni :: * -> *) fun (m :: * -> *) a.
PirTCEnv uni fun m a -> PirTCEnv uni fun m a
withNoEscapingTypes (ann
-> Term TyName Name uni fun ann
-> Normalized (Type TyName uni ())
-> PirTCEnv uni fun m ()
forall err (uni :: * -> *) fun ann (m :: * -> *).
MonadTypeCheckPir err uni fun ann m =>
ann
-> Term TyName Name uni fun ann
-> Normalized (Type TyName uni ())
-> PirTCEnv uni fun m ()
checkTypeM ann
ann Term TyName Name uni fun ann
rhs (Normalized (Type TyName uni ()) -> PirTCEnv uni fun m ())
-> (Normalized (Type TyName uni ann)
    -> Normalized (Type TyName uni ()))
-> Normalized (Type TyName uni ann)
-> PirTCEnv uni fun m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type TyName uni ann -> Type TyName uni ())
-> Normalized (Type TyName uni ann)
-> Normalized (Type TyName uni ())
forall a b. (a -> b) -> Normalized a -> Normalized b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Type TyName uni ann -> Type TyName uni ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Normalized (Type TyName uni ann) -> PirTCEnv uni fun m ())
-> ReaderT
     (TypeCheckEnv uni fun (PirTCConfig uni fun))
     m
     (Normalized (Type TyName uni ann))
-> PirTCEnv uni fun m ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Type TyName uni ann
-> ReaderT
     (TypeCheckEnv uni fun (PirTCConfig uni fun))
     m
     (Normalized (Type TyName uni ann))
forall (uni :: * -> *) (m :: * -> *) ann fun cfg.
MonadNormalizeType uni m =>
Type TyName uni ann
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ann))
normalizeTypeM Type TyName uni ann
ty)
    DatatypeBind ann
_ dt :: Datatype TyName Name uni ann
dt@(Datatype ann
ann TyVarDecl TyName ann
_ [TyVarDecl TyName ann]
tyargs Name
_ [VarDecl TyName Name uni ann]
constrs) ->
        [Type TyName uni ann]
-> (Type TyName uni ann -> PirTCEnv uni fun m ())
-> PirTCEnv uni fun m ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ (VarDecl TyName Name uni ann -> Type TyName uni ann
forall tyname name (uni :: * -> *) ann.
VarDecl tyname name uni ann -> Type tyname uni ann
_varDeclType (VarDecl TyName Name uni ann -> Type TyName uni ann)
-> [VarDecl TyName Name uni ann] -> [Type TyName uni ann]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [VarDecl TyName Name uni ann]
constrs) ((Type TyName uni ann -> PirTCEnv uni fun m ())
 -> PirTCEnv uni fun m ())
-> (Type TyName uni ann -> PirTCEnv uni fun m ())
-> PirTCEnv uni fun m ()
forall a b. (a -> b) -> a -> b
$
            \ Type TyName uni ann
ty -> Type TyName uni ann -> PirTCEnv uni fun m ()
checkConRes Type TyName uni ann
ty PirTCEnv uni fun m ()
-> PirTCEnv uni fun m () -> PirTCEnv uni fun m ()
forall a b.
ReaderT (TypeCheckEnv uni fun (PirTCConfig uni fun)) m a
-> ReaderT (TypeCheckEnv uni fun (PirTCConfig uni fun)) m b
-> ReaderT (TypeCheckEnv uni fun (PirTCConfig uni fun)) m b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Type TyName uni ann -> PirTCEnv uni fun m ()
checkNonRecScope Type TyName uni ann
ty
      where
       Type TyName uni ann
appliedTyCon :: Type TyName uni ann = ann -> Datatype TyName Name uni ann -> Type TyName uni ann
forall a (uni :: * -> *).
a -> Datatype TyName Name uni a -> Type TyName uni a
mkDatatypeValueType ann
ann Datatype TyName Name uni ann
dt
       checkConRes :: Type TyName uni ann -> PirTCEnv uni fun m ()
       checkConRes :: Type TyName uni ann -> PirTCEnv uni fun m ()
checkConRes Type TyName uni ann
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 m () -> PirTCEnv uni fun m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Type TyName uni ann -> Type TyName uni ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Type TyName uni ann -> Type TyName uni ann
forall tyname (uni :: * -> *) a.
Type tyname uni a -> Type tyname uni a
PLC.funTyResultType Type TyName uni ann
ty) Type TyName uni () -> Type TyName uni () -> Bool
forall a. Eq a => a -> a -> Bool
/= Type TyName uni ann -> Type TyName uni ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Type TyName uni ann
appliedTyCon) (PirTCEnv uni fun m () -> PirTCEnv uni fun m ())
-> (TypeErrorExt uni ann -> PirTCEnv uni fun m ())
-> TypeErrorExt uni ann
-> PirTCEnv uni fun m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
               AReview err (TypeErrorExt uni ann)
-> TypeErrorExt uni ann -> PirTCEnv uni fun m ()
forall e (m :: * -> *) t x.
MonadError e m =>
AReview e t -> t -> m x
throwing AReview err (TypeErrorExt uni ann)
forall r (uni :: * -> *) ann.
AsTypeErrorExt r uni ann =>
Prism' r (TypeErrorExt uni ann)
Prism' err (TypeErrorExt uni ann)
_TypeErrorExt (TypeErrorExt uni ann -> PirTCEnv uni fun m ())
-> TypeErrorExt uni ann -> PirTCEnv uni fun m ()
forall a b. (a -> b) -> a -> b
$ ann -> Type TyName uni ann -> TypeErrorExt uni ann
forall (uni :: * -> *) ann.
ann -> Type TyName uni ann -> TypeErrorExt uni ann
MalformedDataConstrResType ann
ann Type TyName uni ann
appliedTyCon

       -- if nonrec binding, make sure that type-constructor is not part of the data-constructor's argument types.
       checkNonRecScope :: Type TyName uni ann -> PirTCEnv uni fun m ()
       checkNonRecScope :: Type TyName uni ann -> PirTCEnv uni fun m ()
checkNonRecScope Type TyName uni ann
ty = case Recursivity
recurs of
           Recursivity
Rec -> () -> PirTCEnv uni fun m ()
forall a.
a -> ReaderT (TypeCheckEnv uni fun (PirTCConfig uni fun)) m a
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 ann]
-> PirTCEnv uni fun m () -> PirTCEnv uni fun m ()
forall ann (uni :: * -> *) fun cfg (m :: * -> *) a.
[TyVarDecl TyName ann]
-> TypeCheckT uni fun cfg m a -> TypeCheckT uni fun cfg m a
withTyVarDecls [TyVarDecl TyName ann]
tyargs (PirTCEnv uni fun m () -> PirTCEnv uni fun m ())
-> PirTCEnv uni fun m () -> PirTCEnv uni fun m ()
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 ann]
-> (Type TyName uni ann
    -> ReaderT
         (TypeCheckEnv uni fun (PirTCConfig uni fun)) m (Kind ()))
-> PirTCEnv uni fun m ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ (Type TyName uni ann -> [Type TyName uni ann]
forall tyname (uni :: * -> *) a.
Type tyname uni a -> [Type tyname uni a]
PLC.funTyArgs Type TyName uni ann
ty) Type TyName uni ann
-> ReaderT (TypeCheckEnv uni fun (PirTCConfig uni fun)) m (Kind ())
forall err term (uni :: * -> *) fun ann (m :: * -> *) cfg.
(MonadKindCheck err term uni fun ann m, HasKindCheckConfig cfg) =>
Type TyName uni ann -> TypeCheckT uni fun cfg m (Kind ())
inferKindM

-- | 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
    :: MonadKindCheck err (Term TyName Name uni fun ()) uni fun ann m
    => ann -> Normalized (Type TyName uni ()) -> PirTCEnv uni fun m ()
checkStarInferred :: forall err (uni :: * -> *) fun ann (m :: * -> *).
MonadKindCheck err (Term TyName Name uni fun ()) uni fun ann m =>
ann -> Normalized (Type TyName uni ()) -> PirTCEnv uni fun m ()
checkStarInferred ann
ann Normalized (Type TyName uni ())
t = do
    AllowEscape
allowEscape <- Getting
  AllowEscape
  (TypeCheckEnv uni fun (PirTCConfig uni fun))
  AllowEscape
-> ReaderT
     (TypeCheckEnv uni fun (PirTCConfig uni fun)) m 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)) m AllowEscape)
-> Getting
     AllowEscape
     (TypeCheckEnv uni fun (PirTCConfig uni fun))
     AllowEscape
-> ReaderT
     (TypeCheckEnv uni fun (PirTCConfig uni fun)) m 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 :: * -> *) fun1 cfg1 fun2 cfg2 (f :: * -> *).
Functor f =>
(cfg1 -> f cfg2)
-> TypeCheckEnv uni fun1 cfg1 -> f (TypeCheckEnv uni fun2 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 (f :: * -> *).
Functor f =>
(AllowEscape -> f AllowEscape)
-> PirTCConfig uni fun -> f (PirTCConfig uni fun)
pirConfigAllowEscape
    case AllowEscape
allowEscape of
        AllowEscape
NoEscape  -> ann -> Type TyName uni ann -> Kind () -> PirTCEnv uni fun m ()
forall err term (uni :: * -> *) fun ann (m :: * -> *) cfg.
(MonadKindCheck err term uni fun ann m, HasKindCheckConfig cfg) =>
ann
-> Type TyName uni ann -> Kind () -> TypeCheckT uni fun cfg m ()
checkKindM ann
ann (ann
ann ann -> Type TyName uni () -> Type TyName uni ann
forall a b. a -> Type TyName uni b -> Type TyName uni a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Normalized (Type TyName uni ()) -> Type TyName uni ()
forall a. Normalized a -> a
unNormalized Normalized (Type TyName uni ())
t) (Kind () -> PirTCEnv uni fun m ())
-> Kind () -> PirTCEnv uni fun m ()
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 m ()
forall a.
a -> ReaderT (TypeCheckEnv uni fun (PirTCConfig uni fun)) m a
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 m a -> PirTCEnv uni fun m a
withNoEscapingTypes :: forall (uni :: * -> *) fun (m :: * -> *) a.
PirTCEnv uni fun m a -> PirTCEnv uni fun m a
withNoEscapingTypes = (TypeCheckEnv uni fun (PirTCConfig uni fun)
 -> TypeCheckEnv uni fun (PirTCConfig uni fun))
-> ReaderT (TypeCheckEnv uni fun (PirTCConfig uni fun)) m a
-> ReaderT (TypeCheckEnv uni fun (PirTCConfig uni fun)) m a
forall r (m :: * -> *) a.
(r -> r) -> ReaderT r m a -> ReaderT r m a
local ((TypeCheckEnv uni fun (PirTCConfig uni fun)
  -> TypeCheckEnv uni fun (PirTCConfig uni fun))
 -> ReaderT (TypeCheckEnv uni fun (PirTCConfig uni fun)) m a
 -> ReaderT (TypeCheckEnv uni fun (PirTCConfig uni fun)) m a)
-> (TypeCheckEnv uni fun (PirTCConfig uni fun)
    -> TypeCheckEnv uni fun (PirTCConfig uni fun))
-> ReaderT (TypeCheckEnv uni fun (PirTCConfig uni fun)) m a
-> ReaderT (TypeCheckEnv uni fun (PirTCConfig uni fun)) m 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 :: * -> *) fun1 cfg1 fun2 cfg2 (f :: * -> *).
Functor f =>
(cfg1 -> f cfg2)
-> TypeCheckEnv uni fun1 cfg1 -> f (TypeCheckEnv uni fun2 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 (f :: * -> *).
Functor f =>
(AllowEscape -> f AllowEscape)
-> PirTCConfig uni fun -> f (PirTCConfig uni fun)
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 :: PirTCConfig uni fun -> PirTCEnv uni fun m a -> m a
runTypeCheckM :: forall (uni :: * -> *) fun (m :: * -> *) a.
PirTCConfig uni fun -> PirTCEnv uni fun m a -> m a
runTypeCheckM PirTCConfig uni fun
config PirTCEnv uni fun m a
a = PirTCEnv uni fun m a
-> TypeCheckEnv uni fun (PirTCConfig uni fun) -> m a
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT PirTCEnv uni fun m a
a (TypeCheckEnv uni fun (PirTCConfig uni fun) -> m a)
-> TypeCheckEnv uni fun (PirTCConfig uni fun) -> m a
forall a b. (a -> b) -> a -> b
$ 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 cfg ann m a.
       MonadNormalizeType uni m
    => Recursivity
    -> Binding TyName Name uni fun ann
    -> TypeCheckT uni fun cfg m a
    -> TypeCheckT uni fun cfg m a
withVarsOfBinding :: forall (uni :: * -> *) fun cfg ann (m :: * -> *) a.
MonadNormalizeType uni m =>
Recursivity
-> Binding TyName Name uni fun ann
-> TypeCheckT uni fun cfg m a
-> TypeCheckT uni fun cfg m a
withVarsOfBinding Recursivity
_ TypeBind{} TypeCheckT uni fun cfg m a
k = TypeCheckT uni fun cfg m a
k
withVarsOfBinding Recursivity
_ (TermBind ann
_ Strictness
_ VarDecl TyName Name uni ann
vdecl Term TyName Name uni fun ann
_) TypeCheckT uni fun cfg m a
k = do
    Normalized (Type TyName uni ann)
vTy <- Type TyName uni ann
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ann))
forall (uni :: * -> *) (m :: * -> *) ann fun cfg.
MonadNormalizeType uni m =>
Type TyName uni ann
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ann))
normalizeTypeM (Type TyName uni ann
 -> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ann)))
-> Type TyName uni ann
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ann))
forall a b. (a -> b) -> a -> b
$ VarDecl TyName Name uni ann -> Type TyName uni ann
forall tyname name (uni :: * -> *) ann.
VarDecl tyname name uni ann -> Type tyname uni ann
_varDeclType VarDecl TyName Name uni ann
vdecl
    -- no need to rename here
    Name
-> Normalized (Type TyName uni ())
-> TypeCheckT uni fun cfg m a
-> TypeCheckT uni fun cfg m a
forall (uni :: * -> *) fun cfg (m :: * -> *) a.
Name
-> Normalized (Type TyName uni ())
-> TypeCheckT uni fun cfg m a
-> TypeCheckT uni fun cfg m a
withVar (VarDecl TyName Name uni ann -> Name
forall tyname name (uni :: * -> *) ann.
VarDecl tyname name uni ann -> name
_varDeclName VarDecl TyName Name uni ann
vdecl) (Type TyName uni ann -> Type TyName uni ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Type TyName uni ann -> Type TyName uni ())
-> Normalized (Type TyName uni ann)
-> Normalized (Type TyName uni ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Normalized (Type TyName uni ann)
vTy) TypeCheckT uni fun cfg m a
k
withVarsOfBinding Recursivity
r (DatatypeBind ann
_ Datatype TyName Name uni ann
dt) TypeCheckT uni fun cfg m a
k = do
    -- generate all the definitions
    -- options don't matter, we're just doing it for the types
    (Def (TyVarDecl TyName (Provenance ann)) (PLCRecType uni Any ann)
_tyconstrDef, [Def
   (VarDecl TyName Name uni (Provenance ann)) (PIRTerm uni Any ann)]
constrDefs, Def
  (VarDecl TyName Name uni (Provenance ann)) (PIRTerm uni Any ann)
destrDef) <- DatatypeCompilationOpts
-> Recursivity
-> Datatype TyName Name uni (Provenance ann)
-> ReaderT
     (TypeCheckEnv uni fun cfg)
     m
     (Def (TyVarDecl TyName (Provenance ann)) (PLCRecType uni Any ann),
      [Def
         (VarDecl TyName Name uni (Provenance ann)) (PIRTerm uni Any ann)],
      Def
        (VarDecl TyName Name uni (Provenance ann)) (PIRTerm uni Any ann))
forall (m :: * -> *) (uni :: * -> *) a fun.
MonadQuote m =>
DatatypeCompilationOpts
-> Recursivity
-> Datatype TyName Name uni (Provenance a)
-> m (Def (TyVarDecl TyName (Provenance a)) (PLCRecType uni fun a),
      [Def (VarDecl TyName Name uni (Provenance a)) (PIRTerm uni fun a)],
      Def (VarDecl TyName Name uni (Provenance a)) (PIRTerm uni fun a))
compileDatatypeDefs DatatypeCompilationOpts
defaultDatatypeCompilationOpts Recursivity
r (Datatype TyName Name uni ann
-> Datatype TyName Name uni (Provenance ann)
forall (f :: * -> *) a. Functor f => f a -> f (Provenance a)
original Datatype TyName Name uni ann
dt)
    -- ignore the generated rhs terms of constructors/destructor
    let structorDecls :: [VarDecl TyName Name uni (Provenance ann)]
structorDecls = Def
  (VarDecl TyName Name uni (Provenance ann)) (PIRTerm uni Any ann)
-> VarDecl TyName Name uni (Provenance ann)
forall var val. Def var val -> var
PIR.defVar (Def
   (VarDecl TyName Name uni (Provenance ann)) (PIRTerm uni Any ann)
 -> VarDecl TyName Name uni (Provenance ann))
-> [Def
      (VarDecl TyName Name uni (Provenance ann)) (PIRTerm uni Any ann)]
-> [VarDecl TyName Name uni (Provenance ann)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Def
  (VarDecl TyName Name uni (Provenance ann)) (PIRTerm uni Any ann)
destrDefDef
  (VarDecl TyName Name uni (Provenance ann)) (PIRTerm uni Any ann)
-> [Def
      (VarDecl TyName Name uni (Provenance ann)) (PIRTerm uni Any ann)]
-> [Def
      (VarDecl TyName Name uni (Provenance ann)) (PIRTerm uni Any ann)]
forall a. a -> [a] -> [a]
:[Def
   (VarDecl TyName Name uni (Provenance ann)) (PIRTerm uni Any ann)]
constrDefs
    (VarDecl TyName Name uni (Provenance ann)
 -> TypeCheckT uni fun cfg m a -> TypeCheckT uni fun cfg m a)
-> TypeCheckT uni fun cfg m a
-> [VarDecl TyName Name uni (Provenance ann)]
-> TypeCheckT uni fun cfg m a
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr VarDecl TyName Name uni (Provenance ann)
-> TypeCheckT uni fun cfg m a -> TypeCheckT uni fun cfg m a
normRenameScope TypeCheckT uni fun cfg m a
k [VarDecl TyName Name uni (Provenance ann)]
structorDecls
    where
      -- normalize, then introduce the vardecl to scope
      normRenameScope :: VarDecl TyName Name uni (Provenance ann)
                      -> TypeCheckT uni fun cfg m a -> TypeCheckT uni fun cfg m a
      normRenameScope :: VarDecl TyName Name uni (Provenance ann)
-> TypeCheckT uni fun cfg m a -> TypeCheckT uni fun cfg m a
normRenameScope VarDecl TyName Name uni (Provenance ann)
v TypeCheckT uni fun cfg m a
acc = do
          Normalized (Type TyName uni (Provenance ann))
normRenamedTy <- Type TyName uni (Provenance ann)
-> TypeCheckT
     uni fun cfg m (Normalized (Type TyName uni (Provenance ann)))
forall (uni :: * -> *) (m :: * -> *) ann fun cfg.
MonadNormalizeType uni m =>
Type TyName uni ann
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ann))
normalizeTypeM (Type TyName uni (Provenance ann)
 -> TypeCheckT
      uni fun cfg m (Normalized (Type TyName uni (Provenance ann))))
-> Type TyName uni (Provenance ann)
-> TypeCheckT
     uni fun cfg m (Normalized (Type TyName uni (Provenance ann)))
forall a b. (a -> b) -> a -> b
$ VarDecl TyName Name uni (Provenance ann)
-> Type TyName uni (Provenance ann)
forall tyname name (uni :: * -> *) ann.
VarDecl tyname name uni ann -> Type tyname uni ann
_varDeclType VarDecl TyName Name uni (Provenance ann)
v
          Name
-> Normalized (Type TyName uni ())
-> TypeCheckT uni fun cfg m a
-> TypeCheckT uni fun cfg m a
forall (uni :: * -> *) fun cfg (m :: * -> *) a.
Name
-> Normalized (Type TyName uni ())
-> TypeCheckT uni fun cfg m a
-> TypeCheckT uni fun cfg m a
withVar (VarDecl TyName Name uni (Provenance ann) -> Name
forall tyname name (uni :: * -> *) ann.
VarDecl tyname name uni ann -> name
_varDeclName VarDecl TyName Name uni (Provenance ann)
v) (Type TyName uni (Provenance ann) -> Type TyName uni ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Type TyName uni (Provenance ann) -> Type TyName uni ())
-> Normalized (Type TyName uni (Provenance ann))
-> Normalized (Type TyName uni ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Normalized (Type TyName uni (Provenance ann))
normRenamedTy) TypeCheckT uni fun cfg m a
acc


withVarsOfBindings
    :: (MonadNormalizeType uni m, Foldable t)
    => Recursivity
    -> t (Binding TyName Name uni fun ann)
    -> TypeCheckT uni fun cfg m a
    -> TypeCheckT uni fun cfg m a
withVarsOfBindings :: forall (uni :: * -> *) (m :: * -> *) (t :: * -> *) fun ann cfg a.
(MonadNormalizeType uni m, Foldable t) =>
Recursivity
-> t (Binding TyName Name uni fun ann)
-> TypeCheckT uni fun cfg m a
-> TypeCheckT uni fun cfg m a
withVarsOfBindings Recursivity
r t (Binding TyName Name uni fun ann)
bs TypeCheckT uni fun cfg m a
k = (Binding TyName Name uni fun ann
 -> TypeCheckT uni fun cfg m a -> TypeCheckT uni fun cfg m a)
-> TypeCheckT uni fun cfg m a
-> t (Binding TyName Name uni fun ann)
-> TypeCheckT uni fun cfg m a
forall a b. (a -> b -> b) -> b -> t a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Recursivity
-> Binding TyName Name uni fun ann
-> TypeCheckT uni fun cfg m a
-> TypeCheckT uni fun cfg m a
forall (uni :: * -> *) fun cfg ann (m :: * -> *) a.
MonadNormalizeType uni m =>
Recursivity
-> Binding TyName Name uni fun ann
-> TypeCheckT uni fun cfg m a
-> TypeCheckT uni fun cfg m a
withVarsOfBinding Recursivity
r) TypeCheckT uni fun cfg m a
k t (Binding TyName Name uni fun ann)
bs

-- | Scope a typechecking computation with the given binding's newly-introducing type (if there is one)
withTyVarsOfBinding
    :: Binding TyName name uni fun ann
    -> TypeCheckT uni fun cfg m a
    -> TypeCheckT uni fun cfg m a
withTyVarsOfBinding :: forall name (uni :: * -> *) fun ann cfg (m :: * -> *) a.
Binding TyName name uni fun ann
-> TypeCheckT uni fun cfg m a -> TypeCheckT uni fun cfg m a
withTyVarsOfBinding = \case
       TypeBind ann
_ TyVarDecl TyName ann
tvdecl Type TyName uni ann
_                      -> [TyVarDecl TyName ann]
-> TypeCheckT uni fun cfg m a -> TypeCheckT uni fun cfg m a
forall ann (uni :: * -> *) fun cfg (m :: * -> *) a.
[TyVarDecl TyName ann]
-> TypeCheckT uni fun cfg m a -> TypeCheckT uni fun cfg m a
withTyVarDecls [TyVarDecl TyName ann
tvdecl]
       DatatypeBind ann
_ (Datatype ann
_ TyVarDecl TyName ann
tvdecl [TyVarDecl TyName ann]
_ name
_ [VarDecl TyName name uni ann]
_) -> [TyVarDecl TyName ann]
-> TypeCheckT uni fun cfg m a -> TypeCheckT uni fun cfg m a
forall ann (uni :: * -> *) fun cfg (m :: * -> *) a.
[TyVarDecl TyName ann]
-> TypeCheckT uni fun cfg m a -> TypeCheckT uni fun cfg m a
withTyVarDecls [TyVarDecl TyName ann
tvdecl]
       TermBind{}                               -> TypeCheckT uni fun cfg m a -> TypeCheckT uni fun cfg m a
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)
    -> TypeCheckT uni fun cfg m a
    -> TypeCheckT uni fun cfg m a
withTyVarsOfBindings :: forall (f :: * -> *) name (uni :: * -> *) fun ann cfg (m :: * -> *)
       a.
Foldable f =>
f (Binding TyName name uni fun ann)
-> TypeCheckT uni fun cfg m a -> TypeCheckT uni fun cfg m a
withTyVarsOfBindings = (TypeCheckT uni fun cfg m a
 -> f (Binding TyName name uni fun ann)
 -> TypeCheckT uni fun cfg m a)
-> f (Binding TyName name uni fun ann)
-> TypeCheckT uni fun cfg m a
-> TypeCheckT uni fun cfg m a
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((TypeCheckT uni fun cfg m a
  -> f (Binding TyName name uni fun ann)
  -> TypeCheckT uni fun cfg m a)
 -> f (Binding TyName name uni fun ann)
 -> TypeCheckT uni fun cfg m a
 -> TypeCheckT uni fun cfg m a)
-> (TypeCheckT uni fun cfg m a
    -> f (Binding TyName name uni fun ann)
    -> TypeCheckT uni fun cfg m a)
-> f (Binding TyName name uni fun ann)
-> TypeCheckT uni fun cfg m a
-> TypeCheckT uni fun cfg m a
forall a b. (a -> b) -> a -> b
$ (Binding TyName name uni fun ann
 -> TypeCheckT uni fun cfg m a -> TypeCheckT uni fun cfg m a)
-> TypeCheckT uni fun cfg m a
-> f (Binding TyName name uni fun ann)
-> TypeCheckT uni fun cfg m a
forall a b. (a -> b -> b) -> b -> f a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Binding TyName name uni fun ann
-> TypeCheckT uni fun cfg m a -> TypeCheckT uni fun cfg m a
forall name (uni :: * -> *) fun ann cfg (m :: * -> *) a.
Binding TyName name uni fun ann
-> TypeCheckT uni fun cfg m a -> TypeCheckT uni fun cfg m a
withTyVarsOfBinding

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

-- | Substitute `TypeBind`s from the given list of `Binding`s in the given `Type`.
-- This is so that @let a = (con integer) in \(x : a) -> x@ typechecks.
substTypeBinds ::
    MonadNormalizeType uni m =>
    NonEmpty (Binding TyName Name uni fun ann) ->
    Normalized (Type TyName uni ()) ->
    PirTCEnv uni fun m (Normalized (Type TyName uni ()))
substTypeBinds :: forall (uni :: * -> *) (m :: * -> *) fun ann.
MonadNormalizeType uni m =>
NonEmpty (Binding TyName Name uni fun ann)
-> Normalized (Type TyName uni ())
-> PirTCEnv uni fun m (Normalized (Type TyName uni ()))
substTypeBinds = (Normalized (Type TyName uni ())
 -> NonEmpty (Binding TyName Name uni fun ann)
 -> PirTCEnv uni fun m (Normalized (Type TyName uni ())))
-> NonEmpty (Binding TyName Name uni fun ann)
-> Normalized (Type TyName uni ())
-> PirTCEnv uni fun m (Normalized (Type TyName uni ()))
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((Normalized (Type TyName uni ())
  -> NonEmpty (Binding TyName Name uni fun ann)
  -> PirTCEnv uni fun m (Normalized (Type TyName uni ())))
 -> NonEmpty (Binding TyName Name uni fun ann)
 -> Normalized (Type TyName uni ())
 -> PirTCEnv uni fun m (Normalized (Type TyName uni ())))
-> ((Binding TyName Name uni fun ann
     -> Normalized (Type TyName uni ())
     -> PirTCEnv uni fun m (Normalized (Type TyName uni ())))
    -> Normalized (Type TyName uni ())
    -> NonEmpty (Binding TyName Name uni fun ann)
    -> PirTCEnv uni fun m (Normalized (Type TyName uni ())))
-> (Binding TyName Name uni fun ann
    -> Normalized (Type TyName uni ())
    -> PirTCEnv uni fun m (Normalized (Type TyName uni ())))
-> NonEmpty (Binding TyName Name uni fun ann)
-> Normalized (Type TyName uni ())
-> PirTCEnv uni fun m (Normalized (Type TyName uni ()))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Binding TyName Name uni fun ann
 -> Normalized (Type TyName uni ())
 -> PirTCEnv uni fun m (Normalized (Type TyName uni ())))
-> Normalized (Type TyName uni ())
-> NonEmpty (Binding TyName Name uni fun ann)
-> PirTCEnv uni fun m (Normalized (Type TyName uni ()))
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> b -> m b) -> b -> t a -> m b
foldrM ((Binding TyName Name uni fun ann
  -> Normalized (Type TyName uni ())
  -> PirTCEnv uni fun m (Normalized (Type TyName uni ())))
 -> NonEmpty (Binding TyName Name uni fun ann)
 -> Normalized (Type TyName uni ())
 -> PirTCEnv uni fun m (Normalized (Type TyName uni ())))
-> (Binding TyName Name uni fun ann
    -> Normalized (Type TyName uni ())
    -> PirTCEnv uni fun m (Normalized (Type TyName uni ())))
-> NonEmpty (Binding TyName Name uni fun ann)
-> Normalized (Type TyName uni ())
-> PirTCEnv uni fun m (Normalized (Type TyName uni ()))
forall a b. (a -> b) -> a -> b
$ \Binding TyName Name uni fun ann
b Normalized (Type TyName uni ())
ty -> case Binding TyName Name uni fun ann
b of
    TypeBind ann
_ TyVarDecl TyName ann
tvar Type TyName uni ann
rhs -> do
        Normalized (Type TyName uni ())
rhs' <- Type TyName uni ()
-> PirTCEnv uni fun m (Normalized (Type TyName uni ()))
forall (uni :: * -> *) (m :: * -> *) ann fun cfg.
MonadNormalizeType uni m =>
Type TyName uni ann
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ann))
normalizeTypeM (Type TyName uni ann -> Type TyName uni ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Type TyName uni ann
rhs)
        -- See Note [Normalizing substitution] for why `substNormalizeTypeM`
        -- doesn't take a normalized type.
        Normalized (Type TyName uni ())
-> TyName
-> Type TyName uni ()
-> PirTCEnv uni fun m (Normalized (Type TyName uni ()))
forall (uni :: * -> *) (m :: * -> *) fun cfg.
MonadNormalizeType uni m =>
Normalized (Type TyName uni ())
-> TyName
-> Type TyName uni ()
-> TypeCheckT uni fun cfg m (Normalized (Type TyName uni ()))
substNormalizeTypeM Normalized (Type TyName uni ())
rhs' (TyVarDecl TyName ann
tvar TyVarDecl TyName ann
-> Getting TyName (TyVarDecl TyName ann) TyName -> TyName
forall s a. s -> Getting a s a -> a
^. Getting TyName (TyVarDecl TyName ann) TyName
forall tyname1 ann tyname2 (f :: * -> *).
Functor f =>
(tyname1 -> f tyname2)
-> TyVarDecl tyname1 ann -> f (TyVarDecl tyname2 ann)
tyVarDeclName) (Normalized (Type TyName uni ()) -> Type TyName uni ()
forall a. Normalized a -> a
unNormalized Normalized (Type TyName uni ())
ty)
    Binding TyName Name uni fun ann
_ -> Normalized (Type TyName uni ())
-> PirTCEnv uni fun m (Normalized (Type TyName uni ()))
forall a.
a -> ReaderT (TypeCheckEnv uni fun (PirTCConfig uni fun)) m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Normalized (Type TyName uni ())
ty