Commits

Anonymous committed 3ad5397
  • Participants
  • Parent commits 003f87c

Comments (0)

Files changed (8)

testsuite/tests/typing-gadts/pr5689.ml

+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 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
+;;
+
+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
+;;
+
+(* 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
+;;
+
+(* 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
+;;

testsuite/tests/typing-gadts/pr5689.ml.principal.reference

+
+#               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
+#                         val inlineseq_from_astseq : ast_t list -> inkind inline_t list = <fun>
+#           type _ linkp = Nonlink : [ `Nonlink ] linkp | Maylink : inkind linkp
+#                           val inlineseq_from_astseq : ast_t list -> inkind inline_t list = <fun>
+#       type _ linkp2 = Kind : 'a linkp -> ([< inkind ] as 'a) linkp2
+#                         Characters 272-279:
+      | (Kind Maylink, Ast_Link lnk)    -> Link lnk
+              ^^^^^^^
+Error: This pattern matches values of type inkind linkp
+       but a pattern was expected which matches values of type
+         ([< inkind ] as 'a) linkp
+       Type inkind = [ `Link | `Nonlink ] is not compatible with type
+         'a = [< `Link | `Nonlink ] 
+       Types for tag `Nonlink are incompatible
+# 

testsuite/tests/typing-gadts/pr5689.ml.reference

+
+#               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
+#                         val inlineseq_from_astseq : ast_t list -> inkind inline_t list = <fun>
+#           type _ linkp = Nonlink : [ `Nonlink ] linkp | Maylink : inkind linkp
+#                           val inlineseq_from_astseq : ast_t list -> inkind inline_t list = <fun>
+#       type _ linkp2 = Kind : 'a linkp -> ([< inkind ] as 'a) linkp2
+#                         Characters 272-279:
+      | (Kind Maylink, Ast_Link lnk)    -> Link lnk
+              ^^^^^^^
+Error: This pattern matches values of type inkind linkp
+       but a pattern was expected which matches values of type
+         ([< inkind ] as 'a) linkp
+       Type inkind = [ `Link | `Nonlink ] is not compatible with type
+         'a = [< `Link | `Nonlink ] 
+       Types for tag `Nonlink are incompatible
+# 
   | {desc=Tvariant row'} -> row_more row'
   | ty -> ty
 
+let row_fixed row =
+  let row = row_repr row in
+  row.row_fixed ||
+  match (repr row.row_more).desc with
+    Tvar _ | Tnil -> false
+  | Tunivar _ | Tconstr _ -> true
+  | _ -> assert false
+
 let static_row row =
   let row = row_repr row in
   row.row_closed &&
         (* Return the canonical representative of a row field *)
 val row_more: row_desc -> type_expr
         (* Return the extension variable of the row *)
+val row_fixed: row_desc -> bool
+        (* Return whether the row should be treated as fixed or not *)
 val static_row: row_desc -> bool
         (* Return whether the row is static or not *)
 val hash_variant: label -> int
         with Not_found -> ())
       r2
   end;
+  let fixed1 = row_fixed row1 and fixed2 = row_fixed row2 in
   let more =
-    if row1.row_fixed then rm1 else
-    if row2.row_fixed then rm2 else
+    if fixed1 then rm1 else
+    if fixed2 then rm2 else
     newty2 (min rm1.level rm2.level) (Tvar None) in
-  let fixed = row1.row_fixed || row2.row_fixed
+  let fixed = fixed1 || fixed2
   and closed = row1.row_closed || row2.row_closed in
   let keep switch =
     List.for_all
       if closed then
         filter_row_fields row.row_closed rest
       else rest in
-    if rest <> [] && (row.row_closed || row.row_fixed)
-    || closed && row.row_fixed && not row.row_closed then begin
+    if rest <> [] && (row.row_closed || row_fixed row)
+    || closed && row_fixed row && not row.row_closed then begin
       let t1 = mkvariant [] true and t2 = mkvariant rest false in
       raise (Unify [if row == row1 then (t1,t2) else (t2,t1)])
     end;
     if !trace_gadt_instances && rm.desc = Tnil then () else
     if !trace_gadt_instances then
       update_level !env rm.level (newgenty (Tvariant row));
-    if row.row_fixed then
+    if row_fixed row then
       if more == rm then () else
       if is_Tvar rm then link_type rm more else unify env rm more
     else
     set_more row1 r2;
     List.iter
       (fun (l,f1,f2) ->
-        try unify_row_field env row1.row_fixed row2.row_fixed more l f1 f2
+        try unify_row_field env fixed1 fixed2 more l f1 f2
         with Unify trace ->
           raise (Unify ((mkvariant [l,f1] true,
                          mkvariant [l,f2] true) :: trace)))
   | Reither(c1, tl1, m1, e1), Reither(c2, tl2, m2, e2) ->
       if e1 == e2 then () else
       let redo =
-        (m1 || m2 ||
+        (m1 || m2 || fixed1 || fixed2 ||
          !rigid_variants && (List.length tl1 = 1 || List.length tl2 = 1)) &&
         begin match tl1 @ tl2 with [] -> false
         | t1 :: tl ->
       let f1' = Reither(c1 || c2, tl1', m1 || m2, e)
       and f2' = Reither(c1 || c2, tl2', m1 || m2, e) in
       set_row_field e1 f1'; set_row_field e2 f2';
-  | Reither(_, _, false, e1), Rabsent -> set_row_field e1 f2
-  | Rabsent, Reither(_, _, false, e2) -> set_row_field e2 f1
+  | Reither(_, _, false, e1), Rabsent when not fixed1 -> set_row_field e1 f2
+  | Rabsent, Reither(_, _, false, e2) when not fixed2 -> set_row_field e2 f1
   | Rabsent, Rabsent -> ()
   | Reither(false, tl, _, e1), Rpresent(Some t2) when not fixed1 ->
       set_row_field e1 f2;
     | Tvariant row ->
         let row = row_repr row in
         let more = repr row.row_more in
-        if is_Tvar more && not row.row_fixed then begin
+        if is_Tvar more && not (row_fixed row) then begin
           let more' = newty2 more.level more.desc in
           let row' = {row with row_fixed=true; row_fields=[]; row_more=more'}
           in link_type more (newty2 ty.level (Tvariant row'))

typing/parmatch.ml

         env
     in
     let row = row_of_pat p in
-    if closing && not row.row_fixed then
+    if closing && not (Btype.row_fixed row) then
       (* closing=true, we are considering the variant as closed *)
       List.for_all
         (fun (tag,f) ->
             begin match constrs, tdefs with
               ({pat_desc=Tpat_variant _} as p,_):: _, Some env ->
                 let row = row_of_pat p in
-                if row.row_fixed
+                if Btype.row_fixed row
                 || pressure_variants None (filter_extra pss) then ()
                 else close_variant env row
             | _ -> ()

typing/typecore.ml

           begin match opat with None -> assert false
           | Some pat -> List.iter (unify_pat pat.pat_env pat) (ty::tl)
           end
-      | Reither (c, l, true, e) when not row.row_fixed ->
+      | Reither (c, l, true, e) when not (row_fixed row) ->
           set_row_field e (Reither (c, [], false, ref None))
       | _ -> ()
       end;