Checking if type variables are unbound in class and instance definitions

src/Solcore/Frontend/TypeInference/TcContract.hs

@@ -289,6 +289,7 @@ checkClass icls@(Class bvs ps n vs v sigs)
   = do
       let p = InCls n (TyVar v) (TyVar <$> vs)
           ms' = map sigName sigs
+      checkAllTypeVarsBound icls (v : vs) bvs
       bound <- askBoundVariableCondition n
       unless bound (checkBoundVariable ps (v:vs) `wrapError` icls)
       addClassInfo n (length vs) ms' ps p
@@ -299,8 +300,7 @@ checkClass icls@(Class bvs ps n vs v sigs)
             pst <- mapM tyParam ps
             t' <- maybe (pure unit) pure mt
             let ft = funtype pst t'
-            unless (all (`elem` bvs) (v : vs))
-                   (unboundTypeVars sig ((v : vs) \\ bvs))
+            checkAllTypeVarsBound sig (v : vs) bvs
             addClassMethod p sig `wrapError` icls
 
 addClassInfo :: Name -> Arity -> [Method] -> [Pred] -> Pred -> TcM ()

src/Solcore/Frontend/TypeInference/TcStmt.hs

@@ -480,15 +480,18 @@ argumentAnnotation (Untyped _)
 argumentAnnotation (Typed _ t)
   = pure t
 
+checkAllTypeVarsBound :: Pretty a => a -> [Tyvar] -> [Tyvar] -> TcM ()
+checkAllTypeVarsBound context used declared =
+    let unbound = used \\ declared
+    in unless (null unbound) $ unboundTypeVars context unbound
+
 annotatedScheme :: [Tyvar] -> Signature Name -> TcM Scheme
 annotatedScheme vs' sig@(Signature vs ps n args rt)
   = do
       ts <- mapM argumentAnnotation args
       t <- maybe freshTyVar pure rt
       -- check if all variables are bound in signature.
-      when (any (\ v -> v `notElem` (vs ++ vs')) (bv sig)) $ do
-         let unbound_vars = bv sig \\ (vs ++ vs')
-         unboundTypeVars sig unbound_vars
+      checkAllTypeVarsBound sig (vs ++ vs') (bv sig)
       pure (Forall vs (ps :=> (funtype ts t)))
 
 tcFunDef :: Bool -> [Tyvar] -> [Pred] -> FunDef Name -> TcM (FunDef Id, Scheme)
@@ -497,9 +500,7 @@ tcFunDef incl vs' qs d@(FunDef sig@(Signature vs ps n args rt) bd)
       info ["\n# tcFunDef ", pretty d]
       let vars = vs `union` vs'
       -- check if all variables are bound in signature.
-      when (any (\ v -> v `notElem` vars) (bv sig)) $ do
-         let unbound_vars = bv sig \\ vars
-         unboundTypeVars sig unbound_vars
+      checkAllTypeVarsBound sig (bv sig) vars
       -- instantiate signatures in function definition
       sks <- mapM (const freshTyVar) vars
       let
@@ -803,6 +804,8 @@ checkConstraints = mapM_ checkConstraint
 checkInstance :: Instance Name -> TcM ()
 checkInstance idef@(Instance d vs ctx n ts t funs)
   = do
+      -- checking if all variables are declared
+      checkAllTypeVarsBound idef (bv idef) vs
       -- kind check all types in instance head
       mapM_ kindCheck (t : ts) `wrapError` idef
       -- check if the class is defined

test/Cases.hs

@@ -232,6 +232,7 @@ cases =
     , runTestExpectingFailure "xref.solc" caseFolder
     , runTestForFile "yul-function-typing.solc" caseFolder
     , runTestForFile "yul-return.solc" caseFolder
+    , runTestExpectingFailure "unbound-instance-var.solc" caseFolder
     ]
  where
   caseFolder = "./test/examples/cases"

test/examples/cases/bound-with-pragma.solc

@@ -11,4 +11,4 @@ data TestType(x) = TestType;
 
 // Variable 'bad' appears in context but not in instance head
 // But pragma disables the check, so should pass
-forall x . bad:TestHelper(x) => instance TestType(x):TestBound {}
+forall x bad . bad:TestHelper(x) => instance TestType(x):TestBound {}

test/examples/cases/pragma_merge_base.solc

@@ -41,7 +41,7 @@ instance TestType2:TestClassC2(TestType2, TestType2) {}
 // === Bound Variable Violations ===
 
 // Fails Bound Variable & Patterson: Variable 'c' appears in context but not in instance head
-forall a . c:TestClassB2(a) => instance TestType1(a):TestClassB1 {}
+forall a c . c:TestClassB2(a) => instance TestType1(a):TestClassB1 {}
 
 // Bound Variable OK: Simple instance without context
 instance TestType1(TestType2):TestClassB2(TestType2) {}

test/examples/cases/pragma_merge_import.solc

@@ -19,8 +19,8 @@ forall i j . (i,j):TestClassP1 => instance i:TestClassC3(j) {}
 forall i j . (i,j):TestClassP1 => instance i:TestClassP3(j) {}
 
 // fails bound var & patterson (pragma set here)
-forall a . c:TestClassB1(a) => instance TestType1(a):TestClassB4 {}
+forall a c . c:TestClassB1(a) => instance TestType1(a):TestClassB4 {}
 
 // fails bound var & patterson (pragma set in base)
-forall a . c:TestClassB1(a) => instance TestType1(a):TestClassB3 {}
+forall a c . c:TestClassB1(a) => instance TestType1(a):TestClassB3 {}
 

test/examples/cases/unbound-instance-var.solc

@@ -0,0 +1,16 @@
+forall self.
+class self:C {
+    function size(x:self) -> word;
+}
+
+instance ():C {
+    function size(x:()) -> word {
+        return 0;
+    }
+}
+
+instance uint:C {
+    function size(x:uint) -> word {
+        return 1;
+    }
+}