Added the type pos&neg tests

plutus-ir/plutus-ir.cabal

@@ -24,6 +24,7 @@ library
         Language.PlutusIR.Compiler
         Language.PlutusIR.Compiler.Names
         Language.PlutusIR.Compiler.Definitions
+        Language.PlutusIR.Compiler.Error
         Language.PlutusIR.Generators.AST
         Language.PlutusIR.Parser
         Language.PlutusIR.MkPir
@@ -34,19 +35,18 @@ library
         Language.PlutusIR.Transform.Rename
         Language.PlutusIR.Transform.NonStrict
         Language.PlutusIR.Transform.LetFloat
+        Language.PlutusIR.TypeCheck
     hs-source-dirs: src
     other-modules:
         Language.PlutusIR.Analysis.Dependencies
         Language.PlutusIR.Analysis.Usages
-        Language.PlutusIR.Compiler.Error
         Language.PlutusIR.Compiler.Let
         Language.PlutusIR.Compiler.Datatype
         Language.PlutusIR.Compiler.Provenance
         Language.PlutusIR.Compiler.Recursion
         Language.PlutusIR.Compiler.Types
         Language.PlutusIR.Compiler.Lower
         Language.PlutusIR.Normalize
-        Language.PlutusIR.TypeCheck
         Language.PlutusIR.TypeCheck.Internal
     default-language: Haskell2010
     default-extensions: ExplicitForAll ScopedTypeVariables
@@ -89,6 +89,7 @@ test-suite plutus-ir-test
         OptimizerSpec
         TransformSpec
         ParserSpec
+        TypeSpec
         TestLib
     default-language: Haskell2010
     build-depends:

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

@@ -50,6 +50,14 @@ data TypeError uni ann
     | InternalTypeErrorE ann (PLC.InternalTypeError uni ann)
     | FreeTypeVariableE ann PLC.TyName
     | FreeVariableE ann PLC.Name
+    -- FIXME: attach info
+    | ConflictingRecBinds
+    | DuplicateDeclaredIdent ann T.Text
+    | MalformedDataConstrResType ann
+        --  expected
+        (PLC.Type PLC.TyName uni ())
+        -- actual
+        (PLC.Normalized (PLC.Type PLC.TyName uni ()))
     -- TODO: enable back deriving NFData because PIR.Term does not have it
     -- TODO: enable back deriving Eq because PIR.Term does not have it, see similar src/Language/PlutusCore/Core/Instance/Eq.hs
     deriving (Show, Generic) 

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

@@ -40,13 +40,15 @@ import Data.Foldable
 import           Control.Monad.Except
 import           Control.Monad.Reader
 import           Control.Lens.TH
+import Control.Lens
 
 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
-
+import Data.List
+import qualified Data.Text as T
 {- Note [Global uniqueness]
 WARNING: type inference/checking works under the assumption that the global uniqueness condition
 is satisfied. The invariant is not checked, enforced or automatically fulfilled. So you must ensure
@@ -435,9 +437,18 @@ inferTypeM (Let ann recurs bs inTerm) = do
             inferTypeM inTerm
     -- G !- inTerm :: *
     -- TODO: here is the problem of existential-type escaping
-    checkKindM ann (ann <$ unNormalized tyInTerm) $ Type ()
+    -- FIXME: reenable the check
+    -- checkKindM ann (ann <$ unNormalized tyInTerm) $ Type ()
     pure tyInTerm
 
+  where
+    withBinds :: forall uni ann a. NonEmpty (Binding TyName Name uni ann) -> TypeCheckM uni ann a -> TypeCheckM uni ann a
+    withBinds = flip . foldr $ withBind
+
+    checkWellformBinds :: forall uni ann. (GShow uni, GEq uni, DefaultUni <: uni)
+                       => NonEmpty (Binding TyName Name uni ann) -> TypeCheckM uni ann ()
+    checkWellformBinds = traverse_ checkWellformBind
+
 
 -- See the [Global uniqueness] and [Type rules] notes.
 -- | Check a 'Term' against a 'NormalizedType'.
@@ -452,16 +463,17 @@ 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)
+-- | Extends the environment(s) with a bind.
+-- NOTE: there are no well-formed or duplication checks here, it just adds to the environment(s) like withVar/withTyVar do.
+-- For checks see `checkWellformBind`.
 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
+      -- which performs normalization there as well
       vTy <- normalizeTypeM $ void ty
       withVar n vTy m
   TypeBind _ (TyVarDecl _ tn k) _rhs ->
@@ -506,11 +518,6 @@ withBind b m = case b of
                        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.
@@ -526,39 +533,39 @@ checkWellformBind = \case
       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
