blob: a14616d76657d66ff78e587e3870e75a55784c55 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
|
(* TEST
* expect
*)
type _ t = I : int t;;
let f (type a) (x : a t) =
let module M = struct
let (I : a t) = x (* fail because of toplevel let *)
let x = (I : a t)
end in
() ;;
[%%expect{|
type _ t = I : int t
Line 5, characters 9-10:
5 | let (I : a t) = x (* fail because of toplevel let *)
^
Error: This pattern matches values of type int t
but a pattern was expected which matches values of type a t
Type int is not compatible with type a
|}];;
(* extra example by Stephen Dolan, using recursive modules *)
(* Should not be allowed! *)
type (_,_) eq = Refl : ('a, 'a) eq;;
let bad (type a) =
let module N = struct
module rec M : sig
val e : (int, a) eq
end = struct
let (Refl : (int, a) eq) = M.e (* must fail for soundness *)
let e : (int, a) eq = Refl
end
end in N.M.e
;;
[%%expect{|
type (_, _) eq = Refl : ('a, 'a) eq
Line 8, characters 10-14:
8 | let (Refl : (int, a) eq) = M.e (* must fail for soundness *)
^^^^
Error: This pattern matches values of type (int, int) eq
but a pattern was expected which matches values of type (int, a) eq
Type int is not compatible with type a
|}];;
|
