diff options
| -rw-r--r-- | testsuite/tests/typing-gadts/dynamic_frisch.ml.principal.reference | 20 | ||||
| -rw-r--r-- | testsuite/tests/typing-gadts/dynamic_frisch.ml.reference | 20 | ||||
| -rw-r--r-- | testsuite/tests/typing-gadts/omega07.ml.principal.reference | 48 | ||||
| -rw-r--r-- | testsuite/tests/typing-gadts/omega07.ml.reference | 48 | ||||
| -rw-r--r-- | testsuite/tests/typing-gadts/pr5332.ml.reference | 2 | ||||
| -rw-r--r-- | testsuite/tests/typing-gadts/term-conv.ml.principal.reference | 20 | ||||
| -rw-r--r-- | testsuite/tests/typing-gadts/term-conv.ml.reference | 20 | ||||
| -rw-r--r-- | testsuite/tests/typing-gadts/test.ml.principal.reference | 12 | ||||
| -rw-r--r-- | testsuite/tests/typing-gadts/test.ml.reference | 14 | ||||
| -rw-r--r-- | testsuite/tests/typing-gadts/yallop_bugs.ml.principal.reference | 4 | ||||
| -rw-r--r-- | testsuite/tests/typing-gadts/yallop_bugs.ml.reference | 4 | ||||
| -rw-r--r-- | testsuite/tests/typing-poly/poly.ml.principal.reference | 10 | ||||
| -rw-r--r-- | testsuite/tests/typing-poly/poly.ml.reference | 10 | ||||
| -rw-r--r-- | typing/ctype.ml | 12 | ||||
| -rw-r--r-- | typing/ctype.mli | 1 | ||||
| -rw-r--r-- | typing/typecore.ml | 10 |
16 files changed, 131 insertions, 124 deletions
diff --git a/testsuite/tests/typing-gadts/dynamic_frisch.ml.principal.reference b/testsuite/tests/typing-gadts/dynamic_frisch.ml.principal.reference index 39102239a..f9c67023c 100644 --- a/testsuite/tests/typing-gadts/dynamic_frisch.ml.principal.reference +++ b/testsuite/tests/typing-gadts/dynamic_frisch.ml.principal.reference @@ -9,9 +9,9 @@ | VString of string | VList of variant list | VPair of variant * variant -val variantize : 'a ty -> 'a -> variant = <fun> +val variantize : 't ty -> 't -> variant = <fun> exception VariantMismatch -val devariantize : 'a ty -> variant -> 'a = <fun> +val devariantize : 't ty -> variant -> 't = <fun> # type 'a ty = Int : int ty | String : string ty @@ -27,7 +27,7 @@ and ('a, 'b) field = { label : string; field_type : 'b ty; get : 'a -> 'b; } | VList of variant list | VPair of variant * variant | VRecord of (string * variant) list -val variantize : 'a ty -> 'a -> variant = <fun> +val variantize : 't ty -> 't -> variant = <fun> # type 'a ty = Int : int ty | String : string ty @@ -48,7 +48,7 @@ and ('a, 'builder, 'b) field_ = { get : 'a -> 'b; set : 'builder -> 'b -> unit; } -val devariantize : 'a ty -> variant -> 'a = <fun> +val devariantize : 't ty -> variant -> 't = <fun> # type my_record = { a : int; b : string list; } val my_record : my_record ty = Record @@ -87,8 +87,8 @@ and ('a, 'b) ty_case = # type ('a, 'b) eq = Eq : ('a, 'a) eq val eq_sel : ('a, 'b) ty_sel -> ('a, 'c) ty_sel -> ('b, 'c) eq option = <fun> val get_case : - ('a, 'b) ty_sel -> - (string * ('c, 'a) ty_case) list -> string * ('b, 'c) ty option = <fun> + ('b, 'a) ty_sel -> + (string * ('e, 'b) ty_case) list -> string * ('a, 'e) ty option = <fun> # type variant = VInt of int | VString of string @@ -98,8 +98,8 @@ val get_case : | VConv of string * variant | VSum of string * variant option val may_map : ('a -> 'b) -> 'a option -> 'b option = <fun> -val variantize : 'a ty_env -> ('b, 'a) ty -> 'b -> variant = <fun> -# val devariantize : 'a ty_env -> ('b, 'a) ty -> variant -> 'b = <fun> +val variantize : 'e ty_env -> ('a, 'e) ty -> 'a -> variant = <fun> +# val devariantize : 'e ty_env -> ('t, 'e) ty -> variant -> 't = <fun> # val wrap_A : ('a, 'b) ty -> ([ `A of 'a ], 'b) ty = <fun> # val ty : ('a, ([ `A of ('a * 'b) option ] as 'b) -> 'c) ty -> ('b, 'c) ty = <fun> @@ -124,7 +124,7 @@ val v : variant = sum_inj = <fun>} # val a : [ `A of int | `B of string | `C ] = `A 3 type 'a vlist = [ `Cons of 'a * 'a vlist | `Nil ] -val ty_list : ('a, 'b) ty -> ('a vlist, 'b) ty = <fun> +val ty_list : ('a, 'e) ty -> ('a vlist, 'e) ty = <fun> val v : variant = VSum ("Cons", Some @@ -172,5 +172,5 @@ and ('a, 'b) ty_case = | TCnoarg : ('b, noarg) ty_sel -> ('e, 'b) ty_case # val ty_abc : ([ `A of int | `B of string | `C ], 'e) ty = Sum <obj> type 'a vlist = [ `Cons of 'a * 'a vlist | `Nil ] -val ty_list : ('a, 'b) ty -> ('a vlist, 'b) ty = <fun> +val ty_list : ('a, 'e) ty -> ('a vlist, 'e) ty = <fun> # * * * * * * * * * diff --git a/testsuite/tests/typing-gadts/dynamic_frisch.ml.reference b/testsuite/tests/typing-gadts/dynamic_frisch.ml.reference index 39102239a..f9c67023c 100644 --- a/testsuite/tests/typing-gadts/dynamic_frisch.ml.reference +++ b/testsuite/tests/typing-gadts/dynamic_frisch.ml.reference @@ -9,9 +9,9 @@ | VString of string | VList of variant list | VPair of variant * variant -val variantize : 'a ty -> 'a -> variant = <fun> +val variantize : 't ty -> 't -> variant = <fun> exception VariantMismatch -val devariantize : 'a ty -> variant -> 'a = <fun> +val devariantize : 't ty -> variant -> 't = <fun> # type 'a ty = Int : int ty | String : string ty @@ -27,7 +27,7 @@ and ('a, 'b) field = { label : string; field_type : 'b ty; get : 'a -> 'b; } | VList of variant list | VPair of variant * variant | VRecord of (string * variant) list -val variantize : 'a ty -> 'a -> variant = <fun> +val variantize : 't ty -> 't -> variant = <fun> # type 'a ty = Int : int ty | String : string ty @@ -48,7 +48,7 @@ and ('a, 'builder, 'b) field_ = { get : 'a -> 'b; set : 'builder -> 'b -> unit; } -val devariantize : 'a ty -> variant -> 'a = <fun> +val devariantize : 't ty -> variant -> 't = <fun> # type my_record = { a : int; b : string list; } val my_record : my_record ty = Record @@ -87,8 +87,8 @@ and ('a, 'b) ty_case = # type ('a, 'b) eq = Eq : ('a, 'a) eq val eq_sel : ('a, 'b) ty_sel -> ('a, 'c) ty_sel -> ('b, 'c) eq option = <fun> val get_case : - ('a, 'b) ty_sel -> - (string * ('c, 'a) ty_case) list -> string * ('b, 'c) ty option = <fun> + ('b, 'a) ty_sel -> + (string * ('e, 'b) ty_case) list -> string * ('a, 'e) ty option = <fun> # type variant = VInt of int | VString of string @@ -98,8 +98,8 @@ val get_case : | VConv of string * variant | VSum of string * variant option val may_map : ('a -> 'b) -> 'a option -> 'b option = <fun> -val variantize : 'a ty_env -> ('b, 'a) ty -> 'b -> variant = <fun> -# val devariantize : 'a ty_env -> ('b, 'a) ty -> variant -> 'b = <fun> +val variantize : 'e ty_env -> ('a, 'e) ty -> 'a -> variant = <fun> +# val devariantize : 'e ty_env -> ('t, 'e) ty -> variant -> 't = <fun> # val wrap_A : ('a, 'b) ty -> ([ `A of 'a ], 'b) ty = <fun> # val ty : ('a, ([ `A of ('a * 'b) option ] as 'b) -> 'c) ty -> ('b, 'c) ty = <fun> @@ -124,7 +124,7 @@ val v : variant = sum_inj = <fun>} # val a : [ `A of int | `B of string | `C ] = `A 3 type 'a vlist = [ `Cons of 'a * 'a vlist | `Nil ] -val ty_list : ('a, 'b) ty -> ('a vlist, 'b) ty = <fun> +val ty_list : ('a, 'e) ty -> ('a vlist, 'e) ty = <fun> val v : variant = VSum ("Cons", Some @@ -172,5 +172,5 @@ and ('a, 'b) ty_case = | TCnoarg : ('b, noarg) ty_sel -> ('e, 'b) ty_case # val ty_abc : ([ `A of int | `B of string | `C ], 'e) ty = Sum <obj> type 'a vlist = [ `Cons of 'a * 'a vlist | `Nil ] -val ty_list : ('a, 'b) ty -> ('a vlist, 'b) ty = <fun> +val ty_list : ('a, 'e) ty -> ('a vlist, 'e) ty = <fun> # * * * * * * * * * diff --git a/testsuite/tests/typing-gadts/omega07.ml.principal.reference b/testsuite/tests/typing-gadts/omega07.ml.principal.reference index 60ef06cb3..2565d932b 100644 --- a/testsuite/tests/typing-gadts/omega07.ml.principal.reference +++ b/testsuite/tests/typing-gadts/omega07.ml.principal.reference @@ -10,10 +10,10 @@ type 'a nat = NZ : zero nat | NS : 'a nat -> 'a succ nat # * type ('a, 'b, 'c) 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> +# val length : ('a, 'n) seq -> 'n nat = <fun> # * type ('a, 'b, 'c) 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> +val app : ('a, 'n) seq -> ('a, 'm) seq -> ('a, 'n, 'm) app = <fun> # * type tp type nd type ('a, 'b) fk @@ -35,9 +35,9 @@ type 'a boolean = BT : tt boolean | BF : ff boolean | 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 = +# val find : ('a -> 'a -> bool) -> 'a -> ('sh, 'a) tree -> ('sh, 'a) path list = <fun> -# val extract : ('b, 'a) path -> ('b, 'a) tree -> 'a = <fun> +# val extract : ('sh, 'a) path -> ('sh, 'a) tree -> 'a = <fun> # type ('a, 'b) le = LeZ : 'a nat -> (zero, 'a) le | LeS : ('n, 'm) le -> ('n succ, 'm succ) le @@ -68,8 +68,8 @@ Here is an example of a value that is not matched: 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 : ('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> +val leS' : ('m, 'n) le -> ('m, 'n succ) le = <fun> +# val filter : ('a -> bool) -> ('a, 'n) seq -> ('a, 'n) filter = <fun> # type ('a, 'b, 'c) balance = Less : ('h, 'h succ, 'h succ) balance | Same : ('h, 'h, 'h) balance @@ -80,21 +80,21 @@ type 'a avl = 'hR avl -> 'hMax succ avl type avl' = Avl : 'h avl -> avl' # val empty : avl' = Avl Leaf -val elem : int -> 'a avl -> bool = <fun> +val elem : int -> 'h avl -> bool = <fun> # val rotr : - 'a succ succ avl -> - int -> 'a avl -> ('a succ succ avl, 'a succ succ succ avl) sum = <fun> + 'n succ succ avl -> + int -> 'n avl -> ('n succ succ avl, 'n succ succ succ avl) sum = <fun> # val rotl : - 'a avl -> - int -> 'a succ succ avl -> ('a succ succ avl, 'a succ succ succ avl) sum = + 'n avl -> + int -> 'n succ succ avl -> ('n succ succ avl, 'n succ succ succ avl) sum = <fun> -# val ins : int -> 'a avl -> ('a avl, 'a succ avl) sum = <fun> +# val ins : int -> 'n avl -> ('n avl, 'n succ avl) sum = <fun> # val insert : int -> avl' -> avl' = <fun> -# val del_min : 'a succ avl -> int * ('a avl, 'a succ avl) sum = <fun> +# val del_min : 'n succ avl -> int * ('n avl, 'n succ avl) sum = <fun> type 'a 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 del : int -> 'n avl -> 'n avl_del = <fun> # val delete : int -> avl' -> avl' = <fun> # type red type black @@ -114,8 +114,8 @@ type ('a, 'b) ctxt = (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> -# val fill : ('a, 'b) ctxt -> ('a, 'b) sub_tree -> rb_tree = <fun> +val color : ('c, 'n) sub_tree -> 'c crep = <fun> +# val fill : ('c, 'n) ctxt -> ('c, 'n) sub_tree -> rb_tree = <fun> # val recolor : dir -> int -> @@ -132,8 +132,8 @@ val color : ('a, 'b) sub_tree -> 'a crep = <fun> int -> (black, 'a) sub_tree -> (red, 'a) sub_tree -> (black, 'a succ) sub_tree = <fun> -# val repair : (red, 'a) sub_tree -> ('b, 'a) ctxt -> rb_tree = <fun> -# val ins : int -> ('a, 'b) sub_tree -> ('a, 'b) ctxt -> rb_tree = <fun> +# val repair : (red, 'n) sub_tree -> ('c, 'n) ctxt -> rb_tree = <fun> +# val ins : int -> ('c, 'n) sub_tree -> ('c, 'n) ctxt -> rb_tree = <fun> # val insert : int -> rb_tree -> rb_tree = <fun> # type 'a term = Const : int -> int term @@ -189,7 +189,7 @@ val ex2 : ('a, ('b -> 'c) -> 'b -> 'c) lam = # type 'a env = Enil : rnil env | Econs : 'a * 't * 'e env -> ('a, 't, 'e) rcons env -val eval_lam : 'a env -> ('a, 'b) lam -> 'b = <fun> +val eval_lam : 'e env -> ('e, 't) lam -> 't = <fun> # type add = Add type suc = Suc val env0 : @@ -246,8 +246,8 @@ type 'a ctx = # type 'a checked = Cerror of string | 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 lookup : string -> 'e ctx -> 'e checked = <fun> +# val tc : 'n nat -> 'e ctx -> term -> 'e checked = <fun> # val ctx0 : (zero, int, (suc, int -> int, (add, int -> int -> int, rnil) rcons) rcons) rcons ctx = @@ -291,18 +291,18 @@ type ('a, 'b, 'c) 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> +val mode : ('m, 'e, 't) lam -> 'm mode = <fun> # type ('a, 'b) sub = 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> +# val subst : ('m1, 'r, 't) lam -> ('r, 's) sub -> ('s, 't) lam' = <fun> # type closed = rnil type 'a rlam = ((pexp, closed, 'a) lam, (pval, closed, 'a) lam) sum # val rule : (pval, closed, ('a, 'b) tarr) lam -> (pval, closed, 'a) lam -> 'b rlam = <fun> -# val onestep : ('a, closed, 'b) lam -> 'b rlam = <fun> +# val onestep : ('m, closed, 't) lam -> 't rlam = <fun> # diff --git a/testsuite/tests/typing-gadts/omega07.ml.reference b/testsuite/tests/typing-gadts/omega07.ml.reference index 60ef06cb3..2565d932b 100644 --- a/testsuite/tests/typing-gadts/omega07.ml.reference +++ b/testsuite/tests/typing-gadts/omega07.ml.reference @@ -10,10 +10,10 @@ type 'a nat = NZ : zero nat | NS : 'a nat -> 'a succ nat # * type ('a, 'b, 'c) 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> +# val length : ('a, 'n) seq -> 'n nat = <fun> # * type ('a, 'b, 'c) 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> +val app : ('a, 'n) seq -> ('a, 'm) seq -> ('a, 'n, 'm) app = <fun> # * type tp type nd type ('a, 'b) fk @@ -35,9 +35,9 @@ type 'a boolean = BT : tt boolean | BF : ff boolean | 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 = +# val find : ('a -> 'a -> bool) -> 'a -> ('sh, 'a) tree -> ('sh, 'a) path list = <fun> -# val extract : ('b, 'a) path -> ('b, 'a) tree -> 'a = <fun> +# val extract : ('sh, 'a) path -> ('sh, 'a) tree -> 'a = <fun> # type ('a, 'b) le = LeZ : 'a nat -> (zero, 'a) le | LeS : ('n, 'm) le -> ('n succ, 'm succ) le @@ -68,8 +68,8 @@ Here is an example of a value that is not matched: 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 : ('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> +val leS' : ('m, 'n) le -> ('m, 'n succ) le = <fun> +# val filter : ('a -> bool) -> ('a, 'n) seq -> ('a, 'n) filter = <fun> # type ('a, 'b, 'c) balance = Less : ('h, 'h succ, 'h succ) balance | Same : ('h, 'h, 'h) balance @@ -80,21 +80,21 @@ type 'a avl = 'hR avl -> 'hMax succ avl type avl' = Avl : 'h avl -> avl' # val empty : avl' = Avl Leaf -val elem : int -> 'a avl -> bool = <fun> +val elem : int -> 'h avl -> bool = <fun> # val rotr : - 'a succ succ avl -> - int -> 'a avl -> ('a succ succ avl, 'a succ succ succ avl) sum = <fun> + 'n succ succ avl -> + int -> 'n avl -> ('n succ succ avl, 'n succ succ succ avl) sum = <fun> # val rotl : - 'a avl -> - int -> 'a succ succ avl -> ('a succ succ avl, 'a succ succ succ avl) sum = + 'n avl -> + int -> 'n succ succ avl -> ('n succ succ avl, 'n succ succ succ avl) sum = <fun> -# val ins : int -> 'a avl -> ('a avl, 'a succ avl) sum = <fun> +# val ins : int -> 'n avl -> ('n avl, 'n succ avl) sum = <fun> # val insert : int -> avl' -> avl' = <fun> -# val del_min : 'a succ avl -> int * ('a avl, 'a succ avl) sum = <fun> +# val del_min : 'n succ avl -> int * ('n avl, 'n succ avl) sum = <fun> type 'a 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 del : int -> 'n avl -> 'n avl_del = <fun> # val delete : int -> avl' -> avl' = <fun> # type red type black @@ -114,8 +114,8 @@ type ('a, 'b) ctxt = (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> -# val fill : ('a, 'b) ctxt -> ('a, 'b) sub_tree -> rb_tree = <fun> +val color : ('c, 'n) sub_tree -> 'c crep = <fun> +# val fill : ('c, 'n) ctxt -> ('c, 'n) sub_tree -> rb_tree = <fun> # val recolor : dir -> int -> @@ -132,8 +132,8 @@ val color : ('a, 'b) sub_tree -> 'a crep = <fun> int -> (black, 'a) sub_tree -> (red, 'a) sub_tree -> (black, 'a succ) sub_tree = <fun> -# val repair : (red, 'a) sub_tree -> ('b, 'a) ctxt -> rb_tree = <fun> -# val ins : int -> ('a, 'b) sub_tree -> ('a, 'b) ctxt -> rb_tree = <fun> +# val repair : (red, 'n) sub_tree -> ('c, 'n) ctxt -> rb_tree = <fun> +# val ins : int -> ('c, 'n) sub_tree -> ('c, 'n) ctxt -> rb_tree = <fun> # val insert : int -> rb_tree -> rb_tree = <fun> # type 'a term = Const : int -> int term @@ -189,7 +189,7 @@ val ex2 : ('a, ('b -> 'c) -> 'b -> 'c) lam = # type 'a env = Enil : rnil env | Econs : 'a * 't * 'e env -> ('a, 't, 'e) rcons env -val eval_lam : 'a env -> ('a, 'b) lam -> 'b = <fun> +val eval_lam : 'e env -> ('e, 't) lam -> 't = <fun> # type add = Add type suc = Suc val env0 : @@ -246,8 +246,8 @@ type 'a ctx = # type 'a checked = Cerror of string | 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 lookup : string -> 'e ctx -> 'e checked = <fun> +# val tc : 'n nat -> 'e ctx -> term -> 'e checked = <fun> # val ctx0 : (zero, int, (suc, int -> int, (add, int -> int -> int, rnil) rcons) rcons) rcons ctx = @@ -291,18 +291,18 @@ type ('a, 'b, 'c) 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> +val mode : ('m, 'e, 't) lam -> 'm mode = <fun> # type ('a, 'b) sub = 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> +# val subst : ('m1, 'r, 't) lam -> ('r, 's) sub -> ('s, 't) lam' = <fun> # type closed = rnil type 'a rlam = ((pexp, closed, 'a) lam, (pval, closed, 'a) lam) sum # val rule : (pval, closed, ('a, 'b) tarr) lam -> (pval, closed, 'a) lam -> 'b rlam = <fun> -# val onestep : ('a, closed, 'b) lam -> 'b rlam = <fun> +# val onestep : ('m, closed, 't) lam -> 't rlam = <fun> # diff --git a/testsuite/tests/typing-gadts/pr5332.ml.reference b/testsuite/tests/typing-gadts/pr5332.ml.reference index a77459917..4cf48a22c 100644 --- a/testsuite/tests/typing-gadts/pr5332.ml.reference +++ b/testsuite/tests/typing-gadts/pr5332.ml.reference @@ -14,6 +14,6 @@ Warning 8: this pattern-matching is not exhaustive. Here is an example of a value that is not matched: (Tbool, Tvar _) -val f : ('a, 'b) typ -> ('a, 'b) typ -> int = <fun> +val f : ('env, 'a) typ -> ('env, 'a) typ -> int = <fun> # Exception: Match_failure ("//toplevel//", 9, 1). # diff --git a/testsuite/tests/typing-gadts/term-conv.ml.principal.reference b/testsuite/tests/typing-gadts/term-conv.ml.principal.reference index 3c6b335f6..ca6f94776 100644 --- a/testsuite/tests/typing-gadts/term-conv.ml.principal.reference +++ b/testsuite/tests/typing-gadts/term-conv.ml.principal.reference @@ -9,8 +9,8 @@ | Fun : ('a ty * 'b ty) -> ('a -> 'b) ty type ('a, 'b) eq = Eq : ('a, 'a) eq exception CastFailure - val check_eq : 'a ty -> 'b ty -> ('a, 'b) eq - val gcast : 'a ty -> 'b ty -> 'a -> 'b + val check_eq : 't ty -> 't' ty -> ('t, 't') eq + val gcast : 't ty -> 't' ty -> 't -> 't' end # module HOAS : sig @@ -19,14 +19,14 @@ | Con : 't -> 't term | Lam : 's Typeable.ty * ('s term -> 't term) -> ('s -> 't) term | App : ('s -> 't) term * 's term -> 't term - val intp : 'a term -> 'a + val intp : 't term -> 't end # module DeBruijn : sig type ('env, 't) ix = ZeroIx : ('env * 't, 't) ix | SuccIx : ('env, 't) ix -> ('env * 's, 't) ix - val to_int : ('a, 'b) ix -> int + val to_int : ('env, 't) ix -> int type ('env, 't) term = Var : ('env, 't) ix -> ('env, 't) term | Con : 't -> ('env, 't) term @@ -35,8 +35,8 @@ type 'a stack = Empty : unit stack | Push : 'env stack * 't -> ('env * 't) stack - val prj : ('a, 'b) ix -> 'a stack -> 'b - val intp : ('a, 'b) term -> 'a stack -> 'b + val prj : ('env, 't) ix -> 'env stack -> 't + val intp : ('env, 't) term -> 'env stack -> 't end # module Convert : sig @@ -44,11 +44,11 @@ EmptyLayout : ('env, unit) layout | PushLayout : 't Typeable.ty * ('env, 'env') layout * ('env, 't) DeBruijn.ix -> ('env, 'env' * 't) layout - val size : ('a, 'b) layout -> int - val inc : ('a, 'b) layout -> ('a * 't, 'b) layout + val size : ('env, 'env') layout -> int + val inc : ('env, 'env') layout -> ('env * 't, 'env') layout val prj : - 'a Typeable.ty -> int -> ('b, 'c) layout -> ('b, 'a) DeBruijn.ix - val cvt : ('a, 'a) layout -> 'b HOAS.term -> ('a, 'b) DeBruijn.term + 't Typeable.ty -> int -> ('env, 'env') layout -> ('env, 't) DeBruijn.ix + val cvt : ('env, 'env) layout -> 't HOAS.term -> ('env, 't) DeBruijn.term val convert : 'a HOAS.term -> (unit, 'a) DeBruijn.term end # module Main : diff --git a/testsuite/tests/typing-gadts/term-conv.ml.reference b/testsuite/tests/typing-gadts/term-conv.ml.reference index 3c6b335f6..ca6f94776 100644 --- a/testsuite/tests/typing-gadts/term-conv.ml.reference +++ b/testsuite/tests/typing-gadts/term-conv.ml.reference @@ -9,8 +9,8 @@ | Fun : ('a ty * 'b ty) -> ('a -> 'b) ty type ('a, 'b) eq = Eq : ('a, 'a) eq exception CastFailure - val check_eq : 'a ty -> 'b ty -> ('a, 'b) eq - val gcast : 'a ty -> 'b ty -> 'a -> 'b + val check_eq : 't ty -> 't' ty -> ('t, 't') eq + val gcast : 't ty -> 't' ty -> 't -> 't' end # module HOAS : sig @@ -19,14 +19,14 @@ | Con : 't -> 't term | Lam : 's Typeable.ty * ('s term -> 't term) -> ('s -> 't) term | App : ('s -> 't) term * 's term -> 't term - val intp : 'a term -> 'a + val intp : 't term -> 't end # module DeBruijn : sig type ('env, 't) ix = ZeroIx : ('env * 't, 't) ix | SuccIx : ('env, 't) ix -> ('env * 's, 't) ix - val to_int : ('a, 'b) ix -> int + val to_int : ('env, 't) ix -> int type ('env, 't) term = Var : ('env, 't) ix -> ('env, 't) term | Con : 't -> ('env, 't) term @@ -35,8 +35,8 @@ type 'a stack = Empty : unit stack | Push : 'env stack * 't -> ('env * 't) stack - val prj : ('a, 'b) ix -> 'a stack -> 'b - val intp : ('a, 'b) term -> 'a stack -> 'b + val prj : ('env, 't) ix -> 'env stack -> 't + val intp : ('env, 't) term -> 'env stack -> 't end # module Convert : sig @@ -44,11 +44,11 @@ EmptyLayout : ('env, unit) layout | PushLayout : 't Typeable.ty * ('env, 'env') layout * ('env, 't) DeBruijn.ix -> ('env, 'env' * 't) layout - val size : ('a, 'b) layout -> int - val inc : ('a, 'b) layout -> ('a * 't, 'b) layout + val size : ('env, 'env') layout -> int + val inc : ('env, 'env') layout -> ('env * 't, 'env') layout val prj : - 'a Typeable.ty -> int -> ('b, 'c) layout -> ('b, 'a) DeBruijn.ix - val cvt : ('a, 'a) layout -> 'b HOAS.term -> ('a, 'b) DeBruijn.term + 't Typeable.ty -> int -> ('env, 'env') layout -> ('env, 't) DeBruijn.ix + val cvt : ('env, 'env) layout -> 't HOAS.term -> ('env, 't) DeBruijn.term val convert : 'a HOAS.term -> (unit, 'a) DeBruijn.term end # module Main : diff --git a/testsuite/tests/typing-gadts/test.ml.principal.reference b/testsuite/tests/typing-gadts/test.ml.principal.reference index 5e4458a98..6cdc7de00 100644 --- a/testsuite/tests/typing-gadts/test.ml.principal.reference +++ b/testsuite/tests/typing-gadts/test.ml.principal.reference @@ -7,7 +7,7 @@ | 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 + val eval : 's t -> 's val discern : 'a t -> int end # module List : @@ -35,17 +35,17 @@ module Nonexhaustive : sig type 'a u = C1 : int -> int u | C2 : bool -> bool u type 'a v = C1 : int -> int v - val unexhaustive : 'a u -> 'a + val unexhaustive : 's u -> 's module M : sig type t type u end type 'a t = Foo : M.t -> M.t t | Bar : M.u -> M.u t - val same_type : 'a t * 'a t -> bool + val same_type : 's t * 's t -> bool end # module Exhaustive : sig type t = int type u = bool type 'a v = Foo : t -> t v | Bar : u -> u v - val same_type : 'a v * 'a v -> bool + val same_type : 's v * 's v -> bool end # Characters 119-120: let eval (D x) = x @@ -205,8 +205,8 @@ Error: This expression has type [> `A of a ] ....f : type a b. (a,b) eq -> [< `A of a | `B] -> [< `A of b | `B] = fun Eq o -> o.............. Error: This definition has type - ('c, 'd) eq -> ([< `A of 'd & 'c | `B ] as 'e) -> 'e - which is less general than 'a 'b. ('a, 'b) eq -> 'e -> 'e + ('a, 'b) eq -> ([< `A of 'b & 'a | `B ] as 'c) -> 'c + which is less general than 'a0 'b0. ('a0, 'b0) eq -> 'c -> 'c # val f : ('a, 'b) eq -> [ `A of 'a | `B ] -> [ `A of 'b | `B ] = <fun> # val f : ('a, int) eq -> [ `A of 'a ] -> bool = <fun> # Characters 166-167: diff --git a/testsuite/tests/typing-gadts/test.ml.reference b/testsuite/tests/typing-gadts/test.ml.reference index 3b62fdef8..80542d949 100644 --- a/testsuite/tests/typing-gadts/test.ml.reference +++ b/testsuite/tests/typing-gadts/test.ml.reference @@ -7,7 +7,7 @@ | 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 + val eval : 's t -> 's val discern : 'a t -> int end # module List : @@ -35,17 +35,17 @@ module Nonexhaustive : sig type 'a u = C1 : int -> int u | C2 : bool -> bool u type 'a v = C1 : int -> int v - val unexhaustive : 'a u -> 'a + val unexhaustive : 's u -> 's module M : sig type t type u end type 'a t = Foo : M.t -> M.t t | Bar : M.u -> M.u t - val same_type : 'a t * 'a t -> bool + val same_type : 's t * 's t -> bool end # module Exhaustive : sig type t = int type u = bool type 'a v = Foo : t -> t v | Bar : u -> u v - val same_type : 'a v * 'a v -> bool + val same_type : 's v * 's v -> bool end # Characters 119-120: let eval (D x) = x @@ -70,7 +70,7 @@ Error: This pattern matches values of type ([? `A ] as 'a) * bool t # module Propagation : sig type 'a t = IntLit : int -> int t | BoolLit : bool -> bool t - val check : 'a t -> 'a + val check : 's t -> 's end # Characters 87-88: let f = function A -> 1 | B -> 2 @@ -199,8 +199,8 @@ Error: This expression has type [> `A of a ] ....f : type a b. (a,b) eq -> [< `A of a | `B] -> [< `A of b | `B] = fun Eq o -> o.............. Error: This definition has type - ('c, 'd) eq -> ([< `A of 'd & 'c | `B ] as 'e) -> 'e - which is less general than 'a 'b. ('a, 'b) eq -> 'e -> 'e + ('a, 'b) eq -> ([< `A of 'b & 'a | `B ] as 'c) -> 'c + which is less general than 'a0 'b0. ('a0, 'b0) eq -> 'c -> 'c # val f : ('a, 'b) eq -> [ `A of 'a | `B ] -> [ `A of 'b | `B ] = <fun> # val f : ('a, int) eq -> [ `A of 'a ] -> bool = <fun> # val f : ('a, 'b) eq -> [ `A of 'a | `B ] -> [ `A of 'b | `B ] = <fun> diff --git a/testsuite/tests/typing-gadts/yallop_bugs.ml.principal.reference b/testsuite/tests/typing-gadts/yallop_bugs.ml.principal.reference index 5b1016c97..0859c1335 100644 --- a/testsuite/tests/typing-gadts/yallop_bugs.ml.principal.reference +++ b/testsuite/tests/typing-gadts/yallop_bugs.ml.principal.reference @@ -16,7 +16,7 @@ Warning 8: this pattern-matching is not exhaustive. Here is an example of a value that is not matched: (IntLit, 0) type 'a t = IntLit : int t | BoolLit : bool t -val check : 'a t * 'a -> bool = <fun> +val check : 's t * 's -> bool = <fun> # Characters 91-180: .............................................function | {fst = BoolLit; snd = false} -> false @@ -25,5 +25,5 @@ Warning 8: this pattern-matching is not exhaustive. Here is an example of a value that is not matched: {fst=IntLit; snd=0} type ('a, 'b) pair = { fst : 'a; snd : 'b; } -val check : ('a t, 'a) pair -> bool = <fun> +val check : ('s t, 's) pair -> bool = <fun> # diff --git a/testsuite/tests/typing-gadts/yallop_bugs.ml.reference b/testsuite/tests/typing-gadts/yallop_bugs.ml.reference index 5b1016c97..0859c1335 100644 --- a/testsuite/tests/typing-gadts/yallop_bugs.ml.reference +++ b/testsuite/tests/typing-gadts/yallop_bugs.ml.reference @@ -16,7 +16,7 @@ Warning 8: this pattern-matching is not exhaustive. Here is an example of a value that is not matched: (IntLit, 0) type 'a t = IntLit : int t | BoolLit : bool t -val check : 'a t * 'a -> bool = <fun> +val check : 's t * 's -> bool = <fun> # Characters 91-180: .............................................function | {fst = BoolLit; snd = false} -> false @@ -25,5 +25,5 @@ Warning 8: this pattern-matching is not exhaustive. Here is an example of a value that is not matched: {fst=IntLit; snd=0} type ('a, 'b) pair = { fst : 'a; snd : 'b; } -val check : ('a t, 'a) pair -> bool = <fun> +val check : ('s t, 's) pair -> bool = <fun> # diff --git a/testsuite/tests/typing-poly/poly.ml.principal.reference b/testsuite/tests/typing-poly/poly.ml.principal.reference index 65043c786..b95349162 100644 --- a/testsuite/tests/typing-poly/poly.ml.principal.reference +++ b/testsuite/tests/typing-poly/poly.ml.principal.reference @@ -576,8 +576,8 @@ val g : 'a -> int = <fun> # Characters 34-74: function Leaf _ -> 1 | Node x -> 1 + d x ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -Error: This definition has type 'b t -> int which is less general than - 'a. 'a t -> int +Error: This definition has type 'a t -> int which is less general than + 'a0. 'a0 t -> int # Characters 34-78: function Leaf x -> x | Node x -> 1 + depth x;; (* fails *) ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ @@ -586,12 +586,12 @@ Error: This definition has type int t -> int which is less general than # Characters 34-74: function Leaf x -> x | Node x -> depth x;; (* fails *) ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -Error: This definition has type 'b t -> 'b which is less general than - 'a. 'a t -> 'b +Error: This definition has type 'a t -> 'a which is less general than + 'a0. 'a0 t -> 'a # Characters 38-78: function Leaf x -> x | Node x -> depth x;; (* fails *) ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -Error: This definition has type 'c. 'c t -> 'c which is less general than +Error: This definition has type 'b. 'b t -> 'b which is less general than 'b 'a. 'a t -> 'b # val r : 'a list * '_b list ref = ([], {contents = []}) val q : unit -> 'a list * '_b list ref = <fun> diff --git a/testsuite/tests/typing-poly/poly.ml.reference b/testsuite/tests/typing-poly/poly.ml.reference index 37601416b..71befc582 100644 --- a/testsuite/tests/typing-poly/poly.ml.reference +++ b/testsuite/tests/typing-poly/poly.ml.reference @@ -539,8 +539,8 @@ val g : 'a -> int = <fun> # Characters 34-74: function Leaf _ -> 1 | Node x -> 1 + d x ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -Error: This definition has type 'b t -> int which is less general than - 'a. 'a t -> int +Error: This definition has type 'a t -> int which is less general than + 'a0. 'a0 t -> int # Characters 34-78: function Leaf x -> x | Node x -> 1 + depth x;; (* fails *) ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ @@ -549,12 +549,12 @@ Error: This definition has type int t -> int which is less general than # Characters 34-74: function Leaf x -> x | Node x -> depth x;; (* fails *) ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -Error: This definition has type 'b t -> 'b which is less general than - 'a. 'a t -> 'b +Error: This definition has type 'a t -> 'a which is less general than + 'a0. 'a0 t -> 'a # Characters 38-78: function Leaf x -> x | Node x -> depth x;; (* fails *) ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -Error: This definition has type 'c. 'c t -> 'c which is less general than +Error: This definition has type 'b. 'b t -> 'b which is less general than 'b 'a. 'a t -> 'b # val r : 'a list * '_b list ref = ([], {contents = []}) val q : unit -> 'a list * '_b list ref = <fun> diff --git a/typing/ctype.ml b/typing/ctype.ml index 5e27441ea..cbd9ec144 100644 --- a/typing/ctype.ml +++ b/typing/ctype.ml @@ -1176,9 +1176,15 @@ let rec copy_sep fixed free bound visited ty = t end -let instance_poly fixed univars sch = - let vars = List.map (fun _ -> newvar ()) univars in - let pairs = List.map2 (fun u v -> repr u, (v, [])) univars vars in +let instance_poly ?(keep_names=false) fixed univars sch = + let univars = List.map repr univars in + let copy_var ty = + match ty.desc with + Tunivar name -> if keep_names then newty (Tvar name) else newvar () + | _ -> assert false + in + let vars = List.map copy_var univars in + let pairs = List.map2 (fun u v -> u, (v, [])) univars vars in delayed_copy := []; let ty = copy_sep fixed (compute_univars sch) [] pairs sch in List.iter Lazy.force !delayed_copy; diff --git a/typing/ctype.mli b/typing/ctype.mli index 0c42edafd..c4d4ff13a 100644 --- a/typing/ctype.mli +++ b/typing/ctype.mli @@ -128,6 +128,7 @@ val instance_declaration: type_declaration -> type_declaration val instance_class: type_expr list -> class_type -> type_expr list * class_type val instance_poly: + ?keep_names:bool -> bool -> type_expr list -> type_expr -> type_expr list * type_expr (* Take an instance of a type scheme containing free univars *) val instance_label: diff --git a/typing/typecore.ml b/typing/typecore.ml index 263e86a07..299cd8809 100644 --- a/typing/typecore.ml +++ b/typing/typecore.ml @@ -521,7 +521,7 @@ let rec type_pat ~constrs ~labels ~no_existentials ~mode ~env sp expected_ty = begin match ty.desc with | Tpoly (body, tyl) -> begin_def (); - let _, ty' = instance_poly false tyl body in + let _, ty' = instance_poly ~keep_names:true false tyl body in end_def (); generalize ty'; let id = enter_variable loc name ty' in @@ -2619,7 +2619,8 @@ and type_let env rec_flag spat_sexp_list scope allow = let pat = match pat.pat_type.desc with | Tpoly (ty, tl) -> - {pat with pat_type = snd (instance_poly false tl ty)} + {pat with pat_type = + snd (instance_poly ~keep_names:true false tl ty)} | _ -> pat in unify_pat env pat (type_approx env sexp)) pat_list spat_sexp_list; @@ -2653,7 +2654,7 @@ and type_let env rec_flag spat_sexp_list scope allow = | Tpoly (ty, tl) -> begin_def (); if !Clflags.principal then begin_def (); - let vars, ty' = instance_poly true tl ty in + let vars, ty' = instance_poly ~keep_names:true true tl ty in if !Clflags.principal then begin end_def (); generalize_structure ty' @@ -2674,8 +2675,7 @@ and type_let env rec_flag spat_sexp_list scope allow = iter_pattern (fun pat -> generalize_expansive env pat.pat_type) pat) pat_list exp_list; List.iter - (fun pat -> iter_pattern - (fun pat -> generalize pat.pat_type) pat) + (fun pat -> iter_pattern (fun pat -> generalize pat.pat_type) pat) pat_list; (List.combine pat_list exp_list, new_env, unpacks) |