+  DatatypeBind _ (Datatype ann tvdecl@(TyVarDecl _ dataName _) tvdecls des vdecls) -> do
+      assertNoDuplicate allNewTyNames
+      assertNoDuplicate allNewNames
       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
-
-
+          -- check the data-constructors' argument-types to be kinded by *
+          (traverse_
+              (\(VarDecl ann1 _ 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 <- constrResultTy <$> 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 () dataName)
+                          tvdecls
+                  when (expectedConstrResultType /= unNormalized actualConstrResultType) $
+                      throwError $ MalformedDataConstrResType ann1 expectedConstrResultType actualConstrResultType
+              )
+              vdecls)
+          allNewTyDecls
+   where
+      allNewTyDecls = tvdecl:tvdecls
+      allNewTyNames = fmap (nameString . unTyName . tyVarDeclName) allNewTyDecls
+      allNewNames = nameString des : fmap (nameString . varDeclName) vdecls
+
+      assertNoDuplicate :: [T.Text] -> TypeCheckM uni ann ()
+      assertNoDuplicate = maybe (pure ())
+                                (throwError . DuplicateDeclaredIdent ann)
+                          . hasDuplicate
 -- HELPERS
 
 -- | Get the result type of a constructor's type that has been prior normalized.
@@ -574,3 +581,6 @@ constrResultTy (Normalized t) = Normalized $ constrResultTy' t
           -- TyForall _ _ _ t -> constrResultTy' t
           t' -> t'
 
+hasDuplicate :: Ord a => [a] -> Maybe a
+hasDuplicate l = head <$> (find (\ g -> length g > 1) .  group $ sort l)
+

plutus-ir/test/Spec.hs

@@ -15,6 +15,7 @@ import           TestLib
 import           OptimizerSpec
 import           ParserSpec
 import           TransformSpec
+import           TypeSpec
 
 import           Language.PlutusCore.Pretty (PrettyConst)
 import           Language.PlutusCore.Quote
@@ -35,7 +36,6 @@ import           Control.Monad.Morph
 import           Control.Monad.Reader
 
 import           Data.Functor.Identity
-import           Text.Megaparsec.Pos
 
 main :: IO ()
 main = defaultMain $ runTestNestedIn ["test"] tests
@@ -45,9 +45,6 @@ instance ( PLC.GShow uni, PLC.GEq uni, PLC.DefaultUni PLC.<: uni
          ) => GetProgram (Term TyName Name uni a) uni where
     getProgram = asIfThrown . fmap (trivialProgram . void) . compileAndMaybeTypecheck True
 
-instance Pretty SourcePos where
-    pretty = pretty . sourcePosPretty
-
 -- | Adapt an computation that keeps its errors in an 'Except' into one that looks as if it caught them in 'IO'.
 asIfThrown
     :: Exception e
@@ -76,6 +73,8 @@ tests = testGroup "plutus-ir" <$> sequence
     , errors
     , optimizer
     , transform
+    , types
+    , typeErrors
     ]
 
 prettyprinting :: TestNested
@@ -89,7 +88,6 @@ lets :: TestNested
 lets = testNested "lets"
     [ goldenPlcFromPir term "letInLet"
     , goldenPlcFromPir term "letDep"
-    , goldenPlcFromPir term "rectypebind"
     ]
 
 datatypes :: TestNested
@@ -122,4 +120,5 @@ roundTripPirTerm = deserialise . serialise . void
 errors :: TestNested
 errors = testNested "errors"
     [ goldenPlcFromPirCatch term "mutuallyRecursiveTypes"
+    , goldenPlcFromPirCatch term "recursiveTypeBind"
     ]

plutus-ir/test/TestLib.hs

