# HG changeset patch
# User wenzelm
# Date 1301345054 -7200
# Node ID 786ccfffcd67f8b4ef98ba2af345ee6b0020989b
# Parent  d24a93025feb7c4440bdb6e067c87bd1777fc016
address serious problem of type inference (introduced in 6f085332c7d3): _type_constraint_ needs type scheme A --> A with proper scope of parameters, otherwise term "(f :: _ => _) :: 'c => 'c" will get type "'a => 'b", for example;

diff -r d24a93025feb -r 786ccfffcd67 src/Pure/type_infer.ML
--- a/src/Pure/type_infer.ML	Mon Mar 28 17:33:16 2011 +0200
+++ b/src/Pure/type_infer.ML	Mon Mar 28 22:44:14 2011 +0200
@@ -93,7 +93,7 @@
 
 (* prepare_term *)
 
-fun prepare_term const_type tm (vparams, params, idx) =
+fun prepare_term ctxt const_type tm (vparams, params, idx) =
   let
     fun add_vparm xi (ps_idx as (ps, idx)) =
       if not (Vartab.defined ps xi) then
@@ -118,9 +118,12 @@
 
     fun prepare (Const ("_type_constraint_", T) $ t) ps_idx =
           let
-            val (T', ps_idx') = prepare_typ T ps_idx;
+            fun err () =
+              error ("Malformed internal type constraint: " ^ Syntax.string_of_typ ctxt T);
+            val A = (case T of Type ("fun", [A, B]) => if A = B then A else err () | _ => err ());
+            val (A', ps_idx') = prepare_typ A ps_idx;
             val (t', ps_idx'') = prepare t ps_idx';
-          in (Const ("_type_constraint_", T') $ t', ps_idx'') end
+          in (Const ("_type_constraint_", A' --> A') $ t', ps_idx'') end
       | prepare (Const (c, T)) (ps, idx) =
           (case const_type c of
             SOME U =>
@@ -344,8 +347,8 @@
 
     val ts = burrow_types (Syntax.check_typs ctxt) raw_ts;
     val (ts', (_, _, idx)) =
-      fold_map (prepare_term const_type o constrain_vars) ts
-      (Vartab.empty, Vartab.empty, 0);
+      fold_map (prepare_term ctxt const_type o constrain_vars) ts
+        (Vartab.empty, Vartab.empty, 0);
   in (idx, ts') end;
 
 fun infer_types ctxt const_type var_type raw_ts =