unison/unison-src/transcripts/fix2167.md
2024-06-25 11:11:07 -07:00

697 B

scratch/main> builtins.merge

This is just a simple transcript to regression check an ability inference/checking issue.

structural 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.