2024-03-08 23:18:35 +03:00
|
|
|
|
|
|
|
Tests an improvement to type checking related to abilities.
|
|
|
|
|
|
|
|
`foo` below typechecks fine as long as all the branches are _checked_
|
|
|
|
against their expected type. However, it's annoying to have to
|
|
|
|
annotate them. The old code was checking a match by just synthesizing
|
|
|
|
and subtyping, but we can instead check a match by pushing the
|
|
|
|
expected type into each case, allowing top-level annotations to act
|
|
|
|
like annotations on each case.
|
|
|
|
|
|
|
|
```ucm:hide
|
2024-06-12 01:22:09 +03:00
|
|
|
scratch/main> builtins.merge
|
2024-03-08 23:18:35 +03:00
|
|
|
```
|
|
|
|
|
|
|
|
```unison
|
|
|
|
ability X a where yield : {X a} ()
|
|
|
|
ability Y where y : ()
|
|
|
|
|
|
|
|
type Foo b a = One a
|
|
|
|
type Bar a
|
|
|
|
= Leaf a
|
|
|
|
| Branch (Bar a) (Bar a)
|
|
|
|
|
|
|
|
f : (a -> ()) -> '{g, X a} () -> '{g, X a} () -> '{g, X a} ()
|
|
|
|
f _ x y = y
|
|
|
|
|
|
|
|
abra : a -> '{Y, X z} r
|
|
|
|
abra = bug ""
|
|
|
|
|
|
|
|
cadabra : (y -> z) -> '{g, X y} r -> '{g, X z} r
|
|
|
|
cadabra = bug ""
|
|
|
|
|
|
|
|
foo : Bar (Optional b) -> '{Y, X (Foo z ('{Y} r))} ()
|
|
|
|
foo = cases
|
|
|
|
Leaf a -> match a with
|
|
|
|
None -> abra a
|
|
|
|
Some _ -> cadabra One (abra a)
|
|
|
|
Branch l r ->
|
|
|
|
f (_ -> ()) (foo l) (foo r)
|
|
|
|
```
|