From f5c454216ae78e5133e068c05afb0803293731ff Mon Sep 17 00:00:00 2001 From: Dan Doel Date: Thu, 8 Jul 2021 15:22:30 -0400 Subject: [PATCH 1/3] Sort before pruning abilities - Handling concrete ability unification before variables seems more likely to produce good results, since the concrete ability equality is more restrictive about how variables must behave, and will narrow things down more. --- parser-typechecker/src/Unison/Typechecker/Context.hs | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/parser-typechecker/src/Unison/Typechecker/Context.hs b/parser-typechecker/src/Unison/Typechecker/Context.hs index 50d5e1199..49c818b4d 100644 --- a/parser-typechecker/src/Unison/Typechecker/Context.hs +++ b/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 @@ -2108,8 +2109,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 From f5ce1c75d245d3f2faa436996cf09bf8f2499c38 Mon Sep 17 00:00:00 2001 From: Dan Doel Date: Fri, 9 Jul 2021 17:34:17 -0400 Subject: [PATCH 2/3] Propagate necessary existentials out of matches - Match branches do some context manipulation which can cause existentials to be dropped from the context even though they are still necessary to make sense of the wanted abilities. This change re-adds those existentials to the context to ensure that the abilities remain sensical. --- .../src/Unison/Typechecker/Context.hs | 16 ++++++++++++++-- 1 file changed, 14 insertions(+), 2 deletions(-) diff --git a/parser-typechecker/src/Unison/Typechecker/Context.hs b/parser-typechecker/src/Unison/Typechecker/Context.hs index 49c818b4d..4716c4078 100644 --- a/parser-typechecker/src/Unison/Typechecker/Context.hs +++ b/parser-typechecker/src/Unison/Typechecker/Context.hs @@ -1699,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 From 99ff3208206a3e758dab7507119859a2f1131a78 Mon Sep 17 00:00:00 2001 From: Dan Doel Date: Mon, 12 Jul 2021 10:45:07 -0400 Subject: [PATCH 3/3] Add tests --- .../transcripts-using-base/fix2158-1.md | 25 ++++++++++++ .../fix2158-1.output.md | 39 +++++++++++++++++++ unison-src/transcripts/fix2167.md | 28 +++++++++++++ unison-src/transcripts/fix2167.output.md | 37 ++++++++++++++++++ 4 files changed, 129 insertions(+) create mode 100644 unison-src/transcripts-using-base/fix2158-1.md create mode 100644 unison-src/transcripts-using-base/fix2158-1.output.md create mode 100644 unison-src/transcripts/fix2167.md create mode 100644 unison-src/transcripts/fix2167.output.md diff --git a/unison-src/transcripts-using-base/fix2158-1.md b/unison-src/transcripts-using-base/fix2158-1.md new file mode 100644 index 000000000..c80faa3f1 --- /dev/null +++ b/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. diff --git a/unison-src/transcripts-using-base/fix2158-1.output.md b/unison-src/transcripts-using-base/fix2158-1.output.md new file mode 100644 index 000000000..f9419e4a4 --- /dev/null +++ b/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. diff --git a/unison-src/transcripts/fix2167.md b/unison-src/transcripts/fix2167.md new file mode 100644 index 000000000..cb5a64f30 --- /dev/null +++ b/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. diff --git a/unison-src/transcripts/fix2167.output.md b/unison-src/transcripts/fix2167.output.md new file mode 100644 index 000000000..4a6f3de65 --- /dev/null +++ b/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.