# HG changeset patch
# User wenzelm
# Date 1284300363 -7200
# Node ID 1f8131a7bcb9a546837af529884db6aae215505f
# Parent  85728a4b56205b2756695b368fbb5f3dd0ccde8f
tuned messages;
tuned comments;

diff -r 85728a4b5620 -r 1f8131a7bcb9 src/Pure/type_infer.ML
--- a/src/Pure/type_infer.ML	Fri Sep 10 23:11:58 2010 +0200
+++ b/src/Pure/type_infer.ML	Sun Sep 12 16:06:03 2010 +0200
@@ -34,7 +34,7 @@
 val constrain = Syntax.type_constraint;
 
 
-(* user parameters *)
+(* type inference parameters -- may get instantiated *)
 
 fun is_param (x, _: int) = String.isPrefix "?" x;
 fun param i (x, S) = TVar (("?" ^ x, i), S);
@@ -73,7 +73,6 @@
 
 (** pretyps and preterms **)
 
-(*parameters may get instantiated, anything else is rigid*)
 datatype pretyp =
   PType of string * pretyp list |
   PTFree of string * sort |
@@ -168,7 +167,7 @@
             SOME U =>
               let val (pU, idx') = polyT_of U idx
               in constraint T (PConst (c, pU)) (ps, idx') end
-          | NONE => raise TYPE ("No such constant: " ^ quote c, [], []))
+          | NONE => raise TYPE ("Undeclared constant: " ^ quote c, [], []))
       | pre_of (Var (xi, Type ("_polymorphic_", [T]))) (ps, idx) =
           let val (pT, idx') = polyT_of T idx
           in (PVar (xi, pT), (ps, idx')) end
@@ -258,7 +257,6 @@
 
 fun unify pp tsig =
   let
-
     (* adjust sorts of parameters *)
 
     fun not_of_sort x S' S =
@@ -304,13 +302,17 @@
 
     (* unification *)
 
+    fun show_tycon (a, Ts) =
+      quote (Pretty.string_of_typ pp (Type (a, replicate (length Ts) dummyT)));
+
     fun unif (T1, T2) (tye_idx as (tye, idx)) =
       (case (deref tye T1, deref tye T2) of
         (Param (i, S), T) => assign i T S tye_idx
       | (T, Param (i, S)) => assign i T S tye_idx
       | (PType (a, Ts), PType (b, Us)) =>
           if a <> b then
-            raise NO_UNIFIER ("Clash of types " ^ quote a ^ " and " ^ quote b, tye)
+            raise NO_UNIFIER
+              ("Clash of types " ^ show_tycon (a, Ts) ^ " and " ^ show_tycon (b, Us), tye)
           else fold unif (Ts ~~ Us) tye_idx
       | (T, U) => if T = U then tye_idx else raise NO_UNIFIER ("", tye));