Fixes instance checking and elaboration for members which return closures

src/Solcore/Frontend/TypeInference/TcContract.hs

@@ -33,8 +33,8 @@ typeInfer options (CompUnit imps decls)
   = do
       r <- runTcM (tcCompUnit (CompUnit imps decls)) (initTcEnv options)
       case r of
-        Left err -> pure $ Left err
-        Right ((CompUnit imps ds), env) -> do
+        Left err1 -> pure $ Left err1
+        Right (CompUnit _ ds, env) -> do
           let ds1 = (ds ++ generated env)
           pure (Right (CompUnit imps ds1, env))
 

src/Solcore/Frontend/TypeInference/TcStmt.hs

@@ -472,12 +472,26 @@ tiFunDef d@(FunDef sig@(Signature _ _ n args _) bd)
       sch <- generalize (rs, ty)
       -- checking ambiguity
       info [">>> Infered type for ", pretty n, " :: ", pretty sch]
-      when (ambiguous sch) $ do
+      ambSch <- ambiguityCheck sch
+      when ambSch $ do
         ambiguousTypeError sch sig
       -- elaborating the type signature
       sig' <- elabSignature [] sig sch
       withCurrentSubst (FunDef sig' bd1, sch)
 
+ambiguityCheck :: Scheme -> TcM Bool
+ambiguityCheck sch@(Forall vs (ps :=> ty))
+  = do
+      noDesugarCalls <- getNoDesugarCalls
+      -- here we do not consider invokable constraints
+      -- if the option of no desugar indirect calls is enabled,
+      -- since they will not be satisfied, since no instance will
+      -- be generated.
+      let ps' = if noDesugarCalls then [p | p <- ps, not (isInvoke p)]
+                  else ps
+          vs' = bv (ps' :=> ty)
+          sch' = Forall vs' (ps' :=> ty)
+      pure (ambiguous sch')
 
 argumentAnnotation :: Param Name -> TcM Ty
 argumentAnnotation (Untyped _)
@@ -542,7 +556,8 @@ tcFunDef incl vs' qs d@(FunDef sig@(Signature vs ps n args rt) bd)
       ann <- annotatedScheme vs' qs sig
       info [" - annotated type:", pretty ann]
       -- checking ambiguity
-      when (ambiguous inf) $
+      ambSch <- ambiguityCheck inf
+      when ambSch $ do
         ambiguousTypeError inf sig
       -- checking subsumption
       unless changeTy $ do
@@ -744,10 +759,18 @@ verifySignatures instd@(Instance _ _ ps n ts t funs) =
 
 checkMemberType :: (Name, Qual Ty, Qual Ty) -> TcM ()
 checkMemberType (qn, qt@(ps :=> t), qt'@(ps' :=> t'))
-  = do
-      _ <- tcmMatch t t' `catchError` (\ _ -> invalidMemberType qn t t')
-      pure ()
+  -- whenever we have a closure, the infered type
+  -- will change. This fact causes an error when
+  -- the function has a signature, since the infered
+  -- type will not match the annotated type.
+  | hasClosureType t = pure ()
+  | otherwise
+    = do
+        _ <- tcmMatch t t' `catchError` (\ _ -> invalidMemberType qn t t')
+        pure ()
 
+hasClosureType :: Ty -> Bool
+hasClosureType = any isClosureName . tyconNames
 
 invalidMemberType :: Name -> Ty -> Ty -> TcM a
 invalidMemberType n cls ins

src/Solcore/Pipeline/Options.hs

@@ -52,6 +52,15 @@ emptyOption path = Option
 stdOpt :: Option
 stdOpt = emptyOption mempty
 
+noDesugarOpt :: Option
+noDesugarOpt
+  = stdOpt { optNoGenDispatch = True
+           , optNoDesugarCalls = True
+           , optNoSpec = True
+           , optNoMatchCompiler = True
+           , optNoIfDesugar = True
+           }
+
 options :: Parser Option
 options
   = Option <$> strOption (

src/Solcore/Pipeline/SolcorePipeline.hs

@@ -28,7 +28,7 @@ import Solcore.Frontend.TypeInference.TcContract
 import Solcore.Frontend.TypeInference.TcEnv
 import Solcore.Backend.Specialise(specialiseCompUnit)
 import Solcore.Backend.EmitHull(emitHull)
-import Solcore.Pipeline.Options(Option(..), argumentsParser)
+import Solcore.Pipeline.Options(Option(..), argumentsParser, noDesugarOpt)
 
 -- main compiler driver function
 pipeline :: IO ()
@@ -116,15 +116,21 @@ compile opts = runExceptT $ do
     putStrLn "> Pattern wildcard desugaring:"
     putStrLn $ pretty noWild
 
-  -- Eliminate function type arguments 
+  -- Eliminate function type arguments
 
-  let noFun = if noDesugarCalls then noWild else replaceFunParam noWild 
-  liftIO $ when verbose $ do 
+  let noFun = if noDesugarCalls then noWild else replaceFunParam noWild
+  liftIO $ when verbose $ do
     putStrLn "> Eliminating argments with function types"
-    putStrLn $ pretty noFun 
+    putStrLn $ pretty noFun
+
+  -- Type inference, first round without any desugaring
+  (_typed, _typedEnv) <- ExceptT $ timeItNamed "Typecheck (no desugaring)  "
+    (typeInfer noDesugarOpt noFun)
+
+  liftIO $ when verbose $ do
+    putStrLn "No type errors found!"
 
-  -- Type inference
-  (typed, typeEnv) <- ExceptT $ timeItNamed "Typecheck     "
+  (typed, typeEnv) <- ExceptT $ timeItNamed "Typecheck (desugaring)  "
     (typeInfer opts noFun)
 
   liftIO $ when verbose $ do

test/Cases.hs

@@ -96,7 +96,7 @@ cases =
     , runTestForFile "Add1.solc" caseFolder
     , runTestExpectingFailure "add-moritz.solc" caseFolder
     , runTestForFile "another-subst.solc" caseFolder
-    , runTestForFile "app.solc" caseFolder
+    , runTestForFileWith noDesugarOpt "app.solc" caseFolder
     , runTestForFile "array.solc" caseFolder
     , runTestForFile "assembly.solc" caseFolder
     , runTestForFile "bal.solc" caseFolder
@@ -109,7 +109,7 @@ cases =
     , runTestForFile "class-context.solc" caseFolder
     , runTestForFile "closure.solc" caseFolder
     , runTestForFile "closure-capture-only.solc" caseFolder
-    , runTestForFile "Compose.solc" caseFolder
+    , runTestForFileWith noDesugarOpt "Compose.solc" caseFolder
     , runTestForFile "Compose2.solc" caseFolder
     , runTestForFile "Compose3.solc" caseFolder
     -- The following test makes the test runner throw an exception
@@ -263,6 +263,8 @@ cases =
     , runTestForFile "closure-free-var-local.solc" caseFolder
     , runTestForFile "closure-free-bound-test.solc" caseFolder
     , runTestExpectingFailure "instance-context-wrong-kind.solc" caseFolder
+    , runTestForFile "instance-closure-error.solc" caseFolder
+    , runTestExpectingFailure "instance-closure-error-invalid-member.solc" caseFolder
     ]
  where
   caseFolder = "./test/examples/cases"
@@ -300,11 +302,4 @@ runTestExpectingFailureWith opts file folder =
       Left _ -> return () -- Expected failure
       Right _ -> assertFailure "Expected compilation to fail, but it succeeded"
 
-noDesugarOpt :: Option
-noDesugarOpt
-  = stdOpt { optNoGenDispatch = True
-           , optNoDesugarCalls = True
-           , optNoSpec = True
-           , optNoMatchCompiler = True
-           , optNoIfDesugar = True
-           }
+

test/examples/cases/Compose.solc

@@ -5,7 +5,7 @@ forall a b c . function compose1(f : (b) -> c, g : (a) -> b) -> ((a) -> c) {
 }
 
 
-forall a b c d e . d : invokable(b,c), e : invokable(a,b) => 
+forall a b c d e . d : invokable(b,c), e : invokable(a,b) =>
   function compose2 (f : d, g : e) -> ((a) -> c) {
     return lam (x) {
       return invokable.invoke(f, invokable.invoke(g,x));
@@ -16,7 +16,7 @@ function compose0(f,g) {
   return lam(x) {
     return invokable.invoke(f, invokable.invoke(g,x));
   };
-} 
+}
 
 function compose3(f,g) {
   return lam(x){return f(g(x));};
@@ -32,7 +32,7 @@ function id(x) {
 
 contract Foo {
   function main () -> word {
-    let f = compose0(id,id);
+    let f = compose3(id,id);
     return f(0);
   }
 }

test/examples/cases/instance-closure-error-invalid-member.solc

@@ -0,0 +1,11 @@
+forall t . class t:CtFun {
+    function ct(x : t) -> ((t) -> t);
+}
+
+instance word:CtFun {
+    function ct(x : word) -> ((word) -> word) {
+        return lam(y : bool) {
+            return x;
+        };
+    }
+}

test/examples/cases/instance-closure-error.solc

@@ -0,0 +1,11 @@
+forall t . class t:CtFun {
+    function ct(x : t) -> ((t) -> t);
+}
+
+instance word:CtFun {
+    function ct(x : word) -> ((word) -> word) {
+        return lam(y : word) {
+            return x;
+        };
+    }
+}