mirror of
https://github.com/unisonweb/unison.git
synced 2024-09-11 10:35:57 +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.
60 lines
1.5 KiB
Markdown
60 lines
1.5 KiB
Markdown
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.
|
|
|
|
``` 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)
|
|
```
|
|
|
|
``` 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`:
|
|
|
|
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))} ()
|
|
|
|
```
|