2021-07-12 17:45:07 +03:00
|
|
|
This is just a simple transcript to regression check an ability
|
|
|
|
inference/checking issue.
|
|
|
|
|
2024-07-10 17:46:18 +03:00
|
|
|
``` unison
|
2021-08-24 21:33:27 +03:00
|
|
|
structural ability R t where
|
2021-07-12 17:45:07 +03:00
|
|
|
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 ()
|
|
|
|
```
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2021-07-12 17:45:07 +03:00
|
|
|
|
2023-12-22 14:55:24 +03:00
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
|
2021-07-12 17:45:07 +03:00
|
|
|
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`:
|
|
|
|
|
2021-08-24 21:33:27 +03:00
|
|
|
structural ability R t
|
2021-07-12 17:45:07 +03:00
|
|
|
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.
|
2024-07-10 17:46:18 +03:00
|
|
|
|