mirror of
https://github.com/unisonweb/unison.git
synced 2024-08-15 13:30:27 +03:00
0031542faf
This is for consistency with the `cmark` style. Now the blocks we still pretty-print ourselves will match the bulk of them that `cmark` produces.
1.5 KiB
1.5 KiB
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.
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)
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`:
type Bar a
type Foo b a
ability X a
ability Y
abra : a -> '{Y, X z} r
cadabra : (y ->{h} z) -> '{g, X y} r -> '{g, X z} r
f : (a ->{h} ())
-> '{g, X a} ()
-> '{g, X a} ()
-> '{g, X a} ()
foo : Bar (Optional b) -> '{Y, X (Foo z ('{Y} r))} ()