1(* Injectivity *) 2 3type (_, _) eq = Refl : ('a, 'a) eq 4 5let magic : 'a 'b. 'a -> 'b = 6 fun (type a b) (x : a) -> 7 let module M = 8 (functor (T : sig type 'a t end) -> 9 struct 10 let f (Refl : (a T.t, b T.t) eq) = (x :> b) 11 end) 12 (struct type 'a t = unit end) 13 in M.f Refl 14;; 15[%%expect{| 16type (_, _) eq = Refl : ('a, 'a) eq 17Line _, characters 44-52: 18Error: Type a is not a subtype of b 19|}];; 20 21(* Variance and subtyping *) 22 23type (_, +_) eq = Refl : ('a, 'a) eq 24 25let magic : 'a 'b. 'a -> 'b = 26 fun (type a) (type b) (x : a) -> 27 let bad_proof (type a) = 28 (Refl : (< m : a>, <m : a>) eq :> (<m : a>, < >) eq) in 29 let downcast : type a. (a, < >) eq -> < > -> a = 30 fun (type a) (Refl : (a, < >) eq) (s : < >) -> (s :> a) in 31 (downcast bad_proof ((object method m = x end) :> < >)) # m 32;; 33[%%expect{| 34Line _, characters 0-36: 35Error: In this GADT definition, the variance of some parameter 36 cannot be checked 37|}];; 38 39(* Record patterns *) 40 41type _ t = 42 | IntLit : int t 43 | BoolLit : bool t 44 45let check : type s . s t * s -> bool = function 46 | BoolLit, false -> false 47 | IntLit , 6 -> false 48;; 49[%%expect{| 50type _ t = IntLit : int t | BoolLit : bool t 51Line _, characters 39-99: 52Warning 8: this pattern-matching is not exhaustive. 53Here is an example of a case that is not matched: 54(IntLit, 0) 55val check : 's t * 's -> bool = <fun> 56|}];; 57 58type ('a, 'b) pair = { fst : 'a; snd : 'b } 59 60let check : type s . (s t, s) pair -> bool = function 61 | {fst = BoolLit; snd = false} -> false 62 | {fst = IntLit ; snd = 6} -> false 63;; 64[%%expect{| 65type ('a, 'b) pair = { fst : 'a; snd : 'b; } 66Line _, characters 45-134: 67Warning 8: this pattern-matching is not exhaustive. 68Here is an example of a case that is not matched: 69{fst=IntLit; snd=0} 70val check : ('s t, 's) pair -> bool = <fun> 71|}];; 72