# HG changeset patch
# User huffman
# Date 1312136018 25200
# Node ID 421f8bc19ce4d8bea1c2a584c4576e636e3e079b
# Parent  a9fcbafdf208f3f6b32a9823abb20d12c8f11b27
domain package: more informative error message for illegal indirect recursion

diff -r a9fcbafdf208 -r 421f8bc19ce4 src/HOL/HOLCF/Tools/Domain/domain.ML
--- a/src/HOL/HOLCF/Tools/Domain/domain.ML	Thu Jul 28 16:56:14 2011 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain.ML	Sun Jul 31 11:13:38 2011 -0700
@@ -119,28 +119,34 @@
        non-pcpo-types and invalid use of recursive type
        replace sorts in type variables on rhs *)
     val rec_tab = Domain_Take_Proofs.get_rec_tab thy
-    fun check_rec rec_ok (T as TFree (v,_))  =
+    fun check_rec no_rec (T as TFree (v,_))  =
         if AList.defined (op =) sorts v then T
         else error ("Free type variable " ^ quote v ^ " on rhs.")
-      | check_rec rec_ok (T as Type (s, Ts)) =
+      | check_rec no_rec (T as Type (s, Ts)) =
         (case AList.lookup (op =) dtnvs' s of
           NONE =>
-            let val rec_ok' = rec_ok andalso Symtab.defined rec_tab s
-            in Type (s, map (check_rec rec_ok') Ts) end
+            let val no_rec' =
+                  if no_rec = NONE then
+                    if Symtab.defined rec_tab s then NONE else SOME s
+                  else no_rec
+            in Type (s, map (check_rec no_rec') Ts) end
         | SOME typevars =>
           if typevars <> Ts
           then error ("Recursion of type " ^ 
                       quote (Syntax.string_of_typ_global tmp_thy T) ^ 
                       " with different arguments")
-          else if rec_ok then T
-          else error ("Illegal indirect recursion of type " ^ 
-                      quote (Syntax.string_of_typ_global tmp_thy T)))
-      | check_rec rec_ok (TVar _) = error "extender:check_rec"
+          else (case no_rec of
+                  NONE => T
+                | SOME c =>
+                  error ("Illegal indirect recursion of type " ^ 
+                         quote (Syntax.string_of_typ_global tmp_thy T) ^
+                         " under type constructor " ^ quote c)))
+      | check_rec no_rec (TVar _) = error "extender:check_rec"
 
     fun prep_arg (lazy, sel, raw_T) =
       let
         val T = prep_typ tmp_thy sorts raw_T
-        val _ = check_rec true T
+        val _ = check_rec NONE T
         val _ = check_pcpo (lazy, sel, T)
       in (lazy, sel, T) end
     fun prep_con (b, args, mx) = (b, map prep_arg args, mx)