Fix bug when defining polymorphic datatype type with name "a"

One remaining annoyance is that the constructor is stored with a
default type that does not use 'a, but will instead use the type
variable 'aa. This is visible when prim_mk_const is used, but not
much (if at all) otherwise.

Closes #1140

doc/next-release.md

@@ -48,6 +48,8 @@ New features:
 Bugs fixed:
 -----------
 
+- Fix [a failure to define a polymorphic datatype with name `a`](https://github.com/HOL-Theorem-Prover/HOL/issues/1140).
+
 New theories:
 -------------
 

src/datatype/Datatype.sml

@@ -174,55 +174,78 @@ in
   app warn common
 end
 
+fun ast_tyvar_strings (dAQ ty) = map dest_vartype $ type_vars ty
+  | ast_tyvar_strings (dVartype s) = [s]
+  | ast_tyvar_strings (dTyop {Args, ...}) =
+      List.concat (map ast_tyvar_strings Args)
 
-local fun tyname_as_tyvar n = mk_vartype ("'" ^ n)
-      fun stage1 (s,Constructors l) = (s,l)
-        | stage1 (s,Record fields)  = (s,[(mk_recordtype_constructor s,
-                                           map snd fields)])
-      fun check_fields (s,Record fields) =
-          (case duplicate_names (map fst fields)
-           of NONE => ()
-            | SOME n => raise ERR "check_fields" ("Duplicate field name: "^n))
-        | check_fields _ = ()
-      fun cnames (s,Record _) A = s::A
-        | cnames (_,Constructors l) A = map fst l @ A
-      fun check_constrs asts =
-            case duplicate_names (itlist cnames asts [])
-             of NONE => ()
-              | SOME n => raise ERR "check_constrs"
-                                    ("Duplicate constructor name: "^n)
+local
+  fun strvariant avoids s = if mem s avoids then strvariant avoids (s ^ "a")
+                            else s
+  fun tyname_as_tyvar n = mk_vartype ("'" ^ n)
+  fun stage1 (s,Constructors l) = (s,l)
+    | stage1 (s,Record fields)  = (s,[(mk_recordtype_constructor s,
+                                       map snd fields)])
+  fun check_fields (s,Record fields) =
+      (case duplicate_names (map fst fields) of
+           NONE => ()
+         | SOME n => raise ERR "check_fields" ("Duplicate field name: "^n))
+    | check_fields _ = ()
+  fun cnames (s,Record _) A = s::A
+    | cnames (_,Constructors l) A = map fst l @ A
+  fun check_constrs asts =
+      case duplicate_names (itlist cnames asts []) of
+          NONE => ()
+        | SOME n => raise ERR "check_constrs"
+                          ("Duplicate constructor name: "^n)
 in
 fun to_tyspecs ASTs =
  let val _ = List.app check_fields ASTs
      val _ = check_constrs ASTs
      val _ = check_constrs_unique_in_theory ASTs
      val asts = map stage1 ASTs
      val new_type_names = map #1 asts
-     fun mk_hol_ty (dAQ ty) = ty
-       | mk_hol_ty (dVartype s) = mk_vartype s
-       | mk_hol_ty (dTyop{Tyop=s, Args, Thy}) =
+
+     fun mk_hol_ty d (dAQ ty) = ty
+       | mk_hol_ty d (dVartype s) = mk_vartype (valOf $ Symtab.lookup d s)
+       | mk_hol_ty d (dTyop{Tyop=s, Args, Thy}) =
             if Lib.mem s new_type_names andalso
                (Thy = NONE orelse Thy = SOME (current_theory()))
             then if null Args then tyname_as_tyvar s
                  else raise ERR "to_tyspecs"
                      ("Omit arguments to new type:"^Lib.quote s)
             else
               case Thy of
-                NONE => mk_type(s, map mk_hol_ty Args)
+                NONE => mk_type(s, map (mk_hol_ty d) Args)
               | SOME t => mk_thy_type {Tyop = s, Thy = t,
-                                       Args = map mk_hol_ty Args}
-     fun mk_hol_type pty = let
-       val ty = mk_hol_ty pty
+                                       Args = map (mk_hol_ty d) Args}
+     fun mk_hol_type d pty = let
+       val ty = mk_hol_ty d pty
      in
        if Theory.uptodate_type ty then ty
        else let val tyname = #1 (dest_type ty)
             in raise ERR "to_tyspecs" (tyname^" not up-to-date")
             end
      end
-
-     fun constructor (cname, ptys) = (cname, map mk_hol_type ptys)
+     val allvars = let
+       fun perc ((cnm, ptys), A) =
+           List.foldl
+             (fn (pt,A) => HOLset.addList(A,ast_tyvar_strings pt)) A ptys
+       fun perty ((nm, cs), A) = List.foldl perc A cs
+     in
+       HOLset.listItems (List.foldl perty (HOLset.empty String.compare) asts)
+     end
+     val (dict,_) = List.foldl
+                  (fn (nm, (d,avds)) =>
+                      let val nm' = strvariant avds nm
+                      in
+                        (Symtab.update(nm,nm') d, nm'::avds)
+                      end)
+                  (Symtab.empty, map (fn (s,_) => "'" ^ s) asts)
+                  allvars
+     fun constructor (cname, ptys) = (cname, map (mk_hol_type dict) ptys)
   in
-     map (tyname_as_tyvar##map constructor) asts
+    map (tyname_as_tyvar ## map constructor) asts
   end
 end;
 

src/datatype/selftest.sml

@@ -234,6 +234,31 @@ val _ = Datatype.Datatype`
   uvmhol3 = <| uvmfld1 : num # (num -> bool); uvmfld2 : bool |>
 `;
 
+(* github issue #1140 *)
+val _ = tprint "a = aCtr ('a # bool)"
+val _ = testutils.quietly Datatype.Datatype‘
+  a = aCtr ('a # bool)
+’;
+val aCtr_t =
+    prim_mk_const{Thy = "scratch", Name = "aCtr"}
+    handle HOL_ERR _ => (die "constant aCtr doesn't exist"; boolSyntax.T)
+val (cty_d,cty_r) = dom_rng $ type_of aCtr_t
+val _ = let val {Thy,Tyop,Args} = dest_thy_type cty_d
+        in
+          if Thy = "pair" andalso Tyop = "prod" andalso length Args = 2 andalso
+             is_vartype (hd Args)
+          then
+            let val {Thy,Tyop,Args} = dest_thy_type cty_r
+            in
+              if Thy = "scratch" andalso Tyop = "a" andalso
+                 length Args = 1 andalso is_vartype (hd Args)
+              then
+                OK()
+              else die "New type has wrong name/type"
+            end
+          else die ("Argument to aCtr is wrong type: "^type_to_string cty_d)
+        end
+
 val _ = tprint "Testing independence of case variables"
 val t = Lib.total Parse.Term `case (x:valbind) of
                                 bind p e => 3
@@ -469,5 +494,6 @@ val _ = quiet_warnings (fn () =>
 val _ = quiet_warnings (fn () =>
            (Datatype`a_rec = A ((a_rec # unit # num option # (unit + num)) list) | B unit`)
            ) () handle _ => die "FAILED!"
+val _ = OK()
 
 val _ = Process.exit Process.success;