mirror of
https://github.com/unisonweb/unison.git
synced 2024-09-11 02:25:39 +03:00
45 lines
1.2 KiB
Markdown
45 lines
1.2 KiB
Markdown
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
|
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
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 Storage d g
|
|
save : a ->{g, Storage d g} d a
|
|
|
|
```
|