mirror of
https://github.com/unisonweb/unison.git
synced 2024-09-11 02:25:39 +03:00
1.1 KiB
1.1 KiB
scratch/main> builtins.merge
structural ability X t where
x : t -> a -> a
structural ability Abort where
abort : a
scratch/main> add
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
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
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
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