Ekdohibs
/
ocaml
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

fix gadt type variables 

git-svn-id: http://caml.inria.fr/svn/ocaml/trunk@11211 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
master
Jacques Garrigue 2011-09-27 06:37:06 +00:00
parent 156fff1b8a
commit ac275d142b
7 changed files with 531 additions and 159 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

363
experimental/garrigue/gadt-escape-check.diffs Normal file
View File

@ -0,0 +1,363 @@
Index: typing/env.ml
===================================================================
--- typing/env.ml (revision 11210)
+++ typing/env.ml (working copy)
@@ -56,7 +56,7 @@
cltypes: (Path.t * cltype_declaration) Ident.tbl;
summary: summary;
local_constraints: bool;
- level_map: (int * int) list;
+ gadt_instances: (int * Btype.TypeSet.t ref) list;
}
and module_components = module_components_repr Lazy.t
@@ -96,7 +96,7 @@
modules = Ident.empty; modtypes = Ident.empty;
components = Ident.empty; classes = Ident.empty;
cltypes = Ident.empty;
- summary = Env_empty; local_constraints = false; level_map = [] }
+ summary = Env_empty; local_constraints = false; gadt_instances = [] }
let diff_keys is_local tbl1 tbl2 =
let keys2 = Ident.keys tbl2 in
@@ -286,13 +286,14 @@
(* the level is changed when updating newtype definitions *)
if !Clflags.principal then begin
match level, decl.type_newtype_level with
- Some level, Some def_level when level < def_level -> raise Not_found
+ Some level, Some (_, exp_level) when level < exp_level -> raise Not_found
| _ -> ()
end;
match decl.type_manifest with
| Some body when decl.type_private = Public
|| decl.type_kind <> Type_abstract
- || Btype.has_constr_row body -> (decl.type_params, body)
+ || Btype.has_constr_row body ->
+ (decl.type_params, body, may_map snd decl.type_newtype_level)
(* The manifest type of Private abstract data types without
private row are still considered unknown to the type system.
Hence, this case is caught by the following clause that also handles
@@ -308,7 +309,7 @@
match decl.type_manifest with
(* The manifest type of Private abstract data types can still get
an approximation using their manifest type. *)
- | Some body -> (decl.type_params, body)
+ | Some body -> (decl.type_params, body, may_map snd decl.type_newtype_level)
| _ -> raise Not_found
let find_modtype_expansion path env =
@@ -453,33 +454,35 @@
and lookup_cltype =
lookup (fun env -> env.cltypes) (fun sc -> sc.comp_cltypes)
-(* Level handling *)
+(* GADT instance tracking *)
-(* The level map is a list of pairs describing separate segments (lv,lv'),
- lv < lv', organized in decreasing order.
- The definition level is obtained by mapping a level in a segment to the
- high limit of this segment.
- The definition level of a newtype should be greater or equal to
- the highest level of the newtypes in its manifest type.
- *)
+let gadt_instance_level env t =
+ let rec find_instance = function
+ [] -> None
+ | (lv, r) :: rem ->
+ if Btype.TypeSet.mem t !r then Some lv else find_instance rem
+ in find_instance env.gadt_instances
-let rec map_level lv = function
- | [] -> lv
- | (lv1, lv2) :: rem ->
- if lv > lv2 then lv else
- if lv >= lv1 then lv2 else map_level lv rem
+let add_gadt_instances env lv tl =
+ let r =
+ try List.assoc lv env.gadt_instances with Not_found -> assert false in
+ r := List.fold_right Btype.TypeSet.add tl !r
-let map_newtype_level env lv = map_level lv env.level_map
+(* Only use this after expand_head! *)
+let add_gadt_instance_chain env lv t =
+ let r =
+ try List.assoc lv env.gadt_instances with Not_found -> assert false in
+ let rec add_instance t =
+ let t = Btype.repr t in
+ if not (Btype.TypeSet.mem t !r) then begin
+ r := Btype.TypeSet.add t !r;
+ match t.desc with
+ Tconstr (p, _, memo) ->
+ may add_instance (Btype.find_expans Private p !memo)
+ | _ -> ()
+ end
+ in add_instance t
-(* precondition: lv < lv' *)
-let rec add_level lv lv' = function
- | [] -> [lv, lv']
- | (lv1, lv2) :: rem as l ->
- if lv2 < lv then (lv, lv') :: l else
- if lv' < lv1 then (lv1, lv2) :: add_level lv lv' rem
- else add_level (max lv lv1) (min lv' lv2) rem
-
-
(* Expand manifest module type names at the top of the given module type *)
let rec scrape_modtype mty env =
@@ -773,14 +776,13 @@
and add_cltype id ty env =
store_cltype id (Pident id) ty env
-let add_local_constraint id info mlv env =
+let add_local_constraint id info elv env =
match info with
- {type_manifest = Some ty; type_newtype_level = Some lv} ->
- (* use the newtype level for this definition, lv is the old one *)
- let env = add_type id {info with type_newtype_level = Some mlv} env in
- let level_map =
- if lv < mlv then add_level lv mlv env.level_map else env.level_map in
- { env with local_constraints = true; level_map = level_map }
+ {type_manifest = Some ty; type_newtype_level = Some (lv, _)} ->
+ (* elv is the expansion level, lv is the definition level *)
+ let env =
+ add_type id {info with type_newtype_level = Some (lv, elv)} env in
+ { env with local_constraints = true }
| _ -> assert false
(* Insertion of bindings by name *)
Index: typing/typecore.ml
===================================================================
--- typing/typecore.ml (revision 11210)
+++ typing/typecore.ml (working copy)
@@ -1989,6 +1989,7 @@
end
| Pexp_newtype(name, sbody) ->
(* Create a fake abstract type declaration for name. *)
+ let level = get_current_level () in
let decl = {
type_params = [];
type_arity = 0;
@@ -1996,7 +1997,7 @@
type_private = Public;
type_manifest = None;
type_variance = [];
- type_newtype_level = Some (get_current_level ());
+ type_newtype_level = Some (level, level);
}
in
let ty = newvar () in
Index: typing/typedecl.ml
===================================================================
--- typing/typedecl.ml (revision 11210)
+++ typing/typedecl.ml (working copy)
@@ -404,7 +404,7 @@
else if to_check path' && not (List.mem path' prev_exp) then begin
try
(* Attempt expansion *)
- let (params0, body0) = Env.find_type_expansion path' env in
+ let (params0, body0, _) = Env.find_type_expansion path' env in
let (params, body) =
Ctype.instance_parameterized_type params0 body0 in
begin
Index: typing/types.mli
===================================================================
--- typing/types.mli (revision 11210)
+++ typing/types.mli (working copy)
@@ -144,9 +144,9 @@
type_manifest: type_expr option;
type_variance: (bool * bool * bool) list;
(* covariant, contravariant, weakly contravariant *)
- type_newtype_level: int option }
+ type_newtype_level: (int * int) option }
+ (* definition level * expansion level *)
-
and type_kind =
Type_abstract
| Type_record of
Index: typing/ctype.ml
===================================================================
--- typing/ctype.ml (revision 11210)
+++ typing/ctype.ml (working copy)
@@ -470,7 +470,7 @@
free_variables := (ty, real) :: !free_variables
| Tconstr (path, tl, _), Some env ->
begin try
- let (_, body) = Env.find_type_expansion path env in
+ let (_, body, _) = Env.find_type_expansion path env in
if (repr body).level <> generic_level then
free_variables := (ty, real) :: !free_variables
with Not_found -> ()
@@ -687,7 +687,7 @@
try
match (Env.find_type p env).type_newtype_level with
| None -> Path.binding_time p
- | Some x -> x
+ | Some (x, _) -> x
with
| _ ->
(* no newtypes in predef *)
@@ -696,9 +696,13 @@
let rec update_level env level ty =
let ty = repr ty in
if ty.level > level then begin
+ if !Clflags.principal && Env.has_local_constraints env then begin
+ match Env.gadt_instance_level env ty with
+ Some lv -> if level < lv then raise (Unify [(ty, newvar2 level)])
+ | None -> ()
+ end;
match ty.desc with
- Tconstr(p, tl, abbrev)
- when level < Env.map_newtype_level env (get_level env p) ->
+ Tconstr(p, tl, abbrev) when level < get_level env p ->
(* Try first to replace an abbreviation by its expansion. *)
begin try
(* if is_newtype env p then raise Cannot_expand; *)
@@ -1025,7 +1029,7 @@
| Some (env, newtype_lev) ->
let existentials = List.map copy cstr.cstr_existentials in
let process existential =
- let decl = new_declaration (Some newtype_lev) None in
+ let decl = new_declaration (Some (newtype_lev, newtype_lev)) None in
let (id, new_env) =
Env.enter_type (get_new_abstract_name ()) decl !env in
env := new_env;
@@ -1271,7 +1275,7 @@
end;
ty
| None ->
- let (params, body) =
+ let (params, body, lv) =
try find_type_expansion level path env with Not_found ->
raise Cannot_expand
in
@@ -1284,6 +1288,15 @@
ty.desc <- Tvariant { row with row_name = Some (path, args) }
| _ -> ()
end;
+ (* For gadts, remember type as non exportable *)
+ if !Clflags.principal then begin
+ match lv with
+ Some lv -> Env.add_gadt_instances env lv [ty; ty']
+ | None ->
+ match Env.gadt_instance_level env ty with
+ Some lv -> Env.add_gadt_instances env lv [ty']
+ | None -> ()
+ end;
ty'
end
| _ ->
@@ -1306,15 +1319,7 @@
let try_expand_once env ty =
let ty = repr ty in
match ty.desc with
- Tconstr (p, _, _) ->
- let ty' = repr (expand_abbrev env ty) in
- if !Clflags.principal then begin
- match (Env.find_type p env).type_newtype_level with
- Some lv when ty.level < Env.map_newtype_level env lv ->
- link_type ty ty'
- | _ -> ()
- end;
- ty'
+ Tconstr (p, _, _) -> repr (expand_abbrev env ty)
| _ -> raise Cannot_expand
let _ = forward_try_expand_once := try_expand_once
@@ -1324,11 +1329,16 @@
May raise Unify, if a recursion was hidden in the type. *)
let rec try_expand_head env ty =
let ty' = try_expand_once env ty in
- begin try
- try_expand_head env ty'
- with Cannot_expand ->
- ty'
- end
+ let ty'' =
+ try try_expand_head env ty'
+ with Cannot_expand -> ty'
+ in
+ if !Clflags.principal then begin
+ match Env.gadt_instance_level env ty'' with
+ None -> ()
+ | Some lv -> Env.add_gadt_instance_chain env lv ty
+ end;
+ ty''
(* Expand once the head of a type *)
let expand_head_once env ty =
@@ -1405,7 +1415,7 @@
*)
let generic_abbrev env path =
try
- let (_, body) = Env.find_type_expansion path env in
+ let (_, body, _) = Env.find_type_expansion path env in
(repr body).level = generic_level
with
Not_found ->
@@ -1742,7 +1752,7 @@
let reify env t =
let newtype_level = get_newtype_level () in
let create_fresh_constr lev row =
- let decl = new_declaration (Some (newtype_level)) None in
+ let decl = new_declaration (Some (newtype_level, newtype_level)) None in
let name =
let name = get_new_abstract_name () in
if row then name ^ "#row" else name
@@ -2091,6 +2101,15 @@
if unify_eq !env t1' t2' then () else
let t1 = repr t1 and t2 = repr t2 in
+ if !Clflags.principal then begin
+ match Env.gadt_instance_level !env t1',Env.gadt_instance_level !env t2' with
+ Some lv1, Some lv2 ->
+ if lv1 > lv2 then Env.add_gadt_instance_chain !env lv1 t2 else
+ if lv2 > lv2 then Env.add_gadt_instance_chain !env lv2 t1
+ | Some lv1, None -> Env.add_gadt_instance_chain !env lv1 t2
+ | None, Some lv2 -> Env.add_gadt_instance_chain !env lv2 t1
+ | None, None -> ()
+ end;
if unify_eq !env t1 t1' || not (unify_eq !env t2 t2') then
unify3 env t1 t1' t2 t2'
else
Index: typing/env.mli
===================================================================
--- typing/env.mli (revision 11210)
+++ typing/env.mli (working copy)
@@ -33,14 +33,18 @@
val find_cltype: Path.t -> t -> cltype_declaration
val find_type_expansion:
- ?use_local:bool -> ?level:int -> Path.t -> t -> type_expr list * type_expr
-val find_type_expansion_opt: Path.t -> t -> type_expr list * type_expr
+ ?use_local:bool -> ?level:int -> Path.t -> t ->
+ type_expr list * type_expr * int option
+val find_type_expansion_opt:
+ Path.t -> t -> type_expr list * type_expr * int option
(* Find the manifest type information associated to a type for the sake
of the compiler's type-based optimisations. *)
val find_modtype_expansion: Path.t -> t -> Types.module_type
val has_local_constraints: t -> bool
-val map_newtype_level: t -> int -> int
+val gadt_instance_level: t -> type_expr -> int option
+val add_gadt_instances: t -> int -> type_expr list -> unit
+val add_gadt_instance_chain: t -> int -> type_expr -> unit
(* Lookup by long identifiers *)
Index: typing/types.ml
===================================================================
--- typing/types.ml (revision 11210)
+++ typing/types.ml (working copy)
@@ -146,8 +146,8 @@
type_private: private_flag;
type_manifest: type_expr option;
type_variance: (bool * bool * bool) list;
- type_newtype_level: int option }
(* covariant, contravariant, weakly contravariant *)
+ type_newtype_level: (int * int) option }
and type_kind =
Type_abstract

141
testsuite/tests/typing-gadts/omega07.ml.principal.reference
View File

@ -2,17 +2,17 @@
# * * * * * type ('a, 'b) sum = Inl of 'a | Inr of 'b
type zero = Zero
type 'a succ
type 'a nat = NZ : zero nat | NS : 'b nat -> 'b succ nat
type 'a nat = NZ : zero nat | NS : 'a nat -> 'a succ nat
# type ('a, 'b) seq =
Snil : ('c, zero) seq
| Scons : 'd * ('d, 'e) seq -> ('d, 'e succ) seq
Snil : ('a, zero) seq
| Scons : 'a * ('a, 'n) seq -> ('a, 'n succ) seq
# val l1 : (int, zero succ succ) seq = Scons (3, Scons (5, Snil))
# * type ('a, 'b, 'c) plus =
PlusZ : 'd nat -> (zero, 'd, 'd) plus
| PlusS : ('e, 'f, 'g) plus -> ('e succ, 'f, 'g succ) plus
PlusZ : 'a nat -> (zero, 'a, 'a) plus
| PlusS : ('a, 'b, 'c) plus -> ('a succ, 'b, 'c succ) plus
# val length : ('a, 'b) seq -> 'b nat = <fun>
# * type ('a, 'b, 'c) app =
App : ('d, 'g) seq * ('e, 'f, 'g) plus -> ('d, 'e, 'f) app
App : ('a, 'p) seq * ('n, 'm, 'p) plus -> ('a, 'n, 'm) app
val app : ('a, 'b) seq -> ('a, 'c) seq -> ('a, 'b, 'c) app = <fun>
# * type tp
type nd
@ -20,28 +20,28 @@ type ('a, 'b) fk
type 'a shape =
Tp : tp shape
| Nd : nd shape
| Fk : 'b shape * 'c shape -> ('b, 'c) fk shape
| Fk : 'a shape * 'b shape -> ('a, 'b) fk shape
# type tt
type ff
type 'a boolean = BT : tt boolean | BF : ff boolean
# type ('a, 'b) path =
Pnone : 'c -> (tp, 'c) path
| Phere : (nd, 'd) path
| Pleft : ('e, 'g) path -> (('e, 'f) fk, 'g) path
| Pright : ('i, 'j) path -> (('h, 'i) fk, 'j) path
Pnone : 'a -> (tp, 'a) path
| Phere : (nd, 'a) path
| Pleft : ('x, 'a) path -> (('x, 'y) fk, 'a) path
| Pright : ('y, 'a) path -> (('x, 'y) fk, 'a) path
# type ('a, 'b) tree =
Ttip : (tp, 'c) tree
| Tnode : 'd -> (nd, 'd) tree
| Tfork : ('e, 'g) tree * ('f, 'g) tree -> (('e, 'f) fk, 'g) tree
Ttip : (tp, 'a) tree
| Tnode : 'a -> (nd, 'a) tree
| Tfork : ('x, 'a) tree * ('y, 'a) tree -> (('x, 'y) fk, 'a) tree
# val tree1 : (((tp, nd) fk, (nd, nd) fk) fk, int) tree =
Tfork (Tfork (Ttip, Tnode 4), Tfork (Tnode 4, Tnode 3))
# val find : ('a -> 'a -> bool) -> 'a -> ('b, 'a) tree -> ('b, 'a) path list =
<fun>
# val extract : ('a, 'b) path -> ('a, 'b) tree -> 'b = <fun>
# val extract : ('b, 'a) path -> ('b, 'a) tree -> 'a = <fun>
# type ('a, 'b) le =
LeZ : 'c nat -> (zero, 'c) le
| LeS : ('d, 'e) le -> ('d succ, 'e succ) le
# type 'a even = EvenZ : zero even | EvenSS : 'b even -> 'b succ succ even
LeZ : 'a nat -> (zero, 'a) le
| LeS : ('n, 'm) le -> ('n succ, 'm succ) le
# type 'a even = EvenZ : zero even | EvenSS : 'n even -> 'n succ succ even
# type one = zero succ
type two = one succ
type three = two succ
@ -51,10 +51,10 @@ val even2 : two even = EvenSS EvenZ
val even4 : four even = EvenSS (EvenSS EvenZ)
# val p1 : (two, one, three) plus = PlusS (PlusS (PlusZ (NS NZ)))
# val summandLessThanSum : ('a, 'b, 'c) plus -> ('a, 'c) le = <fun>
# type ('a, 'b) equal = Eq : ('c, 'c) equal
# type ('a, 'b) equal = Eq : ('a, 'a) equal
val sameNat : 'a nat -> 'b nat -> ('a, 'b) equal option = <fun>
# val smaller : ('a succ, 'b succ) le -> ('a, 'b) le = <fun>
# type ('a, 'b) diff = Diff : 'e nat * ('c, 'e, 'd) plus -> ('c, 'd) diff
# type ('a, 'b) diff = Diff : 'c nat * ('a, 'c, 'b) plus -> ('a, 'b) diff
# * * * * * * * * * val diff : ('a, 'b) le -> 'a nat -> 'b nat -> ('a, 'b) diff = <fun>
# Characters 87-243:
..match a, b,le with (* warning *)
@ -66,17 +66,18 @@ Here is an example of a value that is not matched:
(NS _, NZ, _)
val diff : ('a, 'b) le -> 'a nat -> 'b nat -> ('a, 'b) diff = <fun>
# val diff : ('a, 'b) le -> 'b nat -> ('a, 'b) diff = <fun>
# type ('a, 'b) filter = Filter : ('e, 'd) le * ('c, 'e) seq -> ('c, 'd) filter
# type ('a, 'b) filter = Filter : ('m, 'n) le * ('a, 'm) seq -> ('a, 'n) filter
val leS' : ('a, 'b) le -> ('a, 'b succ) le = <fun>
# val filter : ('a -> bool) -> ('a, 'b) seq -> ('a, 'b) filter = <fun>
# type ('a, 'b, 'c) balance =
Less : ('d, 'd succ, 'd succ) balance
| Same : ('e, 'e, 'e) balance
| More : ('f succ, 'f, 'f succ) balance
Less : ('h, 'h succ, 'h succ) balance
| Same : ('h, 'h, 'h) balance
| More : ('h succ, 'h, 'h succ) balance
type 'a avl =
Leaf : zero avl
| Node : ('c, 'd, 'b) balance * 'c avl * int * 'd avl -> 'b succ avl
type avl' = Avl : 'a avl -> avl'
| Node : ('hL, 'hR, 'hMax) balance * 'hL avl * int *
'hR avl -> 'hMax succ avl
type avl' = Avl : 'h avl -> avl'
# val empty : avl' = Avl Leaf
val elem : int -> 'a avl -> bool = <fun>
# val rotr :
@ -90,26 +91,26 @@ val elem : int -> 'a avl -> bool = <fun>
# val insert : int -> avl' -> avl' = <fun>
# val del_min : 'a succ avl -> int * ('a avl, 'a succ avl) sum = <fun>
type 'a avl_del =
Dsame : 'b avl -> 'b avl_del
| Ddecr : ('d succ, 'c) equal * 'd avl -> 'c avl_del
Dsame : 'n avl -> 'n avl_del
| Ddecr : ('m succ, 'n) equal * 'm avl -> 'n avl_del
val del : int -> 'a avl -> 'a avl_del = <fun>
# val delete : int -> avl' -> avl' = <fun>
# type red
type black
type ('a, 'b) sub_tree =
Bleaf : (black, zero) sub_tree
| Rnode : (black, 'c) sub_tree * int *
(black, 'c) sub_tree -> (red, 'c) sub_tree
| Bnode : ('e, 'd) sub_tree * int *
('f, 'd) sub_tree -> (black, 'd succ) sub_tree
type rb_tree = Root : (black, 'a) sub_tree -> rb_tree
| Rnode : (black, 'n) sub_tree * int *
(black, 'n) sub_tree -> (red, 'n) sub_tree
| Bnode : ('cL, 'n) sub_tree * int *
('cR, 'n) sub_tree -> (black, 'n succ) sub_tree
type rb_tree = Root : (black, 'n) sub_tree -> rb_tree
# type dir = LeftD | RightD
type ('a, 'b) ctxt =
CNil : (black, 'c) ctxt
| CRed : int * dir * (black, 'd) sub_tree *
(red, 'd) ctxt -> (black, 'd) ctxt
| CBlk : int * dir * ('g, 'f) sub_tree *
(black, 'f succ) ctxt -> ('e, 'f) ctxt
CNil : (black, 'n) ctxt
| CRed : int * dir * (black, 'n) sub_tree *
(red, 'n) ctxt -> (black, 'n) ctxt
| CBlk : int * dir * ('c1, 'n) sub_tree *
(black, 'n succ) ctxt -> ('c, 'n) ctxt
# val blacken : (red, 'a) sub_tree -> (black, 'a succ) sub_tree = <fun>
type 'a crep = Red : red crep | Black : black crep
val color : ('a, 'b) sub_tree -> 'a crep = <fun>
@ -137,8 +138,8 @@ val color : ('a, 'b) sub_tree -> 'a crep = <fun>
Const : int -> int term
| Add : (int * int -> int) term
| LT : (int * int -> bool) term
| Ap : ('c -> 'b) term * 'c term -> 'b term
| Pair : 'd term * 'e term -> ('d * 'e) term
| Ap : ('a -> 'b) term * 'a term -> 'b term
| Pair : 'a term * 'b term -> ('a * 'b) term
val ex1 : int term = Ap (Add, Pair (Const 3, Const 5))
val ex2 : (int * int) term =
Pair (Ap (Add, Pair (Const 3, Const 5)), Const 1)
@ -146,20 +147,20 @@ val eval_term : 'a term -> 'a = <fun>
type 'a rep =
Rint : int rep
| Rbool : bool rep
| Rpair : 'b rep * 'c rep -> ('b * 'c) rep
| Rfun : 'd rep * 'e rep -> ('d -> 'e) rep
type ('a, 'b) equal = Eq : ('c, 'c) equal
| Rpair : 'a rep * 'b rep -> ('a * 'b) rep
| Rfun : 'a rep * 'b rep -> ('a -> 'b) rep
type ('a, 'b) equal = Eq : ('a, 'a) equal
val rep_equal : 'a rep -> 'b rep -> ('a, 'b) equal option = <fun>
# type assoc = Assoc : string * 'a rep * 'a -> assoc
val assoc : string -> 'a rep -> assoc list -> 'a = <fun>
type 'a term =
Var : string * 'b rep -> 'b term
| Abs : string * 'c rep * 'd term -> ('c -> 'd) term
Var : string * 'a rep -> 'a term
| Abs : string * 'a rep * 'b term -> ('a -> 'b) term
| Const : int -> int term
| Add : (int * int -> int) term
| LT : (int * int -> bool) term
| Ap : ('f -> 'e) term * 'f term -> 'e term
| Pair : 'g term * 'h term -> ('g * 'h) term
| Ap : ('a -> 'b) term * 'a term -> 'b term
| Pair : 'a term * 'b term -> ('a * 'b) term
val eval_term : assoc list -> 'a term -> 'a = <fun>
# val ex3 : (int -> int) term =
Abs ("x", Rint, Ap (Add, Pair (Var ("x", Rint), Var ("x", Rint))))
@ -171,13 +172,13 @@ val v4 : int = 6
type ('a, 'b, 'c) rcons
type 'a is_row =
Rnil : rnil is_row
| Rcons : 'd is_row -> ('b, 'c, 'd) rcons is_row
| Rcons : 'c is_row -> ('a, 'b, 'c) rcons is_row
type ('a, 'b) lam =
Const : int -> ('c, int) lam
| Var : 'd -> (('d, 'e, 'f) rcons, 'e) lam
| Shift : ('i, 'j) lam -> (('g, 'h, 'i) rcons, 'j) lam
| Abs : 'n * (('n, 'l, 'k) rcons, 'm) lam -> ('k, 'l -> 'm) lam
| App : ('o, 'q -> 'p) lam * ('o, 'q) lam -> ('o, 'p) lam
Const : int -> ('e, int) lam
| Var : 'a -> (('a, 't, 'e) rcons, 't) lam
| Shift : ('e, 't) lam -> (('a, 'q, 'e) rcons, 't) lam
| Abs : 'a * (('a, 's, 'e) rcons, 't) lam -> ('e, 's -> 't) lam
| App : ('e, 's -> 't) lam * ('e, 's) lam -> ('e, 't) lam
type x = X
type y = Y
val ex1 : ((x, 'a -> 'b, (y, 'a, 'c) rcons) rcons, 'b) lam =
@ -186,7 +187,7 @@ val ex2 : ('a, ('b -> 'c) -> 'b -> 'c) lam =
Abs (<poly>, Abs (<poly>, App (Shift (Var <poly>), Var <poly>)))
# type 'a env =
Enil : rnil env
| Econs : 'b * 'c * 'd env -> ('b, 'c, 'd) rcons env
| Econs : 'a * 't * 'e env -> ('a, 't, 'e) rcons env
val eval_lam : 'a env -> ('a, 'b) lam -> 'b = <fun>
# type add = Add
type suc = Suc
@ -231,7 +232,7 @@ val ex3 :
App (Shift (Var Suc),
App (Shift (Var Suc), App (Shift (Var Suc), Var Zero))))
# val v3 : int = 6
# * type 'a rep = I : int rep | Ar : 'b rep * 'c rep -> ('b -> 'c) rep
# * type 'a rep = I : int rep | Ar : 'a rep * 'b rep -> ('a -> 'b) rep
val compare : 'a rep -> 'b rep -> (string, ('a, 'b) equal) sum = <fun>
# type term =
C of int
@ -240,10 +241,10 @@ val compare : 'a rep -> 'b rep -> (string, ('a, 'b) equal) sum = <fun>
| V of string
type 'a ctx =
Cnil : rnil ctx
| Ccons : 'b * string * 'c rep * 'd ctx -> ('b, 'c, 'd) rcons ctx
| Ccons : 't * string * 'x rep * 'e ctx -> ('t, 'x, 'e) rcons ctx
# type 'a checked =
Cerror of string
| Cok : ('b, 'c) lam * 'c rep -> 'b checked
| Cok : ('e, 't) lam * 't rep -> 'e checked
val lookup : string -> 'a ctx -> 'a checked = <fun>
# val tc : 'a nat -> 'b ctx -> term -> 'b checked = <fun>
# val ctx0 :
@ -278,24 +279,24 @@ type ('a, 'b) tarr
type tint
type ('a, 'b) rel =
IntR : (tint, int) rel
| IntTo : ('c, 'd) rel -> ((tint, 'c) tarr, int -> 'd) rel
| IntTo : ('b, 's) rel -> ((tint, 'b) tarr, int -> 's) rel
type ('a, 'b, 'c) lam =
Const : ('e, 'f) rel * 'f -> (pval, 'd, 'e) lam
| Var : 'g -> (pval, ('g, 'h, 'i) rcons, 'h) lam
| Shift : ('j, 'm, 'n) lam -> ('j, ('k, 'l, 'm) rcons, 'n) lam
| Lam : 'r *
('s, ('r, 'p, 'o) rcons, 'q) lam -> (pval, 'o, ('p, 'q) tarr) lam
| App : ('v, 't, ('w, 'u) tarr) lam *
('x, 't, 'w) lam -> (pexp, 't, 'u) lam
Const : ('a, 'b) rel * 'b -> (pval, 'env, 'a) lam
| Var : 'a -> (pval, ('a, 't, 'e) rcons, 't) lam
| Shift : ('m, 'e, 't) lam -> ('m, ('a, 'q, 'e) rcons, 't) lam
| Lam : 'a *
('m, ('a, 's, 'e) rcons, 't) lam -> (pval, 'e, ('s, 't) tarr) lam
| App : ('m1, 'e, ('s, 't) tarr) lam *
('m2, 'e, 's) lam -> (pexp, 'e, 't) lam
# val ex1 : (pexp, 'a, tint) lam =
App (Lam (<poly>, Var <poly>), Const (IntR, <poly>))
val mode : ('a, 'b, 'c) lam -> 'a mode = <fun>
# type ('a, 'b) sub =
Id : ('c, 'c) sub
| Bind : 'd * ('h, 'g, 'e) lam *
('f, 'g) sub -> (('d, 'e, 'f) rcons, 'g) sub
| Push : ('k, 'l) sub -> (('i, 'j, 'k) rcons, ('i, 'j, 'l) rcons) sub
type ('a, 'b) lam' = Ex : ('e, 'c, 'd) lam -> ('c, 'd) lam'
Id : ('r, 'r) sub
| Bind : 't * ('m, 'r2, 'x) lam *
('r, 'r2) sub -> (('t, 'x, 'r) rcons, 'r2) sub
| Push : ('r1, 'r2) sub -> (('a, 'b, 'r1) rcons, ('a, 'b, 'r2) rcons) sub
type ('a, 'b) lam' = Ex : ('m, 's, 't) lam -> ('s, 't) lam'
# val subst : ('a, 'b, 'c) lam -> ('b, 'd) sub -> ('d, 'c) lam' = <fun>
# type closed = rnil
type 'a rlam = ((pexp, closed, 'a) lam, (pval, closed, 'a) lam) sum

141
testsuite/tests/typing-gadts/omega07.ml.reference
View File

@ -2,17 +2,17 @@
# * * * * * type ('a, 'b) sum = Inl of 'a | Inr of 'b
type zero = Zero
type 'a succ
type 'a nat = NZ : zero nat | NS : 'b nat -> 'b succ nat
type 'a nat = NZ : zero nat | NS : 'a nat -> 'a succ nat
# type ('a, 'b) seq =
Snil : ('c, zero) seq
| Scons : 'd * ('d, 'e) seq -> ('d, 'e succ) seq
Snil : ('a, zero) seq
| Scons : 'a * ('a, 'n) seq -> ('a, 'n succ) seq
# val l1 : (int, zero succ succ) seq = Scons (3, Scons (5, Snil))
# * type ('a, 'b, 'c) plus =
PlusZ : 'd nat -> (zero, 'd, 'd) plus
| PlusS : ('e, 'f, 'g) plus -> ('e succ, 'f, 'g succ) plus
PlusZ : 'a nat -> (zero, 'a, 'a) plus
| PlusS : ('a, 'b, 'c) plus -> ('a succ, 'b, 'c succ) plus
# val length : ('a, 'b) seq -> 'b nat = <fun>
# * type ('a, 'b, 'c) app =
App : ('d, 'g) seq * ('e, 'f, 'g) plus -> ('d, 'e, 'f) app
App : ('a, 'p) seq * ('n, 'm, 'p) plus -> ('a, 'n, 'm) app
val app : ('a, 'b) seq -> ('a, 'c) seq -> ('a, 'b, 'c) app = <fun>
# * type tp
type nd
@ -20,28 +20,28 @@ type ('a, 'b) fk
type 'a shape =
Tp : tp shape
| Nd : nd shape
| Fk : 'b shape * 'c shape -> ('b, 'c) fk shape
| Fk : 'a shape * 'b shape -> ('a, 'b) fk shape
# type tt
type ff
type 'a boolean = BT : tt boolean | BF : ff boolean
# type ('a, 'b) path =
Pnone : 'c -> (tp, 'c) path
| Phere : (nd, 'd) path
| Pleft : ('e, 'g) path -> (('e, 'f) fk, 'g) path
| Pright : ('i, 'j) path -> (('h, 'i) fk, 'j) path
Pnone : 'a -> (tp, 'a) path
| Phere : (nd, 'a) path
| Pleft : ('x, 'a) path -> (('x, 'y) fk, 'a) path
| Pright : ('y, 'a) path -> (('x, 'y) fk, 'a) path
# type ('a, 'b) tree =
Ttip : (tp, 'c) tree
| Tnode : 'd -> (nd, 'd) tree
| Tfork : ('e, 'g) tree * ('f, 'g) tree -> (('e, 'f) fk, 'g) tree
Ttip : (tp, 'a) tree
| Tnode : 'a -> (nd, 'a) tree
| Tfork : ('x, 'a) tree * ('y, 'a) tree -> (('x, 'y) fk, 'a) tree
# val tree1 : (((tp, nd) fk, (nd, nd) fk) fk, int) tree =
Tfork (Tfork (Ttip, Tnode 4), Tfork (Tnode 4, Tnode 3))
# val find : ('a -> 'a -> bool) -> 'a -> ('b, 'a) tree -> ('b, 'a) path list =
<fun>
# val extract : ('a, 'b) path -> ('a, 'b) tree -> 'b = <fun>
# val extract : ('b, 'a) path -> ('b, 'a) tree -> 'a = <fun>
# type ('a, 'b) le =
LeZ : 'c nat -> (zero, 'c) le
| LeS : ('d, 'e) le -> ('d succ, 'e succ) le
# type 'a even = EvenZ : zero even | EvenSS : 'b even -> 'b succ succ even
LeZ : 'a nat -> (zero, 'a) le
| LeS : ('n, 'm) le -> ('n succ, 'm succ) le
# type 'a even = EvenZ : zero even | EvenSS : 'n even -> 'n succ succ even
# type one = zero succ
type two = one succ
type three = two succ
@ -51,10 +51,10 @@ val even2 : two even = EvenSS EvenZ
val even4 : four even = EvenSS (EvenSS EvenZ)
# val p1 : (two, one, three) plus = PlusS (PlusS (PlusZ (NS NZ)))
# val summandLessThanSum : ('a, 'b, 'c) plus -> ('a, 'c) le = <fun>
# type ('a, 'b) equal = Eq : ('c, 'c) equal
# type ('a, 'b) equal = Eq : ('a, 'a) equal
val sameNat : 'a nat -> 'b nat -> ('a, 'b) equal option = <fun>
# val smaller : ('a succ, 'b succ) le -> ('a, 'b) le = <fun>
# type ('a, 'b) diff = Diff : 'e nat * ('c, 'e, 'd) plus -> ('c, 'd) diff
# type ('a, 'b) diff = Diff : 'c nat * ('a, 'c, 'b) plus -> ('a, 'b) diff
# * * * * * * * * * val diff : ('a, 'b) le -> 'a nat -> 'b nat -> ('a, 'b) diff = <fun>
# Characters 87-243:
..match a, b,le with (* warning *)
@ -66,17 +66,18 @@ Here is an example of a value that is not matched:
(NS _, NZ, _)
val diff : ('a, 'b) le -> 'a nat -> 'b nat -> ('a, 'b) diff = <fun>
# val diff : ('a, 'b) le -> 'b nat -> ('a, 'b) diff = <fun>
# type ('a, 'b) filter = Filter : ('e, 'd) le * ('c, 'e) seq -> ('c, 'd) filter
# type ('a, 'b) filter = Filter : ('m, 'n) le * ('a, 'm) seq -> ('a, 'n) filter
val leS' : ('a, 'b) le -> ('a, 'b succ) le = <fun>
# val filter : ('a -> bool) -> ('a, 'b) seq -> ('a, 'b) filter = <fun>
# type ('a, 'b, 'c) balance =
Less : ('d, 'd succ, 'd succ) balance
| Same : ('e, 'e, 'e) balance
| More : ('f succ, 'f, 'f succ) balance
Less : ('h, 'h succ, 'h succ) balance
| Same : ('h, 'h, 'h) balance
| More : ('h succ, 'h, 'h succ) balance
type 'a avl =
Leaf : zero avl
| Node : ('c, 'd, 'b) balance * 'c avl * int * 'd avl -> 'b succ avl
type avl' = Avl : 'a avl -> avl'
| Node : ('hL, 'hR, 'hMax) balance * 'hL avl * int *
'hR avl -> 'hMax succ avl
type avl' = Avl : 'h avl -> avl'
# val empty : avl' = Avl Leaf
val elem : int -> 'a avl -> bool = <fun>
# val rotr :
@ -90,26 +91,26 @@ val elem : int -> 'a avl -> bool = <fun>
# val insert : int -> avl' -> avl' = <fun>
# val del_min : 'a succ avl -> int * ('a avl, 'a succ avl) sum = <fun>
type 'a avl_del =
Dsame : 'b avl -> 'b avl_del
| Ddecr : ('d succ, 'c) equal * 'd avl -> 'c avl_del
Dsame : 'n avl -> 'n avl_del
| Ddecr : ('m succ, 'n) equal * 'm avl -> 'n avl_del
val del : int -> 'a avl -> 'a avl_del = <fun>
# val delete : int -> avl' -> avl' = <fun>
# type red
type black
type ('a, 'b) sub_tree =
Bleaf : (black, zero) sub_tree
| Rnode : (black, 'c) sub_tree * int *
(black, 'c) sub_tree -> (red, 'c) sub_tree
| Bnode : ('e, 'd) sub_tree * int *
('f, 'd) sub_tree -> (black, 'd succ) sub_tree
type rb_tree = Root : (black, 'a) sub_tree -> rb_tree
| Rnode : (black, 'n) sub_tree * int *
(black, 'n) sub_tree -> (red, 'n) sub_tree
| Bnode : ('cL, 'n) sub_tree * int *
('cR, 'n) sub_tree -> (black, 'n succ) sub_tree
type rb_tree = Root : (black, 'n) sub_tree -> rb_tree
# type dir = LeftD | RightD
type ('a, 'b) ctxt =
CNil : (black, 'c) ctxt
| CRed : int * dir * (black, 'd) sub_tree *
(red, 'd) ctxt -> (black, 'd) ctxt
| CBlk : int * dir * ('g, 'f) sub_tree *
(black, 'f succ) ctxt -> ('e, 'f) ctxt
CNil : (black, 'n) ctxt
| CRed : int * dir * (black, 'n) sub_tree *
(red, 'n) ctxt -> (black, 'n) ctxt
| CBlk : int * dir * ('c1, 'n) sub_tree *
(black, 'n succ) ctxt -> ('c, 'n) ctxt
# val blacken : (red, 'a) sub_tree -> (black, 'a succ) sub_tree = <fun>
type 'a crep = Red : red crep | Black : black crep
val color : ('a, 'b) sub_tree -> 'a crep = <fun>
@ -137,8 +138,8 @@ val color : ('a, 'b) sub_tree -> 'a crep = <fun>
Const : int -> int term
| Add : (int * int -> int) term
| LT : (int * int -> bool) term
| Ap : ('c -> 'b) term * 'c term -> 'b term
| Pair : 'd term * 'e term -> ('d * 'e) term
| Ap : ('a -> 'b) term * 'a term -> 'b term
| Pair : 'a term * 'b term -> ('a * 'b) term
val ex1 : int term = Ap (Add, Pair (Const 3, Const 5))
val ex2 : (int * int) term =
Pair (Ap (Add, Pair (Const 3, Const 5)), Const 1)
@ -146,20 +147,20 @@ val eval_term : 'a term -> 'a = <fun>
type 'a rep =
Rint : int rep
| Rbool : bool rep
| Rpair : 'b rep * 'c rep -> ('b * 'c) rep
| Rfun : 'd rep * 'e rep -> ('d -> 'e) rep
type ('a, 'b) equal = Eq : ('c, 'c) equal
| Rpair : 'a rep * 'b rep -> ('a * 'b) rep
| Rfun : 'a rep * 'b rep -> ('a -> 'b) rep
type ('a, 'b) equal = Eq : ('a, 'a) equal
val rep_equal : 'a rep -> 'b rep -> ('a, 'b) equal option = <fun>
# type assoc = Assoc : string * 'a rep * 'a -> assoc
val assoc : string -> 'a rep -> assoc list -> 'a = <fun>
type 'a term =
Var : string * 'b rep -> 'b term
| Abs : string * 'c rep * 'd term -> ('c -> 'd) term
Var : string * 'a rep -> 'a term
| Abs : string * 'a rep * 'b term -> ('a -> 'b) term
| Const : int -> int term
| Add : (int * int -> int) term
| LT : (int * int -> bool) term
| Ap : ('f -> 'e) term * 'f term -> 'e term
| Pair : 'g term * 'h term -> ('g * 'h) term
| Ap : ('a -> 'b) term * 'a term -> 'b term
| Pair : 'a term * 'b term -> ('a * 'b) term
val eval_term : assoc list -> 'a term -> 'a = <fun>
# val ex3 : (int -> int) term =
Abs ("x", Rint, Ap (Add, Pair (Var ("x", Rint), Var ("x", Rint))))
@ -171,13 +172,13 @@ val v4 : int = 6
type ('a, 'b, 'c) rcons
type 'a is_row =
Rnil : rnil is_row
| Rcons : 'd is_row -> ('b, 'c, 'd) rcons is_row
| Rcons : 'c is_row -> ('a, 'b, 'c) rcons is_row
type ('a, 'b) lam =
Const : int -> ('c, int) lam
| Var : 'd -> (('d, 'e, 'f) rcons, 'e) lam
| Shift : ('i, 'j) lam -> (('g, 'h, 'i) rcons, 'j) lam
| Abs : 'n * (('n, 'l, 'k) rcons, 'm) lam -> ('k, 'l -> 'm) lam
| App : ('o, 'q -> 'p) lam * ('o, 'q) lam -> ('o, 'p) lam
Const : int -> ('e, int) lam
| Var : 'a -> (('a, 't, 'e) rcons, 't) lam
| Shift : ('e, 't) lam -> (('a, 'q, 'e) rcons, 't) lam
| Abs : 'a * (('a, 's, 'e) rcons, 't) lam -> ('e, 's -> 't) lam
| App : ('e, 's -> 't) lam * ('e, 's) lam -> ('e, 't) lam
type x = X
type y = Y
val ex1 : ((x, 'a -> 'b, (y, 'a, 'c) rcons) rcons, 'b) lam =
@ -186,7 +187,7 @@ val ex2 : ('a, ('b -> 'c) -> 'b -> 'c) lam =
Abs (<poly>, Abs (<poly>, App (Shift (Var <poly>), Var <poly>)))
# type 'a env =
Enil : rnil env
| Econs : 'b * 'c * 'd env -> ('b, 'c, 'd) rcons env
| Econs : 'a * 't * 'e env -> ('a, 't, 'e) rcons env
val eval_lam : 'a env -> ('a, 'b) lam -> 'b = <fun>
# type add = Add
type suc = Suc
@ -231,7 +232,7 @@ val ex3 :
App (Shift (Var Suc),
App (Shift (Var Suc), App (Shift (Var Suc), Var Zero))))
# val v3 : int = 6
# * type 'a rep = I : int rep | Ar : 'b rep * 'c rep -> ('b -> 'c) rep
# * type 'a rep = I : int rep | Ar : 'a rep * 'b rep -> ('a -> 'b) rep
val compare : 'a rep -> 'b rep -> (string, ('a, 'b) equal) sum = <fun>
# type term =
C of int
@ -240,10 +241,10 @@ val compare : 'a rep -> 'b rep -> (string, ('a, 'b) equal) sum = <fun>
| V of string
type 'a ctx =
Cnil : rnil ctx
| Ccons : 'b * string * 'c rep * 'd ctx -> ('b, 'c, 'd) rcons ctx
| Ccons : 't * string * 'x rep * 'e ctx -> ('t, 'x, 'e) rcons ctx
# type 'a checked =
Cerror of string
| Cok : ('b, 'c) lam * 'c rep -> 'b checked
| Cok : ('e, 't) lam * 't rep -> 'e checked
val lookup : string -> 'a ctx -> 'a checked = <fun>
# val tc : 'a nat -> 'b ctx -> term -> 'b checked = <fun>
# val ctx0 :
@ -278,24 +279,24 @@ type ('a, 'b) tarr
type tint
type ('a, 'b) rel =
IntR : (tint, int) rel
| IntTo : ('c, 'd) rel -> ((tint, 'c) tarr, int -> 'd) rel
| IntTo : ('b, 's) rel -> ((tint, 'b) tarr, int -> 's) rel
type ('a, 'b, 'c) lam =
Const : ('e, 'f) rel * 'f -> (pval, 'd, 'e) lam
| Var : 'g -> (pval, ('g, 'h, 'i) rcons, 'h) lam
| Shift : ('j, 'm, 'n) lam -> ('j, ('k, 'l, 'm) rcons, 'n) lam
| Lam : 'r *
('s, ('r, 'p, 'o) rcons, 'q) lam -> (pval, 'o, ('p, 'q) tarr) lam
| App : ('v, 't, ('w, 'u) tarr) lam *
('x, 't, 'w) lam -> (pexp, 't, 'u) lam
Const : ('a, 'b) rel * 'b -> (pval, 'env, 'a) lam
| Var : 'a -> (pval, ('a, 't, 'e) rcons, 't) lam
| Shift : ('m, 'e, 't) lam -> ('m, ('a, 'q, 'e) rcons, 't) lam
| Lam : 'a *
('m, ('a, 's, 'e) rcons, 't) lam -> (pval, 'e, ('s, 't) tarr) lam
| App : ('m1, 'e, ('s, 't) tarr) lam *
('m2, 'e, 's) lam -> (pexp, 'e, 't) lam
# val ex1 : (pexp, 'a, tint) lam =
App (Lam (<poly>, Var <poly>), Const (IntR, <poly>))
val mode : ('a, 'b, 'c) lam -> 'a mode = <fun>
# type ('a, 'b) sub =
Id : ('c, 'c) sub
| Bind : 'd * ('h, 'g, 'e) lam *
('f, 'g) sub -> (('d, 'e, 'f) rcons, 'g) sub
| Push : ('k, 'l) sub -> (('i, 'j, 'k) rcons, ('i, 'j, 'l) rcons) sub
type ('a, 'b) lam' = Ex : ('e, 'c, 'd) lam -> ('c, 'd) lam'
Id : ('r, 'r) sub
| Bind : 't * ('m, 'r2, 'x) lam *
('r, 'r2) sub -> (('t, 'x, 'r) rcons, 'r2) sub
| Push : ('r1, 'r2) sub -> (('a, 'b, 'r1) rcons, ('a, 'b, 'r2) rcons) sub
type ('a, 'b) lam' = Ex : ('m, 's, 't) lam -> ('s, 't) lam'
# val subst : ('a, 'b, 'c) lam -> ('b, 'd) sub -> ('d, 'c) lam' = <fun>
# type closed = rnil
type 'a rlam = ((pexp, closed, 'a) lam, (pval, closed, 'a) lam) sum

14
testsuite/tests/typing-gadts/pr5332.ml.reference
View File

@ -1,11 +1,11 @@
# type ('a, 'b) var =
Zero : ('c * 'd, 'c) var
| Succ : ('f, 'g) var -> ('e * 'f, 'g) var
# type ('a, 'b) typ =
Tint : ('c, int) typ
| Tbool : ('d, bool) typ
| Tvar : ('e, 'f) var -> ('e, 'f) typ
# type ('env, 'a) var =
Zero : ('a * 'env, 'a) var
| Succ : ('env, 'a) var -> ('b * 'env, 'a) var
# type ('env, 'a) typ =
Tint : ('env, int) typ
| Tbool : ('env, bool) typ
| Tvar : ('env, 'a) var -> ('env, 'a) typ
# Characters 72-156:
.match ta, tb with
| Tint, Tint -> 0

10
testsuite/tests/typing-gadts/test.ml.principal.reference
View File

@ -4,15 +4,15 @@
type 'a t =
IntLit : int -> int t
| BoolLit : bool -> bool t
| Pair : 'b t * 'c t -> ('b * 'c) t
| App : ('e -> 'd) t * 'e t -> 'd t
| Abs : ('f -> 'g) -> ('f -> 'g) t
| Pair : 'a t * 'b t -> ('a * 'b) t
| App : ('a -> 'b) t * 'a t -> 'b t
| Abs : ('a -> 'b) -> ('a -> 'b) t
val eval : 'a t -> 'a
end
# module List :
sig
type zero
type 'a t = Nil : zero t | Cons : 'b * 'c t -> ('b * 'c) t
type 'a t = Nil : zero t | Cons : 'a * 'b t -> ('a * 'b) t
val head : ('a * 'b) t -> 'a
val tail : ('a * 'b) t -> 'b t
val length : 'a t -> int
@ -130,7 +130,7 @@ Error: This expression has type int but an expression was expected of type a
# val f : 'a t -> 'a -> int = <fun>
# type 'a t = A of int | B of bool | C of float | D of 'a
type 'a ty =
TE : 'b ty -> 'b array ty
TE : 'a ty -> 'a array ty
| TA : int ty
| TB : bool ty
| TC : float ty

10
testsuite/tests/typing-gadts/test.ml.reference
View File

@ -4,15 +4,15 @@
type 'a t =
IntLit : int -> int t
| BoolLit : bool -> bool t
| Pair : 'b t * 'c t -> ('b * 'c) t
| App : ('e -> 'd) t * 'e t -> 'd t
| Abs : ('f -> 'g) -> ('f -> 'g) t
| Pair : 'a t * 'b t -> ('a * 'b) t
| App : ('a -> 'b) t * 'a t -> 'b t
| Abs : ('a -> 'b) -> ('a -> 'b) t
val eval : 'a t -> 'a
end
# module List :
sig
type zero
type 'a t = Nil : zero t | Cons : 'b * 'c t -> ('b * 'c) t
type 'a t = Nil : zero t | Cons : 'a * 'b t -> ('a * 'b) t
val head : ('a * 'b) t -> 'a
val tail : ('a * 'b) t -> 'b t
val length : 'a t -> int
@ -119,7 +119,7 @@ Error: This expression has type int but an expression was expected of type a
# val f : 'a t -> 'a -> 'a = <fun>
# type 'a t = A of int | B of bool | C of float | D of 'a
type 'a ty =
TE : 'b ty -> 'b array ty
TE : 'a ty -> 'a array ty
| TA : int ty
| TB : bool ty
| TC : float ty

11
typing/printtyp.ml
View File

@ -642,8 +642,15 @@ let rec tree_of_type_decl id decl =
in
(name, args, ty, priv, constraints)
and tree_of_constructor (name, args,ret_type_opt) =
(name, tree_of_typlist false args,tree_of_constructor_ret ret_type_opt)
and tree_of_constructor (name, args, ret_type_opt) =
if ret_type_opt = None then (name, tree_of_typlist false args, None) else
let nm = !names in
names := [];
let ret = may_map (tree_of_typexp false) ret_type_opt in
let args = tree_of_typlist false args in
names := nm;
(name, args, ret)
and tree_of_constructor_ret =
function