mirror of
https://github.com/unisonweb/unison.git
synced 2024-09-17 13:27:30 +03:00
1dc181b99a
`cmark`’s pretty-printer matches our output pretty well, with a few differences: - it puts a space between the fence and the info string for in code blocks; - it prefers `-` over `*` for bulleted lists (as do I) and it indents them; - it `\`-escapes certain chars very conservatively; - it prefers indented/unfenced code blocks if there is no info string; and - it prefers `*` over `_` (unlike any sane person). This also shows how the change fixes a number of issues: - fix2158-1.output.md also illustrates how this change fixes #1809; - alias-many.output.md and input-parse-errors.output.md show how fenced code blocks without an info string would use the beginning of the content as the info string; - transcripts-round-trip/main.output.md shows how output blocks for generated `unison` stanzas (which could contain nested fenced blocks) might not have long-enough fences; and - error-messages.output.md and generic-parse-errors.output.md show how Unison errors were reported on the wrong line number (and thus the printed error lines were also incorrect).
2.6 KiB
2.6 KiB
structural ability X t where
x : t -> a -> a
structural ability Abort where
abort : a
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 ability Abort
structural ability X t
scratch/main> add
⍟ I've added these definitions:
structural ability Abort
structural 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.
h0 : Request {X t} b -> Optional b
h0 req = match req with
{ X.x _ c -> _ } -> handle c with h0
{ d } -> Some d
Loading changes detected in scratch.u.
Each case of a match / with expression need to have the same
type.
Here, one is: Optional b
and another is: Optional a
3 | { X.x _ c -> _ } -> handle c with h0
from these spots, respectively:
1 | h0 : Request {X t} b -> Optional b
This code should not check because t
does not match b
.
h1 : Request {X t} b -> Optional b
h1 req = match req with
{ X.x t _ -> _ } -> handle t with h1
{ d } -> Some d
Loading changes detected in scratch.u.
Each case of a match / with expression need to have the same
type.
Here, one is: Optional b
and another is: Optional t
3 | { X.x t _ -> _ } -> handle t with h1
from these spots, respectively:
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.
h2 : Request {Abort} r -> r
h2 req = match req with
{ Abort.abort -> k } -> handle k 5 with h2
{ r } -> r
Loading changes detected in scratch.u.
The 1st argument to `k`
has type: Nat
but I expected: a
3 | { Abort.abort -> k } -> handle k 5 with h2
This should work fine.
h3 : Request {X b, Abort} b -> Optional b
h3 = cases
{ r } -> Some r
{ Abort.abort -> _ } -> None
{ X.x b _ -> _ } -> Some b
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`:
h3 : Request {X b, Abort} b -> Optional b