Merge pull request #2197 from unisonweb/fix/abilities

Fix some ability checking regressions.

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

@@ -56,6 +56,7 @@ import           Data.Functor.Compose           ( Compose(..) )
 import           Data.List
 import           Data.List.NonEmpty             ( NonEmpty )
 import qualified Data.Map                      as Map
+import           Data.Ord                       ( comparing )
 import qualified Data.Sequence                 as Seq
 import           Data.Sequence.NonEmpty         ( NESeq )
 import qualified Data.Sequence.NonEmpty        as NESeq
@@ -1698,9 +1699,21 @@ substAndDefaultWanted
 substAndDefaultWanted want ctx
   | want <- (fmap.fmap) (applyCtx ctx) want
   , want <- filter q want
-  = coalesceWanted want []
+  , repush <- filter keep ctx
+  = appendContext repush *> coalesceWanted want []
   where
-  p (Var v@TypeVar.Existential{}) = Just v
+  isExistential TypeVar.Existential{} = True
+  isExistential _ = False
+
+  -- get the free variables of things that aren't just variables
+  necessary (Type.Var' _) = mempty
+  necessary t = Set.filter isExistential $ Type.freeVars t
+
+  keeps = foldMap (necessary.snd) want
+  keep (Var v) = v `Set.member` keeps
+  keep _ = False
+
+  p (Var v) | isExistential v = Just v
   p _ = Nothing
 
   outScope = Set.fromList $ mapMaybe p ctx
@@ -2108,8 +2121,12 @@ pruneAbilities
   -> M v loc (Wanted v loc)
 pruneAbilities want0 have0
   | debugShow ("pruneAbilities", want0, have0) = undefined
-pruneAbilities want0 have0 = go [] want0 have0
+pruneAbilities want0 have0
+  = go [] (sortBy (comparing (isVar.snd)) want0) have0
   where
+  isVar (Type.Var' _) = True
+  isVar _ = False
+
   isExistential (Type.Var' TypeVar.Existential{}) = True
   isExistential _ = False
 

unison-src/transcripts-using-base/fix2158-1.md

@@ -0,0 +1,25 @@
+This transcript tests an ability check failure regression.
+
+```unison
+ability Async t g where
+  fork : '{Async t g, g} a -> t a
+  await : t a -> a
+
+Async.parMap : (a ->{Async t g, g} b) -> [a] ->{Async t g} [b]
+Async.parMap f as = 
+  tasks = List.map (a -> fork '(f a)) as 
+  List.map await tasks
+```
+
+The issue was that certain ability processing was happing in less
+optimal order. `g` appears both as an ability used and as a parameter
+to `Async`. However, the latter occurrence is more strict. Unifying
+the types `Async t g1` and `Async t g2` requires `g1` and `g2` to
+be equal, while abilities that occur directly in a row are subject to
+some subtyping.
+
+However, the ability handling was just processing rows in whatever
+order they occurred, and during inference it happened that `g`
+occurred in the row before `Async t g`. Processing the stricter parts
+first is better, becauase it can solve things more precisely and avoid
+ambiguities relating to subtyping.

unison-src/transcripts-using-base/fix2158-1.output.md

@@ -0,0 +1,39 @@
+This transcript tests an ability check failure regression.
+
+```unison
+ability Async t g where
+  fork : '{Async t g, g} a -> t a
+  await : t a -> a
+
+Async.parMap : (a ->{Async t g, g} b) -> [a] ->{Async t g} [b]
+Async.parMap f as = 
+  tasks = List.map (a -> fork '(f a)) as 
+  List.map await tasks
+```
+
+```ucm
+
+  I found and typechecked these definitions in scratch.u. If you
+  do an `add` or `update`, here's how your codebase would
+  change:
+  
+    ⍟ These new definitions are ok to `add`:
+    
+      ability Async t g
+      Async.parMap : (a ->{g, Async t g} b)
+                     -> [a]
+                     ->{Async t g} [b]
+
+```
+The issue was that certain ability processing was happing in less
+optimal order. `g` appears both as an ability used and as a parameter
+to `Async`. However, the latter occurrence is more strict. Unifying
+the types `Async t g1` and `Async t g2` requires `g1` and `g2` to
+be equal, while abilities that occur directly in a row are subject to
+some subtyping.
+
+However, the ability handling was just processing rows in whatever
+order they occurred, and during inference it happened that `g`
+occurred in the row before `Async t g. Processing the stricter parts
+first is better, becauase it can solve things more precisely and avoid
+ambiguities relating to subtyping.

unison-src/transcripts/fix2167.md

@@ -0,0 +1,28 @@
+```ucm:hide
+.> builtins.merge
+```
+
+This is just a simple transcript to regression check an ability
+inference/checking issue.
+
+```unison
+ability R t where
+  die : () -> x
+  near.impl : Nat -> Either () [Nat]
+
+R.near n = match near.impl n with
+  Left e -> die ()
+  Right a -> a
+
+R.near1 region loc = match R.near 42 with
+  [loc] -> loc
+  ls -> R.die ()
+```
+
+The issue was that abilities with parameters like this were sometimes
+causing failures like this because the variable in the parameter would
+escape to a scope where it no longer made sense. Then solving would
+fail because the type was invalid.
+
+The fix was to avoid dropping certain existential variables out of
+scope.

unison-src/transcripts/fix2167.output.md

@@ -0,0 +1,37 @@
+This is just a simple transcript to regression check an ability
+inference/checking issue.
+
+```unison
+ability R t where
+  die : () -> x
+  near.impl : Nat -> Either () [Nat]
+
+R.near n = match near.impl n with
+  Left e -> die ()
+  Right a -> a
+
+R.near1 region loc = match R.near 42 with
+  [loc] -> loc
+  ls -> R.die ()
+```
+
+```ucm
+
+  I found and typechecked these definitions in scratch.u. If you
+  do an `add` or `update`, here's how your codebase would
+  change:
+  
+    ⍟ These new definitions are ok to `add`:
+    
+      ability R t
+      R.near  : Nat ->{R t} [Nat]
+      R.near1 : region -> loc ->{R t} Nat
+
+```
+The issue was that abilities with parameters like this were sometimes
+causing failures like this because the variable in the parameter would
+escape to a scope where it no longer made sense. Then solving would
+fail because the type was invalid.
+
+The fix was to avoid dropping certain existential variables out of
+scope.