unison/unison-src/transcripts/fix693.output.md

120 lines
2.4 KiB
Markdown
Raw Normal View History

```unison
ability X t where
x : t -> a -> a
ability Abort where
abort : a
```
```ucm
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`:
ability Abort
ability X t
```
```ucm
.> add
⍟ I've added these definitions:
ability Abort
ability X t
```
This code should not type check. The match on X.x ought to introduce a
skolem variable `a` such that `c : a` and the continuation has type
`a ->{X} b`. Thus, `handle c with h : Optional a`, which is not the
correct result type.
```unison
h0 : Request {X t} b -> Optional b
h0 req = match req with
{ X.x _ c -> _ } -> handle c with h0
{ d } -> Some d
```
```ucm
I found a value of type builtin.Optional a1 where I expected to find one of type builtin.Optional a:
1 | h0 : Request {X t} b -> Optional b
2 | h0 req = match req with
3 | { X.x _ c -> _ } -> handle c with h0
from right here:
1 | h0 : Request {X t} b -> Optional b
```
This code should not check because `t` does not match `b`.
```unison
h1 : Request {X t} b -> Optional b
h1 req = match req with
{ X.x t _ -> _ } -> handle t with h1
{ d } -> Some d
```
```ucm
Each case of a match / with expression need to have the same
type. Here, one is builtin.Optional t and another is
builtin.Optional b :
3 | { X.x t _ -> _ } -> handle t with h1
4 | { d } -> Some d
from right here:
1 | h1 : Request {X t} b -> Optional b
```
This code should not check for reasons similar to the first example,
but with the continuation rather than a parameter.
```unison
h2 : Request {Abort} r -> r
h2 req = match req with
{ Abort.abort -> k } -> handle k 5 with h2
{ r } -> r
```
```ucm
The 1st argument to the function k is builtin.Nat, but I was expecting a:
3 | { Abort.abort -> k } -> handle k 5 with h2
```
This should work fine.
```unison
h3 : Request {X b, Abort} b -> Optional b
h3 = cases
{ r } -> Some r
{ Abort.abort -> _ } -> None
{ X.x b _ -> _ } -> Some b
```
```ucm
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`:
h3 : Request {X b, Abort} b -> Optional b
```