mirror of
https://github.com/unisonweb/unison.git
synced 2024-09-11 02:25:39 +03:00
58 lines
1.2 KiB
Markdown
58 lines
1.2 KiB
Markdown
Tests ability checking in scenarios where one side is concrete and the other is
|
|
a variable. This was supposed to be covered, but the method wasn't actually
|
|
symmetric, so doing `equate l r` might work, but not `equate r l`.
|
|
|
|
Below were cases that caused the failing order.
|
|
|
|
``` unison
|
|
structural type W es = W
|
|
|
|
unique ability Zoot where
|
|
zoot : ()
|
|
|
|
-- here only to put a kind constraint on W
|
|
structural type C = C (W {})
|
|
|
|
woot : W {g} -> '{g, Zoot} a ->{Zoot} a
|
|
woot w a = todo ()
|
|
|
|
ex = do
|
|
w = (W : W {Zoot})
|
|
woot w do bug "why don't you typecheck?"
|
|
|
|
w1 : W {Zoot}
|
|
w1 = W
|
|
|
|
w2 : W {g} -> W {g}
|
|
w2 = cases W -> W
|
|
|
|
> w2 w1
|
|
```
|
|
|
|
``` 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`:
|
|
|
|
structural type C
|
|
structural type W es
|
|
ability Zoot
|
|
ex : '{Zoot} r
|
|
w1 : W {Zoot}
|
|
w2 : W {g} -> W {g}
|
|
woot : W {g} -> '{g, Zoot} a ->{Zoot} a
|
|
|
|
Now evaluating any watch expressions (lines starting with
|
|
`>`)... Ctrl+C cancels.
|
|
|
|
22 | > w2 w1
|
|
⧩
|
|
W
|
|
|
|
```
|