@@ -1,5 +1,6 @@
 {-# LANGUAGE FlexibleContexts  #-}
 {-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE ScopedTypeVariables #-}
 module TestLib where
 
 import           Common
@@ -13,11 +14,15 @@ import           Control.Monad.Reader         as Reader
 import qualified Language.PlutusCore.DeBruijn as PLC
 import           Language.PlutusCore.Pretty
 import           Language.PlutusCore.Quote
+import           Language.PlutusCore.Rename
 import qualified Language.PlutusCore.Universe as PLC
 import           Language.PlutusIR
 import           Language.PlutusIR.Parser     as Parser
-
+import        Language.PlutusIR.Compiler.Error as PIR
+import        Language.PlutusIR.TypeCheck
 import           System.FilePath              (joinPath, (</>))
+import Data.Text.Prettyprint.Doc
+import           Text.Megaparsec.Pos
 
 import           Text.Megaparsec.Error        as Megaparsec
 
@@ -58,3 +63,20 @@ goldenPlcFromPirCatch = goldenPirM (\ast -> ppCatch $ do
 
 goldenEvalPir :: (GetProgram a PLC.DefaultUni) => Parser a -> String -> TestNested
 goldenEvalPir = goldenPirM (\ast -> ppThrow $ runPlc [ast])
+
+
+goldenTypeFromPir :: forall a. (Pretty a, Typeable a)
+                  => Parser (Term TyName Name PLC.DefaultUni a) -> String -> TestNested
+goldenTypeFromPir = goldenPirM (\ast -> ppThrow $
+                                withExceptT (toException :: PIR.Error PLC.DefaultUni a -> SomeException) $ runQuoteT $ inferType defConfig ast)
+
+goldenTypeFromPirCatch :: forall a. (Pretty a, Typeable a)
+                  => Parser (Term TyName Name PLC.DefaultUni a) -> String -> TestNested
+goldenTypeFromPirCatch = goldenPirM (\ast -> ppCatch $
+                                withExceptT (toException :: PIR.Error PLC.DefaultUni a -> SomeException) $ runQuoteT $ inferType defConfig ast)
+
+
+-- TODO: perhaps move to Common.hs
+instance Pretty SourcePos where
+    pretty = pretty . sourcePosPretty
+

plutus-ir/test/TypeSpec.hs

@@ -0,0 +1,55 @@
+module TypeSpec where
+
+import           Common
+import           TestLib
+
+import           Language.PlutusCore.Quote
+
+import qualified Language.PlutusCore                         as PLC
+import           Language.PlutusIR.Parser
+import qualified Language.PlutusIR.Transform.LetFloat        as LetFloat
+import qualified Language.PlutusIR.Transform.NonStrict       as NonStrict
+import           Language.PlutusIR.Transform.Rename          ()
+import qualified Language.PlutusIR.Transform.ThunkRecursions as ThunkRec
+
+types :: TestNested
+types = testNested "types"
+    $ map (goldenTypeFromPir term)
+  [ "letInLet"
+  ,"listMatch"
+  ,"maybe"
+  ,"ifError"
+  ,"mutuallyRecursiveTypes"
+  ,"mutuallyRecursiveValues"
+  ,"nonrec1"
+  ,"nonrec2"
+  ,"nonrec3"
+  ,"nonrec4"
+  ,"nonrec6"
+  ,"nonrec7"
+  ,"nonrec8"
+  ,"rec1"
+  ,"rec2"
+  ,"rec3"
+  ,"rec4"
+  ,"nonrecToRec"
+  ,"nonrecToNonrec"
+  ,"oldLength"
+  ,"strictValue"
+  ,"strictNonValue"
+  ,"strictNonValue2"
+  ,"strictNonValue3"
+  ,"strictValueNonValue"
+  ,"strictValueValue"
+  ,"even3Eval"
+  ,"sameNameDifferentEnv"
+  ]
+
+typeErrors :: TestNested
+typeErrors = testNested "type-errors"
+    $ map (goldenTypeFromPirCatch term)
+    [ "conflictingRecursiveBinds"
+    , "duplicateDataConstrs"
+    , "duplicateTypeConstrs"
+    , "wrongDataConstrReturnType"
+    ]

plutus-ir/test/errors/recursiveTypeBind.golden

@@ -0,0 +1 @@
+Error during compilation: Type bindings cannot appear in recursive let, use datatypebind instead((recursive) let binding; from recursiveTypeBind:1:2)

plutus-ir/test/type-errors/conflictingRecursiveBinds

@@ -0,0 +1,9 @@
+(lam x (con integer)
+(let
+  (rec)
+    (termbind (strict) (vardecl j (con integer)) (con 3))
+    (termbind (strict) (vardecl j (con integer)) (con 3))
+    (con 5)
+    )
+  )
+

plutus-ir/test/type-errors/conflictingRecursiveBinds.golden

@@ -0,0 +1 @@
+(fun (con integer) (con integer))

plutus-ir/test/type-errors/duplicateDataConstrs

@@ -0,0 +1,14 @@
+(let
+  (nonrec)
+   (datatypebind
+    (datatype
+      (tyvardecl Maybe (fun (type) (type)))
+      (tyvardecl a (type))
+      match_Maybe
+      (vardecl Nothing [Maybe a])
+      (vardecl Just (fun a [Maybe a]))
+      (vardecl Just [Maybe a])
+    )
+  )
+  (con 5)
+)

plutus-ir/test/type-errors/duplicateDataConstrs.golden

@@ -0,0 +1 @@
+Error from the PIR typechecker: