diff options
Diffstat (limited to 'testsuite/tests')
22 files changed, 1689 insertions, 115 deletions
diff --git a/testsuite/tests/typing-gadts/dynamic_frisch.ml b/testsuite/tests/typing-gadts/dynamic_frisch.ml new file mode 100644 index 000000000..895be5a05 --- /dev/null +++ b/testsuite/tests/typing-gadts/dynamic_frisch.ml @@ -0,0 +1,475 @@ +(* Encoding generics using GADTs *) +(* (c) Alain Frisch / Lexifi *) +(* cf. http://www.lexifi.com/blog/dynamic-types *) + +(* Basic tag *) + +type 'a ty = + | Int: int ty + | String: string ty + | List: 'a ty -> 'a list ty + | Pair: ('a ty * 'b ty) -> ('a * 'b) ty +;; + +(* Tagging data *) + +type variant = + | VInt of int + | VString of string + | VList of variant list + | VPair of variant * variant + +let rec variantize: type t. t ty -> t -> variant = + fun ty x -> + (* type t is abstract here *) + match ty with + | Int -> VInt x (* in this branch: t = int *) + | String -> VString x (* t = string *) + | List ty1 -> + VList (List.map (variantize ty1) x) + (* t = 'a list for some 'a *) + | Pair (ty1, ty2) -> + VPair (variantize ty1 (fst x), variantize ty2 (snd x)) + (* t = ('a, 'b) for some 'a and 'b *) + +exception VariantMismatch + +let rec devariantize: type t. t ty -> variant -> t = + fun ty v -> + match ty, v with + | Int, VInt x -> x + | String, VString x -> x + | List ty1, VList vl -> + List.map (devariantize ty1) vl + | Pair (ty1, ty2), VPair (x1, x2) -> + (devariantize ty1 x1, devariantize ty2 x2) + | _ -> raise VariantMismatch +;; + +(* Handling records *) + +type 'a ty = + | Int: int ty + | String: string ty + | List: 'a ty -> 'a list ty + | Pair: ('a ty * 'b ty) -> ('a * 'b) ty + | Record: 'a record -> 'a ty + +and 'a record = + { + path: string; + fields: 'a field_ list; + } + +and 'a field_ = + | Field: ('a, 'b) field -> 'a field_ + +and ('a, 'b) field = + { + label: string; + field_type: 'b ty; + get: ('a -> 'b); + } +;; + +(* Again *) + +type variant = + | VInt of int + | VString of string + | VList of variant list + | VPair of variant * variant + | VRecord of (string * variant) list + +let rec variantize: type t. t ty -> t -> variant = + fun ty x -> + (* type t is abstract here *) + match ty with + | Int -> VInt x (* in this branch: t = int *) + | String -> VString x (* t = string *) + | List ty1 -> + VList (List.map (variantize ty1) x) + (* t = 'a list for some 'a *) + | Pair (ty1, ty2) -> + VPair (variantize ty1 (fst x), variantize ty2 (snd x)) + (* t = ('a, 'b) for some 'a and 'b *) + | Record {fields} -> + VRecord + (List.map (fun (Field{field_type; label; get}) -> + (label, variantize field_type (get x))) fields) +;; + +(* Extraction *) + +type 'a ty = + | Int: int ty + | String: string ty + | List: 'a ty -> 'a list ty + | Pair: ('a ty * 'b ty) -> ('a * 'b) ty + | Record: ('a, 'builder) record -> 'a ty + +and ('a, 'builder) record = + { + path: string; + fields: ('a, 'builder) field list; + create_builder: (unit -> 'builder); + of_builder: ('builder -> 'a); + } + +and ('a, 'builder) field = + | Field: ('a, 'builder, 'b) field_ -> ('a, 'builder) field + +and ('a, 'builder, 'b) field_ = + { + label: string; + field_type: 'b ty; + get: ('a -> 'b); + set: ('builder -> 'b -> unit); + } + +let rec devariantize: type t. t ty -> variant -> t = + fun ty v -> + match ty, v with + | Int, VInt x -> x + | String, VString x -> x + | List ty1, VList vl -> + List.map (devariantize ty1) vl + | Pair (ty1, ty2), VPair (x1, x2) -> + (devariantize ty1 x1, devariantize ty2 x2) + | Record {fields; create_builder; of_builder}, VRecord fl -> + if List.length fields <> List.length fl then raise VariantMismatch; + let builder = create_builder () in + List.iter2 + (fun (Field {label; field_type; set}) (lab, v) -> + if label <> lab then raise VariantMismatch; + set builder (devariantize field_type v) + ) + fields fl; + of_builder builder + | _ -> raise VariantMismatch +;; + +type my_record = + { + a: int; + b: string list; + } + +let my_record = + let fields = + [ + Field {label = "a"; field_type = Int; + get = (fun {a} -> a); + set = (fun (r, _) x -> r := Some x)}; + Field {label = "b"; field_type = List String; + get = (fun {b} -> b); + set = (fun (_, r) x -> r := Some x)}; + ] + in + let create_builder () = (ref None, ref None) in + let of_builder (a, b) = + match !a, !b with + | Some a, Some b -> {a; b} + | _ -> failwith "Some fields are missing in record of type my_record" + in + Record {path = "My_module.my_record"; fields; create_builder; of_builder} +;; + +(* Extension to recursive types and polymorphic variants *) +(* by Jacques Garrigue *) + +type noarg = Noarg + +type (_,_) ty = + | Int: (int,_) ty + | String: (string,_) ty + | List: ('a,'e) ty -> ('a list, 'e) ty + | Option: ('a,'e) ty -> ('a option, 'e) ty + | Pair: (('a,'e) ty * ('b,'e) ty) -> ('a * 'b,'e) ty + (* Support for type variables and recursive types *) + | Var: ('a, 'a -> 'e) ty + | Rec: ('a, 'a -> 'e) ty -> ('a,'e) ty + | Pop: ('a, 'e) ty -> ('a, 'b -> 'e) ty + (* Change the representation of a type *) + | Conv: string * ('a -> 'b) * ('b -> 'a) * ('b, 'e) ty -> ('a, 'e) ty + (* Sum types (both normal sums and polymorphic variants) *) + | Sum: ('a, 'e, 'b) ty_sum -> ('a, 'e) ty + +and ('a, 'e, 'b) ty_sum = + { sum_proj: 'a -> string * 'e ty_dyn option; + sum_cases: (string * ('e,'b) ty_case) list; + sum_inj: 'c. ('b,'c) ty_sel * 'c -> 'a; } + +and 'e ty_dyn = (* dynamic type *) + | Tdyn : ('a,'e) ty * 'a -> 'e ty_dyn + +and (_,_) ty_sel = (* selector from a list of types *) + | Thd : ('a -> 'b, 'a) ty_sel + | Ttl : ('b -> 'c, 'd) ty_sel -> ('a -> 'b -> 'c, 'd) ty_sel + +and (_,_) ty_case = (* type a sum case *) + | TCarg : ('b,'a) ty_sel * ('a,'e) ty -> ('e,'b) ty_case + | TCnoarg : ('b,noarg) ty_sel -> ('e,'b) ty_case +;; + +type _ ty_env = (* type variable substitution *) + | Enil : unit ty_env + | Econs : ('a,'e) ty * 'e ty_env -> ('a -> 'e) ty_env +;; + +(* Comparing selectors *) +type (_,_) eq = Eq: ('a,'a) eq + +let rec eq_sel : type a b c. (a,b) ty_sel -> (a,c) ty_sel -> (b,c) eq option = + fun s1 s2 -> + match s1, s2 with + | Thd, Thd -> Some Eq + | Ttl s1, Ttl s2 -> + (match eq_sel s1 s2 with None -> None | Some Eq -> Some Eq) + | _ -> None + +(* Auxiliary function to get the type of a case from its selector *) +let rec get_case : type a b e. + (b, a) ty_sel -> (string * (e,b) ty_case) list -> string * (a, e) ty option = + fun sel cases -> + match cases with + | (name, TCnoarg sel') :: rem -> + begin match eq_sel sel sel' with + | None -> get_case sel rem + | Some Eq -> name, None + end + | (name, TCarg (sel', ty)) :: rem -> + begin match eq_sel sel sel' with + | None -> get_case sel rem + | Some Eq -> name, Some ty + end + | [] -> raise Not_found +;; + +(* Untyped representation of values *) +type variant = + | VInt of int + | VString of string + | VList of variant list + | VOption of variant option + | VPair of variant * variant + | VConv of string * variant + | VSum of string * variant option + +let may_map f = function Some x -> Some (f x) | None -> None + +let rec variantize : type a e. e ty_env -> (a,e) ty -> a -> variant = + fun e ty v -> + match ty with + | Int -> VInt v + | String -> VString v + | List t -> VList (List.map (variantize e t) v) + | Option t -> VOption (may_map (variantize e t) v) + | Pair (t1, t2) -> VPair (variantize e t1 (fst v), variantize e t2 (snd v)) + | Rec t -> variantize (Econs (ty, e)) t v + | Pop t -> (match e with Econs (_, e') -> variantize e' t v) + | Var -> (match e with Econs (t, e') -> variantize e' t v) + | Conv (s, proj, inj, t) -> VConv (s, variantize e t (proj v)) + | Sum ops -> + let tag, arg = ops.sum_proj v in + VSum (tag, may_map (function Tdyn (ty,arg) -> variantize e ty arg) arg) +;; + +let rec devariantize : type t e. e ty_env -> (t, e) ty -> variant -> t = + fun e ty v -> + match ty, v with + | Int, VInt x -> x + | String, VString x -> x + | List ty1, VList vl -> + List.map (devariantize e ty1) vl + | Pair (ty1, ty2), VPair (x1, x2) -> + (devariantize e ty1 x1, devariantize e ty2 x2) + | Rec t, _ -> devariantize (Econs (ty, e)) t v + | Pop t, _ -> (match e with Econs (_, e') -> devariantize e' t v) + | Var, _ -> (match e with Econs (t, e') -> devariantize e' t v) + | Conv (s, proj, inj, t), VConv (s', v) when s = s' -> + inj (devariantize e t v) + | Sum ops, VSum (tag, a) -> + begin try match List.assoc tag ops.sum_cases, a with + | TCarg (sel, t), Some a -> ops.sum_inj (sel, devariantize e t a) + | TCnoarg sel, None -> ops.sum_inj (sel, Noarg) + | _ -> raise VariantMismatch + with Not_found -> raise VariantMismatch + end + | _ -> raise VariantMismatch +;; + +(* First attempt: represent 1-constructor variants using Conv *) +let wrap_A t = Conv ("`A", (fun (`A x) -> x), (fun x -> `A x), t);; + +let ty a = Rec (wrap_A (Option (Pair (a, Var)))) ;; +let v = variantize Enil (ty Int);; +let x = v (`A (Some (1, `A (Some (2, `A None))))) ;; + +(* Can also use it to decompose a tuple *) + +let triple t1 t2 t3 = + Conv ("Triple", (fun (a,b,c) -> (a,(b,c))), + (fun (a,(b,c)) -> (a,b,c)), Pair (t1, Pair (t2, t3))) + +let v = variantize Enil (triple String Int Int) ("A", 2, 3) ;; + +(* Second attempt: introduce a real sum construct *) +let ty_abc = + (* Could also use [get_case] for proj, but direct definition is shorter *) + let proj = function + `A n -> "A", Some (Tdyn (Int, n)) + | `B s -> "B", Some (Tdyn (String, s)) + | `C -> "C", None + (* Define inj in advance to be able to write the type annotation easily *) + and inj : type c. (int -> string -> noarg -> unit, c) ty_sel * c -> + [`A of int | `B of string | `C] = function + Thd, v -> `A v + | Ttl Thd, v -> `B v + | Ttl (Ttl Thd), Noarg -> `C + in + (* Coherence of sum_inj and sum_cases is checked by the typing *) + Sum { sum_proj = proj; sum_inj = inj; sum_cases = + [ "A", TCarg (Thd, Int); "B", TCarg (Ttl Thd, String); + "C", TCnoarg (Ttl (Ttl Thd)) ] } +;; + +let v = variantize Enil ty_abc (`A 3) +let a = devariantize Enil ty_abc v + +(* And an example with recursion... *) +type 'a vlist = [`Nil | `Cons of 'a * 'a vlist] + +let ty_list : type a e. (a, e) ty -> (a vlist, e) ty = fun t -> + let tcons = Pair (Pop t, Var) in + Rec (Sum { + sum_proj = (function + `Nil -> "Nil", None + | `Cons p -> "Cons", Some (Tdyn (tcons, p))); + sum_cases = ["Nil", TCnoarg Thd; "Cons", TCarg (Ttl Thd, tcons)]; + sum_inj = fun (type c) -> + (function + | Thd, Noarg -> `Nil + | Ttl Thd, v -> `Cons v + : (noarg -> a * a vlist -> unit, c) ty_sel * c -> a vlist) + (* One can also write the type annotation directly *) + }) + +let v = variantize Enil (ty_list Int) (`Cons (1, `Cons (2, `Nil))) ;; + + +(* Simpler but weaker approach *) + +type (_,_) ty = + | Int: (int,_) ty + | String: (string,_) ty + | List: ('a,'e) ty -> ('a list, 'e) ty + | Option: ('a,'e) ty -> ('a option, 'e) ty + | Pair: (('a,'e) ty * ('b,'e) ty) -> ('a * 'b,'e) ty + | Var: ('a, 'a -> 'e) ty + | Rec: ('a, 'a -> 'e) ty -> ('a,'e) ty + | Pop: ('a, 'e) ty -> ('a, 'b -> 'e) ty + | Conv: string * ('a -> 'b) * ('b -> 'a) * ('b, 'e) ty -> ('a, 'e) ty + | Sum: ('a -> string * 'e ty_dyn option) * (string * 'e ty_dyn option -> 'a) + -> ('a, 'e) ty +and 'e ty_dyn = + | Tdyn : ('a,'e) ty * 'a -> 'e ty_dyn + +let ty_abc : ([`A of int | `B of string | `C],'e) ty = + (* Could also use [get_case] for proj, but direct definition is shorter *) + Sum ( + (function + `A n -> "A", Some (Tdyn (Int, n)) + | `B s -> "B", Some (Tdyn (String, s)) + | `C -> "C", None), + (function + "A", Some (Tdyn (Int, n)) -> `A n + | "B", Some (Tdyn (String, s)) -> `B s + | "C", None -> `C + | _ -> invalid_arg "ty_abc")) +;; + +(* Breaks: no way to pattern-match on a full recursive type *) +let ty_list : type a e. (a,e) ty -> (a vlist,e) ty = fun t -> + let targ = Pair (Pop t, Var) in + Rec (Sum ( + (function `Nil -> "Nil", None + | `Cons p -> "Cons", Some (Tdyn (targ, p))), + (function "Nil", None -> `Nil + | "Cons", Some (Tdyn (Pair (_, Var), (p : a * a vlist))) -> `Cons p))) +;; + +(* Define Sum using object instead of record for first-class polymorphism *) + +type (_,_) ty = + | Int: (int,_) ty + | String: (string,_) ty + | List: ('a,'e) ty -> ('a list, 'e) ty + | Option: ('a,'e) ty -> ('a option, 'e) ty + | Pair: (('a,'e) ty * ('b,'e) ty) -> ('a * 'b,'e) ty + | Var: ('a, 'a -> 'e) ty + | Rec: ('a, 'a -> 'e) ty -> ('a,'e) ty + | Pop: ('a, 'e) ty -> ('a, 'b -> 'e) ty + | Conv: string * ('a -> 'b) * ('b -> 'a) * ('b, 'e) ty -> ('a, 'e) ty + | Sum: < proj: 'a -> string * 'e ty_dyn option; + cases: (string * ('e,'b) ty_case) list; + inj: 'c. ('b,'c) ty_sel * 'c -> 'a > + -> ('a, 'e) ty + +and 'e ty_dyn = + | Tdyn : ('a,'e) ty * 'a -> 'e ty_dyn + +and (_,_) ty_sel = + | Thd : ('a -> 'b, 'a) ty_sel + | Ttl : ('b -> 'c, 'd) ty_sel -> ('a -> 'b -> 'c, 'd) ty_sel + +and (_,_) ty_case = + | TCarg : ('b,'a) ty_sel * ('a,'e) ty -> ('e,'b) ty_case + | TCnoarg : ('b,noarg) ty_sel -> ('e,'b) ty_case +;; + +let ty_abc : ([`A of int | `B of string | `C] as 'a, 'e) ty = + Sum (object + method proj = function + `A n -> "A", Some (Tdyn (Int, n)) + | `B s -> "B", Some (Tdyn (String, s)) + | `C -> "C", None + method cases = + [ "A", TCarg (Thd, Int); "B", TCarg (Ttl Thd, String); + "C", TCnoarg (Ttl (Ttl Thd)) ]; + method inj : type c. + (int -> string -> noarg -> unit, c) ty_sel * c -> + [`A of int | `B of string | `C] = + function + Thd, v -> `A v + | Ttl Thd, v -> `B v + | Ttl (Ttl Thd), Noarg -> `C + | _ -> assert false + end) + +type 'a vlist = [`Nil | `Cons of 'a * 'a vlist] + +let ty_list : type a e. (a, e) ty -> (a vlist, e) ty = fun t -> + let tcons = Pair (Pop t, Var) in + Rec (Sum (object + method proj = function + `Nil -> "Nil", None + | `Cons p -> "Cons", Some (Tdyn (tcons, p)) + method cases = ["Nil", TCnoarg Thd; "Cons", TCarg (Ttl Thd, tcons)] + method inj : type c.(noarg -> a * a vlist -> unit, c) ty_sel * c -> a vlist + = function + | Thd, Noarg -> `Nil + | Ttl Thd, v -> `Cons v + end)) +;; + +(* +type (_,_) ty_assoc = + | Anil : (unit,'e) ty_assoc + | Acons : string * ('a,'e) ty * ('b,'e) ty_assoc -> ('a -> 'b, 'e) ty_assoc + +and (_,_) ty_pvar = + | Pnil : ('a,'e) ty_pvar + | Pconst : 't * ('b,'e) ty_pvar -> ('t -> 'b, 'e) ty_pvar + | Parg : 't * ('a,'e) ty * ('b,'e) ty_pvar -> ('t * 'a -> 'b, 'e) ty_pvar +*) diff --git a/testsuite/tests/typing-gadts/dynamic_frisch.ml.principal.reference b/testsuite/tests/typing-gadts/dynamic_frisch.ml.principal.reference new file mode 100644 index 000000000..dda0a0fa7 --- /dev/null +++ b/testsuite/tests/typing-gadts/dynamic_frisch.ml.principal.reference @@ -0,0 +1,176 @@ + +# type 'a ty = + Int : int ty + | String : string ty + | List : 'a ty -> 'a list ty + | Pair : ('a ty * 'b ty) -> ('a * 'b) ty +# type variant = + VInt of int + | VString of string + | VList of variant list + | VPair of variant * variant +val variantize : 'a ty -> 'a -> variant = <fun> +exception VariantMismatch +val devariantize : 'a ty -> variant -> 'a = <fun> +# type 'a ty = + Int : int ty + | String : string ty + | List : 'a ty -> 'a list ty + | Pair : ('a ty * 'b ty) -> ('a * 'b) ty + | Record : 'a record -> 'a ty +and 'a record = { path : string; fields : 'a field_ list; } +and 'a field_ = Field : ('a, 'b) field -> 'a field_ +and ('a, 'b) field = { label : string; field_type : 'b ty; get : 'a -> 'b; } +# type variant = + VInt of int + | VString of string + | VList of variant list + | VPair of variant * variant + | VRecord of (string * variant) list +val variantize : 'a ty -> 'a -> variant = <fun> +# type 'a ty = + Int : int ty + | String : string ty + | List : 'a ty -> 'a list ty + | Pair : ('a ty * 'b ty) -> ('a * 'b) ty + | Record : ('a, 'builder) record -> 'a ty +and ('a, 'builder) record = { + path : string; + fields : ('a, 'builder) field list; + create_builder : unit -> 'builder; + of_builder : 'builder -> 'a; +} +and ('a, 'builder) field = + Field : ('a, 'builder, 'b) field_ -> ('a, 'builder) field +and ('a, 'builder, 'b) field_ = { + label : string; + field_type : 'b ty; + get : 'a -> 'b; + set : 'builder -> 'b -> unit; +} +val devariantize : 'a ty -> variant -> 'a = <fun> +# type my_record = { a : int; b : string list; } +val my_record : my_record ty = + Record + {path = "My_module.my_record"; + fields = + [Field {label = "a"; field_type = Int; get = <fun>; set = <fun>}; + Field {label = "b"; field_type = List String; get = <fun>; set = <fun>}]; + create_builder = <fun>; of_builder = <fun>} +# type noarg = Noarg +type ('a, 'b) ty = + Int : (int, 'c) ty + | String : (string, 'd) ty + | List : ('a, 'e) ty -> ('a list, 'e) ty + | Option : ('a, 'e) ty -> ('a option, 'e) ty + | Pair : (('a, 'e) ty * ('b, 'e) ty) -> ('a * 'b, 'e) ty + | Var : ('a, 'a -> 'e) ty + | Rec : ('a, 'a -> 'e) ty -> ('a, 'e) ty + | Pop : ('a, 'e) ty -> ('a, 'b -> 'e) ty + | Conv : string * ('a -> 'b) * ('b -> 'a) * ('b, 'e) ty -> ('a, 'e) ty + | Sum : ('a, 'e, 'b) ty_sum -> ('a, 'e) ty +and ('a, 'e, 'b) ty_sum = { + sum_proj : 'a -> string * 'e ty_dyn option; + sum_cases : (string * ('e, 'b) ty_case) list; + sum_inj : 'c. ('b, 'c) ty_sel * 'c -> 'a; +} +and 'e ty_dyn = Tdyn : ('a, 'e) ty * 'a -> 'e ty_dyn +and ('a, 'b) ty_sel = + Thd : ('a -> 'b, 'a) ty_sel + | Ttl : ('b -> 'c, 'd) ty_sel -> ('a -> 'b -> 'c, 'd) ty_sel +and ('a, 'b) ty_case = + TCarg : ('b, 'a) ty_sel * ('a, 'e) ty -> ('e, 'b) ty_case + | TCnoarg : ('b, noarg) ty_sel -> ('e, 'b) ty_case +# type 'a ty_env = + Enil : unit ty_env + | Econs : ('a, 'e) ty * 'e ty_env -> ('a -> 'e) ty_env +# 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> +# type variant = + VInt of int + | VString of string + | VList of variant list + | VOption of variant option + | VPair of variant * variant + | 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 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> +# val v : ([ `A of (int * 'a) option ] as 'a) -> variant = <fun> +# val x : variant = + VConv ("`A", + VOption + (Some + (VPair (VInt 1, + VConv ("`A", + VOption (Some (VPair (VInt 2, VConv ("`A", VOption None))))))))) +# val triple : + ('a, 'b) ty -> ('c, 'b) ty -> ('d, 'b) ty -> ('a * 'c * 'd, 'b) ty = <fun> +val v : variant = + VConv ("Triple", VPair (VString "A", VPair (VInt 2, VInt 3))) +# val ty_abc : ([ `A of int | `B of string | `C ], 'a) ty = + Sum + {sum_proj = <fun>; + sum_cases = + [("A", TCarg (Thd, Int)); ("B", TCarg (Ttl Thd, String)); + ("C", TCnoarg (Ttl (Ttl Thd)))]; + 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 v : variant = + VSum ("Cons", + Some + (VPair (VInt 1, VSum ("Cons", Some (VPair (VInt 2, VSum ("Nil", None))))))) +# type ('a, 'b) ty = + Int : (int, 'c) ty + | String : (string, 'd) ty + | List : ('a, 'e) ty -> ('a list, 'e) ty + | Option : ('a, 'e) ty -> ('a option, 'e) ty + | Pair : (('a, 'e) ty * ('b, 'e) ty) -> ('a * 'b, 'e) ty + | Var : ('a, 'a -> 'e) ty + | Rec : ('a, 'a -> 'e) ty -> ('a, 'e) ty + | Pop : ('a, 'e) ty -> ('a, 'b -> 'e) ty + | Conv : string * ('a -> 'b) * ('b -> 'a) * ('b, 'e) ty -> ('a, 'e) ty + | Sum : ('a -> string * 'e ty_dyn option) * + (string * 'e ty_dyn option -> 'a) -> ('a, 'e) ty +and 'e ty_dyn = Tdyn : ('a, 'e) ty * 'a -> 'e ty_dyn +val ty_abc : ([ `A of int | `B of string | `C ], 'e) ty = Sum (<fun>, <fun>) +# Characters 327-344: + | "Cons", Some (Tdyn (Pair (_, Var), (p : a * a vlist))) -> `Cons p))) + ^^^^^^^^^^^^^^^^^ +Error: This pattern matches values of type a * a vlist + but a pattern was expected which matches values of type + ex#42 = ex#43 * ex#44 +# type ('a, 'b) ty = + Int : (int, 'd) ty + | String : (string, 'f) ty + | List : ('a, 'e) ty -> ('a list, 'e) ty + | Option : ('a, 'e) ty -> ('a option, 'e) ty + | Pair : (('a, 'e) ty * ('b, 'e) ty) -> ('a * 'b, 'e) ty + | Var : ('a, 'a -> 'e) ty + | Rec : ('a, 'a -> 'e) ty -> ('a, 'e) ty + | Pop : ('a, 'e) ty -> ('a, 'b -> 'e) ty + | Conv : string * ('a -> 'b) * ('b -> 'a) * ('b, 'e) ty -> ('a, 'e) ty + | Sum : + < cases : (string * ('e, 'b) ty_case) list; + inj : 'c. ('b, 'c) ty_sel * 'c -> 'a; + proj : 'a -> string * 'e ty_dyn option > -> ('a, 'e) ty +and 'e ty_dyn = Tdyn : ('a, 'e) ty * 'a -> 'e ty_dyn +and ('a, 'b) ty_sel = + Thd : ('a -> 'b, 'a) ty_sel + | Ttl : ('b -> 'c, 'd) ty_sel -> ('a -> 'b -> 'c, 'd) ty_sel +and ('a, 'b) ty_case = + TCarg : ('b, 'a) ty_sel * ('a, 'e) ty -> ('e, '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> +# * * * * * * * * * diff --git a/testsuite/tests/typing-gadts/dynamic_frisch.ml.reference b/testsuite/tests/typing-gadts/dynamic_frisch.ml.reference new file mode 100644 index 000000000..dda0a0fa7 --- /dev/null +++ b/testsuite/tests/typing-gadts/dynamic_frisch.ml.reference @@ -0,0 +1,176 @@ + +# type 'a ty = + Int : int ty + | String : string ty + | List : 'a ty -> 'a list ty + | Pair : ('a ty * 'b ty) -> ('a * 'b) ty +# type variant = + VInt of int + | VString of string + | VList of variant list + | VPair of variant * variant +val variantize : 'a ty -> 'a -> variant = <fun> +exception VariantMismatch +val devariantize : 'a ty -> variant -> 'a = <fun> +# type 'a ty = + Int : int ty + | String : string ty + | List : 'a ty -> 'a list ty + | Pair : ('a ty * 'b ty) -> ('a * 'b) ty + | Record : 'a record -> 'a ty +and 'a record = { path : string; fields : 'a field_ list; } +and 'a field_ = Field : ('a, 'b) field -> 'a field_ +and ('a, 'b) field = { label : string; field_type : 'b ty; get : 'a -> 'b; } +# type variant = + VInt of int + | VString of string + | VList of variant list + | VPair of variant * variant + | VRecord of (string * variant) list +val variantize : 'a ty -> 'a -> variant = <fun> +# type 'a ty = + Int : int ty + | String : string ty + | List : 'a ty -> 'a list ty + | Pair : ('a ty * 'b ty) -> ('a * 'b) ty + | Record : ('a, 'builder) record -> 'a ty +and ('a, 'builder) record = { + path : string; + fields : ('a, 'builder) field list; + create_builder : unit -> 'builder; + of_builder : 'builder -> 'a; +} +and ('a, 'builder) field = + Field : ('a, 'builder, 'b) field_ -> ('a, 'builder) field +and ('a, 'builder, 'b) field_ = { + label : string; + field_type : 'b ty; + get : 'a -> 'b; + set : 'builder -> 'b -> unit; +} +val devariantize : 'a ty -> variant -> 'a = <fun> +# type my_record = { a : int; b : string list; } +val my_record : my_record ty = + Record + {path = "My_module.my_record"; + fields = + [Field {label = "a"; field_type = Int; get = <fun>; set = <fun>}; + Field {label = "b"; field_type = List String; get = <fun>; set = <fun>}]; + create_builder = <fun>; of_builder = <fun>} +# type noarg = Noarg +type ('a, 'b) ty = + Int : (int, 'c) ty + | String : (string, 'd) ty + | List : ('a, 'e) ty -> ('a list, 'e) ty + | Option : ('a, 'e) ty -> ('a option, 'e) ty + | Pair : (('a, 'e) ty * ('b, 'e) ty) -> ('a * 'b, 'e) ty + | Var : ('a, 'a -> 'e) ty + | Rec : ('a, 'a -> 'e) ty -> ('a, 'e) ty + | Pop : ('a, 'e) ty -> ('a, 'b -> 'e) ty + | Conv : string * ('a -> 'b) * ('b -> 'a) * ('b, 'e) ty -> ('a, 'e) ty + | Sum : ('a, 'e, 'b) ty_sum -> ('a, 'e) ty +and ('a, 'e, 'b) ty_sum = { + sum_proj : 'a -> string * 'e ty_dyn option; + sum_cases : (string * ('e, 'b) ty_case) list; + sum_inj : 'c. ('b, 'c) ty_sel * 'c -> 'a; +} +and 'e ty_dyn = Tdyn : ('a, 'e) ty * 'a -> 'e ty_dyn +and ('a, 'b) ty_sel = + Thd : ('a -> 'b, 'a) ty_sel + | Ttl : ('b -> 'c, 'd) ty_sel -> ('a -> 'b -> 'c, 'd) ty_sel +and ('a, 'b) ty_case = + TCarg : ('b, 'a) ty_sel * ('a, 'e) ty -> ('e, 'b) ty_case + | TCnoarg : ('b, noarg) ty_sel -> ('e, 'b) ty_case +# type 'a ty_env = + Enil : unit ty_env + | Econs : ('a, 'e) ty * 'e ty_env -> ('a -> 'e) ty_env +# 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> +# type variant = + VInt of int + | VString of string + | VList of variant list + | VOption of variant option + | VPair of variant * variant + | 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 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> +# val v : ([ `A of (int * 'a) option ] as 'a) -> variant = <fun> +# val x : variant = + VConv ("`A", + VOption + (Some + (VPair (VInt 1, + VConv ("`A", + VOption (Some (VPair (VInt 2, VConv ("`A", VOption None))))))))) +# val triple : + ('a, 'b) ty -> ('c, 'b) ty -> ('d, 'b) ty -> ('a * 'c * 'd, 'b) ty = <fun> +val v : variant = + VConv ("Triple", VPair (VString "A", VPair (VInt 2, VInt 3))) +# val ty_abc : ([ `A of int | `B of string | `C ], 'a) ty = + Sum + {sum_proj = <fun>; + sum_cases = + [("A", TCarg (Thd, Int)); ("B", TCarg (Ttl Thd, String)); + ("C", TCnoarg (Ttl (Ttl Thd)))]; + 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 v : variant = + VSum ("Cons", + Some + (VPair (VInt 1, VSum ("Cons", Some (VPair (VInt 2, VSum ("Nil", None))))))) +# type ('a, 'b) ty = + Int : (int, 'c) ty + | String : (string, 'd) ty + | List : ('a, 'e) ty -> ('a list, 'e) ty + | Option : ('a, 'e) ty -> ('a option, 'e) ty + | Pair : (('a, 'e) ty * ('b, 'e) ty) -> ('a * 'b, 'e) ty + | Var : ('a, 'a -> 'e) ty + | Rec : ('a, 'a -> 'e) ty -> ('a, 'e) ty + | Pop : ('a, 'e) ty -> ('a, 'b -> 'e) ty + | Conv : string * ('a -> 'b) * ('b -> 'a) * ('b, 'e) ty -> ('a, 'e) ty + | Sum : ('a -> string * 'e ty_dyn option) * + (string * 'e ty_dyn option -> 'a) -> ('a, 'e) ty +and 'e ty_dyn = Tdyn : ('a, 'e) ty * 'a -> 'e ty_dyn +val ty_abc : ([ `A of int | `B of string | `C ], 'e) ty = Sum (<fun>, <fun>) +# Characters 327-344: + | "Cons", Some (Tdyn (Pair (_, Var), (p : a * a vlist))) -> `Cons p))) + ^^^^^^^^^^^^^^^^^ +Error: This pattern matches values of type a * a vlist + but a pattern was expected which matches values of type + ex#42 = ex#43 * ex#44 +# type ('a, 'b) ty = + Int : (int, 'd) ty + | String : (string, 'f) ty + | List : ('a, 'e) ty -> ('a list, 'e) ty + | Option : ('a, 'e) ty -> ('a option, 'e) ty + | Pair : (('a, 'e) ty * ('b, 'e) ty) -> ('a * 'b, 'e) ty + | Var : ('a, 'a -> 'e) ty + | Rec : ('a, 'a -> 'e) ty -> ('a, 'e) ty + | Pop : ('a, 'e) ty -> ('a, 'b -> 'e) ty + | Conv : string * ('a -> 'b) * ('b -> 'a) * ('b, 'e) ty -> ('a, 'e) ty + | Sum : + < cases : (string * ('e, 'b) ty_case) list; + inj : 'c. ('b, 'c) ty_sel * 'c -> 'a; + proj : 'a -> string * 'e ty_dyn option > -> ('a, 'e) ty +and 'e ty_dyn = Tdyn : ('a, 'e) ty * 'a -> 'e ty_dyn +and ('a, 'b) ty_sel = + Thd : ('a -> 'b, 'a) ty_sel + | Ttl : ('b -> 'c, 'd) ty_sel -> ('a -> 'b -> 'c, 'd) ty_sel +and ('a, 'b) ty_case = + TCarg : ('b, 'a) ty_sel * ('a, 'e) ty -> ('e, '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> +# * * * * * * * * * diff --git a/testsuite/tests/typing-gadts/omega07.ml b/testsuite/tests/typing-gadts/omega07.ml index 22f67d99a..cddfe460b 100644 --- a/testsuite/tests/typing-gadts/omega07.ml +++ b/testsuite/tests/typing-gadts/omega07.ml @@ -138,6 +138,8 @@ let rec summandLessThanSum : type a b c. (a,b,c) plus -> (a,c) le = fun p -> type (_,_) equal = Eq : ('a,'a) equal +let convert : type a b. (a,b) equal -> a -> b = fun Eq x -> x + let rec sameNat : type a b. a nat -> b nat -> (a,b) equal option = fun a b -> match a, b with | NZ, NZ -> Some Eq diff --git a/testsuite/tests/typing-gadts/omega07.ml.principal.reference b/testsuite/tests/typing-gadts/omega07.ml.principal.reference index d8cd31f2c..60ef06cb3 100644 --- a/testsuite/tests/typing-gadts/omega07.ml.principal.reference +++ b/testsuite/tests/typing-gadts/omega07.ml.principal.reference @@ -51,7 +51,8 @@ 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 : ('a, 'a) equal +# type ('a, 'b) equal = Eq : ('a, 'a) equal +val convert : ('a, 'b) equal -> 'a -> 'b = <fun> 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 : 'c nat * ('a, 'c, 'b) plus -> ('a, 'b) diff diff --git a/testsuite/tests/typing-gadts/omega07.ml.reference b/testsuite/tests/typing-gadts/omega07.ml.reference index d8cd31f2c..60ef06cb3 100644 --- a/testsuite/tests/typing-gadts/omega07.ml.reference +++ b/testsuite/tests/typing-gadts/omega07.ml.reference @@ -51,7 +51,8 @@ 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 : ('a, 'a) equal +# type ('a, 'b) equal = Eq : ('a, 'a) equal +val convert : ('a, 'b) equal -> 'a -> 'b = <fun> 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 : 'c nat * ('a, 'c, 'b) plus -> ('a, 'b) diff diff --git a/testsuite/tests/typing-gadts/term-conv.ml b/testsuite/tests/typing-gadts/term-conv.ml new file mode 100644 index 000000000..9b53cd6ea --- /dev/null +++ b/testsuite/tests/typing-gadts/term-conv.ml @@ -0,0 +1,139 @@ +(* HOAS to de Bruijn, by chak *) +(* http://www.cse.unsw.edu.au/~chak/haskell/term-conv/ *) + +module Typeable = struct + type 'a ty = + | Int: int ty + | String: string ty + | List: 'a ty -> 'a list ty + | Pair: ('a ty * 'b ty) -> ('a * 'b) ty + | Fun: ('a ty * 'b ty) -> ('a -> 'b) ty + + type (_,_) eq = Eq : ('a,'a) eq + + exception CastFailure + let rec check_eq : type t t'. t ty -> t' ty -> (t,t') eq = fun t t' -> + match t, t' with + | Int, Int -> Eq + | String, String -> Eq + | List t, List t' -> (match check_eq t t' with Eq -> Eq) + | Pair (t1,t2), Pair (t1',t2') -> + (match check_eq t1 t1', check_eq t2 t2' with Eq, Eq -> Eq) + | Fun (t1,t2), Fun (t1',t2') -> + (match check_eq t1 t1', check_eq t2 t2' with Eq, Eq -> Eq) + | _ -> raise CastFailure + + let gcast : type t t'. t ty -> t' ty -> t -> t' = fun t t' x -> + match check_eq t t' with Eq -> x +end;; + +module HOAS = struct + open Typeable + + type _ term = + | Tag : 't ty * int -> 't term + | Con : 't -> 't term + | Lam : 's ty * ('s term -> 't term) -> ('s -> 't) term + | App : ('s -> 't) term * 's term -> 't term + + let rec intp : type t. t term -> t = function + | Tag (_, ix) -> failwith "HOAS.intp" + | Con v -> v + | Lam (_, f) -> fun x -> intp (f (Con x)) + | App (f, a) -> intp f (intp a) +end;; + +module DeBruijn = struct + type ('env,'t) ix = + | ZeroIx : ('env * 't, 't) ix + | SuccIx : ('env,'t) ix -> ('env * 's, 't) ix + + let rec to_int : type env t. (env,t) ix -> int = function + | ZeroIx -> 0 + | SuccIx n -> to_int n + 1 + + type ('env,'t) term = + | Var : ('env,'t) ix -> ('env,'t) term + | Con : 't -> ('env,'t) term + | Lam : ('env * 's, 't) term -> ('env, 's -> 't) term + | App : ('env, 's -> 't) term * ('env, 's) term -> ('env, 't) term + + type _ stack = + | Empty : unit stack + | Push : 'env stack * 't -> ('env * 't) stack + + let rec prj : type env t. (env,t) ix -> env stack -> t = fun i s -> + match i, s with + | ZeroIx, Push (s,v) -> v + | SuccIx i, Push (s,_) -> prj i s + + let rec intp : type env t. (env,t) term -> env stack -> t = fun t s -> + match t with + | Var ix -> prj ix s + | Con v -> v + | Lam b -> fun x -> intp b (Push (s, x)) + | App(f,a) -> intp f s (intp a s) +end;; + +module Convert = struct + type (_,_) layout = + | EmptyLayout : ('env, unit) layout + | PushLayout : + 't Typeable.ty * ('env,'env') layout * ('env,'t) DeBruijn.ix + -> ('env,'env' * 't) layout + + let rec size : type env env'. (env,env') layout -> int = function + | EmptyLayout -> 0 + | PushLayout (_, lyt, _) -> size lyt + 1 + + let rec inc : type env env'. (env,env') layout -> (env * 't, env') layout = + function + | EmptyLayout -> EmptyLayout + | PushLayout (t, lyt, ix) -> PushLayout (t, inc lyt, DeBruijn.SuccIx ix) + + let rec prj : type env env' t. + t Typeable.ty -> int -> (env,env') layout -> (env,t) DeBruijn.ix + = fun t n -> function + | EmptyLayout -> failwith "Convert.prj: internal error" + | PushLayout (t', l, ix) -> + if n = 0 then + match Typeable.check_eq t t' with Typeable.Eq -> ix + else prj t (n-1) l + + let rec cvt : + type env t. (env,env) layout -> t HOAS.term -> (env,t) DeBruijn.term = + fun lyt -> function + | HOAS.Tag (t, sz) -> DeBruijn.Var (prj t (size lyt - sz -1) lyt) + | HOAS.Con v -> DeBruijn.Con v + | HOAS.Lam (t, f) -> + let lyt' = PushLayout (t, inc lyt, DeBruijn.ZeroIx) in + DeBruijn.Lam (cvt lyt' (f (HOAS.Tag (t, size lyt)))) + | HOAS.App (f, a) -> + DeBruijn.App (cvt lyt f, cvt lyt a) + + let convert t = cvt EmptyLayout t +end;; + +module Main = struct + open HOAS + let i t = Lam (t, fun x -> x) + let zero t = Lam (Typeable.Fun(t,t), fun f -> Lam(t, fun x -> x)) + let one t = Lam (Typeable.Fun(t,t), fun f -> Lam(t, fun x -> App (f, x))) + let two t = + Lam (Typeable.Fun(t,t), fun f -> Lam(t, fun x -> App (f, App (f, x)))) + let three t = + Lam (Typeable.Fun(t,t), + fun f -> Lam(t, fun x -> App (f, App (f, App (f, x))))) + let plus t = + let t1 = Typeable.Fun(t,t) in let t2 = Typeable.Fun(t1,t1) in + Lam (t2, fun m -> Lam (t2, fun n -> + Lam (t1, fun f -> Lam(t, fun x -> App(App(m,f), App(App(n,f),x)))))) + + let plus_2_3 t = App (App (plus t, two t), three t) + + open Convert + + let i' = convert (i Typeable.Int) + let plus_2_3' = convert (plus_2_3 Typeable.Int) + let eval_plus_2_3' = DeBruijn.intp plus_2_3' DeBruijn.Empty succ 0 +end;; diff --git a/testsuite/tests/typing-gadts/term-conv.ml.principal.reference b/testsuite/tests/typing-gadts/term-conv.ml.principal.reference new file mode 100644 index 000000000..3c6b335f6 --- /dev/null +++ b/testsuite/tests/typing-gadts/term-conv.ml.principal.reference @@ -0,0 +1,71 @@ + +# module Typeable : + sig + type 'a ty = + Int : int ty + | String : string ty + | List : 'a ty -> 'a list ty + | Pair : ('a ty * 'b ty) -> ('a * 'b) ty + | 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 + end +# module HOAS : + sig + type 'a term = + Tag : 't Typeable.ty * int -> 't term + | 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 + 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 + type ('env, 't) term = + Var : ('env, 't) ix -> ('env, 't) term + | Con : 't -> ('env, 't) term + | Lam : ('env * 's, 't) term -> ('env, 's -> 't) term + | App : ('env, 's -> 't) term * ('env, 's) term -> ('env, 't) term + 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 + end +# module Convert : + sig + type ('a, 'b) layout = + 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 prj : + 'a Typeable.ty -> int -> ('b, 'c) layout -> ('b, 'a) DeBruijn.ix + val cvt : ('a, 'a) layout -> 'b HOAS.term -> ('a, 'b) DeBruijn.term + val convert : 'a HOAS.term -> (unit, 'a) DeBruijn.term + end +# module Main : + sig + val i : 'a Typeable.ty -> ('a -> 'a) HOAS.term + val zero : 'a Typeable.ty -> (('a -> 'a) -> 'a -> 'a) HOAS.term + val one : 'a Typeable.ty -> (('a -> 'a) -> 'a -> 'a) HOAS.term + val two : 'a Typeable.ty -> (('a -> 'a) -> 'a -> 'a) HOAS.term + val three : 'a Typeable.ty -> (('a -> 'a) -> 'a -> 'a) HOAS.term + val plus : + 'a Typeable.ty -> + ((('a -> 'a) -> 'a -> 'a) -> + (('a -> 'a) -> 'a -> 'a) -> ('a -> 'a) -> 'a -> 'a) + HOAS.term + val plus_2_3 : 'a Typeable.ty -> (('a -> 'a) -> 'a -> 'a) HOAS.term + val i' : (unit, int -> int) DeBruijn.term + val plus_2_3' : (unit, (int -> int) -> int -> int) DeBruijn.term + val eval_plus_2_3' : int + end +# diff --git a/testsuite/tests/typing-gadts/term-conv.ml.reference b/testsuite/tests/typing-gadts/term-conv.ml.reference new file mode 100644 index 000000000..3c6b335f6 --- /dev/null +++ b/testsuite/tests/typing-gadts/term-conv.ml.reference @@ -0,0 +1,71 @@ + +# module Typeable : + sig + type 'a ty = + Int : int ty + | String : string ty + | List : 'a ty -> 'a list ty + | Pair : ('a ty * 'b ty) -> ('a * 'b) ty + | 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 + end +# module HOAS : + sig + type 'a term = + Tag : 't Typeable.ty * int -> 't term + | 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 + 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 + type ('env, 't) term = + Var : ('env, 't) ix -> ('env, 't) term + | Con : 't -> ('env, 't) term + | Lam : ('env * 's, 't) term -> ('env, 's -> 't) term + | App : ('env, 's -> 't) term * ('env, 's) term -> ('env, 't) term + 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 + end +# module Convert : + sig + type ('a, 'b) layout = + 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 prj : + 'a Typeable.ty -> int -> ('b, 'c) layout -> ('b, 'a) DeBruijn.ix + val cvt : ('a, 'a) layout -> 'b HOAS.term -> ('a, 'b) DeBruijn.term + val convert : 'a HOAS.term -> (unit, 'a) DeBruijn.term + end +# module Main : + sig + val i : 'a Typeable.ty -> ('a -> 'a) HOAS.term + val zero : 'a Typeable.ty -> (('a -> 'a) -> 'a -> 'a) HOAS.term + val one : 'a Typeable.ty -> (('a -> 'a) -> 'a -> 'a) HOAS.term + val two : 'a Typeable.ty -> (('a -> 'a) -> 'a -> 'a) HOAS.term + val three : 'a Typeable.ty -> (('a -> 'a) -> 'a -> 'a) HOAS.term + val plus : + 'a Typeable.ty -> + ((('a -> 'a) -> 'a -> 'a) -> + (('a -> 'a) -> 'a -> 'a) -> ('a -> 'a) -> 'a -> 'a) + HOAS.term + val plus_2_3 : 'a Typeable.ty -> (('a -> 'a) -> 'a -> 'a) HOAS.term + val i' : (unit, int -> int) DeBruijn.term + val plus_2_3' : (unit, (int -> int) -> int -> int) DeBruijn.term + val eval_plus_2_3' : int + end +# diff --git a/testsuite/tests/typing-gadts/test.ml b/testsuite/tests/typing-gadts/test.ml index 46e0590c3..1ae0c9748 100644 --- a/testsuite/tests/typing-gadts/test.ml +++ b/testsuite/tests/typing-gadts/test.ml @@ -19,6 +19,12 @@ module Exp = (eval f) (eval a) | Abs f -> f + let discern : type a. a t -> _ = function + IntLit _ -> 1 + | BoolLit _ -> 2 + | Pair _ -> 3 + | App _ -> 4 + | Abs _ -> 5 end ;; @@ -159,17 +165,37 @@ type _ t = Int : int t ;; let ky x y = ignore (x = y); x ;; +let test : type a. a t -> a = + function Int -> ky (1 : a) 1 +;; + +let test : type a. a t -> _ = + function Int -> 1 (* ok *) +;; + +let test : type a. a t -> _ = + function Int -> ky (1 : a) 1 (* fails *) +;; + let test : type a. a t -> a = fun x -> - let r = match x with Int -> ky (1 : a) 1 + let r = match x with Int -> ky (1 : a) 1 (* fails *) in r ;; let test : type a. a t -> a = fun x -> - let r = match x with Int -> ky 1 (1 : a) + let r = match x with Int -> ky 1 (1 : a) (* fails *) + in r +;; +let test (type a) x = + let r = match (x : a t) with Int -> ky 1 1 in r ;; let test : type a. a t -> a = fun x -> - let r = match x with Int -> (1 : a) - in r (* fails too *) + let r = match x with Int -> (1 : a) (* ok! *) + in r +;; +let test : type a. a t -> _ = fun x -> + let r = match x with Int -> 1 (* ok! *) + in r ;; let test : type a. a t -> a = fun x -> let r : a = match x with Int -> 1 @@ -178,7 +204,7 @@ let test : type a. a t -> a = fun x -> let test2 : type a. a t -> a option = fun x -> let r = ref None in begin match x with Int -> r := Some (1 : a) end; - !r (* normalized to int option *) + !r (* ok *) ;; let test2 : type a. a t -> a option = fun x -> let r : a option ref = ref None in @@ -190,19 +216,19 @@ let test2 : type a. a t -> a option = fun x -> let u = ref None in begin match x with Int -> r := Some 1; u := !r end; !u -;; (* fail *) +;; (* ok (u non-ambiguous) *) let test2 : type a. a t -> a option = fun x -> let r : a option ref = ref None in let u = ref None in begin match x with Int -> u := Some 1; r := !u end; !u -;; (* fail *) +;; (* fails because u : (int | a) option ref *) let test2 : type a. a t -> a option = fun x -> let u = ref None in let r : a option ref = ref None in begin match x with Int -> r := Some 1; u := !r end; !u -;; (* fail *) +;; (* ok *) let test2 : type a. a t -> a option = fun x -> let u = ref None in let a = @@ -210,34 +236,136 @@ let test2 : type a. a t -> a option = fun x -> begin match x with Int -> r := Some 1; u := !r end; !u in a +;; (* ok *) +let either = ky +let we_y1x (type a) (x : a) (v : a t) = + match v with Int -> let y = either 1 x in y ;; (* fail *) (* Effect of external consraints *) - let f (type a) (x : a t) y = ignore (y : a); - let r = match x with Int -> (y : a) in (* fails *) + let r = match x with Int -> (y : a) in (* ok *) r ;; let f (type a) (x : a t) y = let r = match x with Int -> (y : a) in - ignore (y : a); (* fails *) + ignore (y : a); (* ok *) r ;; let f (type a) (x : a t) y = ignore (y : a); - let r = match x with Int -> y in + let r = match x with Int -> y in (* ok *) r ;; let f (type a) (x : a t) y = let r = match x with Int -> y in - ignore (y : a); + ignore (y : a); (* ok *) r ;; let f (type a) (x : a t) (y : a) = - match x with Int -> y (* should return an int! *) + match x with Int -> y (* returns 'a *) ;; +(* Combination with local modules *) + +let f (type a) (x : a t) y = + match x with Int -> + let module M = struct type b = a let z = (y : b) end + in M.z +;; (* fails because of aliasing... *) + +let f (type a) (x : a t) y = + match x with Int -> + let module M = struct type b = int let z = (y : b) end + in M.z +;; (* ok *) + +(* Objects and variants *) + +type _ h = + | Has_m : <m : int> h + | Has_b : <b : bool> h + +let f : type a. a h -> a = function + | Has_m -> object method m = 1 end + | Has_b -> object method b = true end +;; +type _ j = + | Has_A : [`A of int] j + | Has_B : [`B of bool] j + +let f : type a. a j -> a = function + | Has_A -> `A 1 + | Has_B -> `B true +;; + +type (_,_) eq = Eq : ('a,'a) eq ;; + +let f : type a b. (a,b) eq -> (<m : a; ..> as 'a) -> (<m : b; ..> as 'a) = + fun Eq o -> o +;; (* fail *) + +let f : type a b. (a,b) eq -> <m : a; ..> -> <m : b; ..> = + fun Eq o -> o +;; (* fail *) + +let f (type a) (type b) (eq : (a,b) eq) (o : <m : a; ..>) : <m : b; ..> = + match eq with Eq -> o ;; (* should fail *) + +let f : type a b. (a,b) eq -> <m : a> -> <m : b> = + fun Eq o -> o +;; (* ok *) + +let int_of_bool : (bool,int) eq = Obj.magic Eq;; + +let x = object method m = true end;; +let y = (x, f int_of_bool x);; + +let f : type a. (a, int) eq -> <m : a> -> bool = + fun Eq o -> ignore (o : <m : int; ..>); o#m = 3 +;; (* should be ok *) + +let f : type a b. (a,b) eq -> < m : a; .. > -> < m : b > = + fun eq o -> + ignore (o : < m : a >); + let r : < m : b > = match eq with Eq -> o in (* fail with principal *) + r;; + +let f : type a b. (a,b) eq -> < m : a; .. > -> < m : b > = + fun eq o -> + let r : < m : b > = match eq with Eq -> o in (* fail *) + ignore (o : < m : a >); + r;; + +let f : type a b. (a,b) eq -> [> `A of a] -> [> `A of b] = + fun Eq o -> o ;; (* fail *) + +let f (type a) (type b) (eq : (a,b) eq) (v : [> `A of a]) : [> `A of b] = + match eq with Eq -> v ;; (* should fail *) + +let f : type a b. (a,b) eq -> [< `A of a | `B] -> [< `A of b | `B] = + fun Eq o -> o ;; (* fail *) + +let f : type a b. (a,b) eq -> [`A of a | `B] -> [`A of b | `B] = + fun Eq o -> o ;; (* ok *) + +let f : type a. (a, int) eq -> [`A of a] -> bool = + fun Eq v -> match v with `A 1 -> true | _ -> false +;; (* ok *) + +let f : type a b. (a,b) eq -> [> `A of a | `B] -> [`A of b | `B] = + fun eq o -> + ignore (o : [< `A of a | `B]); + let r : [`A of b | `B] = match eq with Eq -> o in (* fail with principal *) + r;; + +let f : type a b. (a,b) eq -> [> `A of a | `B] -> [`A of b | `B] = + fun eq o -> + let r : [`A of b | `B] = match eq with Eq -> o in (* fail *) + ignore (o : [< `A of a | `B]); + r;; + (* Pattern matching *) type 'a t = @@ -307,4 +435,4 @@ let f : type a. a ty -> a t -> int = fun x y -> | {left=TE TC; right=D [|1.0|]} -> 14 | {left=TA; right=D 0} -> -1 | {left=TA; right=D z} -> z -;; (* warn *) +;; (* ok *) diff --git a/testsuite/tests/typing-gadts/test.ml.principal.reference b/testsuite/tests/typing-gadts/test.ml.principal.reference index 88065d443..b770efb90 100644 --- a/testsuite/tests/typing-gadts/test.ml.principal.reference +++ b/testsuite/tests/typing-gadts/test.ml.principal.reference @@ -1,5 +1,5 @@ -# module Exp : +# module Exp : sig type 'a t = IntLit : int -> int t @@ -8,6 +8,7 @@ | App : ('a -> 'b) t * 'a t -> 'b t | Abs : ('a -> 'b) -> ('a -> 'b) t val eval : 'a t -> 'a + val discern : 'a t -> int end # module List : sig @@ -49,9 +50,9 @@ module Nonexhaustive : # Characters 119-120: let eval (D x) = x ^ -Error: This expression has type &x7 t but an expression was expected of type - &x7 t - The type constructor &x7 would escape its scope +Error: This expression has type ex#12 t + but an expression was expected of type ex#12 t + The type constructor ex#12 would escape its scope # Characters 157-158: C -> ^ @@ -69,8 +70,7 @@ Error: This pattern matches values of type ([? `A ] as 'a) * bool t # Characters 300-301: | BoolLit b -> b ^ -Error: This expression has type bool but an expression was expected of type - int +Error: This expression has type bool but an expression was expected of type s # Characters 87-88: let f = function A -> 1 | B -> 2 ^ @@ -78,56 +78,153 @@ Error: This pattern matches values of type b but a pattern was expected which matches values of type a # type 'a t = Int : int t # val ky : 'a -> 'a -> 'a = <fun> -# Characters 88-89: - in r - ^ -Error: This expression has type int but an expression was expected of type a -# Characters 87-88: - in r - ^ -Error: This expression has type int but an expression was expected of type a -# Characters 82-83: - in r (* fails too *) - ^ -Error: This expression has type int but an expression was expected of type a # val test : 'a t -> 'a = <fun> -# Characters 122-124: - !r (* normalized to int option *) - ^^ -Error: This expression has type int option - but an expression was expected of type a option +# val test : 'a t -> int = <fun> +# Characters 49-61: + function Int -> ky (1 : a) 1 (* fails *) + ^^^^^^^^^^^^ +Error: This expression has type a = int + but an expression was expected of type a = int + This instance of int is ambiguous: + it would escape the scope of its equation +# Characters 70-82: + let r = match x with Int -> ky (1 : a) 1 (* fails *) + ^^^^^^^^^^^^ +Error: This expression has type a = int + but an expression was expected of type a = int + This instance of int is ambiguous: + it would escape the scope of its equation +# Characters 69-81: + let r = match x with Int -> ky 1 (1 : a) (* fails *) + ^^^^^^^^^^^^ +Error: This expression has type a = int + but an expression was expected of type a = int + This instance of int is ambiguous: + it would escape the scope of its equation +# val test : 'a t -> int = <fun> +# val test : 'a t -> 'a = <fun> +# val test : 'a t -> int = <fun> +# val test : 'a t -> 'a = <fun> # val test2 : 'a t -> 'a option = <fun> -# Characters 162-164: - !u - ^^ -Error: This expression has type int option - but an expression was expected of type a option -# Characters 162-164: - !u - ^^ -Error: This expression has type int option - but an expression was expected of type a option -# Characters 162-164: - !u - ^^ -Error: This expression has type int option - but an expression was expected of type a option -# Characters 186-187: - in a - ^ +# val test2 : 'a t -> 'a option = <fun> +# val test2 : 'a t -> 'a option = <fun> +# Characters 152-154: + begin match x with Int -> u := Some 1; r := !u end; + ^^ Error: This expression has type int option but an expression was expected of type a option -# Characters 116-117: - let r = match x with Int -> (y : a) in (* fails *) - ^ -Error: This expression has type a but an expression was expected of type int -# Characters 80-81: - ignore (y : a); (* fails *) - ^ -Error: This expression has type int but an expression was expected of type a + Type int is not compatible with type a = int + This instance of int is ambiguous: + it would escape the scope of its equation +# val test2 : 'a t -> 'a option = <fun> +# val test2 : 'a t -> 'a option = <fun> +# Characters 100-101: + match v with Int -> let y = either 1 x in y + ^ +Error: This expression has type a = int + but an expression was expected of type a = int + This instance of int is ambiguous: + it would escape the scope of its equation +# val f : 'a t -> 'a -> 'a = <fun> +# val f : 'a t -> 'a -> 'a = <fun> # val f : 'a t -> 'a -> 'a = <fun> # val f : 'a t -> 'a -> 'a = <fun> -# val f : 'a t -> 'a -> int = <fun> +# val f : 'a t -> 'a -> 'a = <fun> +# Characters 136-137: + let module M = struct type b = a let z = (y : b) end + ^ +Error: This expression has type a = int + but an expression was expected of type b = int + This instance of int is ambiguous: + it would escape the scope of its equation +# val f : 'a t -> int -> int = <fun> +# type 'a h = Has_m : < m : int > h | Has_b : < b : bool > h +val f : 'a h -> 'a = <fun> +# type 'a j = Has_A : [ `A of int ] j | Has_B : [ `B of bool ] j +val f : 'a j -> 'a = <fun> +# type ('a, 'b) eq = Eq : ('a, 'a) eq +# Characters 5-91: + ....f : type a b. (a,b) eq -> (<m : a; ..> as 'a) -> (<m : b; ..> as 'a) = + fun Eq o -> o +Error: The universal type variable 'b cannot be generalized: + it is already bound to another variable. +# Characters 74-75: + fun Eq o -> o + ^ +Error: This expression has type < m : a; .. > + but an expression was expected of type < m : b; .. > + Type a is not compatible with type b = a + This instance of a is ambiguous: + it would escape the scope of its equation +# Characters 97-98: + match eq with Eq -> o ;; (* should fail *) + ^ +Error: This expression has type < m : a; .. > + but an expression was expected of type < m : b; .. > + Type a is not compatible with type b = a + This instance of a is ambiguous: + it would escape the scope of its equation +# val f : ('a, 'b) eq -> < m : 'a > -> < m : 'b > = <fun> +# val int_of_bool : (bool, int) eq = Eq +# val x : < m : bool > = <obj> +# val y : < m : bool > * < m : int > = (<obj>, <obj>) +# val f : ('a, int) eq -> < m : 'a > -> bool = <fun> +# Characters 146-147: + let r : < m : b > = match eq with Eq -> o in (* fail with principal *) + ^ +Error: This expression has type < m : a > + but an expression was expected of type < m : b > + Type a is not compatible with type b = a + This instance of a is ambiguous: + it would escape the scope of its equation +# Characters 118-119: + let r : < m : b > = match eq with Eq -> o in (* fail *) + ^ +Error: This expression has type < m : a; .. > + but an expression was expected of type < m : b > + Type a is not compatible with type b = a + This instance of a is ambiguous: + it would escape the scope of its equation +# Characters 74-75: + fun Eq o -> o ;; (* fail *) + ^ +Error: This expression has type [> `A of a ] + but an expression was expected of type [> `A of b ] + Type a is not compatible with type b = a + This instance of a is ambiguous: + it would escape the scope of its equation +# Characters 97-98: + match eq with Eq -> v ;; (* should fail *) + ^ +Error: This expression has type [> `A of a ] + but an expression was expected of type [> `A of b ] + Type a is not compatible with type b = a + This instance of a is ambiguous: + it would escape the scope of its equation +# Characters 5-85: + ....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 +# 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: + let r : [`A of b | `B] = match eq with Eq -> o in (* fail with principal *) + ^ +Error: This expression has type [ `A of a | `B ] + but an expression was expected of type [ `A of b | `B ] + Type a is not compatible with type b = a + This instance of a is ambiguous: + it would escape the scope of its equation +# Characters 131-132: + let r : [`A of b | `B] = match eq with Eq -> o in (* fail *) + ^ +Error: This expression has type [> `A of a | `B ] + but an expression was expected of type [ `A of b | `B ] + Type a is not compatible with type b = a + This instance of a is ambiguous: + it would escape the scope of its equation # type 'a t = A of int | B of bool | C of float | D of 'a type 'a ty = TE : 'a ty -> 'a array ty @@ -168,7 +265,7 @@ Error: This pattern matches values of type 'a array | {left=TA; right=D z} -> z Warning 8: this pattern-matching is not exhaustive. Here is an example of a value that is not matched: -{left=TE TA; right=D [| _ |]} +{left=TE TC; right=D [| |]} type ('a, 'b) pair = { left : 'a; right : 'b; } val f : 'a ty -> 'a t -> int = <fun> # diff --git a/testsuite/tests/typing-gadts/test.ml.reference b/testsuite/tests/typing-gadts/test.ml.reference index 3a4633e03..bb44dce52 100644 --- a/testsuite/tests/typing-gadts/test.ml.reference +++ b/testsuite/tests/typing-gadts/test.ml.reference @@ -1,5 +1,5 @@ -# module Exp : +# module Exp : sig type 'a t = IntLit : int -> int t @@ -8,6 +8,7 @@ | App : ('a -> 'b) t * 'a t -> 'b t | Abs : ('a -> 'b) -> ('a -> 'b) t val eval : 'a t -> 'a + val discern : 'a t -> int end # module List : sig @@ -49,9 +50,9 @@ module Nonexhaustive : # Characters 119-120: let eval (D x) = x ^ -Error: This expression has type &x7 t but an expression was expected of type - &x7 t - The type constructor &x7 would escape its scope +Error: This expression has type ex#12 t + but an expression was expected of type ex#12 t + The type constructor ex#12 would escape its scope # Characters 157-158: C -> ^ @@ -66,11 +67,11 @@ Error: This pattern matches values of type int t ^^^^^^^^^^^^^ Error: This pattern matches values of type ([? `A ] as 'a) * bool t but a pattern was expected which matches values of type 'a * int t -# Characters 300-301: - | BoolLit b -> b - ^ -Error: This expression has type bool but an expression was expected of type - int +# module Propagation : + sig + type 'a t = IntLit : int -> int t | BoolLit : bool -> bool t + val check : 'a t -> 'a + end # Characters 87-88: let f = function A -> 1 | B -> 2 ^ @@ -78,45 +79,139 @@ Error: This pattern matches values of type b but a pattern was expected which matches values of type a # type 'a t = Int : int t # val ky : 'a -> 'a -> 'a = <fun> -# Characters 88-89: - in r - ^ -Error: This expression has type int but an expression was expected of type a -# Characters 87-88: - in r - ^ -Error: This expression has type int but an expression was expected of type a -# Characters 82-83: - in r (* fails too *) - ^ -Error: This expression has type int but an expression was expected of type a # val test : 'a t -> 'a = <fun> -# Characters 122-124: - !r (* normalized to int option *) - ^^ -Error: This expression has type int option - but an expression was expected of type a option +# val test : 'a t -> int = <fun> +# Characters 49-61: + function Int -> ky (1 : a) 1 (* fails *) + ^^^^^^^^^^^^ +Error: This expression has type a = int + but an expression was expected of type a = int + This instance of int is ambiguous: + it would escape the scope of its equation +# Characters 70-82: + let r = match x with Int -> ky (1 : a) 1 (* fails *) + ^^^^^^^^^^^^ +Error: This expression has type a = int + but an expression was expected of type a = int + This instance of int is ambiguous: + it would escape the scope of its equation +# Characters 69-81: + let r = match x with Int -> ky 1 (1 : a) (* fails *) + ^^^^^^^^^^^^ +Error: This expression has type a = int + but an expression was expected of type a = int + This instance of int is ambiguous: + it would escape the scope of its equation +# val test : 'a t -> int = <fun> +# val test : 'a t -> 'a = <fun> +# val test : 'a t -> int = <fun> +# val test : 'a t -> 'a = <fun> +# val test2 : 'a t -> 'a option = <fun> # val test2 : 'a t -> 'a option = <fun> # val test2 : 'a t -> 'a option = <fun> -# Characters 162-164: - !u - ^^ +# Characters 152-154: + begin match x with Int -> u := Some 1; r := !u end; + ^^ Error: This expression has type int option but an expression was expected of type a option + Type int is not compatible with type a = int + This instance of int is ambiguous: + it would escape the scope of its equation # val test2 : 'a t -> 'a option = <fun> -# Characters 186-187: - in a - ^ -Error: This expression has type int option - but an expression was expected of type a option -# val f : 'a t -> 'a -> int = <fun> -# Characters 80-81: - ignore (y : a); (* fails *) - ^ -Error: This expression has type int but an expression was expected of type a +# val test2 : 'a t -> 'a option = <fun> +# Characters 100-101: + match v with Int -> let y = either 1 x in y + ^ +Error: This expression has type a = int + but an expression was expected of type a = int + This instance of int is ambiguous: + it would escape the scope of its equation +# val f : 'a t -> 'a -> 'a = <fun> +# val f : 'a t -> 'a -> 'a = <fun> # val f : 'a t -> 'a -> 'a = <fun> # val f : 'a t -> 'a -> 'a = <fun> # val f : 'a t -> 'a -> 'a = <fun> +# Characters 136-137: + let module M = struct type b = a let z = (y : b) end + ^ +Error: This expression has type a = int + but an expression was expected of type b = int + This instance of int is ambiguous: + it would escape the scope of its equation +# val f : 'a t -> int -> int = <fun> +# type 'a h = Has_m : < m : int > h | Has_b : < b : bool > h +val f : 'a h -> 'a = <fun> +# type 'a j = Has_A : [ `A of int ] j | Has_B : [ `B of bool ] j +val f : 'a j -> 'a = <fun> +# type ('a, 'b) eq = Eq : ('a, 'a) eq +# Characters 5-91: + ....f : type a b. (a,b) eq -> (<m : a; ..> as 'a) -> (<m : b; ..> as 'a) = + fun Eq o -> o +Error: The universal type variable 'b cannot be generalized: + it is already bound to another variable. +# Characters 74-75: + fun Eq o -> o + ^ +Error: This expression has type < m : a; .. > + but an expression was expected of type < m : b; .. > + Type a is not compatible with type b = a + This instance of a is ambiguous: + it would escape the scope of its equation +# Characters 97-98: + match eq with Eq -> o ;; (* should fail *) + ^ +Error: This expression has type < m : a; .. > + but an expression was expected of type < m : b; .. > + Type a is not compatible with type b = a + This instance of a is ambiguous: + it would escape the scope of its equation +# val f : ('a, 'b) eq -> < m : 'a > -> < m : 'b > = <fun> +# val int_of_bool : (bool, int) eq = Eq +# val x : < m : bool > = <obj> +# val y : < m : bool > * < m : int > = (<obj>, <obj>) +# val f : ('a, int) eq -> < m : 'a > -> bool = <fun> +# val f : ('a, 'b) eq -> < m : 'a > -> < m : 'b > = <fun> +# Characters 118-119: + let r : < m : b > = match eq with Eq -> o in (* fail *) + ^ +Error: This expression has type < m : a; .. > + but an expression was expected of type < m : b > + Type a is not compatible with type b = a + This instance of a is ambiguous: + it would escape the scope of its equation +# Characters 74-75: + fun Eq o -> o ;; (* fail *) + ^ +Error: This expression has type [> `A of a ] + but an expression was expected of type [> `A of b ] + Type a is not compatible with type b = a + This instance of a is ambiguous: + it would escape the scope of its equation +# Characters 97-98: + match eq with Eq -> v ;; (* should fail *) + ^ +Error: This expression has type [> `A of a ] + but an expression was expected of type [> `A of b ] + Type a is not compatible with type b = a + This instance of a is ambiguous: + it would escape the scope of its equation +# Characters 5-85: + ....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 +# 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> +# Characters 131-132: + let r : [`A of b | `B] = match eq with Eq -> o in (* fail *) + ^ +Error: This expression has type [> `A of a | `B ] + but an expression was expected of type [ `A of b | `B ] + Type a is not compatible with type b = a + This instance of a is ambiguous: + it would escape the scope of its equation # type 'a t = A of int | B of bool | C of float | D of 'a type 'a ty = TE : 'a ty -> 'a array ty @@ -157,7 +252,7 @@ Error: This pattern matches values of type 'a array | {left=TA; right=D z} -> z Warning 8: this pattern-matching is not exhaustive. Here is an example of a value that is not matched: -{left=TE (TE _); right=D [| _ |]} +{left=TE TC; right=D [| |]} type ('a, 'b) pair = { left : 'a; right : 'b; } val f : 'a ty -> 'a t -> int = <fun> # diff --git a/testsuite/tests/typing-gadts/yallop_bugs.ml b/testsuite/tests/typing-gadts/yallop_bugs.ml new file mode 100644 index 000000000..08708a67c --- /dev/null +++ b/testsuite/tests/typing-gadts/yallop_bugs.ml @@ -0,0 +1,45 @@ +(* Injectivity *) + +type (_, _) eq = Refl : ('a, 'a) eq + +let magic : 'a 'b. 'a -> 'b = + fun (type a) (type b) (x : a) -> + let module M = + (functor (T : sig type 'a t end) -> + struct + let f (Refl : (a T.t, b T.t) eq) = (x :> b) + end) + (struct type 'a t = unit end) + in M.f Refl +;; + +(* Variance and subtyping *) + +type (_, +_) eq = Refl : ('a, 'a) eq + +let magic : 'a 'b. 'a -> 'b = + fun (type a) (type b) (x : a) -> + let bad_proof (type a) = + (Refl : (< m : a>, <m : a>) eq :> (<m : a>, < >) eq) in + let downcast : type a. (a, < >) eq -> < > -> a = + fun (type a) (Refl : (a, < >) eq) (s : < >) -> (s :> a) in + (downcast bad_proof ((object method m = x end) :> < >)) # m +;; + +(* Record patterns *) + +type _ t = + | IntLit : int t + | BoolLit : bool t + +let check : type s . s t * s -> bool = function + | BoolLit, false -> false + | IntLit , 6 -> false +;; + +type ('a, 'b) pair = { fst : 'a; snd : 'b } + +let check : type s . (s t, s) pair -> bool = function + | {fst = BoolLit; snd = false} -> false + | {fst = IntLit ; snd = 6} -> false +;; diff --git a/testsuite/tests/typing-gadts/yallop_bugs.ml.principal.reference b/testsuite/tests/typing-gadts/yallop_bugs.ml.principal.reference new file mode 100644 index 000000000..527649649 --- /dev/null +++ b/testsuite/tests/typing-gadts/yallop_bugs.ml.principal.reference @@ -0,0 +1,31 @@ + +# Characters 212-216: + let f (Refl : (a T.t, b T.t) eq) = (x :> b) + ^^^^ +Error: This pattern matches values of type (a T.t, a T.t) eq + but a pattern was expected which matches values of type + (a T.t, b T.t) eq +# Characters 36-67: + type (_, +_) eq = Refl : ('a, 'a) eq + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Error: In this GADT definition, the variance of some parameter + cannot be checked +# Characters 115-175: + .......................................function + | BoolLit, false -> false + | IntLit , 6 -> false +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> +# Characters 91-180: + .............................................function + | {fst = BoolLit; snd = false} -> false + | {fst = IntLit ; snd = 6} -> false +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> +# diff --git a/testsuite/tests/typing-gadts/yallop_bugs.ml.reference b/testsuite/tests/typing-gadts/yallop_bugs.ml.reference new file mode 100644 index 000000000..527649649 --- /dev/null +++ b/testsuite/tests/typing-gadts/yallop_bugs.ml.reference @@ -0,0 +1,31 @@ + +# Characters 212-216: + let f (Refl : (a T.t, b T.t) eq) = (x :> b) + ^^^^ +Error: This pattern matches values of type (a T.t, a T.t) eq + but a pattern was expected which matches values of type + (a T.t, b T.t) eq +# Characters 36-67: + type (_, +_) eq = Refl : ('a, 'a) eq + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Error: In this GADT definition, the variance of some parameter + cannot be checked +# Characters 115-175: + .......................................function + | BoolLit, false -> false + | IntLit , 6 -> false +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> +# Characters 91-180: + .............................................function + | {fst = BoolLit; snd = false} -> false + | {fst = IntLit ; snd = 6} -> false +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> +# diff --git a/testsuite/tests/typing-modules/Test.ml b/testsuite/tests/typing-modules/Test.ml index 82ea468f9..77c9d0970 100644 --- a/testsuite/tests/typing-modules/Test.ml +++ b/testsuite/tests/typing-modules/Test.ml @@ -3,3 +3,9 @@ module type S' = S with type t := int;; module type S = sig module rec M : sig end and N : sig end end;; module type S' = S with module M := String;; + +(* A subtle problem appearing with -principal *) +type -'a t +class type c = object method m : [ `A ] t end;; +module M : sig val v : (#c as 'a) -> 'a end = + struct let v x = ignore (x :> c); x end;; diff --git a/testsuite/tests/typing-modules/Test.ml.principal.reference b/testsuite/tests/typing-modules/Test.ml.principal.reference new file mode 100644 index 000000000..258b3ee3d --- /dev/null +++ b/testsuite/tests/typing-modules/Test.ml.principal.reference @@ -0,0 +1,9 @@ + +# module type S = sig type t and s = t end +# module type S' = sig type s = int end +# module type S = sig module rec M : sig end and N : sig end end +# module type S' = sig module rec N : sig end end +# type -'a t +class type c = object method m : [ `A ] t end +# module M : sig val v : (#c as 'a) -> 'a end +# diff --git a/testsuite/tests/typing-modules/Test.ml.reference b/testsuite/tests/typing-modules/Test.ml.reference index 823cc1a84..258b3ee3d 100644 --- a/testsuite/tests/typing-modules/Test.ml.reference +++ b/testsuite/tests/typing-modules/Test.ml.reference @@ -3,4 +3,7 @@ # module type S' = sig type s = int end # module type S = sig module rec M : sig end and N : sig end end # module type S' = sig module rec N : sig end end +# type -'a t +class type c = object method m : [ `A ] t end +# module M : sig val v : (#c as 'a) -> 'a end # diff --git a/testsuite/tests/typing-objects/Tests.ml.reference b/testsuite/tests/typing-objects/Tests.ml.reference index 7dde3fba0..a78367fdf 100644 --- a/testsuite/tests/typing-objects/Tests.ml.reference +++ b/testsuite/tests/typing-objects/Tests.ml.reference @@ -268,11 +268,13 @@ Error: Type int -> bool is not a subtype of int -> int fun (x : 'a t as 'a) -> ();; ^^^^^^^^^^ Error: This alias is bound to type 'a t but is used as an instance of type 'a + The type variable 'a occurs inside 'a t # Characters 19-20: fun (x : 'a t) -> (x : 'a); ();; ^ Error: This expression has type 'a t but an expression was expected of type 'a + The type variable 'a occurs inside 'a t # type 'a t = < x : 'a > # - : ('a t as 'a) -> unit = <fun> # Characters 18-26: diff --git a/testsuite/tests/typing-poly/poly.ml b/testsuite/tests/typing-poly/poly.ml index eb3b6f84a..17e643ad1 100644 --- a/testsuite/tests/typing-poly/poly.ml +++ b/testsuite/tests/typing-poly/poly.ml @@ -571,12 +571,17 @@ type u = c option;; let just = function None -> failwith "just" | Some x -> x;; let f x = let l = [Some x; (None : u)] in (just(List.hd l))#id;; let g x = - let none = match None with y -> ignore [y;(None:u)]; y in + let none = (fun y -> ignore [y;(None:u)]; y) None in let x = List.hd [Some x; none] in (just x)#id;; let h x = let none = let y = None in ignore [y;(None:u)]; y in let x = List.hd [Some x; none] in (just x)#id;; +(* Only solved for parameterless abbreviations *) +type 'a u = c option;; +let just = function None -> failwith "just" | Some x -> x;; +let f x = let l = [Some x; (None : _ u)] in (just(List.hd l))#id;; + (* polymorphic recursion *) let rec f : 'a. 'a -> _ = fun x -> 1 and g x = f x;; diff --git a/testsuite/tests/typing-poly/poly.ml.principal.reference b/testsuite/tests/typing-poly/poly.ml.principal.reference index a87694bb7..65043c786 100644 --- a/testsuite/tests/typing-poly/poly.ml.principal.reference +++ b/testsuite/tests/typing-poly/poly.ml.principal.reference @@ -265,8 +265,8 @@ Error: This field value has type 'b option ref option # Characters 145-166: object method virtual visit : 'a.('a visitor -> 'a) end;; ^^^^^^^^^^^^^^^^^^^^^ -Error: This type scheme cannot quantify 'a : -it escapes this scope. +Error: The universal type variable 'a cannot be generalized: + it escapes its scope. # type ('a, 'b) list_visitor = < caseCons : 'b -> 'b list -> 'a; caseNil : 'a > type 'b alist = < visit : 'a. ('a, 'b) list_visitor -> 'a > class type ct = object ('a) method fold : ('b -> 'a -> 'b) -> 'b -> 'b end @@ -555,13 +555,20 @@ Warning 18: this use of a polymorphic method is not principal. # class c : object method id : 'a -> 'a end # type u = c option # val just : 'a option -> 'a = <fun> -# val f : c -> 'a -> 'a = <fun> -# Characters 106-117: +# Characters 42-62: + let f x = let l = [Some x; (None : u)] in (just(List.hd l))#id;; + ^^^^^^^^^^^^^^^^^^^^ +Warning 18: this use of a polymorphic method is not principal. +val f : c -> 'a -> 'a = <fun> +# Characters 101-112: let x = List.hd [Some x; none] in (just x)#id;; ^^^^^^^^^^^ Warning 18: this use of a polymorphic method is not principal. val g : c -> 'a -> 'a = <fun> # val h : < id : 'a; .. > -> 'a = <fun> +# type 'a u = c option +# val just : 'a option -> 'a = <fun> +# val f : c -> 'a -> 'a = <fun> # val f : 'a -> int = <fun> val g : 'a -> int = <fun> # type 'a t = Leaf of 'a | Node of ('a * 'a) t diff --git a/testsuite/tests/typing-poly/poly.ml.reference b/testsuite/tests/typing-poly/poly.ml.reference index 1e11ed099..37601416b 100644 --- a/testsuite/tests/typing-poly/poly.ml.reference +++ b/testsuite/tests/typing-poly/poly.ml.reference @@ -248,8 +248,8 @@ Error: This field value has type 'b option ref option # Characters 145-166: object method virtual visit : 'a.('a visitor -> 'a) end;; ^^^^^^^^^^^^^^^^^^^^^ -Error: This type scheme cannot quantify 'a : -it escapes this scope. +Error: The universal type variable 'a cannot be generalized: + it escapes its scope. # type ('a, 'b) list_visitor = < caseCons : 'b -> 'b list -> 'a; caseNil : 'a > type 'b alist = < visit : 'a. ('a, 'b) list_visitor -> 'a > class type ct = object ('a) method fold : ('b -> 'a -> 'b) -> 'b -> 'b end @@ -529,6 +529,9 @@ Error: Type < m : 'a. [< `A of < > ] as 'a > is not a subtype of # val f : c -> 'a -> 'a = <fun> # val g : c -> 'a -> 'a = <fun> # val h : < id : 'a; .. > -> 'a = <fun> +# type 'a u = c option +# val just : 'a option -> 'a = <fun> +# val f : c -> 'a -> 'a = <fun> # val f : 'a -> int = <fun> val g : 'a -> int = <fun> # type 'a t = Leaf of 'a | Node of ('a * 'a) t |