diff --git a/unison-src/transcripts/fix2350.md b/unison-src/transcripts/fix2350.md new file mode 100644 index 000000000..667b8a419 --- /dev/null +++ b/unison-src/transcripts/fix2350.md @@ -0,0 +1,26 @@ + +This tests an issue where ability variables were being defaulted over +eagerly. In general, we want to avoid collecting up variables from the +use of definitions with types like: + + T ->{e} U + +Since this type works for every `e`, it is, 'pure;' and we might as +well have `e = {}`, since `{}` is a subrow of every other row. +However, if `e` isn't just a quantified variable, but one involved in +ongoing inference, it's undesirable to default it. Previously there +was a check to see if `e` occurred in the context. However, the wanted +abilities being collected aren't in the context, so types like: + + T ->{S e} U ->{e} V + +were a corner case. We would add `S e` to the wanted abilities, then +not realize that `e` shouldn't be defaulted. + +```unison +unique ability Storage d g where + save.impl : a ->{Storage d g} ('{g} (d a)) + +save : a ->{Storage d g, g} (d a) +save a = !(save.impl a) +``` diff --git a/unison-src/transcripts/fix2350.output.md b/unison-src/transcripts/fix2350.output.md new file mode 100644 index 000000000..10f223c86 --- /dev/null +++ b/unison-src/transcripts/fix2350.output.md @@ -0,0 +1,39 @@ + +This tests an issue where ability variables were being defaulted over +eagerly. In general, we want to avoid collecting up variables from the +use of definitions with types like: + + T ->{e} U + +Since this type works for every `e`, it is, 'pure;' and we might as +well have `e = {}`, since `{}` is a subrow of every other row. +However, if `e` isn't just a quantified variable, but one involved in +ongoing inference, it's undesirable to default it. Previously there +was a check to see if `e` occurred in the context. However, the wanted +abilities being collected aren't in the context, so types like: + + T ->{S e} U ->{e} V + +were a corner case. We would add `S e` to the wanted abilities, then +not realize that `e` shouldn't be defaulted. + +```unison +unique ability Storage d g where + save.impl : a ->{Storage d g} ('{g} (d a)) + +save : a ->{Storage d g, g} (d a) +save a = !(save.impl a) +``` + +```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`: + + unique ability Storage d g + save : a ->{g, Storage d g} d a + +``` diff --git a/unison-src/transcripts/fix2474.md b/unison-src/transcripts/fix2474.md new file mode 100644 index 000000000..d79e74e8c --- /dev/null +++ b/unison-src/transcripts/fix2474.md @@ -0,0 +1,35 @@ + +Tests an issue with a lack of generality of handlers. + +In general, a set of cases: + + { e ... -> k } + +should be typed in the following way: + + 1. The scrutinee has type `Request {E, g} r -> s` where `E` is all + the abilities being handled. `g` is a slack variable, because all + abilities that are used in the handled expression pass through + the handler. Previously this was being inferred as merely + `Request {E} r -> s` + 2. The continuation variable `k` should have type `o ->{E, g} r`, + matching the above types (`o` is the result type of `e`). + Previously this was being checked as `o ->{E0} r`, where `E0` is + the ability that contains `e`. + +```ucm +.> builtins.mergeio +``` + +```unison +structural ability Stream a where + emit : a -> () + +Stream.uncons : '{Stream a, g} r ->{g} Either r (a, '{Stream a, g} r) +Stream.uncons s = + go : Request {Stream a,g} r -> Either r (a, '{Stream a,g} r) + go = cases + { r } -> Left r + { Stream.emit a -> tl } -> Right (a, tl : '{Stream a,g} r) + handle !s with go +``` diff --git a/unison-src/transcripts/fix2474.output.md b/unison-src/transcripts/fix2474.output.md new file mode 100644 index 000000000..cedaf7b00 --- /dev/null +++ b/unison-src/transcripts/fix2474.output.md @@ -0,0 +1,51 @@ + +Tests an issue with a lack of generality of handlers. + +In general, a set of cases: + + { e ... -> k } + +should be typed in the following way: + + 1. The scrutinee has type `Request {E, g} r -> s` where `E` is all + the abilities being handled. `g` is a slack variable, because all + abilities that are used in the handled expression pass through + the handler. Previously this was being inferred as merely + `Request {E} r -> s` + 2. The continuation variable `k` should have type `o ->{E, g} r`, + matching the above types (`o` is the result type of `e`). + Previously this was being checked as `o ->{E0} r`, where `E0` is + the ability that contains `e`. + +```ucm +.> builtins.mergeio + + Done. + +``` +```unison +structural ability Stream a where + emit : a -> () + +Stream.uncons : '{Stream a, g} r ->{g} Either r (a, '{Stream a, g} r) +Stream.uncons s = + go : Request {Stream a,g} r -> Either r (a, '{Stream a,g} r) + go = cases + { r } -> Left r + { Stream.emit a -> tl } -> Right (a, tl : '{Stream a,g} r) + handle !s with go +``` + +```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`: + + structural ability Stream a + Stream.uncons : '{g, Stream a} r + ->{g} Either r (a, '{g, Stream a} r) + +```