path: root/testsuite/tests/typing-poly/poly.ml

(* TEST
   * expect
*)

(*
   Polymorphic methods are now available in the main branch.
   Enjoy.
*)

(* Tests for explicit polymorphism *)
open StdLabels;;

type 'a t = { t : 'a };;
type 'a fold = { fold : 'b. f:('b -> 'a -> 'b) -> init:'b -> 'b };;
let f l = { fold = List.fold_left l };;
(f [1;2;3]).fold ~f:(+) ~init:0;;
[%%expect {|
type 'a t = { t : 'a; }
type 'a fold = { fold : 'b. f:('b -> 'a -> 'b) -> init:'b -> 'b; }
val f : 'a list -> 'a fold = <fun>
- : int = 6
|}];;

type pty = {pv : 'a. 'a list};;
[%%expect {|
type pty = { pv : 'a. 'a list; }
|}];;


type id = { id : 'a. 'a -> 'a };;
let id x = x;;
let {id} = id { id };;
[%%expect {|
type id = { id : 'a. 'a -> 'a; }
val id : 'a -> 'a = <fun>
val id : 'a -> 'a = <fun>
|}];;

let px = {pv = []};;
[%%expect {|
val px : pty = {pv = []}
|}];;

match px with
| {pv=[]} -> "OK"
| {pv=5::_} -> "int"
| {pv=true::_} -> "bool"
;;
[%%expect {|
Lines 1-4, characters 0-24:
1 | match px with
2 | | {pv=[]} -> "OK"
3 | | {pv=5::_} -> "int"
4 | | {pv=true::_} -> "bool"
Warning 8 [partial-match]: this pattern-matching is not exhaustive.
Here is an example of a case that is not matched:
{pv=false::_}

- : string = "OK"
|}];;

match px with
| {pv=[]} -> "OK"
| {pv=true::_} -> "bool"
| {pv=5::_} -> "int"
;;
[%%expect {|
Lines 1-4, characters 0-20:
1 | match px with
2 | | {pv=[]} -> "OK"
3 | | {pv=true::_} -> "bool"
4 | | {pv=5::_} -> "int"
Warning 8 [partial-match]: this pattern-matching is not exhaustive.
Here is an example of a case that is not matched:
{pv=0::_}

- : string = "OK"
|}];;

match px with
| {pv=[]} -> "OK"
| {pv=5::_} -> "int"
| {pv=true::_} -> "bool"
| {pv=false::_} -> "bool"
;;
[%%expect {|
- : string = "OK"
|}];;

fun {pv=v} -> true::v, 1::v;;
[%%expect {|
- : pty -> bool list * int list = <fun>
|}];;

class ['b] ilist l = object
  val l = l
  method add x = {< l = x :: l >}
  method fold : 'a. f:('a -> 'b -> 'a) -> init:'a -> 'a =
    List.fold_left l
end
;;
[%%expect {|
class ['b] ilist :
  'b list ->
  object ('c)
    val l : 'b list
    method add : 'b -> 'c
    method fold : f:('a -> 'b -> 'a) -> init:'a -> 'a
  end
|}];;

class virtual ['a] vlist = object (_ : 'self)
  method virtual add : 'a -> 'self
  method virtual fold : 'b. f:('b -> 'a -> 'b) -> init:'b -> 'b
end
;;
[%%expect {|
class virtual ['a] vlist :
  object ('c)
    method virtual add : 'a -> 'c
    method virtual fold : f:('b -> 'a -> 'b) -> init:'b -> 'b
  end
|}];;

class ilist2 l = object
  inherit [int] vlist
  val l = l
  method add x = {< l = x :: l >}
  method fold = List.fold_left l
end
;;
[%%expect {|
class ilist2 :
  int list ->
  object ('a)
    val l : int list
    method add : int -> 'a
    method fold : f:('b -> int -> 'b) -> init:'b -> 'b
  end
|}];;

let ilist2 l = object
  inherit [_] vlist
  val l = l
  method add x = {< l = x :: l >}
  method fold = List.fold_left l
end
;;
[%%expect {|
val ilist2 : 'a list -> 'a vlist = <fun>
|}];;

class ['a] ilist3 l = object
  inherit ['a] vlist
  val l = l
  method add x = {< l = x :: l >}
  method fold = List.fold_left l
end
;;
[%%expect {|
class ['a] ilist3 :
  'a list ->
  object ('c)
    val l : 'a list
    method add : 'a -> 'c
    method fold : f:('b -> 'a -> 'b) -> init:'b -> 'b
  end
|}];;

class ['a] ilist4 (l : 'a list) = object
  val l = l
  method virtual add : _
  method add x = {< l = x :: l >}
  method virtual fold : 'b. f:('b -> 'a -> 'b) -> init:'b -> 'b
  method fold = List.fold_left l
end
;;
[%%expect {|
class ['a] ilist4 :
  'a list ->
  object ('c)
    val l : 'a list
    method add : 'a -> 'c
    method fold : f:('b -> 'a -> 'b) -> init:'b -> 'b
  end
|}];;

class ['a] ilist5 (l : 'a list) = object (self)
  val l = l
  method add x = {< l = x :: l >}
  method virtual fold : 'b. f:('b -> 'a -> 'b) -> init:'b -> 'b
  method virtual fold2 : 'b. f:('b -> 'a -> 'b) -> init:'b -> 'b
  method fold2 ~f ~init = self#fold ~f ~init:(self#fold ~f ~init)
  method fold = List.fold_left l
end
;;
[%%expect {|
class ['a] ilist5 :
  'a list ->
  object ('c)
    val l : 'a list
    method add : 'a -> 'c
    method fold : f:('b -> 'a -> 'b) -> init:'b -> 'b
    method fold2 : f:('b -> 'a -> 'b) -> init:'b -> 'b
  end
|}];;

class ['a] ilist6 l = object (self)
  inherit ['a] vlist
  val l = l
  method add x = {< l = x :: l >}
  method virtual fold2 : 'b. f:('b -> 'a -> 'b) -> init:'b -> 'b
  method fold2 ~f ~init = self#fold ~f ~init:(self#fold ~f ~init)
  method fold = List.fold_left l
end
;;
[%%expect {|
class ['a] ilist6 :
  'a list ->
  object ('c)
    val l : 'a list
    method add : 'a -> 'c
    method fold : f:('b -> 'a -> 'b) -> init:'b -> 'b
    method fold2 : f:('b -> 'a -> 'b) -> init:'b -> 'b
  end
|}];;

class virtual ['a] olist = object
  method virtual fold : 'c. f:('a -> 'c -> 'c) -> init:'c -> 'c
end
;;
[%%expect {|
class virtual ['a] olist :
  object method virtual fold : f:('a -> 'c -> 'c) -> init:'c -> 'c end
|}];;

class ['a] onil = object
  inherit ['a] olist
  method fold ~f ~init = init
end
;;
[%%expect {|
class ['a] onil :
  object method fold : f:('a -> 'c -> 'c) -> init:'c -> 'c end
|}];;

class ['a] ocons ~hd ~tl = object (_ : 'b)
  inherit ['a] olist
  val hd : 'a = hd
  val tl : 'a olist = tl
  method fold ~f ~init = f hd (tl#fold ~f ~init)
end
;;
[%%expect {|
class ['a] ocons :
  hd:'a ->
  tl:'a olist ->
  object
    val hd : 'a
    val tl : 'a olist
    method fold : f:('a -> 'c -> 'c) -> init:'c -> 'c
  end
|}];;

class ['a] ostream ~hd ~tl = object (_ : 'b)
  inherit ['a] olist
  val hd : 'a = hd
  val tl : _ #olist = (tl : 'a ostream)
  method fold ~f ~init = f hd (tl#fold ~f ~init)
  method empty = false
end
;;
[%%expect {|
class ['a] ostream :
  hd:'a ->
  tl:'a ostream ->
  object
    val hd : 'a
    val tl : < empty : bool; fold : 'c. f:('a -> 'c -> 'c) -> init:'c -> 'c >
    method empty : bool
    method fold : f:('a -> 'c -> 'c) -> init:'c -> 'c
  end
|}];;

class ['a] ostream1 ~hd ~tl = object (self : 'b)
  inherit ['a] olist
  val hd = hd
  val tl : 'b = tl
  method hd = hd
  method tl = tl
  method fold ~f ~init =
    self#tl#fold ~f ~init:(f self#hd init)
end
[%%expect {|
class ['a] ostream1 :
  hd:'a ->
  tl:'b ->
  object ('b)
    val hd : 'a
    val tl : 'b
    method fold : f:('a -> 'c -> 'c) -> init:'c -> 'c
    method hd : 'a
    method tl : 'b
  end
|}, Principal{|
Line 8, characters 4-16:
8 |     self#tl#fold ~f ~init:(f self#hd init)
        ^^^^^^^^^^^^
Warning 18 [not-principal]: this use of a polymorphic method is not principal.

class ['a] ostream1 :
  hd:'a ->
  tl:'b ->
  object ('b)
    val hd : 'a
    val tl : 'b
    method fold : f:('a -> 'c -> 'c) -> init:'c -> 'c
    method hd : 'a
    method tl : 'b
  end
|}];;

class vari = object
  method virtual m : 'a. ([< `A|`B|`C] as 'a) -> int
  method m = function `A -> 1 | `B|`C  -> 0
end
;;
[%%expect {|
class vari : object method m : [< `A | `B | `C ] -> int end
|}];;

class vari = object
  method m : 'a. ([< `A|`B|`C] as 'a) -> int = function `A -> 1 | `B|`C -> 0
end
;;
[%%expect {|
class vari : object method m : [< `A | `B | `C ] -> int end
|}];;

module V =
  struct
    type v = [`A | `B | `C]
    let m : [< v] -> int = function `A -> 1 | #v -> 0
  end
;;
[%%expect {|
module V : sig type v = [ `A | `B | `C ] val m : [< v ] -> int end
|}];;

class varj = object
  method virtual m : 'a. ([< V.v] as 'a) -> int
  method m = V.m
end
;;
[%%expect {|
class varj : object method m : [< V.v ] -> int end
|}];;


module type T = sig
  class vari : object method m : 'a. ([< `A | `B | `C] as 'a) -> int end
end
;;
[%%expect {|
module type T =
  sig class vari : object method m : [< `A | `B | `C ] -> int end end
|}];;

module M0 = struct
  class vari = object
    method virtual m : 'a. ([< `A|`B|`C] as 'a) -> int
    method m = function `A -> 1 | `B|`C -> 0
  end
end
;;
[%%expect {|
module M0 :
  sig class vari : object method m : [< `A | `B | `C ] -> int end end
|}];;

module M : T = M0
;;
[%%expect {|
module M : T
|}];;

let v = new M.vari;;
[%%expect {|
val v : M.vari = <obj>
|}];;

v#m `A;;
[%%expect {|
- : int = 1
|}];;


class point ~x ~y = object
  val x : int = x
  val y : int = y
  method x = x
  method y = y
end
;;
[%%expect {|
class point :
  x:int ->
  y:int -> object val x : int val y : int method x : int method y : int end
|}];;

class color_point ~x ~y ~color = object
  inherit point ~x ~y
  val color : string = color
  method color = color
end
;;
[%%expect {|
class color_point :
  x:int ->
  y:int ->
  color:string ->
  object
    val color : string
    val x : int
    val y : int
    method color : string
    method x : int
    method y : int
  end
|}];;

class circle (p : #point) ~r = object
  val p = (p :> point)
  val r = r
  method virtual distance : 'a. (#point as 'a) -> float
  method distance p' =
    let dx = p#x - p'#x and dy = p#y - p'#y in
    let d = sqrt (float (dx * dx + dy * dy)) -. float r in
    if d < 0. then 0. else d
end
;;
[%%expect {|
class circle :
  #point ->
  r:int ->
  object val p : point val r : int method distance : #point -> float end
|}];;

let p0 = new point ~x:3 ~y:5
let p1 = new point ~x:10 ~y:13
let cp = new color_point ~x:12 ~y:(-5) ~color:"green"
let c = new circle p0 ~r:2
let d = floor (c#distance cp)
;;
let f (x : < m : 'a. 'a -> 'a >) = (x : < m : 'b. 'b -> 'b >)
;;
let f (x : < m : 'a. 'a -> 'a list >) = (x : < m : 'b. 'b -> 'c >)
;;
[%%expect {|
val p0 : point = <obj>
val p1 : point = <obj>
val cp : color_point = <obj>
val c : circle = <obj>
val d : float = 11.
val f : < m : 'a. 'a -> 'a > -> < m : 'b. 'b -> 'b > = <fun>
Line 9, characters 41-42:
9 | let f (x : < m : 'a. 'a -> 'a list >) = (x : < m : 'b. 'b -> 'c >)
                                             ^
Error: This expression has type < m : 'b. 'b -> 'b list >
       but an expression was expected of type < m : 'b. 'b -> 'c >
       The method m has type 'b. 'b -> 'b list,
       but the expected method type was 'b. 'b -> 'c
       The universal variable 'b would escape its scope
|}];;

class id = object
  method virtual id : 'a. 'a -> 'a
  method id x = x
end
;;
[%%expect {|
class id : object method id : 'a -> 'a end
|}];;

class type id_spec = object
  method id : 'a -> 'a
end
;;
[%%expect {|
class type id_spec = object method id : 'a -> 'a end
|}];;

class id_impl = object (_ : #id_spec)
  method id x = x
end
;;
[%%expect {|
class id_impl : object method id : 'a -> 'a end
|}];;

class a = object
  method m = (new b : id_spec)#id true
end
and b = object (_ : #id_spec)
  method id x = x
end
;;
[%%expect {|
class a : object method m : bool end
and b : object method id : 'a -> 'a end
|}];;


class ['a] id1 = object
  method virtual id : 'b. 'b -> 'a
  method id x = x
end
;;
[%%expect {|
Line 3, characters 12-17:
3 |   method id x = x
                ^^^^^
Error: This method has type 'a -> 'a which is less general than 'b. 'b -> 'a
|}];;

class id2 (x : 'a) = object
  method virtual id : 'b. 'b -> 'a
  method id x = x
end
;;
[%%expect {|
Line 3, characters 12-17:
3 |   method id x = x
                ^^^^^
Error: This method has type 'a -> 'a which is less general than 'b. 'b -> 'a
|}];;

class id3 x = object
  val x = x
  method virtual id : 'a. 'a -> 'a
  method id _ = x
end
;;
[%%expect {|
Line 4, characters 12-17:
4 |   method id _ = x
                ^^^^^
Error: This method has type 'b -> 'b which is less general than 'a. 'a -> 'a
|}];;

class id4 () = object
  val mutable r = None
  method virtual id : 'a. 'a -> 'a
  method id x =
    match r with
      None -> r <- Some x; x
    | Some y -> y
end
;;
[%%expect {|
Lines 4-7, characters 12-17:
4 | ............x =
5 |     match r with
6 |       None -> r <- Some x; x
7 |     | Some y -> y
Error: This method has type 'b -> 'b which is less general than 'a. 'a -> 'a
|}];;

class c = object
  method virtual m : 'a 'b. 'a -> 'b -> 'a
  method m x y = x
end
;;
[%%expect {|
class c : object method m : 'a -> 'b -> 'a end
|}];;


let f1 (f : id) = f#id 1, f#id true
;;
let f2 f = (f : id)#id 1, (f : id)#id true
;;
let f3 f = f#id 1, f#id true
;;
let f4 f = ignore(f : id); f#id 1, f#id true
;;
[%%expect {|
val f1 : id -> int * bool = <fun>
val f2 : id -> int * bool = <fun>
Line 5, characters 24-28:
5 | let f3 f = f#id 1, f#id true
                            ^^^^
Error: This expression has type bool but an expression was expected of type
         int
|}];;

class c = object
  method virtual m : 'a. (#id as 'a) -> int * bool
  method m (f : #id) = f#id 1, f#id true
end
;;
[%%expect {|
class c : object method m : #id -> int * bool end
|}];;


class id2 = object (_ : 'b)
  method virtual id : 'a. 'a -> 'a
  method id x = x
  method mono (x : int) = x
end
;;
let app = new c #m (new id2)
;;
type 'a foo = 'a foo list
;;
[%%expect {|
class id2 : object method id : 'a -> 'a method mono : int -> int end
val app : int * bool = (1, true)
Line 9, characters 0-25:
9 | type 'a foo = 'a foo list
    ^^^^^^^^^^^^^^^^^^^^^^^^^
Error: The type abbreviation foo is cyclic:
         'a foo = 'a foo list,
         'a foo list contains 'a foo
|}];;

class ['a] bar (x : 'a) = object end
;;
type 'a foo = 'a foo bar
;;
[%%expect {|
class ['a] bar : 'a -> object  end
type 'a foo = 'a foo bar
|}];;

fun x -> (x : < m : 'a. 'a * 'b > as 'b)#m;;
fun x -> (x : < m : 'a. 'b * 'a list> as 'b)#m;;
let f x = (x : < m : 'a. 'b * (< n : 'a; .. > as 'a) > as 'b)#m;;
fun (x : < p : 'a. < m : 'a ; n : 'b ; .. > as 'a > as 'b) -> x#p;;
fun (x : <m:'a. 'a * <p:'b. 'b * 'c * 'd> as 'c> as 'd) -> x#m;;
(* printer is wrong on the next (no official syntax) *)
fun (x : <m:'a.<p:'a;..> >) -> x#m;;
[%%expect {|
- : (< m : 'a. 'a * 'b > as 'b) -> 'c * 'b = <fun>
- : (< m : 'a. 'b * 'a list > as 'b) -> 'b * 'c list = <fun>
val f :
  (< m : 'b. 'a * (< n : 'b; .. > as 'b) > as 'a) ->
  'a * (< n : 'c; .. > as 'c) = <fun>
- : (< p : 'b. < m : 'b; n : 'a; .. > as 'b > as 'a) ->
    (< m : 'c; n : 'a; .. > as 'c)
= <fun>
- : (< m : 'a. 'a * < p : 'b. 'b * 'd * 'c > as 'd > as 'c) ->
    ('f * < p : 'b. 'b * 'e * 'c > as 'e)
= <fun>
- : < m : 'a. < p : 'a; .. > as 'b > -> 'b = <fun>
|}, Principal{|
- : (< m : 'a. 'a * 'b > as 'b) -> 'c * (< m : 'a. 'a * 'd > as 'd) = <fun>
- : (< m : 'a. 'b * 'a list > as 'b) ->
    (< m : 'a. 'c * 'a list > as 'c) * 'd list
= <fun>
val f :
  (< m : 'b. 'a * (< n : 'b; .. > as 'b) > as 'a) ->
  (< m : 'd. 'c * (< n : 'd; .. > as 'd) > as 'c) * (< n : 'e; .. > as 'e) =
  <fun>
- : (< p : 'b. < m : 'b; n : 'a; .. > as 'b > as 'a) ->
    (< m : 'c; n : < p : 'e. < m : 'e; n : 'd; .. > as 'e > as 'd; .. > as 'c)
= <fun>
- : (< m : 'a. 'a * < p : 'b. 'b * 'd * 'c > as 'd > as 'c) ->
    ('f *
     < p : 'b.
             'b * 'e *
             (< m : 'a. 'a * < p : 'b0. 'b0 * 'h * 'g > as 'h > as 'g) >
     as 'e)
= <fun>
- : < m : 'a. < p : 'a; .. > as 'b > -> 'b = <fun>
|}];;

type sum = T of < id: 'a. 'a -> 'a > ;;
fun (T x) -> x#id;;
[%%expect {|
type sum = T of < id : 'a. 'a -> 'a >
- : sum -> 'a -> 'a = <fun>
|}];;

type record = { r: < id: 'a. 'a -> 'a > } ;;
fun x -> x.r#id;;
fun {r=x} -> x#id;;
[%%expect {|
type record = { r : < id : 'a. 'a -> 'a >; }
- : record -> 'a -> 'a = <fun>
- : record -> 'a -> 'a = <fun>
|}];;

class myself = object (self)
  method self : 'a. 'a -> 'b = fun _ -> self
end;;
[%%expect {|
class myself : object ('b) method self : 'a -> 'b end
|}];;

class number = object (self : 'self)
  val num = 0
  method num = num
  method succ = {< num = num + 1 >}
  method prev =
    self#switch ~zero:(fun () -> failwith "zero") ~prev:(fun x -> x)
  method switch : 'a. zero:(unit -> 'a) -> prev:('self -> 'a) -> 'a =
    fun ~zero ~prev ->
      if num = 0 then zero () else prev {< num = num - 1 >}
end
;;
[%%expect {|
class number :
  object ('b)
    val num : int
    method num : int
    method prev : 'b
    method succ : 'b
    method switch : zero:(unit -> 'a) -> prev:('b -> 'a) -> 'a
  end
|}];;

let id x = x
;;
class c = object
  method id : 'a. 'a -> 'a = id
end
;;
class c' = object
  inherit c
  method id = id
end
;;
class d = object
  inherit c as c
  val mutable count = 0
  method id x = count <- count+1; x
  method count = count
  method old : 'a. 'a -> 'a = c#id
end
;;
class ['a] olist l = object
  val l = l
  method fold : 'b. f:('a -> 'b -> 'b) -> init:'b -> 'b
      = List.fold_right l
  method cons a = {< l = a :: l >}
end
;;
let sum (l : 'a #olist) = l#fold ~f:(fun x acc -> x+acc) ~init:0
;;
let count (l : 'a #olist) = l#fold ~f:(fun _ acc -> acc+1) ~init:0
;;
let append (l : 'a #olist) (l' : 'b #olist) =
  l#fold ~init:l' ~f:(fun x acc -> acc#cons x)
;;
[%%expect {|
val id : 'a -> 'a = <fun>
class c : object method id : 'a -> 'a end
class c' : object method id : 'a -> 'a end
class d :
  object
    val mutable count : int
    method count : int
    method id : 'a -> 'a
    method old : 'a -> 'a
  end
class ['a] olist :
  'a list ->
  object ('c)
    val l : 'a list
    method cons : 'a -> 'c
    method fold : f:('a -> 'b -> 'b) -> init:'b -> 'b
  end
val sum : int #olist -> int = <fun>
val count : 'a #olist -> int = <fun>
val append : 'a #olist -> ('a #olist as 'b) -> 'b = <fun>
|}];;

type 'a t = unit
;;
class o = object method x : 'a. ([> `A] as 'a) t -> unit = fun _ -> () end
;;
[%%expect {|
type 'a t = unit
class o : object method x : unit -> unit end
|}];;

class c = object method m = new d () end and d ?(x=0) () = object end;;
class d ?(x=0) () = object end and c = object method m = new d () end;;
[%%expect {|
class c : object method m : d end
and d : ?x:int -> unit -> object  end
class d : ?x:int -> unit -> object  end
and c : object method m : d end
|}];;

class type numeral = object method fold : ('a -> 'a) -> 'a -> 'a end
class zero = object (_ : #numeral) method fold f x = x end
class next (n : #numeral) =
  object (_ : #numeral) method fold f x = n#fold f (f x) end
;;
[%%expect {|
class type numeral = object method fold : ('a -> 'a) -> 'a -> 'a end
class zero : object method fold : ('a -> 'a) -> 'a -> 'a end
class next : #numeral -> object method fold : ('a -> 'a) -> 'a -> 'a end
|}];;

class type node_type =  object
  method as_variant : [> `Node of node_type]
end;;
class node : node_type = object (self)
  method as_variant : 'a. [> `Node of node_type] as 'a
                    = `Node (self :>  node_type)
end;;
class node = object (self : #node_type)
  method as_variant = `Node (self :> node_type)
end;;
[%%expect {|
class type node_type = object method as_variant : [> `Node of node_type ] end
class node : node_type
class node : object method as_variant : [> `Node of node_type ] end
|}];;

type bad = {bad : 'a. 'a option ref};;
let bad = {bad = ref None};;
type bad2 = {mutable bad2 : 'a. 'a option ref option};;
let bad2 = {bad2 = None};;
bad2.bad2 <- Some (ref None);;
[%%expect {|
type bad = { bad : 'a. 'a option ref; }
Line 2, characters 17-25:
2 | let bad = {bad = ref None};;
                     ^^^^^^^^
Error: This field value has type 'b option ref which is less general than
         'a. 'a option ref
|}];;

(* Type variable scope *)

let f (x: <m:'a.<p: 'a * 'b> as 'b>) (y : 'b) = ();;
let f (x: <m:'a. 'a * (<p:int*'b> as 'b)>) (y : 'b) = ();;
[%%expect {|
val f : < m : 'a. < p : 'a * 'c > as 'c > -> 'b -> unit = <fun>
val f : < m : 'a. 'a * (< p : int * 'b > as 'b) > -> 'b -> unit = <fun>
|}, Principal{|
val f : < m : 'a. < p : 'a * 'c > as 'c > -> 'b -> unit = <fun>
val f :
  < m : 'a. 'a * (< p : int * 'b > as 'b) > ->
  (< p : int * 'c > as 'c) -> unit = <fun>
|}];;

(* PR#3643 *)

type 'a t= [`A of 'a];;
class c = object (self)
  method m :  'a. ([> 'a t] as 'a) -> unit
    = fun x -> self#m x
end;;
class c = object (self)
  method m : 'a. ([> 'a t] as 'a) -> unit = function
    | `A x' -> self#m x'
    | _ -> failwith "c#m"
end;;
class c = object (self)
  method m :  'a. ([> 'a t] as 'a) -> 'a = fun x -> self#m x
end;;
[%%expect {|
type 'a t = [ `A of 'a ]
class c : object method m : ([> 'a t ] as 'a) -> unit end
class c : object method m : ([> 'a t ] as 'a) -> unit end
class c : object method m : ([> 'a t ] as 'a) -> 'a end
|}];;

(* use before instancing *)
class c = object method m : 'a. 'a option -> ([> `A] as 'a) = fun x -> `A end;;
[%%expect {|
class c : object method m : ([> `A ] as 'a) option -> 'a end
|}];;

(* various old bugs *)
class virtual ['a] visitor =
object method virtual caseNil : 'a end
and virtual int_list =
object method virtual visit : 'a.('a visitor -> 'a) end;;
[%%expect {|
Line 4, characters 30-51:
4 | object method virtual visit : 'a.('a visitor -> 'a) end;;
                                  ^^^^^^^^^^^^^^^^^^^^^
Error: The universal type variable 'a cannot be generalized:
       it escapes its scope.
|}];;

type ('a,'b) list_visitor = < caseNil : 'a; caseCons : 'b -> 'b list -> 'a >
type 'b alist = < visit : 'a. ('a,'b) list_visitor -> 'a >
[%%expect {|
type ('a, 'b) list_visitor = < caseCons : 'b -> 'b list -> 'a; caseNil : 'a >
type 'b alist = < visit : 'a. ('a, 'b) list_visitor -> 'a >
|}];;

(* PR#8074 *)
class type ct = object ('s)
  method fold : ('b -> 's -> 'b) -> 'b -> 'b
end
type t = {f : 'a 'b. ('b -> (#ct as 'a) -> 'b) -> 'b};;
[%%expect {|
class type ct = object ('a) method fold : ('b -> 'a -> 'b) -> 'b -> 'b end
type t = { f : 'a 'b. ('b -> (#ct as 'a) -> 'b) -> 'b; }
|}];;

(* PR#8124 *)
type t = u and u = t;;
[%%expect {|
Line 1, characters 0-10:
1 | type t = u and u = t;;
    ^^^^^^^^^^
Error: The type abbreviation t is cyclic:
         t = u,
         u = t
|}];;

(* PR#8188 *)
class ['t] a = object constraint 't = [> `A of 't a] end
type t = [ `A of t a ];;
[%%expect {|
class ['a] a : object constraint 'a = [> `A of 'a a ] end
type t = [ `A of t a ]
|}];;

(* Wrong in 3.06 *)
type ('a,'b) t constraint 'a = 'b and ('a,'b) u = ('a,'b) t;;
[%%expect {|
Line 1, characters 50-59:
1 | type ('a,'b) t constraint 'a = 'b and ('a,'b) u = ('a,'b) t;;
                                                      ^^^^^^^^^
Error: Constraints are not satisfied in this type.
       Type ('a, 'b) t should be an instance of ('c, 'c) t
|}];;

(* Full polymorphism if we do not expand *)
type 'a t = 'a and u = int t;;
[%%expect {|
type 'a t = 'a
and u = int t
|}];;

(* Loose polymorphism if we expand *)
type 'a t constraint 'a = int;;
type 'a u = 'a and 'a v = 'a u t;;
type 'a u = 'a and 'a v = 'a u t constraint 'a = int;;
[%%expect {|
type 'a t constraint 'a = int
Line 2, characters 26-32:
2 | type 'a u = 'a and 'a v = 'a u t;;
                              ^^^^^^
Error: Constraints are not satisfied in this type.
       Type 'a u t should be an instance of int t
|}];;

(* Behaviour is unstable *)
type g = int;;
type 'a t = unit constraint 'a = g;;
type 'a u = 'a and 'a v = 'a u t;;
type 'a u = 'a and 'a v = 'a u t constraint 'a = int;;
[%%expect {|
type g = int
type 'a t = unit constraint 'a = g
Line 3, characters 26-32:
3 | type 'a u = 'a and 'a v = 'a u t;;
                              ^^^^^^
Error: Constraints are not satisfied in this type.
       Type 'a u t should be an instance of g t
|}];;

(* Full unification trace reported for "Constraints are not satisfied in this type" *)
type ('a,'b) t constraint 'a = 'b
               constraint 'a = int
  and 'a u = (float,string) t;;
[%%expect {|
Line 3, characters 13-29:
3 |   and 'a u = (float,string) t;;
                 ^^^^^^^^^^^^^^^^
Error: Constraints are not satisfied in this type.
       Type (float, string) t should be an instance of (int, int) t
       Type float is not compatible with type int
|}]

(* Example of wrong expansion *)
type 'a u = < m : 'a v > and 'a v = 'a list u;;
[%%expect {|
Line 1, characters 0-24:
1 | type 'a u = < m : 'a v > and 'a v = 'a list u;;
    ^^^^^^^^^^^^^^^^^^^^^^^^
Error: This recursive type is not regular.
       The type constructor u is defined as
         type 'a u
       but it is used as
         'a list u
       after the following expansion(s):
         < m : 'a v > contains 'a v,
         'a v = 'a list u
       All uses need to match the definition for the recursive type to be regular.
|}];;

(* PR#8198: Ctype.matches *)
type 'a t = 'a
type 'a u = A of 'a t;;
[%%expect {|
type 'a t = 'a
type 'a u = A of 'a t
|}];;

(* Unification of cyclic terms *)
type 'a t = < a : 'a >;;
fun (x : 'a t as 'a) -> (x : 'b t);;
type u = 'a t as 'a;;
[%%expect {|
type 'a t = < a : 'a >
- : ('a t as 'a) -> 'a t = <fun>
type u = 'a t as 'a
|}, Principal{|
type 'a t = < a : 'a >
- : ('a t as 'a) -> ('b t as 'b) t = <fun>
type u = 'a t as 'a
|}];;


(* pass typetexp, but fails during Typedecl.check_recursion *)
type ('a1, 'b1) ty1 = 'a1 -> unit constraint 'a1 = [> `V1 of ('a1, 'b1) ty2 as 'b1]
and  ('a2, 'b2) ty2 = 'b2 -> unit constraint 'b2 = [> `V2 of ('a2, 'b2) ty1 as 'a2];;
[%%expect {|
Line 1, characters 0-83:
1 | type ('a1, 'b1) ty1 = 'a1 -> unit constraint 'a1 = [> `V1 of ('a1, 'b1) ty2 as 'b1]
    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: The definition of ty1 contains a cycle:
         ([> `V1 of 'a ] as 'b, 'a) ty2 as 'a contains 'a
|}];;

(* PR#8359: expanding may change original in Ctype.unify2 *)
(* Note: since 3.11, the abbreviations are not used when printing
   a type where they occur recursively inside. *)
class type ['a, 'b] a = object
  method b: ('a, 'b) #b as 'b
  method as_a: ('a, 'b) a
end and ['a, 'b] b = object
  method a: ('a, 'b) #a as 'a
  method as_b: ('a, 'b) b
end;;
[%%expect {|
class type ['a, 'b] a =
  object
    constraint 'a = < as_a : ('a, 'b) a as 'c; b : 'b; .. >
    constraint 'b = < a : 'a; as_b : ('a, 'b) b; .. >
    method as_a : 'c
    method b : 'b
  end
and ['a, 'b] b =
  object
    constraint 'a = < as_a : ('a, 'b) a; b : 'b; .. >
    constraint 'b = < a : 'a; as_b : ('a, 'b) b; .. >
    method a : 'a
    method as_b : ('a, 'b) b
  end
|}];;

class type ['b] ca = object ('s) inherit ['s, 'b] a end;;
class type ['a] cb = object ('s) inherit ['a, 's] b end;;
[%%expect {|
class type ['a] ca =
  object ('b)
    constraint 'a = < a : 'b; as_b : ('b, 'a) b; .. >
    method as_a : ('b, 'a) a
    method b : 'a
  end
class type ['a] cb =
  object ('b)
    constraint 'a = < as_a : ('a, 'b) a; b : 'b; .. >
    method a : 'a
    method as_b : ('a, 'b) b
  end
|}];;

type bt = 'b ca cb as 'b
;;
[%%expect {|
type bt = 'a ca cb as 'a
|}];;

(* final classes, etc... *)
class c = object method m = 1 end;;
let f () = object (self:c) method m = 1 end;;
let f () = object (self:c) method private n = 1 method m = self#n end;;
let f () = object method private n = 1 method m = {<>}#n end;;
let f () = object (self:c) method n = 1 method m = 2 end;;
let f () = object (_:'s) constraint 's = < n : int > method m = 1 end;;
class c = object (_ : 's)
  method x = 1
  method private m =
    object (self: 's) method x = 3 method private m = self end
end;;
let o = object (_ : 's)
  method x = 1
  method private m =
    object (self: 's) method x = 3 method private m = self end
end;;
[%%expect {|
class c : object method m : int end
val f : unit -> c = <fun>
val f : unit -> c = <fun>
Line 4, characters 11-60:
4 | let f () = object method private n = 1 method m = {<>}#n end;;
               ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Warning 15 [implicit-public-methods]: the following private methods were made public implicitly:
 n.

val f : unit -> < m : int; n : int > = <fun>
Line 5, characters 27-39:
5 | let f () = object (self:c) method n = 1 method m = 2 end;;
                               ^^^^^^^^^^^^
Error: This object is expected to have type : c
       This type does not have a method n.
|}];;


(* Unsound! *)
fun (x : <m : 'a. 'a * <m: 'b. 'a * 'foo> > as 'foo) ->
  (x : <m : 'a. 'a * (<m:'b. 'a * <m:'c. 'c * 'bar> > as 'bar) >);;
type 'a foo = <m: 'b. 'a * 'a foo>
type foo' =   <m: 'a. 'a * 'a foo>
type 'a bar = <m: 'b. 'a * <m: 'c. 'c * 'a bar> >
type bar' =   <m: 'a. 'a * 'a bar >
let f (x : foo') = (x : bar');;
[%%expect {|
Line 2, characters 3-4:
2 |   (x : <m : 'a. 'a * (<m:'b. 'a * <m:'c. 'c * 'bar> > as 'bar) >);;
       ^
Error: This expression has type < m : 'a. 'a * < m : 'a * 'b > > as 'b
       but an expression was expected of type
         < m : 'a. 'a * (< m : 'a * < m : 'c. 'c * 'd > > as 'd) >
       The method m has type
       'a. 'a * (< m : 'a * < m : 'c. 'c * 'd > > as 'd),
       but the expected method type was
       'c. 'c * < m : 'a * < m : 'c. 'e > > as 'e
       The universal variable 'a would escape its scope
|}];;

fun (x : <m : 'a. 'a * ('a * <m : 'a. 'a * 'foo> as 'foo)>) ->
  (x : <m : 'b. 'b * ('b * <m : 'c. 'c * ('c * 'bar)>)> as 'bar);;
fun (x : <m : 'a. 'a * ('a * <m : 'a. 'a * 'foo> as 'foo)>) ->
  (x : <m : 'b. 'b * ('b * <m : 'c. 'c * ('b * 'bar)>)> as 'bar);;
fun (x : <m : 'a. 'a * ('a * 'foo)> as 'foo) ->
  (x : <m : 'b. 'b * ('b * <m:'c. 'c * 'bar> as 'bar)>);;
let f x =
    (x : <m : 'a. 'a -> ('a * <m:'c. 'c -> 'bar> as 'bar)>
       :> <m : 'a. 'a -> ('a * 'foo)> as 'foo);;
[%%expect {|
Line 2, characters 3-4:
2 |   (x : <m : 'b. 'b * ('b * <m : 'c. 'c * ('c * 'bar)>)> as 'bar);;
       ^
Error: This expression has type
         < m : 'b. 'b * ('b * < m : 'c. 'c * 'a > as 'a) >
       but an expression was expected of type
         < m : 'b. 'b * ('b * < m : 'c. 'c * ('c * 'd) >) > as 'd
       Types for method m are incompatible
|}];;

module M
: sig val f : (<m : 'b. 'b * ('b * <m:'c. 'c * 'bar> as 'bar)>) -> unit end
= struct let f (x : <m : 'a. 'a * ('a * 'foo)> as 'foo) = () end;;
module M
: sig type t = <m : 'b. 'b * ('b * <m:'c. 'c * 'bar> as 'bar)> end
= struct type t = <m : 'a. 'a * ('a * 'foo)> as 'foo end;;
[%%expect {|
Line 3, characters 2-64:
3 | = struct let f (x : <m : 'a. 'a * ('a * 'foo)> as 'foo) = () end;;
      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: Signature mismatch:
       Modules do not match:
         sig val f : (< m : 'a. 'a * ('a * 'b) > as 'b) -> unit end
       is not included in
         sig
           val f : < m : 'b. 'b * ('b * < m : 'c. 'c * 'a > as 'a) > -> unit
         end
       Values do not match:
         val f : (< m : 'a. 'a * ('a * 'b) > as 'b) -> unit
       is not included in
         val f : < m : 'b. 'b * ('b * < m : 'c. 'c * 'a > as 'a) > -> unit
       The type (< m : 'a. 'a * ('a * 'd) > as 'd) -> unit
       is not compatible with the type
         < m : 'b. 'b * ('b * < m : 'c. 'c * 'e > as 'e) > -> unit
       The method m has type 'a. 'a * ('a * < m : 'a. 'f >) as 'f,
       but the expected method type was 'c. 'c * ('b * < m : 'c. 'g >) as 'g
       The universal variable 'b would escape its scope
|}];;

module M : sig type 'a t type u = <m: 'a. 'a t> end
= struct type 'a t = int type u = <m: int> end;;
module M : sig type 'a t val f : <m: 'a. 'a t> -> int end
= struct type 'a t = int let f (x : <m:int>) = x#m end;;
(* The following should be accepted too! *)
module M : sig type 'a t val f : <m: 'a. 'a t> -> int end
= struct type 'a t = int let f x = x#m end;;
[%%expect {|
module M : sig type 'a t type u = < m : 'a. 'a t > end
module M : sig type 'a t val f : < m : 'a. 'a t > -> int end
module M : sig type 'a t val f : < m : 'a. 'a t > -> int end
|}];;

let f x y =
  ignore (x :> <m:'a.'a -> 'c * < > > as 'c);
  ignore (y :> <m:'b.'b -> 'd * < > > as 'd);
  x = y;;
[%%expect {|
val f :
  (< m : 'a. 'a -> (< m : 'a. 'a -> 'c * <  > > as 'c) * < .. >; .. > as 'b) ->
  'b -> bool = <fun>
|}];;


(* Subtyping *)

type t = [`A|`B];;
type v = private [> t];;
fun x -> (x : t :> v);;
type u = private [< t];;
fun x -> (x : u :> v);;
fun x -> (x : v :> u);;
type v = private [< t];;
fun x -> (x : u :> v);;
type p = <x:p>;;
type q = private <x:p; ..>;;
fun x -> (x : q :> p);;
fun x -> (x : p :> q);;
[%%expect {|
type t = [ `A | `B ]
type v = private [> t ]
- : t -> v = <fun>
type u = private [< t ]
- : u -> v = <fun>
Line 6, characters 9-21:
6 | fun x -> (x : v :> u);;
             ^^^^^^^^^^^^
Error: Type v = [> `A | `B ] is not a subtype of u = [< `A | `B ]
|}];;

let f1 x =
  (x : <m:'a. (<p:int;..> as 'a) -> int>
    :> <m:'b. (<p:int;q:int;..> as 'b) -> int>);;
let f2 x =
  (x : <m:'a. (<p:<a:int>;..> as 'a) -> int>
    :> <m:'b. (<p:<a:int;b:int>;..> as 'b) -> int>);;
let f3 x =
  (x : <m:'a. (<p:<a:int;b:int>;..> as 'a) -> int>
    :> <m:'b. (<p:<a:int>;..> as 'b) -> int>);;
let f4 x = (x : <p:<a:int;b:int>;..> :> <p:<a:int>;..>);;
let f5 x =
  (x : <m:'a. [< `A of <p:int> ] as 'a> :> <m:'a. [< `A of < > ] as 'a>);;
let f6 x =
  (x : <m:'a. [< `A of < > ] as 'a> :> <m:'a. [< `A of <p:int> ] as 'a>);;
[%%expect {|
Lines 2-3, characters 2-47:
2 | ..(x : <m:'a. (<p:int;..> as 'a) -> int>
3 |     :> <m:'b. (<p:int;q:int;..> as 'b) -> int>)..
Error: Type < m : 'a. (< p : int; .. > as 'a) -> int > is not a subtype of
         < m : 'b. (< p : int; q : int; .. > as 'b) -> int >
       Type < p : int; q : int; .. > is not a subtype of < p : int; .. >
|}];;

(* Keep sharing the epsilons *)
let f x = if true then (x : < m : 'a. 'a -> 'a >) else x;;
fun x -> (f x)#m;; (* Warning 18 *)
let f (x, y) = if true then (x : < m : 'a. 'a -> 'a >) else x;;
fun x -> (f (x,x))#m;; (* Warning 18 *)
let f x = if true then [| (x : < m : 'a. 'a -> 'a >) |] else [|x|];;
fun x -> (f x).(0)#m;; (* Warning 18 *)
[%%expect {|
val f : < m : 'a. 'a -> 'a > -> < m : 'a. 'a -> 'a > = <fun>
- : < m : 'a. 'a -> 'a > -> 'b -> 'b = <fun>
val f : < m : 'a. 'a -> 'a > * 'b -> < m : 'a. 'a -> 'a > = <fun>
- : < m : 'a. 'a -> 'a > -> 'b -> 'b = <fun>
val f : < m : 'a. 'a -> 'a > -> < m : 'a. 'a -> 'a > array = <fun>
- : < m : 'a. 'a -> 'a > -> 'b -> 'b = <fun>
|}, Principal{|
val f : < m : 'a. 'a -> 'a > -> < m : 'a. 'a -> 'a > = <fun>
Line 2, characters 9-16:
2 | fun x -> (f x)#m;; (* Warning 18 *)
             ^^^^^^^
Warning 18 [not-principal]: this use of a polymorphic method is not principal.

- : < m : 'a. 'a -> 'a > -> 'b -> 'b = <fun>
val f : < m : 'a. 'a -> 'a > * 'b -> < m : 'a. 'a -> 'a > = <fun>
Line 4, characters 9-20:
4 | fun x -> (f (x,x))#m;; (* Warning 18 *)
             ^^^^^^^^^^^
Warning 18 [not-principal]: this use of a polymorphic method is not principal.

- : < m : 'a. 'a -> 'a > -> 'b -> 'b = <fun>
val f : < m : 'a. 'a -> 'a > -> < m : 'a. 'a -> 'a > array = <fun>
Line 6, characters 9-20:
6 | fun x -> (f x).(0)#m;; (* Warning 18 *)
             ^^^^^^^^^^^
Warning 18 [not-principal]: this use of a polymorphic method is not principal.

- : < m : 'a. 'a -> 'a > -> 'b -> 'b = <fun>
|}];;

(* Not really principal? *)
class c = object method id : 'a. 'a -> 'a = fun x -> x end;;
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 = (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;;
[%%expect {|
class c : object method id : 'a -> 'a end
type u = c option
val just : 'a option -> 'a = <fun>
val f : c -> 'a -> 'a = <fun>
val g : c -> 'a -> 'a = <fun>
val h : < id : 'a; .. > -> 'a = <fun>
|}, Principal{|
class c : object method id : 'a -> 'a end
type u = c option
val just : 'a option -> 'a = <fun>
Line 4, characters 42-62:
4 | let f x = let l = [Some x; (None : u)] in (just(List.hd l))#id;;
                                              ^^^^^^^^^^^^^^^^^^^^
Warning 18 [not-principal]: this use of a polymorphic method is not principal.

val f : c -> 'a -> 'a = <fun>
Line 7, characters 36-47:
7 |   let x = List.hd [Some x; none] in (just x)#id;;
                                        ^^^^^^^^^^^
Warning 18 [not-principal]: this use of a polymorphic method is not principal.

val g : c -> 'a -> 'a = <fun>
val h : < id : 'a; .. > -> 'a = <fun>
|}];;

(* 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;;
[%%expect {|
type 'a u = c option
val just : 'a option -> 'a = <fun>
val f : c -> 'a -> 'a = <fun>
|}];;

(* polymorphic recursion *)

let rec f : 'a. 'a -> _ = fun x -> 1 and g x = f x;;
type 'a t = Leaf of 'a | Node of ('a * 'a) t;;
let rec depth : 'a. 'a t -> _ =
  function Leaf _ -> 1 | Node x -> 1 + depth x;;
let rec depth : 'a. 'a t -> _ =
  function Leaf _ -> 1 | Node x -> 1 + d x
and d x = depth x;; (* fails *)
let rec depth : 'a. 'a t -> _ =
  function Leaf x -> x | Node x -> 1 + depth x;; (* fails *)
let rec depth : 'a. 'a t -> _ =
  function Leaf x -> x | Node x -> depth x;; (* fails *)
let rec depth : 'a 'b. 'a t -> 'b =
  function Leaf x -> x | Node x -> depth x;; (* fails *)
let rec r : 'a. 'a list * 'b list ref = [], ref []
and q () = r;;
let f : 'a. _ -> _ = fun x -> x;;
let zero : 'a. [> `Int of int | `B of 'a] as 'a  = `Int 0;; (* ok *)
let zero : 'a. [< `Int of int] as 'a = `Int 0;; (* fails *)
[%%expect {|
val f : 'a -> int = <fun>
val g : 'a -> int = <fun>
type 'a t = Leaf of 'a | Node of ('a * 'a) t
val depth : 'a t -> int = <fun>
val depth : 'a t -> int = <fun>
val d : ('a * 'a) t -> int = <fun>
Line 9, characters 2-46:
9 |   function Leaf x -> x | Node x -> 1 + depth x;; (* fails *)
      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: This definition has type int t -> int which is less general than
         'a. 'a t -> int
|}];;

(* compare with records (should be the same) *)
type t = {f: 'a. [> `Int of int | `B of 'a] as 'a}
let zero = {f = `Int 0} ;;
type t = {f: 'a. [< `Int of int] as 'a}
let zero = {f = `Int 0} ;; (* fails *)
[%%expect {|
type t = { f : 'a. [> `B of 'a | `Int of int ] as 'a; }
val zero : t = {f = `Int 0}
type t = { f : 'a. [< `Int of int ] as 'a; }
Line 4, characters 16-22:
4 | let zero = {f = `Int 0} ;; (* fails *)
                    ^^^^^^
Error: This expression has type [> `Int of int ]
       but an expression was expected of type [< `Int of int ]
       The second variant type is bound to the universal type variable 'a,
       it may not allow the tag(s) `Int
|}];;

(* Yet another example *)
let rec id : 'a. 'a -> 'a = fun x -> x
and neg i b = (id (-i), id (not b));;
[%%expect {|
val id : 'a -> 'a = <fun>
val neg : int -> bool -> int * bool = <fun>
|}];;

(* De Xavier *)

type t = A of int | B of (int*t) list | C of (string*t) list
[%%expect {|
type t = A of int | B of (int * t) list | C of (string * t) list
|}];;

let rec transf f = function
  | A x -> f x
  | B l -> B (transf_alist f l)
  | C l -> C (transf_alist f l)
and transf_alist : 'a. _ -> ('a*t) list -> ('a*t) list = fun f -> function
  | [] -> []
  | (k,v)::tl -> (k, transf f v) :: transf_alist f tl
;;
[%%expect {|
val transf : (int -> t) -> t -> t = <fun>
val transf_alist : (int -> t) -> ('a * t) list -> ('a * t) list = <fun>
|}];;

(* PR#4862 *)

type t = {f: 'a. ('a list -> int) Lazy.t}
let l : t = { f = lazy (raise Not_found)};;
[%%expect {|
type t = { f : 'a. ('a list -> int) Lazy.t; }
val l : t = {f = <lazy>}
|}];;

(* variant *)
type t = {f: 'a. 'a -> unit};;
let f ?x y = () in {f};;
let f ?x y = y in {f};; (* fail *)
[%%expect {|
type t = { f : 'a. 'a -> unit; }
- : t = {f = <fun>}
Line 3, characters 19-20:
3 | let f ?x y = y in {f};; (* fail *)
                       ^
Error: This field value has type unit -> unit which is less general than
         'a. 'a -> unit
|}];;

(* Polux Moon caml-list 2011-07-26 *)
module Polux = struct
  type 'par t = 'par
  let ident v = v
  class alias = object method alias : 'a . 'a t -> 'a = ident end
  let f (x : <m : 'a. 'a t>) = (x : <m : 'a. 'a>)
end;;
[%%expect {|
module Polux :
  sig
    type 'par t = 'par
    val ident : 'a -> 'a
    class alias : object method alias : 'a t -> 'a end
    val f : < m : 'a. 'a t > -> < m : 'a. 'a >
  end
|}];;

(* PR#5560 *)

let (a, b) = (raise Exit : int * int);;
type t = { foo : int }
let {foo} = (raise Exit : t);;
type s = A of int
let (A x) = (raise Exit : s);;
[%%expect {|
Exception: Stdlib.Exit.
|}];;

(* PR#5224 *)

type 'x t = < f : 'y. 'y t >;;
[%%expect {|
Line 1, characters 0-28:
1 | type 'x t = < f : 'y. 'y t >;;
    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: This recursive type is not regular.
       The type constructor t is defined as
         type 'x t
       but it is used as
         'y t.
       All uses need to match the definition for the recursive type to be regular.
|}];;

(* PR#6056, PR#6057 *)
let using_match b =
  let f =
    match b with
    | true -> fun x -> x
    | false -> fun x -> x
  in
  f 0,f
;;
[%%expect {|
val using_match : bool -> int * ('a -> 'a) = <fun>
|}];;

match (fun x -> x), fun x -> x with x, y -> x, y;;
match fun x -> x with x -> x, x;;
[%%expect {|
- : ('a -> 'a) * ('b -> 'b) = (<fun>, <fun>)
- : ('a -> 'a) * ('b -> 'b) = (<fun>, <fun>)
|}];;

(* PR#6744 *)
(* ok *)
let n = object
  method m : 'x 'o. ([< `Foo of 'x] as 'o) -> 'x = fun x -> assert false
end;;
[%%expect {|
val n : < m : 'x 'a. ([< `Foo of 'x ] as 'a) -> 'x > = <obj>
|}];;
(* ok *)
let n =
  object method m : 'x. [< `Foo of 'x] -> 'x = fun x -> assert false end;;
[%%expect {|
Line 2, characters 9-68:
2 |   object method m : 'x. [< `Foo of 'x] -> 'x = fun x -> assert false end;;
             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: The method m has type 'a -> 'b but is expected to have type
         [< `Foo of 'x ] -> 'c
       The universal variable 'x would escape its scope
|}];;
(* fail *)
let (n : < m : 'a. [< `Foo of int] -> 'a >) =
  object method m : 'x. [< `Foo of 'x] -> 'x = fun x -> assert false end;;
[%%expect {|
Line 2, characters 9-68:
2 |   object method m : 'x. [< `Foo of 'x] -> 'x = fun x -> assert false end;;
             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: The method m has type 'a -> 'b but is expected to have type
         [< `Foo of 'x ] -> 'c
       The universal variable 'x would escape its scope
|}];;
(* fail *)
let (n : 'b -> < m : 'a . ([< `Foo of int] as 'b) -> 'a >) = fun x ->
  object method m : 'x. [< `Foo of 'x] -> 'x = fun x -> assert false end;;
[%%expect {|
Line 2, characters 9-68:
2 |   object method m : 'x. [< `Foo of 'x] -> 'x = fun x -> assert false end;;
             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: The method m has type 'a -> 'b but is expected to have type
         [< `Foo of 'x ] -> 'c
       The universal variable 'x would escape its scope
|}];;
(* ok *)
let f (n : < m : 'a 'r. [< `Foo of 'a & int | `Bar] as 'r >) =
  (n : < m : 'b 'r. [< `Foo of 'b & int | `Bar] as 'r >)
[%%expect{|
val f :
  < m : 'a 'c. [< `Bar | `Foo of 'a & int ] as 'c > ->
  < m : 'b 'd. [< `Bar | `Foo of 'b & int ] as 'd > = <fun>
|}]
(* fail? *)
let f (n : < m : 'a 'r. [< `Foo of 'a & int | `Bar] as 'r >) =
  (n : < m : 'b 'r. [< `Foo of int & 'b | `Bar] as 'r >)
[%%expect{|
Line 2, characters 3-4:
2 |   (n : < m : 'b 'r. [< `Foo of int & 'b | `Bar] as 'r >)
       ^
Error: This expression has type
         < m : 'a 'c. [< `Bar | `Foo of 'a & int ] as 'c >
       but an expression was expected of type
         < m : 'b 'd. [< `Bar | `Foo of int & 'b ] as 'd >
       Types for tag `Foo are incompatible
|}]
(* fail? *)
let f (n : < m : 'a. [< `Foo of 'a & int | `Bar] >) =
  (n : < m : 'b. [< `Foo of 'b & int | `Bar] >)
[%%expect{|
Line 1:
Error: Values do not match:
         val f :
           < m : 'a. [< `Bar | `Foo of 'a & int ] as 'c > -> < m : 'b. 'c >
       is not included in
         val f :
           < m : 'a. [< `Bar | `Foo of 'b & int ] as 'c > -> < m : 'b. 'c >
       The type
         < m : 'a. [< `Bar | `Foo of 'b & int ] as 'c > -> < m : 'b. 'c >
       is not compatible with the type
         < m : 'a. [< `Bar | `Foo of 'b & int ] as 'd > -> < m : 'b. 'd >
       Types for tag `Foo are incompatible
|}]

(* PR#6171 *)
let f b (x: 'x) =
  let module M = struct type t = A end in
  if b then x else M.A;;
[%%expect {|
Line 3, characters 19-22:
3 |   if b then x else M.A;;
                       ^^^
Error: This expression has type M.t but an expression was expected of type 'x
       The type constructor M.t would escape its scope
|}];;


(* PR#6987 *)
type 'a t = V1 of 'a

type ('c,'t) pvariant = [ `V of ('c * 't t) ]

class ['c] clss =
  object
    method mthod : 't . 'c -> 't t -> ('c, 't) pvariant = fun c x ->
      `V (c, x)
  end;;

let f2 = fun o c x -> match x with | V1 _ -> x

let rec f1 o c x =
  match (o :> _ clss)#mthod c x with
  | `V c -> f2 o c x;;
[%%expect{|
type 'a t = V1 of 'a
type ('c, 't) pvariant = [ `V of 'c * 't t ]
class ['c] clss : object method mthod : 'c -> 't t -> ('c, 't) pvariant end
val f2 : 'a -> 'b -> 'c t -> 'c t = <fun>
val f1 :
  < mthod : 't. 'a -> 't t -> [< `V of 'a * 't t ]; .. > ->
  'a -> 'b t -> 'b t = <fun>
|}]

(* PR#7285 *)
type (+'a,-'b) foo = private int;;
let f (x : int) : ('a,'a) foo = Obj.magic x;;
let x = f 3;;
[%%expect{|
type (+'a, -'b) foo = private int
val f : int -> ('a, 'a) foo = <fun>
val x : ('_weak1, '_weak1) foo = 3
|}]


(* PR#7344*)
let rec f : unit -> < m: 'a. 'a -> 'a> = fun () ->
  let x = f () in
  ignore (x#m 1);
  ignore (x#m "hello");
  assert false;;
[%%expect{|
val f : unit -> < m : 'a. 'a -> 'a > = <fun>
|}]

(* PR#7395 *)
type u
type 'a t = u;;
let c (f : u -> u) =
 object
   method apply: 'a. 'a t -> 'a t = fun x -> f x
 end;;
[%%expect{|
type u
type 'a t = u
val c : (u -> u) -> < apply : 'a. u -> u > = <fun>
|}]

(* PR#7496 *)
let f (x : < m: 'a. ([< `Foo of int & float] as 'a) -> unit>)
         : < m: 'a. ([< `Foo of int & float] as 'a) -> unit> = x;;

type t = { x : 'a. ([< `Foo of int & float ] as 'a) -> unit };;
let f t = { x = t.x };;
[%%expect{|
val f :
  < m : 'a. ([< `Foo of int & float ] as 'a) -> unit > ->
  < m : 'b. ([< `Foo of int & float ] as 'b) -> unit > = <fun>
type t = { x : 'a. ([< `Foo of int & float ] as 'a) -> unit; }
val f : t -> t = <fun>
|}]

type t = <m:int>
type g = <n:string; t>
type h = <x:string; y:int; g>
[%%expect{|
type t = < m : int >
type g = < m : int; n : string >
type h = < m : int; n : string; x : string; y : int >
|}]

type t = <g>
and g = <a:t>
[%%expect{|
Line 1, characters 10-11:
1 | type t = <g>
              ^
Error: The type constructor g is not yet completely defined
|}]

type t = int
type g = <t>
[%%expect{|
type t = int
Line 2, characters 10-11:
2 | type g = <t>
              ^
Error: The type int is not an object type
|}]

type t = <a:int>
type g = <t; t; t;>
[%%expect{|
type t = < a : int >
type g = < a : int >
|}]

type c = <a:int; d:string>
let s:c = object method a=1; method d="123" end
[%%expect{|
type c = < a : int; d : string >
val s : c = <obj>
|}]

type 'a t = < m: 'a >
type s = < int t >
module M = struct type t = < m: int > end
type u = < M.t >
type r = < a : int; < b : int > >
type e = < >
type r1 = < a : int; e >
type r2 = < a : int; < < < > > > >
[%%expect{|
type 'a t = < m : 'a >
type s = < m : int >
module M : sig type t = < m : int > end
type u = < m : int >
type r = < a : int; b : int >
type e = <  >
type r1 = < a : int >
type r2 = < a : int >
|}]

type gg = <a:int->float; a:int>
[%%expect{|
Line 1, characters 27-30:
1 | type gg = <a:int->float; a:int>
                               ^^^
Error: Method 'a' has type int, which should be int -> float
|}]

type t = <a:int; b:string>
type g = <b:float; t;>
[%%expect{|
type t = < a : int; b : string >
Line 2, characters 19-20:
2 | type g = <b:float; t;>
                       ^
Error: Method 'b' has type string, which should be float
|}]

module A = struct
  class type ['a] t1 = object method f : 'a end
end
type t = < int A.t1 >
[%%expect{|
module A : sig class type ['a] t1 = object method f : 'a end end
type t = < f : int >
|}]

type t = < int #A.t1 >
[%%expect{|
Line 1, characters 11-20:
1 | type t = < int #A.t1 >
               ^^^^^^^^^
Error: Illegal open object type
|}]

let g = fun (y : ('a * 'b)) x -> (x : < <m: 'a> ; <m: 'b> >)
[%%expect{|
val g : 'a * 'a -> < m : 'a > -> < m : 'a > = <fun>
|}]

type 'a t = <m: 'a ; m: int>
[%%expect{|
type 'a t = < m : 'a > constraint 'a = int
|}]

(* GPR#1142 *)
external reraise : exn -> 'a = "%reraise"

module M () = struct
  let f : 'a -> 'a = assert false
  let g : 'a -> 'a = raise Not_found
  let h : 'a -> 'a = reraise Not_found
  let i : 'a -> 'a = raise_notrace Not_found
end

[%%expect{|
external reraise : exn -> 'a = "%reraise"
module M :
  functor () ->
    sig
      val f : 'a -> 'a
      val g : 'a -> 'a
      val h : 'a -> 'a
      val i : 'a -> 'a
    end
|}]

(* #8550 *)
class ['a] r = let r : 'a = ref [] in object method get = r end;;
[%%expect{|
Line 1, characters 0-63:
1 | class ['a] r = let r : 'a = ref [] in object method get = r end;;
    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: The type of this class,
       class ['a] r :
         object constraint 'a = '_weak2 list ref method get : 'a end,
       contains type variables that cannot be generalized
|}]

(* #8701 *)
type 'a t = 'a constraint 'a = 'b list;;
type 'a s = 'a list;;
let id x = x;;
[%%expect{|
type 'a t = 'a constraint 'a = 'b list
type 'a s = 'a list
val id : 'a -> 'a = <fun>
|}]

let x : [ `Foo of _ s | `Foo of 'a t ] = id (`Foo []);;
[%%expect{|
val x : [ `Foo of 'a s ] = `Foo []
|}]
let x : [ `Foo of 'a t | `Foo of _ s ] = id (`Foo []);;
[%%expect{|
val x : [ `Foo of 'a list t ] = `Foo []
|}]

(* generalize spine of inherited methods too *)

class c = object (self) method m ?(x=0) () = x method n = self#m () end;;
class d = object (self) inherit c method n' = self#m () end;;
[%%expect{|
class c : object method m : ?x:int -> unit -> int method n : int end
class d :
  object method m : ?x:int -> unit -> int method n : int method n' : int end
|}]

(* #1132 *)
let rec foo : 'a . 'a -> 'd = fun x -> x
[%%expect{|
Line 1, characters 30-40:
1 | let rec foo : 'a . 'a -> 'd = fun x -> x
                                  ^^^^^^^^^^
Error: This definition has type 'b -> 'b which is less general than
         'a. 'a -> 'c
|}]

(* #7741 *)
type 'a s = S

class type ['x] c = object
  method x : 'x list
end
[%%expect{|
type 'a s = S
class type ['x] c = object method x : 'x list end
|}]

let x : 'a c = object
  method x : 'b . 'b s list = [S]
end
[%%expect{|
Lines 1-3, characters 15-3:
1 | ...............object
2 |   method x : 'b . 'b s list = [S]
3 | end
Error: This expression has type < x : 'b. 'b s list >
       but an expression was expected of type 'a c
       The method x has type 'b. 'b s list, but the expected method type was
       'a list
       The universal variable 'b would escape its scope
|}]

type u = < m : 'a. 'a s list * (< m : 'b. 'a s list * 'c > as 'c) >
type v = < m : 'a. 'a s list * 'c > as 'c
[%%expect{|
type u = < m : 'a. 'a s list * (< m : 'a s list * 'b > as 'b) >
type v = < m : 'a. 'a s list * 'b > as 'b
|}]
let f (x : u) = (x : v)
[%%expect{|
Line 1, characters 17-18:
1 | let f (x : u) = (x : v)
                     ^
Error: This expression has type u but an expression was expected of type v
       The method m has type 'a s list * < m : 'b > as 'b,
       but the expected method type was 'a. 'a s list * < m : 'a. 'c > as 'c
       The universal variable 'a would escape its scope
|}]

type 'a s = private int
[%%expect{|
type 'a s = private int
|}]
let x : 'a c = object
  method x : 'b . 'b s list = []
end
[%%expect{|
Lines 1-3, characters 15-3:
1 | ...............object
2 |   method x : 'b . 'b s list = []
3 | end
Error: This expression has type < x : 'b. 'b s list >
       but an expression was expected of type 'a c
       The method x has type 'b. 'b s list, but the expected method type was
       'a list
       The universal variable 'b would escape its scope
|}]

(* #9856 *)
let f x =
  let ref : type a . a option ref = ref None in
  ref := Some x;
  Option.get !ref
[%%expect{|
Line 2, characters 6-44:
2 |   let ref : type a . a option ref = ref None in
          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: This definition has type 'a option ref which is less general than
         'a0. 'a0 option ref
|}]

type pr = { foo : 'a. 'a option ref }
let x = { foo = ref None }
[%%expect{|
type pr = { foo : 'a. 'a option ref; }
Line 2, characters 16-24:
2 | let x = { foo = ref None }
                    ^^^^^^^^
Error: This field value has type 'b option ref which is less general than
         'a. 'a option ref
|}]