WIP: first draft of pir typechecking

plutus-ir/src/Language/PlutusIR/Compiler/Datatype.hs

@@ -2,7 +2,12 @@
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE TypeApplications  #-}
 -- | Functions for compiling let-bound PIR datatypes into PLC.
-module Language.PlutusIR.Compiler.Datatype (compileDatatype, compileRecDatatypes) where
+module Language.PlutusIR.Compiler.Datatype
+    ( compileDatatype
+    , compileRecDatatypes
+    , resultTypeName
+    , constructorCaseType
+    ) where
 
 import           PlutusPrelude                          (showText)
 
@@ -54,7 +59,7 @@ constructorArgTypes = funTyArgs . varDeclType
 unveilDatatype :: Eq tyname => Type tyname uni a -> Datatype tyname name uni a -> Type tyname uni a -> Type tyname uni a
 unveilDatatype dty (Datatype _ tn _ _ _) = typeSubstTyNames (\n -> if n == tyVarDeclName tn then Just dty else Nothing)
 
-resultTypeName :: Compiling m e uni a => Datatype TyName Name uni (Provenance a) -> m TyName
+resultTypeName :: MonadQuote m => Datatype TyName Name uni a -> m TyName
 resultTypeName (Datatype _ tn _ _ _) = liftQuote $ freshTyName $ "out_" <> (nameString $ unTyName $ tyVarDeclName tn)
 
 -- Datatypes

plutus-ir/src/Language/PlutusIR/Normalize.hs

@@ -7,7 +7,7 @@ module Language.PlutusIR.Normalize
     , normalizeTypesInProgram
     ) where
 
-import  Language.PlutusCore.Core as PLC (Type, Normalized (..))
+import  Language.PlutusCore.Core as PLC (Normalized (..))
 import           Language.PlutusCore.Name
 import           Language.PlutusCore.Normalize.Internal hiding (normalizeTypesInM)
 import           Language.PlutusCore.Quote

plutus-ir/src/Language/PlutusIR/TypeCheck.hs

@@ -31,6 +31,21 @@ import           Language.PlutusCore.Universe
 
 import           Control.Monad.Except
 
+{- Note [Goal of PIR typecheker]
+
+Why we do typechecking:
+
+- The deadcode eliminator (at `Optimizer/Deadcode.hs`) may eliminate ill-typed code, which
+would turn, much to a surprise, an ill-typed program to a well-typed one.
+- The let datatypebinds and/or typebinds introduce new types which may escape from the type of the interm.
+Although they may compile fine to PLC and PLC-typecheck correctly, they are invalid in terms of PIR typechecking.
+This would disallow such programs. See for example `./test/recursion/even3Eval` and the discussion at
+<https://groups.google.com/a/iohk.io/forum/#!msg/plutus/6ycMTngVomc/VKeb00DuHwAJ>
+- The error-messages would be more specialized to lets.
+- We can have more flexible or more strict let syntax rules for truly recursive/nonrecursive bindings
+-}
+
+
 -- | The default 'TypeCheckConfig'.
 defConfig :: TypeCheckConfig uni
 defConfig = TypeCheckConfig mempty

plutus-ir/src/Language/PlutusIR/TypeCheck/Internal.hs

@@ -25,24 +25,27 @@ module Language.PlutusIR.TypeCheck.Internal
     , checkTypeM
     ) where
 
-import  Language.PlutusCore.Core as PLC (DynamicBuiltinName, BuiltinName, Builtin (..))
 import           Language.PlutusCore.Constant
 import           Language.PlutusIR
 import           Language.PlutusIR.Compiler.Error
 import           Language.PlutusCore.MkPlc
 import           Language.PlutusCore.Name
 import           Language.PlutusCore.Normalize
-import qualified Language.PlutusCore.Normalize.Internal as Norm
 import           Language.PlutusCore.Quote
 import           Language.PlutusCore.Rename
 import           Language.PlutusCore.Universe
+import Language.PlutusIR.Compiler.Datatype
 import           PlutusPrelude
-
-import           Control.Lens.TH                        (makeLenses)
+import Data.Foldable
 import           Control.Monad.Except
 import           Control.Monad.Reader
+import           Control.Lens.TH
+
+import qualified Language.PlutusCore.Normalize.Internal as Norm
+import qualified Language.PlutusCore.Core as PLC
 import           Data.Map                               (Map)
 import qualified Data.Map                               as Map
