summaryrefslogtreecommitdiff
path: root/testsuite/tests/typing-gadts/pr5689.ml
blob: 87b2bef9e8e6953eca7e512305534063e156d16e (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
(* TEST
 expect;
*)

type inkind = [ `Link | `Nonlink ]

type _ inline_t =
   | Text: string -> [< inkind > `Nonlink ] inline_t
   | Bold: 'a inline_t list -> 'a inline_t
   | Link: string -> [< inkind > `Link ] inline_t
   | Mref: string * [ `Nonlink ] inline_t list -> [< inkind > `Link ] inline_t
;;

let uppercase seq =
   let rec process: type a. a inline_t -> a inline_t = function
       | Text txt       -> Text (String.uppercase_ascii txt)
       | Bold xs        -> Bold (List.map process xs)
       | Link lnk       -> Link lnk
       | Mref (lnk, xs) -> Mref (lnk, List.map process xs)
   in List.map process seq
;;
[%%expect{|
type inkind = [ `Link | `Nonlink ]
type _ inline_t =
    Text : string -> [< inkind > `Nonlink ] inline_t
  | Bold : 'a inline_t list -> 'a inline_t
  | Link : string -> [< inkind > `Link ] inline_t
  | Mref : string *
      [ `Nonlink ] inline_t list -> [< inkind > `Link ] inline_t
val uppercase : 'a inline_t list -> 'a inline_t list = <fun>
|}];;

type ast_t =
   | Ast_Text of string
   | Ast_Bold of ast_t list
   | Ast_Link of string
   | Ast_Mref of string * ast_t list
;;

let inlineseq_from_astseq seq =
   let rec process_nonlink = function
       | Ast_Text txt  -> Text txt
       | Ast_Bold xs   -> Bold (List.map process_nonlink xs)
       | _             -> assert false in
   let rec process_any = function
       | Ast_Text txt       -> Text txt
       | Ast_Bold xs        -> Bold (List.map process_any xs)
       | Ast_Link lnk       -> Link lnk
       | Ast_Mref (lnk, xs) -> Mref (lnk, List.map process_nonlink xs)
   in List.map process_any seq
;;
[%%expect{|
type ast_t =
    Ast_Text of string
  | Ast_Bold of ast_t list
  | Ast_Link of string
  | Ast_Mref of string * ast_t list
val inlineseq_from_astseq : ast_t list -> inkind inline_t list = <fun>
|}];;

(* OK *)
type _ linkp =
 | Nonlink : [ `Nonlink ] linkp
 | Maylink : inkind linkp
;;
let inlineseq_from_astseq seq =
 let rec process : type a. a linkp -> ast_t -> a inline_t =
   fun allow_link ast ->
     match (allow_link, ast) with
     | (Maylink, Ast_Text txt)    -> Text txt
     | (Nonlink, Ast_Text txt)    -> Text txt
     | (x, Ast_Bold xs)           -> Bold (List.map (process x) xs)
     | (Maylink, Ast_Link lnk)    -> Link lnk
     | (Nonlink, Ast_Link _)      -> assert false
     | (Maylink, Ast_Mref (lnk, xs)) ->
         Mref (lnk, List.map (process Nonlink) xs)
     | (Nonlink, Ast_Mref _)      -> assert false
   in List.map (process Maylink) seq
;;
[%%expect{|
type _ linkp = Nonlink : [ `Nonlink ] linkp | Maylink : inkind linkp
val inlineseq_from_astseq : ast_t list -> inkind inline_t list = <fun>
|}];;

(* Bad *)
type _ linkp2 = Kind : 'a linkp -> ([< inkind ] as 'a) linkp2
;;
let inlineseq_from_astseq seq =
let rec process : type a. a linkp2 -> ast_t -> a inline_t =
  fun allow_link ast ->
    match (allow_link, ast) with
    | (Kind _, Ast_Text txt)    -> Text txt
    | (x, Ast_Bold xs)           -> Bold (List.map (process x) xs)
    | (Kind Maylink, Ast_Link lnk)    -> Link lnk
    | (Kind Nonlink, Ast_Link _)      -> assert false
    | (Kind Maylink, Ast_Mref (lnk, xs)) ->
        Mref (lnk, List.map (process (Kind Nonlink)) xs)
    | (Kind Nonlink, Ast_Mref _)      -> assert false
  in List.map (process (Kind Maylink)) seq
;;
[%%expect{|
type _ linkp2 = Kind : 'a linkp -> ([< inkind ] as 'a) linkp2
Line 7, characters 35-43:
7 |     | (Kind _, Ast_Text txt)    -> Text txt
                                       ^^^^^^^^
Error: This expression has type [< inkind > `Nonlink ] inline_t
       but an expression was expected of type a inline_t
       Type [< inkind > `Nonlink ] = [< `Link | `Nonlink > `Nonlink ]
       is not compatible with type a = [< `Link | `Nonlink ]
       The second variant type is bound to $'a,
       it may not allow the tag(s) `Nonlink
|}];;