fix issue in synthesizeApp where existentials were refined to pure function types, not allowing for possibility of effects

Still need to do some cleanup, will do that with separate commit

parser-typechecker/src/Unison/Term.hs

@@ -356,6 +356,9 @@ lam' a vs body = foldr (lam a) body vs
 lam'' :: Ord v => [(a,v)] -> AnnotatedTerm2 vt at ap v a -> AnnotatedTerm2 vt at ap v a
 lam'' vs body = foldr (uncurry lam) body vs
 
+isLam :: AnnotatedTerm2 vt at ap v a -> Bool
+isLam t = arity t > 0
+
 arity :: AnnotatedTerm2 vt at ap v a -> Int
 arity (LamNamed' _ body) = 1 + arity body
 arity (Ann' e _) = arity e

parser-typechecker/src/Unison/Typechecker/Context.hs

@@ -84,6 +84,7 @@ import qualified Unison.Typechecker.TypeLookup as TL
 import qualified Unison.TypeVar                as TypeVar
 import           Unison.Var                     ( Var )
 import qualified Unison.Var                    as Var
+import qualified Unison.TypePrinter            as TP
 
 type TypeVar v loc = TypeVar.TypeVar (B.Blank loc) v
 type Type v loc = AnnotatedType (TypeVar v loc) loc
@@ -681,11 +682,15 @@ synthesizeApp (Type.Effect'' es ft) argp@(arg, argNum) =
     abilityCheck es
     o <$ check arg i
   go (Type.Existential' b a) = do -- a^App
-    [i,o] <- traverse freshenVar [ABT.v' "i", ABT.v' "o"]
+    [i,e,o] <- traverse freshenVar [ABT.v' "i", ABT.v' "synthsizeApp-refined-effect", ABT.v' "o"]
     let it = Type.existential' (loc ft) B.Blank i
         ot = Type.existential' (loc ft) B.Blank o
-        soln = Type.Monotype (Type.arrow (loc ft) it ot)
-        ctxMid = context [existential o, existential i, Solved b a soln]
+        et = Type.existential' (loc ft) B.Blank e
+        soln = Type.Monotype (Type.arrow (loc ft)
+                                         it
+                                         (Type.effect (loc ft) [et] ot))
+        ctxMid = context [existential o, existential e,
+                          existential i, Solved b a soln]
     modifyContext' $ replace (existential a) ctxMid
     synthesizeApp (Type.getPolytype soln) argp
   go _ = getContext >>= \ctx -> failWith $ TypeMismatch ctx
@@ -801,10 +806,17 @@ synthesize e = scope (InSynthesize e) $
         et = Type.existential' l B.Blank e
     appendContext $
       context [existential i, existential e, existential o, Ann arg it]
-    body <- pure $ ABT.bindInheritAnnotation body (Term.var() arg)
-    withEffects0 [et] $ check body ot
+    body' <- pure $ ABT.bindInheritAnnotation body (Term.var() arg)
+    if Term.isLam body' then do
+      traceM $ "Nested lambda taking arg: " <> show (ABT.variable body)
+      withEffects0 [] $ check body' ot
+    else withEffects0 [et] $ check body' ot
     ctx <- getContext
-    pure $ Type.arrow l it (Type.effect l (apply ctx <$> [et]) ot)
+    let t = Type.arrow l it (Type.effect l (apply ctx <$> [et]) ot)
+    traceM $ "Lambda with arg " <> show (ABT.variable body) <> " was synthesized."
+    traceM $ "It had type: " <> TP.pretty' (Just 80) mempty (apply ctx t)
+    -- todo - generalize over `et` if its unsolved?
+    pure t
   go (Term.LetRecNamed' [] body) = synthesize body
   go (Term.LetRecTop' isTop letrec) = do
     (marker, e) <- annotateLetRecBindings isTop letrec
@@ -1145,6 +1157,9 @@ check e0 t0 = scope (InCheck e0 t0) $ do
   go e t = do -- Sub
     a   <- synthesize e
     ctx <- getContext
+    traceM $ "In check, the Sub case, which just uses subtype `a <: t`"
+    traceM $ "a = " <> TP.pretty' (Just 80) mempty (apply ctx a)
+    traceM $ "t = " <> TP.pretty' (Just 80) mempty (apply ctx t)
     subtype (apply ctx a) (apply ctx t)
 
 -- | `subtype ctx t1 t2` returns successfully if `t1` is a subtype of `t2`.

unison-src/tests/lambda-closing-over-effectful-fn.u

@@ -0,0 +1,10 @@
+use Optional None Some
+
+unfold : s -> (s ->{z} Optional (a, s)) ->{z} [a]
+unfold s f =
+  go s acc = case f s of
+    None -> acc
+    Some (hd, s) -> go s (acc `Sequence.snoc` hd)
+  go s []
+
+> unfold 0 (n -> if n Nat.< 5 then Some (n, n + 1) else None)

unison-src/tests/lambda-closing-over-effectful-fn.ur

@@ -0,0 +1 @@
+[0,1,2,3,4]