+import qualified Language.PlutusIR.MkPir                as PIR
 
 {- Note [Global uniqueness]
 WARNING: type inference/checking works under the assumption that the global uniqueness condition
@@ -96,7 +99,7 @@ functions that cannot fail looks like this:
 
 -- | Mapping from 'DynamicBuiltinName's to their 'Type's.
 newtype DynamicBuiltinNameTypes uni = DynamicBuiltinNameTypes
-    { unDynamicBuiltinNameTypes :: Map DynamicBuiltinName (Dupable (Normalized (Type TyName uni ())))
+    { unDynamicBuiltinNameTypes :: Map PLC.DynamicBuiltinName (Dupable (Normalized (Type TyName uni ())))
     } deriving newtype (Semigroup, Monoid)
 
 type TyVarKinds = UniqueMap TypeUnique (Kind ())
@@ -114,6 +117,9 @@ data TypeCheckEnv uni = TypeCheckEnv
     , _tceVarTypes        :: VarTypes uni
     }
 
+instance Show (TypeCheckEnv uni) where
+    show (TypeCheckEnv _ k _) = show k
+
 -- | The type checking monad that the type checker runs in.
 -- In contains a 'TypeCheckEnv' and allows to throw 'TypeError's.
 type TypeCheckM uni ann = ReaderT (TypeCheckEnv uni) (ExceptT (TypeError uni ann) Quote)
@@ -143,7 +149,7 @@ withVar name = local . over tceVarTypes . insertByName name . pure
 
 -- | Look up a 'DynamicBuiltinName' in the 'DynBuiltinNameTypes' environment.
 lookupDynamicBuiltinNameM
-    :: ann -> DynamicBuiltinName -> TypeCheckM uni ann (Normalized (Type TyName uni ()))
+    :: ann -> PLC.DynamicBuiltinName -> TypeCheckM uni ann (Normalized (Type TyName uni ()))
 lookupDynamicBuiltinNameM ann name = do
     DynamicBuiltinNameTypes dbnts <- asks $ _tccDynamicBuiltinNameTypes . _tceTypeCheckConfig
     case Map.lookup name dbnts of
@@ -183,6 +189,9 @@ dummyKind = Type ()
 dummyType :: Type TyName uni ()
 dummyType = TyVar () dummyTyName
 
+dummyTerm :: Term tyname Name unia ()
+dummyTerm = Var () (Name "__var" dummyUnique)
+
 -- ########################
 -- ## Type normalization ##
 -- ########################
@@ -285,7 +294,7 @@ checkKindOfPatternFunctorM ann pat k =
 -- | Return the 'Type' of a 'BuiltinName'.
 typeOfBuiltinName
     :: (GShow uni, GEq uni, DefaultUni <: uni)
-    => BuiltinName -> Type TyName uni ()
+    => PLC.BuiltinName -> Type TyName uni ()
 typeOfBuiltinName bn = withTypedBuiltinName bn typeOfTypedBuiltinName
 
 -- | @unfoldFixOf pat arg k = NORM (vPat (\(a :: k) -> ifix vPat a) arg)@
@@ -307,15 +316,15 @@ unfoldFixOf pat arg k = do
 -- | Infer the type of a 'Builtin'.
 inferTypeOfBuiltinM
     :: (GShow uni, GEq uni, DefaultUni <: uni)
-    => Builtin ann -> TypeCheckM uni ann (Normalized (Type TyName uni ()))
+    => PLC.Builtin ann -> TypeCheckM uni ann (Normalized (Type TyName uni ()))
 -- We have a weird corner case here: the type of a 'BuiltinName' can contain 'TypedBuiltinDyn', i.e.
 -- a static built-in name is allowed to depend on a dynamic built-in type which are not required
 -- to be normalized. For dynamic built-in names we store a map from them to their *normalized types*,
 -- with the normalization happening in this module, but what should we do for static built-in names?
 -- Right now we just renormalize the type of a static built-in name each time we encounter that name.
-inferTypeOfBuiltinM (BuiltinName    _   name) = normalizeType $ typeOfBuiltinName name
+inferTypeOfBuiltinM (PLC.BuiltinName    _   name) = normalizeType $ typeOfBuiltinName name
 -- TODO: inline this definition once we have only dynamic built-in names.
-inferTypeOfBuiltinM (DynBuiltinName ann name) = lookupDynamicBuiltinNameM ann name
+inferTypeOfBuiltinM (PLC.DynBuiltinName ann name) = lookupDynamicBuiltinNameM ann name
 
 -- See the [Global uniqueness] and [Type rules] notes.
 -- | Synthesize the type of a term, returning a normalized type.
@@ -404,18 +413,32 @@ inferTypeM (Unwrap ann term)        = do
             -- Subparts of a normalized type, so normalized.
             unfoldFixOf (Normalized vPat) (Normalized vArg) k
         _                  -> throwError (TypeMismatch ann (void term) (TyIFix () dummyType dummyType) vTermTy)
-
--- TODO:
-inferTypeM (Let {}) =  undefined
-
-
 -- [check| G !- ty :: *]    ty ~>? vTy
 -- -----------------------------------
 -- [infer| G !- error ty : vTy]
 inferTypeM (Error ann ty)           = do
     checkKindM ann ty $ Type ()
     normalizeTypeM $ void ty
 
+
+inferTypeM (Let ann recurs bs inTerm) = do
+    tyInTerm <- case recurs of
+        NonRec ->
+            foldr
+               (\ b acc -> do
+                   checkWellformBind b
+                   withBind b acc)
+               (inferTypeM inTerm)
+               bs
+        Rec -> withBinds bs $ do
+            checkWellformBinds bs
+            inferTypeM inTerm
+    -- G !- inTerm :: *
+    -- TODO: here is the problem of existential-type escaping
+    checkKindM ann (ann <$ unNormalized tyInTerm) $ Type ()
+    pure tyInTerm
+
+
 -- See the [Global uniqueness] and [Type rules] notes.
 -- | Check a 'Term' against a 'NormalizedType'.
 checkTypeM
@@ -428,3 +451,126 @@ checkTypeM
 checkTypeM ann term vTy = do
     vTermTy <- inferTypeM term
     when (vTermTy /= vTy) $ throwError (TypeMismatch ann (void term) (unNormalized vTermTy) vTy)
+
+-- | extends the environment with a bind.
+-- NOTE: does not do any check of binds-name collision checks (which is needed for letrec)
+withBind :: forall uni ann a.
+           Binding TyName Name uni ann
+         -> TypeCheckM uni ann a
+         -> TypeCheckM uni ann a
+withBind b m = case b of
+  TermBind _ _ (VarDecl _ n ty) _rhs -> do
+      -- OPTIMIZE: redundant, usually this function is called together with `checkWellformBind`,
+      -- which performs normalization here as well
+      vTy <- normalizeTypeM $ void ty
+      withVar n vTy m
+  TypeBind _ (TyVarDecl _ tn k) _rhs ->
+      withTyVar tn (void k) m
+  DatatypeBind _ dt@(Datatype ann (TyVarDecl _ tn k) tyargs des vdecls) ->
+      -- add type constructor to environment
+      withTyVar tn (void k) $ do
+          -- add destructor to environment
+          desType <- mkDestructorType
+          withVar des desType $ do
+              -- normalize types of data-constructors
+              normConstrsTypes <- traverse (\ (VarDecl _ n ty) -> do
+                                        -- adds explicit forall tyargs. to the front of each constructor
+                                        vTy <- normalizeTypeM $ void $ PIR.mkIterTyForall tyargs ty
+                                        pure (n,vTy)
+                                ) vdecls
+              -- add data constructors to environment
+              foldr
+                 (uncurry withVar)
+                 m
+                 normConstrsTypes
+   where
+       mkDestructorType :: TypeCheckM uni ann (Normalized (Type TyName uni ()))
+       mkDestructorType = do
+           -- get a fresh result type
+           out <- resultTypeName dt
+           normalizeTypeM $ void $
+             -- forall (a1::*) (a2::*) ... .
+             PIR.mkIterTyForall tyargs $
+               TyFun ann
+                     -- first argument is datatype:  T a1 a2 ... ->
+                     (PIR.mkIterTyApp ann (TyVar ann tn) (fmap (mkTyVar ann) tyargs ))
+                     -- forall (out :: *)
+                     (TyForall ann out (Type ann) $
+                       -- the constructors' types with result-type replaced by out
+                       -- note to self: no need to normalize the individual constructor here;
+                       -- the outer,final,surrounding normalizeTypeM will reach and normalize each constructor
+                       foldr
+                       (TyFun ann . constructorCaseType (TyVar ann out))
+                       -- result type of constructor is: out
+                       (TyVar ann out)
+                       vdecls
+                     )
+
+withBinds :: forall uni ann a.
+            NonEmpty (Binding TyName Name uni ann)
+          -> TypeCheckM uni ann a
+          -> TypeCheckM uni ann a
+withBinds = flip . foldr $ withBind
+
+-- | check that a binding is well-formed (correctly typed, kinded)
+checkWellformBind :: forall uni ann.
+                     (GShow uni, GEq uni, DefaultUni <: uni)
+                    => Binding TyName Name uni ann
+                    -> TypeCheckM uni ann ()
+checkWellformBind = \case
+  TermBind _ _ (VarDecl ann _ ty) rhs -> do
+      checkKindM ann ty $ Type ()
+      -- OPTIMIZE: redundant, usually this function is called together with `withBind`,
+      -- which performs normalization here as well
+      vTy <- normalizeTypeM $ void ty
+      checkTypeM ann rhs vTy
+  TypeBind _ (TyVarDecl ann _ k) rhs ->
+      checkKindM ann rhs (void k)
+  DatatypeBind _ (Datatype _ (TyVarDecl _ dt _) tvdecls _des vdecls) ->
+      -- add the type-arguments to environment
+      foldr (\(TyVarDecl _ tn k) -> withTyVar tn (void k))
+      -- check the data-constructors' argument-types to be kinded by *
+      (traverse_
+          (\(VarDecl ann _ ty) -> do
+              checkKindM ann ty $ Type ()
+              -- check that the normalized result-type of the data-constructor is
+              -- of the form `[DT tyarg1 tyarg2 ... tyargn]`
+              -- Q: is this normalization absolutely necessary?
+              actualConstrResultType <- normalizeTypeM $ void ty
+              -- TODO: after GADTs are added to the language the expected constructor result type
+              -- has to be "relaxed" from `[DT tyarg1 ... tyargn]` to `[DT Same Arity As ... Tvdecls]`
+              -- i.e. we should only check that `DT` is applied to the correct *number* of tyargs as the number of tvdecls,
+              let expectedConstrResultType = foldl
+                      (\acc (TyVarDecl _ tyarg _) -> TyApp () acc $ TyVar () tyarg)
+                      (TyVar () dt)
+                      tvdecls
+              when (expectedConstrResultType /= unNormalized actualConstrResultType) $
+                  -- TODO: probably introduce a more specialized constructor type error,
+                  -- because we don't have a valid "occuring-in-term" to put in the typemismatch-error
+                  throwError $ TypeMismatch ann dummyTerm expectedConstrResultType actualConstrResultType
+        )
+          vdecls)
+      tvdecls
+
+checkWellformBinds :: forall uni ann.
+                     (GShow uni, GEq uni, DefaultUni <: uni)
+                    => NonEmpty (Binding TyName Name uni ann)
+                    -> TypeCheckM uni ann ()
+checkWellformBinds = traverse_ checkWellformBind
+
+
+-- HELPERS
+
+-- | Get the result type of a constructor's type that has been prior normalized.
+-- ex1 (A->B->C) = C
+-- ex2 forall b. b -> c = forall. b ->c
+constrResultTy :: Normalized (Type tyname uni a) -> Normalized (Type tyname uni a)
+constrResultTy (Normalized t) = Normalized $ constrResultTy' t
+    where
+      constrResultTy' ::  Type tyname uni a -> Type tyname uni a
+      constrResultTy' = \case
+          TyFun _ _ t2 -> constrResultTy' t2
+          -- Q: is it necessary to descend inside a forall?
+          -- TyForall _ _ _ t -> constrResultTy' t
+          t' -> t'
+

plutus-ir/test/Spec.hs

@@ -89,6 +89,7 @@ lets :: TestNested
 lets = testNested "lets"
     [ goldenPlcFromPir term "letInLet"
     , goldenPlcFromPir term "letDep"
+    , goldenPlcFromPir term "rectypebind"
     ]
 
 datatypes :: TestNested

plutus-ir/test/lets/rectypebind

@@ -0,0 +1,11 @@
+(let
+  (rec)
+  (typebind (tyvardecl unit (type)) (all a (type) (fun a a)))
+  (let
+    (nonrec)
+    (termbind (strict)
+      (vardecl lazyVal (fun unit (con integer))) (lam x unit (con 3))
+    )
+    lazyVal
+  )
+)

plutus-ir/test/lets/rectypebind.golden

@@ -0,0 +1,13 @@
+(program 1.0.0
+  {
+    (abs
+      unit_i0
+      (type)
+      [
+        (lam lazyVal_i0 (fun unit_i2 (con integer)) lazyVal_i1)
+        (lam x_i0 unit_i2 (con 3))
+      ]
+    )
+    (all a_i0 (type) (fun a_i1 a_i1))
+  }
+)

plutus-ir/test/transform/letFloat/even3Eval

@@ -25,5 +25,3 @@
 )
 )
 )
-)
-)