Merge pull request #2364 from unisonweb/fix/2355

Avoid a loop caused by inferring cyclic abilities

parser-typechecker/src/Unison/PrintError.hs

@@ -364,6 +364,30 @@ renderTypeError e env src = case e of
       ]
     , debugSummary note
     ]
+  AbilityCheckFailure {..}
+    | [tv@(Type.Var' ev)] <- ambient
+    , ev `Set.member` foldMap Type.freeVars requested -> mconcat
+    [ "I tried to infer a cyclic ability."
+    , "\n\n"
+    , "The expression "
+    , describeStyle ErrorSite
+    , " was inferred to require the "
+    , case length requested of
+        1 -> "ability: "
+        _ -> "abilities: "
+    , "\n\n    {"
+    , commas (renderType' env) requested
+    , "}"
+    , "\n\n"
+    , "where `"
+    , renderType' env tv
+    , "` is its overall abilities."
+    , "\n\n"
+    , "I need a type signature to help figure this out."
+    , "\n\n"
+    , annotatedAsErrorSite src abilityCheckFailureSite
+    , debugSummary note
+    ]
   AbilityCheckFailure {..}
     | C.InSubtype{} :<| _ <- C.path note -> mconcat
     [ "The expression "

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

@@ -2109,11 +2109,16 @@ refineEffectVar
   -> [Type v loc]
   -> B.Blank loc
   -> v
+  -> Type v loc
   -> M v loc ()
-refineEffectVar _ es _ v
+refineEffectVar _ es _ v _
   | debugShow ("refineEffectVar", es, v) = undefined
-refineEffectVar _ [] _ _ = pure ()
-refineEffectVar l es blank v = do
+refineEffectVar _ [] _ _ _ = pure ()
+refineEffectVar l es blank v tv
+  | ev <- TypeVar.Existential blank v
+  , any (\e -> ev `Set.member` Type.freeVars e) es
+  = getContext >>= failWith . AbilityCheckFailure [tv] es
+  | otherwise = do
   slack <- freshenVar Var.inferAbility
   evs <- traverse (\e -> freshenVar (nameFrom Var.inferAbility e)) es
   let locs = loc <$> es
@@ -2277,11 +2282,11 @@ subAbilities want have = do
   have <- expandAbilities have
   case (want , mapMaybe ex have) of
     ([], _) -> pure ()
-    (want@((_, w):_), [(b, ve)]) ->
-      refineEffectVar (loc w) (snd <$> want) b ve -- `orElse` die src w
+    (want@((_, w):_), [(b, ve, tv)]) ->
+      refineEffectVar (loc w) (snd <$> want) b ve tv -- `orElse` die src w
     ((src, w):_, _) -> die src w
   where
-  ex (Type.Var' (TypeVar.Existential b v)) = Just (b, v)
+  ex t@(Type.Var' (TypeVar.Existential b v)) = Just (b, v, t)
   ex _ = Nothing
   die src w = maybe id (scope . InSynthesize) src do
     ctx <- getContext

unison-src/transcripts/fix2355.md

@@ -0,0 +1,25 @@
+
+Tests for a loop that was previously occurring in the type checker.
+
+```ucm:hide
+.> builtins.merge
+```
+
+```unison:error
+structural ability A t g where 
+  fork : '{g, A t g} a -> t a
+  await : t a -> a
+  empty! : t a
+  put : a -> t a -> ()
+
+example : '{A t {}} Nat
+example = 'let
+  r = A.empty!
+  go u = 
+    t = A.fork '(go (u + 1))
+    A.await t
+  
+  go 0
+  t2 = A.fork '(A.put 10 r)
+  A.await r
+```

unison-src/transcripts/fix2355.output.md

@@ -0,0 +1,40 @@
+
+Tests for a loop that was previously occurring in the type checker.
+
+```unison
+structural ability A t g where 
+  fork : '{g, A t g} a -> t a
+  await : t a -> a
+  empty! : t a
+  put : a -> t a -> ()
+
+example : '{A t {}} Nat
+example = 'let
+  r = A.empty!
+  go u = 
+    t = A.fork '(go (u + 1))
+    A.await t
+  
+  go 0
+  t2 = A.fork '(A.put 10 r)
+  A.await r
+```
+
+```ucm
+
+  I tried to infer a cyclic ability.
+  
+  The expression in red was inferred to require the ability: 
+  
+      {A t25 {𝕖39, 𝕖18}}
+  
+  where `𝕖18` is its overall abilities.
+  
+  I need a type signature to help figure this out.
+  
+     10 |   go u = 
+     11 |     t = A.fork '(go (u + 1))
+     12 |     A.await t
+  
+
+```