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