blob: ca5eeaa7199c243daa6ca60d8160b507d2424e6a (
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
|
(* TEST
expect;
*)
type (_,_) eq = Refl : ('a,'a) eq
module M = struct type t end
module N : sig type t = private M.t val eq : (t, M.t) eq end =
struct type t = M.t let eq = Refl end;;
(*
as long as we are casting between M.t and N.t
there is no problem, this will type check.
*)
let f x = match N.eq with Refl -> (x : N.t :> M.t);;
[%%expect{|
type (_, _) eq = Refl : ('a, 'a) eq
module M : sig type t end
module N : sig type t = private M.t val eq : (t, M.t) eq end
val f : N.t -> M.t = <fun>
|}]
let f x = match N.eq with Refl -> (x : M.t :> N.t);;
[%%expect{|
Line 1, characters 34-50:
1 | let f x = match N.eq with Refl -> (x : M.t :> N.t);;
^^^^^^^^^^^^^^^^
Error: Type M.t is not a subtype of N.t
|}]
(*
but as soon we're trying to cast to another type,
the type checker will never return and memory
consumption will increase drastically.
*)
|
