Fixes on instance member function type checking

src/Solcore/Frontend/TypeInference/TcContract.hs

@@ -178,25 +178,25 @@ tcDecl (CDataDecl d) = CDataDecl <$> tcDataDecl d
 
 tcDataDecl :: DataTy -> TcM DataTy
 tcDataDecl (DataTy n vs cs)
-  = DataTy n vs <$> mapM tcConstr cs
+  = DataTy n vs <$> mapM (tcConstr vs) cs
 
-tcConstr :: Constr -> TcM Constr
-tcConstr (Constr n ts)
-  = Constr n <$> mapM kindCheck ts
+tcConstr :: [Tyvar] -> Constr -> TcM Constr
+tcConstr vs (Constr n ts)
+  = Constr n <$> mapM (kindCheck vs) ts
 
 -- type checking fields
 
 tcField :: Field Name -> TcM (Field Id)
 tcField d@(Field n t (Just e))
   = do
       (e', ps', t') <- tcExp e
-      kindCheck t `wrapError` d
+      kindCheck [] t `wrapError` d
       s <- mgu t t' `wrapError` d
       extEnv n (monotype t)
       return (Field n t (Just e'))
 tcField d@(Field n t _)
   = do
-      kindCheck t `wrapError` d
+      kindCheck [] t `wrapError` d
       extEnv n (monotype t)
       pure (Field n t Nothing)
 
@@ -214,13 +214,13 @@ tcClass iclass@(Class bvs ctx n vs v sigs)
       pure (Class bvs ctx n vs v sigs')
 
 tcSig :: (Signature Name, Scheme) -> TcM (Signature Id)
-tcSig (sig, (Forall _ (_ :=> t)))
+tcSig (sig, (Forall vs (_ :=> t)))
   = do
       let (ts,r) = splitTy t
           param (Typed n t) t1 = Typed (Id n t1) t1
           param (Untyped n) t1 = Typed (Id n t1) t1
           params' = zipWith param (sigParams sig) ts
-      kindCheck t `wrapError` sig
+      kindCheck vs t `wrapError` sig
       pure (Signature (sigVars sig)
                       (sigContext sig)
                       (sigName sig)

src/Solcore/Frontend/TypeInference/TcMonad.hs

@@ -76,7 +76,7 @@ addUniqueType :: Name -> DataTy -> TcM ()
 addUniqueType n dt
   = do
       modify (\ ctx -> ctx{ uniqueTypes = Map.insert n dt (uniqueTypes ctx)})
-      checkDataType dt 
+      checkDataType dt
 
 lookupUniqueTy :: Name -> TcM (Maybe DataTy)
 lookupUniqueTy n
@@ -163,15 +163,15 @@ isDirectCall n
 checkDataType :: DataTy -> TcM ()
 checkDataType d@(DataTy n vs constrs)
   = do
-      -- check if the type is already defined. 
-      r <- maybeAskTypeInfo n 
-      unless (isNothing r) $ 
-        typeAlreadyDefinedError d n 
+      -- check if the type is already defined.
+      r <- maybeAskTypeInfo n
+      unless (isNothing r) $
+        typeAlreadyDefinedError d n
       let vals' = map (\ (n, ty) -> (n, Forall (bv ty) ([] :=> ty))) vals
       mapM_ (uncurry extEnv) vals'
       modifyTypeInfo n ti
      -- checking kinds
-      mapM_ kindCheck (concatMap constrTy constrs) `wrapError` d
+      mapM_ (kindCheck vs) (concatMap constrTy constrs) `wrapError` d
     where
       ti = TypeInfo (length vs) (map fst vals) []
       tc = TyCon n (TyVar <$> vs)
@@ -180,10 +180,10 @@ checkDataType d@(DataTy n vs constrs)
 
 -- kind check
 
-kindCheck :: Ty -> TcM Ty
-kindCheck (t1 :-> t2)
-  = (:->) <$> kindCheck t1 <*> kindCheck t2
-kindCheck t@(TyCon n ts)
+kindCheck :: [Tyvar] -> Ty -> TcM Ty
+kindCheck vs (t1 :-> t2)
+  = (:->) <$> kindCheck vs t1 <*> kindCheck vs t2
+kindCheck vs t@(TyCon n ts)
   = do
       ti <- askTypeInfo n `wrapError` t
       unless (n == Name "pair" || arity ti == length ts) $
@@ -192,9 +192,17 @@ kindCheck t@(TyCon n ts)
                                show (arity ti) ++ " type arguments"
                              , "but, type " ++ pretty t ++
                                " has " ++ (show $ length ts) ++ " arguments"]
-      mapM_ kindCheck ts
+      mapM_ (kindCheck vs) ts
       pure t
-kindCheck t = pure t
+kindCheck vs t@(TyVar v)
+  = do
+      unless (v `elem` vs) $ do
+          throwError $ unwords [ "Type variable:", pretty v, "is not defined."
+                               , "Declared variables:"
+                               , unwords (map pretty vs)
+                               ]
+      return t
+kindCheck _ t = pure t
 
 
 -- Skolemization
@@ -644,28 +652,28 @@ undefinedClass :: Name -> TcM a
 undefinedClass n
   = throwError $ unlines ["Undefined class:", pretty n]
 
-typeAlreadyDefinedError :: DataTy -> Name -> TcM a 
-typeAlreadyDefinedError d n 
-  = do 
-      -- get type info 
+typeAlreadyDefinedError :: DataTy -> Name -> TcM a
+typeAlreadyDefinedError d n
+  = do
+      -- get type info
       di <- askTypeInfo n
-      d' <- dataTyFromInfo n di `wrapError` d 
+      d' <- dataTyFromInfo n di `wrapError` d
       throwError $ unlines ["Duplicated type definition for " ++ pretty n ++ ":"
                            , pretty d
                            , "and"
                            , pretty d']
 
-dataTyFromInfo :: Name -> TypeInfo -> TcM DataTy 
-dataTyFromInfo n (TypeInfo ar cs _) 
-  = do 
-      -- getting data constructor types 
+dataTyFromInfo :: Name -> TypeInfo -> TcM DataTy
+dataTyFromInfo n (TypeInfo ar cs _)
+  = do
+      -- getting data constructor types
       (constrs, vs) <- unzip <$> mapM constrsFromEnv cs
       pure (DataTy n (concat vs) constrs)
 
 constrsFromEnv :: Name -> TcM (Constr, [Tyvar])
-constrsFromEnv n 
-  = do 
-      (Forall vs (_ :=> ty)) <- askEnv n 
+constrsFromEnv n
+  = do
+      (Forall vs (_ :=> ty)) <- askEnv n
       let (ts, _) = splitTy ty
       pure (Constr n ts, vs)
 

src/Solcore/Frontend/TypeInference/TcStmt.hs

@@ -45,7 +45,10 @@ tcStmt e@(Let n mt me)
       (me', psf, tf) <- case (mt, me) of
                       (Just t, Just e1) -> do
                         (e', ps1, t1) <- tcExp e1
-                        _ <- kindCheck t1 `wrapError` e
+                        -- here we should not have bound
+                        -- variables! Since, they should
+                        -- have been instantiated before.
+                        _ <- kindCheck [] t1 `wrapError` e
                         let bvs = bv t
                         sks <- mapM (const freshTyVar) bvs
                         let t' = insts (zip bvs sks) t
@@ -245,7 +248,9 @@ tcExp e@(Lam args bd _)
          withCurrentSubst (e, ps1, t)
 tcExp e1@(TyExp e ty)
   = do
-      kindCheck ty `wrapError` e1
+      -- again, no bound variables here!
+      -- Variables should have been instantiated.
+      kindCheck [] ty `wrapError` e1
       (e', ps, ty') <- tcExp e
       s <- match ty' ty
       extSubst s
@@ -418,7 +423,8 @@ tcArg (Untyped n)
       pure (Typed (Id n v) v, (n, ty), v)
 tcArg a@(Typed n ty)
   = do
-      ty1 <- kindCheck ty `wrapError` a
+      -- no bound variables here
+      ty1 <- kindCheck [] ty `wrapError` a
       pure (Typed (Id n ty1) ty1, (n, monotype ty1), ty1)
 
 hasAnn :: Signature Name -> Bool
@@ -509,7 +515,7 @@ tcFunDef incl vs' qs d@(FunDef sig@(Signature vs ps n args rt) bd)
       info ["## predicates in signature:", pretty (ps1 ++ qs1)]
       -- getting argument / return types in annotations
       (args', lctx, ts') <- tcArgs args1
-      rt1' <- maybe freshTyVar kindCheck rt1
+      rt1' <- maybe freshTyVar (kindCheck []) rt1
       nt <- freshTyVar
       -- building the typing context with new assumptions
       let lctx' = if incl then (n, monotype nt) : lctx else lctx
@@ -519,7 +525,15 @@ tcFunDef incl vs' qs d@(FunDef sig@(Signature vs ps n args rt) bd)
       -- due to unique type creation.
       let tynames = tyconNames t1'
       changeTy <- or <$> mapM isUniqueTyName tynames
-      let rt2 = if changeTy then t1' else rt1'
+      -- Here, we need to only consider as rt2 = t1' when,
+      -- the function mention unique type as arguments.
+      -- In this situation, its type changed, since some
+      -- arguments are replaced by unique types. However,
+      -- when checking instances this is not necessary.
+      -- Because of that, we conjunct with `incl` argument
+      -- which is False for type checking instance member
+      -- functions.
+      let rt2 = if changeTy && incl then t1' else rt1'
       info ["Trying to unify: ", pretty rt2, " with ", pretty t1']
       unify rt2 t1' `wrapError` d
       info ["Trying to unify: ", pretty nt, " with ", pretty (funtype ts' rt2)]
@@ -532,6 +546,7 @@ tcFunDef incl vs' qs d@(FunDef sig@(Signature vs ps n args rt) bd)
       inf <- generalize (rs, ty)
       info [" - generalized inferred type: ", pretty inf]
       ann <- annotatedScheme vs' sig
+      info [" - annotated type: ", pretty ann]
       -- checking ambiguity
       when (ambiguous inf) $
         ambiguousTypeError inf sig
@@ -658,19 +673,24 @@ tcInstance :: Instance Name -> TcM (Instance Id)
 tcInstance idecl@(Instance d vs ctx n ts t funs)
   = do
       -- checking instance type parameters
-      mapM_ kindCheck (t : ts) `wrapError` idecl
+      mapM_ (kindCheck vs) (t : ts) `wrapError` idecl
       -- checking constraints
-      mapM_ checkConstraint ctx `wrapError` idecl
+      mapM_ (checkConstraint vs) ctx `wrapError` idecl
       vs' <- mapM (const freshVar) vs
       let env = zip vs (map Meta vs')
           idecl'@(Instance _ _ ctx' _ ts' t' funs')
             = everywhere (mkT (insts @Ty env)) idecl
       tcInstance' (Instance d [] ctx' n ts' t' funs')
 
-checkConstraint :: Pred -> TcM ()
-checkConstraint p@(InCls _ t ts) =
-  mapM_ kindCheck (t : ts) `wrapError` p
-checkConstraint (t :~: t') = mapM_ kindCheck [t, t']
+checkConstraint :: [Tyvar] -> Pred -> TcM ()
+checkConstraint vs p@(InCls n t ts) = do
+  -- checking kinds for all types
+  mapM_ (kindCheck vs) (t : ts) `wrapError` p
+  -- checking arity of the type class
+  cinfo <- askClassInfo n
+  unless ((classArity cinfo) == length ts) $
+    constraintArityError p cinfo
+checkConstraint vs (t :~: t') = mapM_ (kindCheck vs) [t, t']
 
 tcInstance' :: Instance Name -> TcM (Instance Id)
 tcInstance' idecl@(Instance d vs ctx n ts t funs)
@@ -684,7 +704,8 @@ tcInstance' idecl@(Instance d vs ctx n ts t funs)
         funs3 = sortBy (\ f f' -> compare (sigName (funSignature f))
                                           (sigName (funSignature f')))
                        (map (updateSignature vs1 n) funs2)
-      verifySignatures (Instance d vs1 ctx' n ts' t' funs3)
+        idecl' = Instance d vs1 ctx' n ts' t' funs3
+      verifySignatures idecl'
 
 verifySignatures :: Instance Id -> TcM (Instance Id)
 verifySignatures instd@(Instance _ _ ps n ts t funs) =
@@ -736,7 +757,8 @@ verifySignatures instd@(Instance _ _ ps n ts t funs) =
 checkMemberType :: (Name, Qual Ty, Qual Ty) -> TcM ()
 checkMemberType (qn, qt@(ps :=> t), qt'@(ps' :=> t'))
   = do
-      _ <- match t t' `catchError` (\ _ -> invalidMemberType qn t t')
+      info ["Checking ", pretty qn, " - infered:", pretty qt, " - annotated:", pretty qt']
+      _ <- match t' t `catchError` (\ _ -> invalidMemberType qn t' t)
       pure ()
 
 
@@ -797,18 +819,18 @@ checkCompleteInstDef n ns
 checkInstances :: [Instance Name] -> TcM ()
 checkInstances = mapM_ checkInstance
 
-checkConstraints :: [Pred] -> TcM ()
-checkConstraints = mapM_ checkConstraint
+checkConstraints :: [Tyvar] -> [Pred] -> TcM ()
+checkConstraints vs = mapM_ (checkConstraint vs)
 
 checkInstance :: Instance Name -> TcM ()
 checkInstance idef@(Instance d vs ctx n ts t funs)
   = do
       -- kind check all types in instance head
-      mapM_ kindCheck (t : ts) `wrapError` idef
+      mapM_ (kindCheck vs) (t : ts) `wrapError` idef
       -- check if the class is defined
       _ <- askClassInfo n `wrapError` idef
       -- check if all the types and classes in the context are valid
-      checkConstraints ctx
+      checkConstraints vs ctx
       let ipred = InCls n t ts
       -- checking the coverage condition
       insts' <- askInstEnv n `wrapError` ipred
@@ -1221,3 +1243,12 @@ notImplemented funName a = error $ concat [funName, " not implemented yet for ",
 
 notImplementedS :: (HasCallStack, Show a) => String -> a -> b
 notImplementedS funName a = error $ concat [funName, " not implemented yet for ", show(pShow a)]
+
+constraintArityError :: Pred -> ClassInfo -> TcM ()
+constraintArityError p@(InCls n _ ts) cinfo
+  = throwError $ unlines [ "Contraint:"
+                         , pretty n
+                         , "has a wrong number of weak type arguments."
+                         , unwords ["It is expected to have:", show (classArity cinfo), "weak arguments."]
+                         , unwords ["but it has:", show (length ts), "weak arguments!"]
+                         ]

std/std.solc

@@ -720,36 +720,36 @@ forall a b . a:ABIAttribs, b:ABIAttribs => instance (a,b):ABIAttribs {
 // if an abi tuple contains dynamic elems we store it in the tail, otherwise we
 // treat it the same as a series of nested pairs
 forall tuple . tuple:ABIAttribs => instance ABITuple(tuple):ABIAttribs {
-    function headSize(ty : Proxy(tuple)) -> word {
+    function headSize(ty : Proxy(ABITuple(tuple))) -> word {
         let px : Proxy(tuple);
         match ABIAttribs.isStatic(px) {
         | true => return ABIAttribs.headSize(px);
         | false => return 32;
         }
     }
-    function isStatic(ty : Proxy(tuple)) -> bool {
+    function isStatic(ty : Proxy(ABITuple(tuple))) -> bool {
         let px : Proxy(tuple);
         return ABIAttribs.isStatic(px);
     }
 }
 
 // for pointer types we fetch the attribs of the pointed to type, not the pointer itself
 forall ty . ty:ABIAttribs => instance memory(ty):ABIAttribs {
-    function headSize(ty : Proxy(ty)) -> word {
+    function headSize(ty : Proxy(memory(ty))) -> word {
         let px : Proxy(ty);
         return ABIAttribs.headSize(px);
     }
-    function isStatic(ty : Proxy(ty)) -> bool {
+    function isStatic(ty : Proxy(memory(ty))) -> bool {
         let px : Proxy(ty);
         return ABIAttribs.isStatic(px);
     }
 }
 forall ty . ty:ABIAttribs => instance calldata(ty):ABIAttribs {
-    function headSize(ty : Proxy(ty)) -> word {
+    function headSize(ty : Proxy(calldata(ty))) -> word {
         let px : Proxy(ty);
         return ABIAttribs.headSize(px);
     }
-    function isStatic(ty : Proxy(ty)) -> bool {
+    function isStatic(ty : Proxy(calldata(ty))) -> bool {
         let px : Proxy(ty);
         return ABIAttribs.isStatic(px);
     }

test/Cases.hs

@@ -204,34 +204,13 @@ cases =
     , runTestForFile "simpleid.solc" caseFolder
     , runTestForFile "SimpleLambda.solc" caseFolder
     , runTestForFile "single-lambda.solc" caseFolder
-    , runTestForFile "SingleFun.solc" caseFolder
-    , runTestExpectingFailure "signature.solc" caseFolder
-    , runTestExpectingFailure "SillyReturn.solc" caseFolder
-    , runTestExpectingFailure "SimpleInvoke.solc" caseFolder
-    , runTestExpectingFailure "string-const.solc" caseFolder
-    , runTestExpectingFailure "StructMembers.sol" caseFolder
-    , runTestExpectingFailure "subject-index.solc" caseFolder
-    , runTestExpectingFailure "subject-reduction.solc" caseFolder
-    , runTestExpectingFailure "subsumption-test.solc" caseFolder
-    , runTestForFile "super-class.solc" caseFolder
-    , runTestForFile "super-class-num.solc" caseFolder
-    , runTestForFile "tiamat.solc" caseFolder
-    , runTestForFile "tuple-trick.solc" caseFolder
-    , runTestForFile "tuva.solc" caseFolder
-    , runTestForFile "tyexp.solc" caseFolder
-    , runTestForFile "typedef.solc" caseFolder
-    , runTestForFile "Uncurry.solc" caseFolder
-    , runTestExpectingFailure "unconstrained-instance.solc" caseFolder
-    , runTestForFile "undefined.solc" caseFolder
-    , runTestForFile "uintdesugared.solc" caseFolder
-    , runTestForFile "unit.solc" caseFolder
-    , runTestExpectingFailure "vartyped.solc" caseFolder
-    , runTestExpectingFailure "weirdfoo.solc" caseFolder
-    , runTestExpectingFailure "withdraw.solc" caseFolder
-    , runTestForFile "word-match.solc" caseFolder
-    , runTestExpectingFailure "xref.solc" caseFolder
-    , runTestForFile "yul-function-typing.solc" caseFolder
-    , runTestForFile "yul-return.solc" caseFolder
+    , runTestExpectingFailure "duplicated-type-name.solc" caseFolder
+    , runTestExpectingFailure "overlapping-heads.solc" caseFolder
+    , runTestExpectingFailure "instance-wrong-sig.solc" caseFolder
+    , runTestForFile "match-yul.solc" caseFolder
+    , runTestExpectingFailure "instance-sig.solc" caseFolder
+    , runTestExpectingFailure "wrong-instance.solc" caseFolder
+    , runTestExpectingFailure "instance-context-wrong-kind.solc" caseFolder
     ]
  where
   caseFolder = "./test/examples/cases"