# HG changeset patch
# User blanchet
# Date 1377777091 -7200
# Node ID 23927b18dce2b4616faae4307a5d01ab2180a61e
# Parent  3c26a7042d8e61ad6c228a21047911b4df3ace03
rationalize message generation + added a warning

diff -r 3c26a7042d8e -r 23927b18dce2 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Thu Aug 29 11:19:27 2013 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Thu Aug 29 13:51:31 2013 +0200
@@ -1128,6 +1128,9 @@
   (for datatype\_compat and prim(co)rec)
 
 * no way to register same type as both data- and codatatype?
+
+* no recursion through unused arguments (unlike with the old package)
+
 *}
 
 
diff -r 3c26a7042d8e -r 23927b18dce2 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu Aug 29 11:19:27 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu Aug 29 13:51:31 2013 +0200
@@ -1047,17 +1047,6 @@
     val unsorted_As = Library.foldr1 merge_type_args unsorted_Ass0;
     val set_bss = map (map fst o type_args_named_constrained_of) specs;
 
-    val _ = has_duplicates (op =) unsorted_As andalso
-      error ("Duplicate parameters in " ^ co_prefix fp ^ "datatype specification");
-
-    val bad_args =
-      map (Logic.type_map (singleton (Variable.polymorphic no_defs_lthy0))) unsorted_As
-      |> filter_out Term.is_TVar;
-    val _ = null bad_args orelse
-      error ("Locally fixed type argument " ^
-        quote (Syntax.string_of_typ no_defs_lthy0 (hd bad_args)) ^ " in " ^ co_prefix fp ^
-        "datatype specification");
-
     val (((Bs0, Cs), Xs), no_defs_lthy) =
       no_defs_lthy0
       |> fold (Variable.declare_typ o resort_tfree dummyS) unsorted_As
@@ -1076,6 +1065,19 @@
     val fake_thy = fold add_fake_type specs;
     val fake_lthy = Proof_Context.background_theory fake_thy no_defs_lthy;
 
+    val qsoty = quote o Syntax.string_of_typ fake_lthy;
+
+    val _ = (case duplicates (op =) unsorted_As of [] => ()
+      | A :: _ => error ("Duplicate type parameter " ^ qsoty A ^ " in " ^ co_prefix fp ^
+          "datatype specification"));
+
+    val bad_args =
+      map (Logic.type_map (singleton (Variable.polymorphic no_defs_lthy0))) unsorted_As
+      |> filter_out Term.is_TVar;
+    val _ = null bad_args orelse
+      error ("Locally fixed type argument " ^ qsoty (hd bad_args) ^ " in " ^ co_prefix fp ^
+        "datatype specification");
+
     fun mk_fake_T b =
       Type (fst (Term.dest_Type (Proof_Context.read_type_name fake_lthy true (Binding.name_of b))),
         unsorted_As);
@@ -1101,20 +1103,17 @@
 
     val (As :: _) :: fake_ctr_Tsss =
       burrow (burrow (Syntax.check_typs fake_lthy)) (Ass0 :: fake_ctr_Tsss0);
-
-    val _ = (case duplicates (op =) unsorted_As of [] => ()
-      | A :: _ => error ("Duplicate type parameter " ^
-          quote (Syntax.string_of_typ no_defs_lthy A)));
+    val As' = map dest_TFree As;
 
     val rhs_As' = fold (fold (fold Term.add_tfreesT)) fake_ctr_Tsss [];
-    val _ = (case subtract (op =) (map dest_TFree As) rhs_As' of
-        [] => ()
-      | A' :: _ => error ("Extra type variable on right-hand side: " ^
-          quote (Syntax.string_of_typ no_defs_lthy (TFree A'))));
+    val _ = (case subtract (op =) As' rhs_As' of [] => ()
+      | extras => error ("Extra type variables on right-hand side: " ^
+          commas (map (qsoty o TFree) extras)));
 
-    fun eq_fpT_check (T as Type (s, Us)) (Type (s', Us')) =
-        s = s' andalso (Us = Us' orelse error ("Illegal occurrence of recursive type " ^
-          quote (Syntax.string_of_typ fake_lthy T)))
+    fun eq_fpT_check (T as Type (s, Ts)) (T' as Type (s', Ts')) =
+        s = s' andalso (Ts = Ts' orelse
+          error ("Wrong type arguments in " ^ co_prefix fp ^ "recursive type " ^ qsoty T ^
+            " (expected " ^ qsoty T' ^ ")"))
       | eq_fpT_check _ _ = false;
 
     fun freeze_fp (T as Type (s, Ts)) =
@@ -1131,6 +1130,11 @@
     val fp_eqs =
       map dest_TFree Xs ~~ map (Term.typ_subst_atomic (As ~~ unsorted_As)) ctrXs_sum_prod_Ts;
 
+    val rhsXs_As' = fold (fold (fold Term.add_tfreesT)) ctrXs_Tsss [];
+    val _ = (case subtract (op =) rhsXs_As' As' of [] => ()
+      | extras => List.app (fn extra => warning ("Unused type variable: " ^ qsoty (TFree extra)))
+          extras);
+
     val (pre_bnfs, (fp_res as {bnfs = fp_bnfs as any_fp_bnf :: _, ctors = ctors0, dtors = dtors0,
            xtor_co_iterss = xtor_co_iterss0, xtor_co_induct, dtor_ctors, ctor_dtors, ctor_injects,
            dtor_injects, xtor_map_thms, xtor_set_thmss, xtor_rel_thms, xtor_co_iter_thmss, ...},
@@ -1141,7 +1145,6 @@
         (case X_backdrop of
           Type (bad_tc, _) =>
           let
-            val qsoty = quote o Syntax.string_of_typ fake_lthy;
             val fake_T = qsoty (unfreeze_fp X);
             val fake_T_backdrop = qsoty (unfreeze_fp X_backdrop);
             fun register_hint () =