two-staged architecture for subtyping;
authortraytel
Mon Nov 29 16:53:08 2010 +0100 (2010-11-29)
changeset 40836a81d66d72e70
parent 40835 fc750e794458
child 40837 dedb893dc692
two-staged architecture for subtyping;
improved error messages of subtyping (using the new architecture);
bugfix: constraint graph consistency check after cycle elimination;
src/Tools/subtyping.ML
     1.1 --- a/src/Tools/subtyping.ML	Tue Nov 30 20:02:01 2010 -0800
     1.2 +++ b/src/Tools/subtyping.ML	Mon Nov 29 16:53:08 2010 +0100
     1.3 @@ -11,6 +11,7 @@
     1.4      term list -> term list
     1.5    val add_type_map: term -> Context.generic -> Context.generic
     1.6    val add_coercion: term -> Context.generic -> Context.generic
     1.7 +  val gen_coercion: Proof.context -> typ Vartab.table -> (typ * typ) -> term
     1.8    val setup: theory -> theory
     1.9  end;
    1.10  
    1.11 @@ -86,8 +87,9 @@
    1.12  val is_fixedvarT = fn (TVar (xi, _)) => not (Type_Infer.is_param xi) | _ => false;
    1.13  
    1.14  
    1.15 -(* unification *)  (* TODO dup? needed for weak unification *)
    1.16 +(* unification *)
    1.17  
    1.18 +exception TYPE_INFERENCE_ERROR of unit -> string;
    1.19  exception NO_UNIFIER of string * typ Vartab.table;
    1.20  
    1.21  fun unify weak ctxt =
    1.22 @@ -185,6 +187,10 @@
    1.23  
    1.24  (** error messages **)
    1.25  
    1.26 +fun gen_msg err msg = 
    1.27 +  err () ^ "\nNow trying to infer coercions:\n\nCoercion inference failed" ^ 
    1.28 +  (if msg = "" then "" else ": " ^ msg) ^ "\n";
    1.29 +
    1.30  fun prep_output ctxt tye bs ts Ts =
    1.31    let
    1.32      val (Ts_bTs', ts') = Type_Infer.finish ctxt tye (Ts @ map snd bs, ts);
    1.33 @@ -195,23 +201,23 @@
    1.34    in (map prep ts', Ts') end;
    1.35  
    1.36  fun err_loose i = error ("Loose bound variable: B." ^ string_of_int i);
    1.37 -
    1.38 -fun inf_failed msg =
    1.39 -  "Subtype inference failed" ^ (if msg = "" then "" else ": " ^ msg) ^ "\n\n";
    1.40 +  
    1.41 +fun unif_failed msg =
    1.42 +  "Type unification failed" ^ (if msg = "" then "" else ": " ^ msg) ^ "\n\n";
    1.43  
    1.44 -fun err_appl ctxt msg tye bs t T u U =
    1.45 +fun subtyping_err_appl_msg ctxt msg tye bs t T u U () =
    1.46    let val ([t', u'], [T', U']) = prep_output ctxt tye bs [t, u] [T, U]
    1.47 -  in error (inf_failed msg ^ Type.appl_error (Syntax.pp ctxt) t' T' u' U' ^ "\n") end;
    1.48 -
    1.49 -fun err_subtype ctxt msg tye (bs, t $ u, U, V, U') =
    1.50 -  err_appl ctxt msg tye bs t (U --> V) u U';
    1.51 +  in msg ^ Type.appl_error (Syntax.pp ctxt) t' T' u' U' ^ "\n" end;
    1.52 +  
    1.53 +fun err_appl_msg ctxt msg tye bs t T u U () =
    1.54 +  let val ([t', u'], [T', U']) = prep_output ctxt tye bs [t, u] [T, U]
    1.55 +  in unif_failed msg ^ Type.appl_error (Syntax.pp ctxt) t' T' u' U' ^ "\n" end;
    1.56  
    1.57  fun err_list ctxt msg tye Ts =
    1.58    let
    1.59      val (_, Ts') = prep_output ctxt tye [] [] Ts;
    1.60 -    val text = cat_lines ([inf_failed msg,
    1.61 -      "Cannot unify a list of types that should be the same,",
    1.62 -      "according to suptype dependencies:",
    1.63 +    val text = cat_lines ([msg,
    1.64 +      "Cannot unify a list of types that should be the same:",
    1.65        (Pretty.string_of (Pretty.list "[" "]" (map (Pretty.typ (Syntax.pp ctxt)) Ts')))]);
    1.66    in
    1.67      error text
    1.68 @@ -222,15 +228,15 @@
    1.69      val pp = Syntax.pp ctxt;
    1.70      val (ts, Ts) = fold
    1.71        (fn (bs, t $ u, U, _, U') => fn (ts, Ts) =>
    1.72 -        let val (t', T') = prep_output ctxt tye bs [t, u] [U, U']
    1.73 +        let val (t', T') = prep_output ctxt tye bs [t, u] [U', U]
    1.74          in (t' :: ts, T' :: Ts) end)
    1.75        packs ([], []);
    1.76 -    val text = cat_lines ([inf_failed msg, "Cannot fullfill subtype constraints:"] @
    1.77 +    val text = cat_lines ([msg, "Cannot fulfil subtype constraints:"] @
    1.78          (map2 (fn [t, u] => fn [T, U] => Pretty.string_of (
    1.79            Pretty.block [
    1.80              Pretty.typ pp T, Pretty.brk 2, Pretty.str "<:", Pretty.brk 2, Pretty.typ pp U,
    1.81              Pretty.brk 3, Pretty.str "from function application", Pretty.brk 2,
    1.82 -            Pretty.block [Pretty.term pp t, Pretty.brk 1, Pretty.term pp u]]))
    1.83 +            Pretty.block [Pretty.term pp (t $ u)]]))
    1.84          ts Ts))
    1.85    in
    1.86      error text
    1.87 @@ -240,7 +246,7 @@
    1.88  
    1.89  (** constraint generation **)
    1.90  
    1.91 -fun generate_constraints ctxt =
    1.92 +fun generate_constraints ctxt err =
    1.93    let
    1.94      fun gen cs _ (Const (_, T)) tye_idx = (T, tye_idx, cs)
    1.95        | gen cs _ (Free (_, T)) tye_idx = (T, tye_idx, cs)
    1.96 @@ -257,7 +263,7 @@
    1.97              val U = Type_Infer.mk_param idx [];
    1.98              val V = Type_Infer.mk_param (idx + 1) [];
    1.99              val tye_idx''= strong_unify ctxt (U --> V, T) (tye, idx + 2)
   1.100 -              handle NO_UNIFIER (msg, tye') => err_appl ctxt msg tye' bs t T u U;
   1.101 +              handle NO_UNIFIER (msg, tye') => error (gen_msg err msg);
   1.102              val error_pack = (bs, t $ u, U, V, U');
   1.103            in (V, tye_idx'', ((U', U), error_pack) :: cs'') end;
   1.104    in
   1.105 @@ -270,7 +276,7 @@
   1.106  
   1.107  exception BOUND_ERROR of string;
   1.108  
   1.109 -fun process_constraints ctxt cs tye_idx =
   1.110 +fun process_constraints ctxt err cs tye_idx =
   1.111    let
   1.112      val coes_graph = coes_graph_of ctxt;
   1.113      val tmaps = tmaps_of ctxt;
   1.114 @@ -289,9 +295,8 @@
   1.115      (* check whether constraint simplification will terminate using weak unification *)
   1.116  
   1.117      val _ = fold (fn (TU, error_pack) => fn tye_idx =>
   1.118 -      (weak_unify ctxt TU tye_idx handle NO_UNIFIER (msg, tye) =>
   1.119 -        err_subtype ctxt ("Weak unification of subtype constraints fails:\n" ^ msg)
   1.120 -          tye error_pack)) cs tye_idx;
   1.121 +      weak_unify ctxt TU tye_idx handle NO_UNIFIER (msg, tye) =>
   1.122 +        error (gen_msg err ("weak unification of subtype constraints fails\n" ^ msg))) cs tye_idx;
   1.123  
   1.124  
   1.125      (* simplify constraints *)
   1.126 @@ -310,7 +315,8 @@
   1.127                  COVARIANT => (constraint :: cs, tye_idx)
   1.128                | CONTRAVARIANT => (swap constraint :: cs, tye_idx)
   1.129                | INVARIANT => (cs, strong_unify ctxt constraint tye_idx
   1.130 -                  handle NO_UNIFIER (msg, tye) => err_subtype ctxt msg tye error_pack));
   1.131 +                  handle NO_UNIFIER (msg, tye) => 
   1.132 +                    error (gen_msg err ("failed to unify invariant arguments\n" ^ msg))));
   1.133              val (new, (tye', idx')) = apfst (fn cs => (cs ~~ replicate (length cs) error_pack))
   1.134                (fold new_constraints (arg_var ~~ (Ts ~~ Us)) ([], (tye, idx)));
   1.135              val test_update = is_compT orf is_freeT orf is_fixedvarT;
   1.136 @@ -348,7 +354,7 @@
   1.137            in
   1.138              if subsort (S', S) (*TODO check this*)
   1.139              then simplify done' todo' (tye', idx)
   1.140 -            else err_subtype ctxt "Sort mismatch" tye error_pack
   1.141 +            else error (gen_msg err "sort mismatch")
   1.142            end
   1.143          and simplify done [] tye_idx = (done, tye_idx)
   1.144            | simplify done (((T, U), error_pack) :: todo) (tye_idx as (tye, idx)) =
   1.145 @@ -356,9 +362,10 @@
   1.146                  (Type (a, []), Type (b, [])) =>
   1.147                    if a = b then simplify done todo tye_idx
   1.148                    else if Graph.is_edge coes_graph (a, b) then simplify done todo tye_idx
   1.149 -                  else err_subtype ctxt (a ^ " is not a subtype of " ^ b) (fst tye_idx) error_pack
   1.150 +                  else error (gen_msg err (a ^ " is not a subtype of " ^ b))
   1.151                | (Type (a, Ts), Type (b, Us)) =>
   1.152 -                  if a <> b then err_subtype ctxt "Different constructors" (fst tye_idx) error_pack
   1.153 +                  if a <> b then error (gen_msg err "different constructors")
   1.154 +                    (fst tye_idx) error_pack
   1.155                    else contract a Ts Us error_pack done todo tye idx
   1.156                | (TVar (xi, S), Type (a, Ts as (_ :: _))) =>
   1.157                    expand true xi S a Ts error_pack done todo tye idx
   1.158 @@ -370,8 +377,7 @@
   1.159                      exists Type_Infer.is_paramT [T, U]
   1.160                    then eliminate [T, U] error_pack done todo tye idx
   1.161                    else if exists (is_freeT orf is_fixedvarT) [T, U]
   1.162 -                  then err_subtype ctxt "Not eliminated free/fixed variables"
   1.163 -                        (fst tye_idx) error_pack
   1.164 +                  then error (gen_msg err "not eliminated free/fixed variables")
   1.165                    else simplify (((T, U), error_pack) :: done) todo tye_idx);
   1.166        in
   1.167          simplify [] cs tye_idx
   1.168 @@ -381,14 +387,22 @@
   1.169      (* do simplification *)
   1.170  
   1.171      val (cs', tye_idx') = simplify_constraints cs tye_idx;
   1.172 -
   1.173 -    fun find_error_pack lower T' =
   1.174 -      map snd (filter (fn ((T, U), _) => if lower then T' = U else T' = T) cs');
   1.175 +    
   1.176 +    fun find_error_pack lower T' = map_filter 
   1.177 +      (fn ((T, U), pack) => if if lower then T' = U else T' = T then SOME pack else NONE) cs';
   1.178 +      
   1.179 +    fun find_cycle_packs nodes = 
   1.180 +      let
   1.181 +        val (but_last, last) = split_last nodes
   1.182 +        val pairs = (last, hd nodes) :: (but_last ~~ tl nodes);
   1.183 +      in
   1.184 +        map_filter
   1.185 +          (fn (TU, pack) => if member (eq_pair (op =) (op =)) pairs TU then SOME pack else NONE) 
   1.186 +          cs'
   1.187 +      end;
   1.188  
   1.189      fun unify_list (T :: Ts) tye_idx =
   1.190 -      fold (fn U => fn tye_idx => strong_unify ctxt (T, U) tye_idx
   1.191 -        handle NO_UNIFIER (msg, tye) => err_list ctxt msg tye (T :: Ts))
   1.192 -      Ts tye_idx;
   1.193 +      fold (fn U => fn tye_idx' => strong_unify ctxt (T, U) tye_idx') Ts tye_idx;
   1.194  
   1.195      (*styps stands either for supertypes or for subtypes of a type T
   1.196        in terms of the subtype-relation (excluding T itself)*)
   1.197 @@ -403,7 +417,7 @@
   1.198            | extract T (U :: Us) =
   1.199                if Graph.is_edge coes_graph (adjust T U) then extract T Us
   1.200                else if Graph.is_edge coes_graph (adjust U T) then extract U Us
   1.201 -              else raise BOUND_ERROR "Uncomparable types in type list";
   1.202 +              else raise BOUND_ERROR "uncomparable types in type list";
   1.203        in
   1.204          t_of (extract T Ts)
   1.205        end;
   1.206 @@ -435,7 +449,7 @@
   1.207          fun candidates T = inter (op =) (filter restriction (T :: styps sup T));
   1.208        in
   1.209          (case fold candidates Ts (filter restriction (T :: styps sup T)) of
   1.210 -          [] => raise BOUND_ERROR ("No " ^ (if sup then "supremum" else "infimum"))
   1.211 +          [] => raise BOUND_ERROR ("no " ^ (if sup then "supremum" else "infimum"))
   1.212          | [T] => t_of T
   1.213          | Ts => minmax sup Ts)
   1.214        end;
   1.215 @@ -449,23 +463,45 @@
   1.216              val (G'', tye_idx') = (add_edge (T, U) G', tye_idx)
   1.217                handle Typ_Graph.CYCLES cycles =>
   1.218                  let
   1.219 -                  val (tye, idx) = fold unify_list cycles tye_idx
   1.220 +                  val (tye, idx) = 
   1.221 +                    fold 
   1.222 +                      (fn cycle => fn tye_idx' => (unify_list cycle tye_idx'
   1.223 +                        handle NO_UNIFIER (msg, tye) => 
   1.224 +                          err_bound ctxt 
   1.225 +                            (gen_msg err ("constraint cycle not unifiable" ^ msg)) (fst tye_idx)
   1.226 +                            (find_cycle_packs cycle)))
   1.227 +                      cycles tye_idx
   1.228                  in
   1.229 -                  (*all cycles collapse to one node,
   1.230 -                    because all of them share at least the nodes x and y*)
   1.231 -                  collapse (tye, idx) (distinct (op =) (flat cycles)) G
   1.232 -                end;
   1.233 +                  collapse (tye, idx) cycles G
   1.234 +                end
   1.235            in
   1.236              build_graph G'' cs tye_idx'
   1.237            end
   1.238 -    and collapse (tye, idx) nodes G = (*nodes non-empty list*)
   1.239 +    and collapse (tye, idx) cycles G = (*nodes non-empty list*)
   1.240        let
   1.241 -        val T = hd nodes;
   1.242 +        (*all cycles collapse to one node,
   1.243 +          because all of them share at least the nodes x and y*)
   1.244 +        val nodes = (distinct (op =) (flat cycles));
   1.245 +        val T = Type_Infer.deref tye (hd nodes);
   1.246          val P = new_imm_preds G nodes;
   1.247          val S = new_imm_succs G nodes;
   1.248          val G' = Typ_Graph.del_nodes (tl nodes) G;
   1.249 +        fun check_and_gen super T' =
   1.250 +          let val U = Type_Infer.deref tye T';
   1.251 +          in
   1.252 +            if not (is_typeT T) orelse not (is_typeT U) orelse T = U
   1.253 +            then if super then (hd nodes, T') else (T', hd nodes)
   1.254 +            else 
   1.255 +              if super andalso 
   1.256 +                Graph.is_edge coes_graph (nameT T, nameT U) then (hd nodes, T')
   1.257 +              else if not super andalso 
   1.258 +                Graph.is_edge coes_graph (nameT U, nameT T) then (T', hd nodes)
   1.259 +              else err_bound ctxt (gen_msg err "cycle elimination produces inconsistent graph")
   1.260 +                    (fst tye_idx) 
   1.261 +                    (maps find_cycle_packs cycles @ find_error_pack super T')
   1.262 +          end;
   1.263        in
   1.264 -        build_graph G' (map (fn x => (x, T)) P @ map (fn x => (T, x)) S) (tye, idx)
   1.265 +        build_graph G' (map (check_and_gen false) P @ map (check_and_gen true) S) (tye, idx)
   1.266        end;
   1.267  
   1.268      fun assign_bound lower G key (tye_idx as (tye, _)) =
   1.269 @@ -488,7 +524,8 @@
   1.270            val assignment =
   1.271              if null bound orelse null not_params then NONE
   1.272              else SOME (tightest lower S styps_and_sorts (map nameT not_params)
   1.273 -                handle BOUND_ERROR msg => err_bound ctxt msg tye (find_error_pack lower key))
   1.274 +                handle BOUND_ERROR msg => 
   1.275 +                  err_bound ctxt (gen_msg err msg) tye (find_error_pack lower key))
   1.276          in
   1.277            (case assignment of
   1.278              NONE => tye_idx
   1.279 @@ -501,9 +538,9 @@
   1.280                  in
   1.281                    if subset (op = o apfst nameT) (filter is_typeT other_bound, s :: styps true s)
   1.282                    then apfst (Vartab.update (xi, T)) tye_idx
   1.283 -                  else err_bound ctxt ("Assigned simple type " ^ s ^
   1.284 +                  else err_bound ctxt (gen_msg err ("assigned simple type " ^ s ^
   1.285                      " clashes with the upper bound of variable " ^
   1.286 -                    Syntax.string_of_typ ctxt (TVar(xi, S))) tye (find_error_pack (not lower) key)
   1.287 +                    Syntax.string_of_typ ctxt (TVar(xi, S)))) tye (find_error_pack (not lower) key)
   1.288                  end
   1.289                else apfst (Vartab.update (xi, T)) tye_idx)
   1.290          end
   1.291 @@ -519,7 +556,8 @@
   1.292            val (tye_idx' as (tye, _)) = fold (assign_lb G) ts tye_idx
   1.293              |> fold (assign_ub G) ts;
   1.294          in
   1.295 -          assign_alternating ts (filter (Type_Infer.is_paramT o Type_Infer.deref tye) ts) G tye_idx'
   1.296 +          assign_alternating ts 
   1.297 +            (filter (Type_Infer.is_paramT o Type_Infer.deref tye) ts) G tye_idx'
   1.298          end;
   1.299  
   1.300      (*Unify all weakly connected components of the constraint forest,
   1.301 @@ -531,7 +569,10 @@
   1.302            filter (Type_Infer.is_paramT o Type_Infer.deref tye) (Typ_Graph.maximals G);
   1.303          val to_unify = map (fn T => T :: get_preds G T) max_params;
   1.304        in
   1.305 -        fold unify_list to_unify tye_idx
   1.306 +        fold 
   1.307 +          (fn Ts => fn tye_idx' => unify_list Ts tye_idx'
   1.308 +            handle NO_UNIFIER (msg, tye) => err_list ctxt (gen_msg err msg) (fst tye_idx) Ts)
   1.309 +          to_unify tye_idx
   1.310        end;
   1.311  
   1.312      fun solve_constraints G tye_idx = tye_idx
   1.313 @@ -546,77 +587,73 @@
   1.314  
   1.315  (** coercion insertion **)
   1.316  
   1.317 +fun gen_coercion ctxt tye (T1, T2) =
   1.318 +  (case pairself (Type_Infer.deref tye) (T1, T2) of
   1.319 +    ((Type (a, [])), (Type (b, []))) =>
   1.320 +        if a = b
   1.321 +        then Abs (Name.uu, Type (a, []), Bound 0)
   1.322 +        else
   1.323 +          (case Symreltab.lookup (coes_of ctxt) (a, b) of
   1.324 +            NONE => raise Fail (a ^ " is not a subtype of " ^ b)
   1.325 +          | SOME co => co)
   1.326 +  | ((Type (a, Ts)), (Type (b, Us))) =>
   1.327 +        if a <> b
   1.328 +        then raise Fail ("Different constructors: " ^ a ^ " and " ^ b)
   1.329 +        else
   1.330 +          let
   1.331 +            fun inst t Ts =
   1.332 +              Term.subst_vars
   1.333 +                (((Term.add_tvar_namesT (fastype_of t) []) ~~ rev Ts), []) t;
   1.334 +            fun sub_co (COVARIANT, TU) = gen_coercion ctxt tye TU
   1.335 +              | sub_co (CONTRAVARIANT, TU) = gen_coercion ctxt tye (swap TU);
   1.336 +            fun ts_of [] = []
   1.337 +              | ts_of (Type ("fun", [x1, x2]) :: xs) = x1 :: x2 :: (ts_of xs);
   1.338 +          in
   1.339 +            (case Symtab.lookup (tmaps_of ctxt) a of
   1.340 +              NONE => raise Fail ("No map function for " ^ a ^ " known")
   1.341 +            | SOME tmap =>
   1.342 +                let
   1.343 +                  val used_coes = map sub_co ((snd tmap) ~~ (Ts ~~ Us));
   1.344 +                in
   1.345 +                  Term.list_comb
   1.346 +                    (inst (fst tmap) (ts_of (map fastype_of used_coes)), used_coes)
   1.347 +                end)
   1.348 +          end
   1.349 +  | (T, U) =>
   1.350 +        if Type.could_unify (T, U)
   1.351 +        then Abs (Name.uu, T, Bound 0)
   1.352 +        else raise Fail ("Cannot generate coercion from "
   1.353 +          ^ Syntax.string_of_typ ctxt T ^ " to " ^ Syntax.string_of_typ ctxt U));
   1.354 +
   1.355  fun insert_coercions ctxt tye ts =
   1.356    let
   1.357 -    fun deep_deref T =
   1.358 -      (case Type_Infer.deref tye T of
   1.359 -        Type (a, Ts) => Type (a, map deep_deref Ts)
   1.360 -      | U => U);
   1.361 -
   1.362 -    fun gen_coercion ((Type (a, [])), (Type (b, []))) =
   1.363 -          if a = b
   1.364 -          then Abs (Name.uu, Type (a, []), Bound 0)
   1.365 -          else
   1.366 -            (case Symreltab.lookup (coes_of ctxt) (a, b) of
   1.367 -              NONE => raise Fail (a ^ " is not a subtype of " ^ b)
   1.368 -            | SOME co => co)
   1.369 -      | gen_coercion ((Type (a, Ts)), (Type (b, Us))) =
   1.370 -          if a <> b
   1.371 -          then raise raise Fail ("Different constructors: " ^ a ^ " and " ^ b)
   1.372 -          else
   1.373 -            let
   1.374 -              fun inst t Ts =
   1.375 -                Term.subst_vars
   1.376 -                  (((Term.add_tvar_namesT (fastype_of t) []) ~~ rev Ts), []) t;
   1.377 -              fun sub_co (COVARIANT, TU) = gen_coercion TU
   1.378 -                | sub_co (CONTRAVARIANT, TU) = gen_coercion (swap TU);
   1.379 -              fun ts_of [] = []
   1.380 -                | ts_of (Type ("fun", [x1, x2]) :: xs) = x1 :: x2 :: (ts_of xs);
   1.381 -            in
   1.382 -              (case Symtab.lookup (tmaps_of ctxt) a of
   1.383 -                NONE => raise Fail ("No map function for " ^ a ^ " known")
   1.384 -              | SOME tmap =>
   1.385 -                  let
   1.386 -                    val used_coes = map sub_co ((snd tmap) ~~ (Ts ~~ Us));
   1.387 -                  in
   1.388 -                    Term.list_comb
   1.389 -                      (inst (fst tmap) (ts_of (map fastype_of used_coes)), used_coes)
   1.390 -                  end)
   1.391 -            end
   1.392 -      | gen_coercion (T, U) =
   1.393 -          if Type.could_unify (T, U)
   1.394 -          then Abs (Name.uu, T, Bound 0)
   1.395 -          else raise Fail ("Cannot generate coercion from "
   1.396 -            ^ Syntax.string_of_typ ctxt T ^ " to " ^ Syntax.string_of_typ ctxt U);
   1.397 -
   1.398      fun insert _ (Const (c, T)) =
   1.399 -          let val T' = deep_deref T;
   1.400 +          let val T' = T;
   1.401            in (Const (c, T'), T') end
   1.402        | insert _ (Free (x, T)) =
   1.403 -          let val T' = deep_deref T;
   1.404 +          let val T' = T;
   1.405            in (Free (x, T'), T') end
   1.406        | insert _ (Var (xi, T)) =
   1.407 -          let val T' = deep_deref T;
   1.408 +          let val T' = T;
   1.409            in (Var (xi, T'), T') end
   1.410        | insert bs (Bound i) =
   1.411 -          let val T = nth bs i handle Subscript =>
   1.412 -            raise TYPE ("Loose bound variable: B." ^ string_of_int i, [], []);
   1.413 +          let val T = nth bs i handle Subscript => err_loose i;
   1.414            in (Bound i, T) end
   1.415        | insert bs (Abs (x, T, t)) =
   1.416            let
   1.417 -            val T' = deep_deref T;
   1.418 +            val T' = T;
   1.419              val (t', T'') = insert (T' :: bs) t;
   1.420            in
   1.421              (Abs (x, T', t'), T' --> T'')
   1.422            end
   1.423        | insert bs (t $ u) =
   1.424            let
   1.425 -            val (t', Type ("fun", [U, T])) = insert bs t;
   1.426 +            val (t', Type ("fun", [U, T])) = apsnd (Type_Infer.deref tye) (insert bs t);
   1.427              val (u', U') = insert bs u;
   1.428            in
   1.429 -            if U <> U'
   1.430 -            then (t' $ (gen_coercion (U', U) $ u'), T)
   1.431 -            else (t' $ u', T)
   1.432 +            if can (fn TU => strong_unify ctxt TU (tye, 0)) (U, U')
   1.433 +            then (t' $ u', T)
   1.434 +            else (t' $ (gen_coercion ctxt tye (U', U) $ u'), T)
   1.435            end
   1.436    in
   1.437      map (fst o insert []) ts
   1.438 @@ -630,14 +667,40 @@
   1.439    let
   1.440      val (idx, ts) = Type_Infer.prepare ctxt const_type var_type raw_ts;
   1.441  
   1.442 -    fun gen_all t (tye_idx, constraints) =
   1.443 -      let
   1.444 -        val (_, tye_idx', constraints') = generate_constraints ctxt t tye_idx
   1.445 -      in (tye_idx', constraints' @ constraints) end;
   1.446 +    fun inf _ (t as (Const (_, T))) tye_idx = (t, T, tye_idx)
   1.447 +      | inf _ (t as (Free (_, T))) tye_idx = (t, T, tye_idx)
   1.448 +      | inf _ (t as (Var (_, T))) tye_idx = (t, T, tye_idx)
   1.449 +      | inf bs (t as (Bound i)) tye_idx =
   1.450 +          (t, snd (nth bs i handle Subscript => err_loose i), tye_idx)
   1.451 +      | inf bs (Abs (x, T, t)) tye_idx =
   1.452 +          let val (t', U, tye_idx') = inf ((x, T) :: bs) t tye_idx
   1.453 +          in (Abs (x, T, t'), T --> U, tye_idx') end
   1.454 +      | inf bs (t $ u) tye_idx =
   1.455 +          let
   1.456 +            val (t', T, tye_idx') = inf bs t tye_idx;
   1.457 +            val (u', U, (tye, idx)) = inf bs u tye_idx';
   1.458 +            val V = Type_Infer.mk_param idx [];
   1.459 +            val (tu, tye_idx'') = (t' $ u', strong_unify ctxt (U --> V, T) (tye, idx + 1))
   1.460 +              handle NO_UNIFIER (msg, tye') => 
   1.461 +                raise TYPE_INFERENCE_ERROR (err_appl_msg ctxt msg tye' bs t T u U);
   1.462 +          in (tu, V, tye_idx'') end;
   1.463  
   1.464 -    val (tye_idx, constraints) = fold gen_all ts ((Vartab.empty, idx), []);
   1.465 -    val (tye, _) = process_constraints ctxt constraints tye_idx;
   1.466 -    val ts' = insert_coercions ctxt tye ts;
   1.467 +    fun infer_single t (ts, tye_idx) = 
   1.468 +      let val (t, _, tye_idx') = inf [] t tye_idx;
   1.469 +      in (ts @ [t], tye_idx') end;
   1.470 +      
   1.471 +    val (ts', (tye, _)) = (fold infer_single ts ([], (Vartab.empty, idx))
   1.472 +      handle TYPE_INFERENCE_ERROR err =>     
   1.473 +        let
   1.474 +          fun gen_single t (tye_idx, constraints) =
   1.475 +            let val (_, tye_idx', constraints') = generate_constraints ctxt err t tye_idx
   1.476 +            in (tye_idx', constraints' @ constraints) end;
   1.477 +      
   1.478 +          val (tye_idx, constraints) = fold gen_single ts ((Vartab.empty, idx), []);
   1.479 +          val (tye, idx) = process_constraints ctxt err constraints tye_idx;
   1.480 +        in 
   1.481 +          (insert_coercions ctxt tye ts, (tye, idx))
   1.482 +        end);
   1.483  
   1.484      val (_, ts'') = Type_Infer.finish ctxt tye ([], ts');
   1.485    in ts'' end;
   1.486 @@ -738,7 +801,7 @@
   1.487          fun complex_coercion tab G (a, b) =
   1.488            let
   1.489              val path = hd (Graph.irreducible_paths G (a, b))
   1.490 -            val path' = (fst (split_last path)) ~~ tl path
   1.491 +            val path' = fst (split_last path) ~~ tl path
   1.492            in Abs (Name.uu, Type (a, []),
   1.493                fold (fn t => fn u => t $ u) (map (the o Symreltab.lookup tab) path') (Bound 0))
   1.494            end;