1--
2-- Copyright 2016, NICTA
3--
4-- This software may be distributed and modified according to the terms of
5-- the GNU General Public License version 2. Note that NO WARRANTY is provided.
6-- See "LICENSE_GPLv2.txt" for details.
7--
8-- @TAG(NICTA_GPL)
9--
10
11type R a b = <Ok a | Bad b>
12
13type A = U32
14type B
15
16c : U16
17c = 23
18
19bar : R A B -> R Bool U32
20
21foo : R A #B -> R Bool U32
22foo x = x | Ok  a -> Ok True
23          | Bad b -> Bad 3
24
25poly : all (a, b). U32 -> R a b
26
27f : all a. a -> U32
28
29use : () -> ()
30use _ = let _ = poly[U32, Bool] 3
31        and x = poly[A, B] 2
32        and _ = bar x
33        and t = poly[Bool, R U32 #B] 1
34        and _ = f[Bool] True
35        and _ = f[U32] c
36        and _ = f[R Bool (R U32 #B)] t
37        in ()
38
39type X a b
40
41baz : X U32 B -> X U32 #B
42
43
44