improved type check error messages;
authorwenzelm
Thu Apr 17 18:46:58 1997 +0200 (1997-04-17)
changeset 2979db6941221197
parent 2978 83a4c4f79dcd
child 2980 98ad57d99427
improved type check error messages;
src/Pure/sign.ML
src/Pure/theory.ML
src/Pure/thm.ML
src/Pure/type.ML
src/Pure/type_infer.ML
     1.1 --- a/src/Pure/sign.ML	Thu Apr 17 18:45:43 1997 +0200
     1.2 +++ b/src/Pure/sign.ML	Thu Apr 17 18:46:58 1997 +0200
     1.3 @@ -36,7 +36,6 @@
     1.4    val certify_typ: sg -> typ -> typ
     1.5    val certify_term: sg -> term -> term * typ * int
     1.6    val read_typ: sg * (indexname -> sort option) -> string -> typ
     1.7 -  val exn_type_msg: sg -> string * typ list * term list -> string
     1.8    val infer_types: sg -> (indexname -> typ option) ->
     1.9      (indexname -> sort option) -> string list -> bool
    1.10      -> term list * typ -> int * term * (indexname * typ) list
    1.11 @@ -77,6 +76,7 @@
    1.12  structure Sign : SIGN =
    1.13  struct
    1.14  
    1.15 +
    1.16  (** datatype sg **)
    1.17  
    1.18  (*the "ref" in stamps ensures that no two signatures are identical -- it is
    1.19 @@ -93,9 +93,8 @@
    1.20  val tsig_of = #tsig o rep_sg;
    1.21  
    1.22  
    1.23 -(* stamps *)
    1.24 +(* inclusion and equality *)
    1.25  
    1.26 -(*inclusion, equality*)
    1.27  local
    1.28    (*avoiding polymorphic equality: factor 10 speedup*)
    1.29    fun mem_stamp (_:string ref, []) = false
    1.30 @@ -136,8 +135,7 @@
    1.31  
    1.32  (* consts *)
    1.33  
    1.34 -fun const_type (Sg {const_tab, ...}) c =
    1.35 -  Symtab.lookup (const_tab, c);
    1.36 +fun const_type (Sg {const_tab, ...}) c = Symtab.lookup (const_tab, c);
    1.37  
    1.38  
    1.39  (* classes and sorts *)
    1.40 @@ -148,6 +146,7 @@
    1.41  val norm_sort = Type.norm_sort o tsig_of;
    1.42  val nonempty_sort = Type.nonempty_sort o tsig_of;
    1.43  
    1.44 +(* FIXME move to Sorts? *)
    1.45  fun pretty_sort [c] = Pretty.str c
    1.46    | pretty_sort cs = Pretty.str_list "{" "}" cs;
    1.47  
    1.48 @@ -193,15 +192,14 @@
    1.49    in
    1.50      Pretty.writeln (Pretty.strs ("stamps:" :: stamp_names stamps));
    1.51      Pretty.writeln (Pretty.strs ("classes:" :: classes));
    1.52 -    Pretty.writeln (Pretty.big_list "classrel:"
    1.53 -                      (map pretty_classrel classrel));
    1.54 +    Pretty.writeln (Pretty.big_list "classrel:" (map pretty_classrel classrel));
    1.55      Pretty.writeln (pretty_default default);
    1.56      Pretty.writeln (Pretty.big_list "types:" (map pretty_ty tycons));
    1.57      Pretty.writeln (Pretty.big_list "abbrs:" (map (pretty_abbr syn) abbrs));
    1.58      Pretty.writeln (Pretty.big_list "arities:"
    1.59 -                      (List.concat (map pretty_arities arities)));
    1.60 +      (List.concat (map pretty_arities arities)));
    1.61      Pretty.writeln (Pretty.big_list "consts:"
    1.62 -                      (map (pretty_const syn) (Symtab.dest const_tab)))
    1.63 +      (map (pretty_const syn) (Symtab.dest const_tab)))
    1.64    end;
    1.65  
    1.66  
    1.67 @@ -251,44 +249,51 @@
    1.68  
    1.69  fun certify_typ (Sg {tsig, ...}) ty = Type.cert_typ tsig ty;
    1.70  
    1.71 -(* check for duplicate TVars with distinct sorts *)
    1.72 -fun nodup_TVars(tvars,T) = (case T of
    1.73 -      Type(_,Ts) => nodup_TVars_list (tvars,Ts)
    1.74 -    | TFree _ => tvars
    1.75 -    | TVar(v as (a,S)) =>
    1.76 -        (case assoc_string_int(tvars,a) of
    1.77 -           Some(S') => if S=S' then tvars
    1.78 -                       else raise_type
    1.79 -                            ("Type variable "^Syntax.string_of_vname a^
    1.80 -                             " has two distinct sorts") [TVar(a,S'),T] []
    1.81 -         | None => v::tvars))
    1.82 -and (*equivalent to foldl nodup_TVars_list, but 3X faster under Poly/ML*)
    1.83 -    nodup_TVars_list (tvars,[]) = tvars
    1.84 -  | nodup_TVars_list (tvars,T::Ts) = nodup_TVars_list(nodup_TVars(tvars,T), 
    1.85 -						      Ts);
    1.86 +(*check for duplicate TVars with distinct sorts*)
    1.87 +fun nodup_TVars (tvars, T) =
    1.88 +  (case T of
    1.89 +    Type (_, Ts) => nodup_TVars_list (tvars, Ts)
    1.90 +  | TFree _ => tvars
    1.91 +  | TVar (v as (a, S)) =>
    1.92 +      (case assoc_string_int (tvars, a) of
    1.93 +        Some S' =>
    1.94 +          if S = S' then tvars
    1.95 +          else raise_type ("Type variable " ^ Syntax.string_of_vname a ^
    1.96 +            " has two distinct sorts") [TVar (a, S'), T] []
    1.97 +      | None => v :: tvars))
    1.98 +(*equivalent to foldl nodup_TVars_list, but 3X faster under Poly/ML*)
    1.99 +and nodup_TVars_list (tvars, []) = tvars
   1.100 +  | nodup_TVars_list (tvars, T :: Ts) =
   1.101 +      nodup_TVars_list (nodup_TVars (tvars, T), Ts);
   1.102  
   1.103 -(* check for duplicate Vars with distinct types *)
   1.104 +(*check for duplicate Vars with distinct types*)
   1.105  fun nodup_Vars tm =
   1.106 -let fun nodups vars tvars tm = (case tm of
   1.107 -          Const(c,T) => (vars, nodup_TVars(tvars,T))
   1.108 -        | Free(a,T) => (vars, nodup_TVars(tvars,T))
   1.109 -        | Var(v as (ixn,T)) =>
   1.110 -            (case assoc_string_int(vars,ixn) of
   1.111 -               Some(T') => if T=T' then (vars,nodup_TVars(tvars,T))
   1.112 -                           else raise_type
   1.113 -                             ("Variable "^Syntax.string_of_vname ixn^
   1.114 -                              " has two distinct types") [T',T] []
   1.115 -             | None => (v::vars,tvars))
   1.116 -        | Bound _ => (vars,tvars)
   1.117 -        | Abs(_,T,t) => nodups vars (nodup_TVars(tvars,T)) t
   1.118 -        | s$t => let val (vars',tvars') = nodups vars tvars s
   1.119 -                 in nodups vars' tvars' t end);
   1.120 -in nodups [] [] tm; () end;
   1.121 +  let
   1.122 +    fun nodups vars tvars tm =
   1.123 +      (case tm of
   1.124 +        Const (c, T) => (vars, nodup_TVars (tvars, T))
   1.125 +      | Free (a, T) => (vars, nodup_TVars (tvars, T))
   1.126 +      | Var (v as (ixn, T)) =>
   1.127 +          (case assoc_string_int (vars, ixn) of
   1.128 +            Some T' =>
   1.129 +              if T = T' then (vars, nodup_TVars (tvars, T))
   1.130 +              else raise_type ("Variable " ^ Syntax.string_of_vname ixn ^
   1.131 +                " has two distinct types") [T', T] []
   1.132 +          | None => (v :: vars, tvars))
   1.133 +      | Bound _ => (vars, tvars)
   1.134 +      | Abs(_, T, t) => nodups vars (nodup_TVars (tvars, T)) t
   1.135 +      | s $ t =>
   1.136 +          let val (vars',tvars') = nodups vars tvars s in
   1.137 +            nodups vars' tvars' t
   1.138 +          end);
   1.139 +  in nodups [] [] tm; () end;
   1.140 +
   1.141  
   1.142  fun mapfilt_atoms f (Abs (_, _, t)) = mapfilt_atoms f t
   1.143    | mapfilt_atoms f (t $ u) = mapfilt_atoms f t @ mapfilt_atoms f u
   1.144    | mapfilt_atoms f a = (case f a of Some y => [y] | None => []);
   1.145  
   1.146 +
   1.147  fun certify_term (sg as Sg {tsig, ...}) tm =
   1.148    let
   1.149      fun valid_const a T =
   1.150 @@ -316,82 +321,67 @@
   1.151    end;
   1.152  
   1.153  
   1.154 -(*package error messages from type checking*)
   1.155 -fun exn_type_msg sg (msg, Ts, ts) =
   1.156 -  let
   1.157 -    val show_typ = string_of_typ sg;
   1.158 -    val show_term = set_ap Syntax.show_brackets true (string_of_term sg);
   1.159 -
   1.160 -    fun term_err [] = ""
   1.161 -      | term_err [t] = "\n\nInvolving this term:\n" ^ show_term t
   1.162 -      | term_err ts =
   1.163 -          "\n\nInvolving these terms:\n" ^ cat_lines (map show_term ts);
   1.164 -  in
   1.165 -    "\nType checking error: " ^ msg ^ "\n" ^
   1.166 -      cat_lines (map show_typ Ts) ^ term_err ts ^ "\n"
   1.167 -  end;
   1.168 -
   1.169 -
   1.170  
   1.171  (** infer_types **)         (*exception ERROR*)
   1.172  
   1.173 -(*ts is the list of alternative parses; only one is hoped to be type-correct.
   1.174 -  T is the expected type for the correct term.
   1.175 -  Other standard arguments:
   1.176 -    types is a partial map from indexnames to types (constrains Free, Var).
   1.177 -    sorts is a partial map from indexnames to sorts (constrains TFree, TVar).
   1.178 -    used is the list of already used type variables.
   1.179 -    If freeze then internal TVars are turned into TFrees, else TVars.*)
   1.180 -fun infer_types sg types sorts used freeze (ts, T) =
   1.181 +(*
   1.182 +  ts: list of alternative parses (hopefully only one is type-correct)
   1.183 +  T: expected type
   1.184 +
   1.185 +  def_type: partial map from indexnames to types (constrains Frees, Vars)
   1.186 +  def_sort: partial map from indexnames to sorts (constrains TFrees, TVars)
   1.187 +  used: list of already used type variables
   1.188 +  freeze: if true then generated parameters are turned into TFrees, else TVars
   1.189 +*)
   1.190 +
   1.191 +fun infer_types sg def_type def_sort used freeze (ts, T) =
   1.192    let
   1.193      val Sg {tsig, ...} = sg;
   1.194 +    val prt = setmp Syntax.show_brackets true (pretty_term sg);
   1.195 +    val prT = pretty_typ sg;
   1.196 +    val infer = Type.infer_types prt prT tsig (const_type sg)
   1.197 +      def_type def_sort used freeze;
   1.198  
   1.199 -    val T' = certify_typ sg T handle TYPE arg => error (exn_type_msg sg arg);
   1.200 -
   1.201 -    val ct = const_type sg;
   1.202 +    val T' = certify_typ sg T handle TYPE (msg, _, _) => error msg;
   1.203  
   1.204 -    fun warn() =
   1.205 -      if length ts > 1 andalso length ts <= !Syntax.ambiguity_level
   1.206 +    fun warn () =
   1.207 +      if length ts > 1 andalso length ts <= ! Syntax.ambiguity_level
   1.208        then (*no warning shown yet*)
   1.209 -           warning "Currently parsed input \
   1.210 -                   \produces more than one parse tree.\n\
   1.211 -                   \For more information lower Syntax.ambiguity_level."
   1.212 +        warning "Currently parsed input \
   1.213 +          \produces more than one parse tree.\n\
   1.214 +          \For more information lower Syntax.ambiguity_level."
   1.215        else ();
   1.216  
   1.217 -    datatype result = One of int * term * (indexname * typ) list
   1.218 -                    | Errs of (string * typ list * term list)list
   1.219 -                    | Ambigs of term list;
   1.220 -
   1.221 -    fun process_term(res,(t,i)) =
   1.222 -       let val ([u],tye) = 
   1.223 -	       Type.infer_types(tsig,ct,types,sorts,used,freeze,[T'],[t])
   1.224 -       in case res of
   1.225 -            One(_,t0,_) => Ambigs([u,t0])
   1.226 -          | Errs _ => One(i,u,tye)
   1.227 -          | Ambigs(us) => Ambigs(u::us)
   1.228 -       end
   1.229 -       handle TYPE arg => (case res of Errs(errs) => Errs(arg::errs)
   1.230 -                                     | _ => res);
   1.231 +    datatype result =
   1.232 +      One of int * term * (indexname * typ) list |
   1.233 +      Errs of string list |
   1.234 +      Ambigs of term list;
   1.235  
   1.236 -  in case foldl process_term (Errs[], ts ~~ (0 upto (length ts - 1))) of
   1.237 -       One(res) =>
   1.238 -         (if length ts > !Syntax.ambiguity_level
   1.239 -          then writeln "Fortunately, only one parse tree is type correct.\n\
   1.240 +    fun process_term (res, (t, i)) =
   1.241 +      let val ([u], tye) = infer [T'] [t] in
   1.242 +        (case res of
   1.243 +          One (_, t0, _) => Ambigs ([u, t0])
   1.244 +        | Errs _ => One (i, u, tye)
   1.245 +        | Ambigs us => Ambigs (u :: us))
   1.246 +      end handle TYPE (msg, _, _) =>
   1.247 +        (case res of
   1.248 +          Errs errs => Errs (msg :: errs)
   1.249 +        | _ => res);
   1.250 +  in
   1.251 +    (case foldl process_term (Errs [], ts ~~ (0 upto (length ts - 1))) of
   1.252 +      One res =>
   1.253 +       (if length ts > ! Syntax.ambiguity_level then
   1.254 +          writeln "Fortunately, only one parse tree is type correct.\n\
   1.255              \It helps (speed!) if you disambiguate your grammar or your input."
   1.256 -          else ();
   1.257 -          res)
   1.258 -     | Errs(errs) => (warn(); error(cat_lines(map (exn_type_msg sg) errs)))
   1.259 -     | Ambigs(us) =>
   1.260 -         (warn();
   1.261 -          let val old_show_brackets = !show_brackets
   1.262 -              val dummy = show_brackets := true;
   1.263 -              val errs = cat_lines(map (string_of_term sg) us)
   1.264 -          in show_brackets := old_show_brackets;
   1.265 -             error("Error: More than one term is type correct:\n" ^ errs)
   1.266 -          end)
   1.267 +        else (); res)
   1.268 +    | Errs errs => (warn (); error (cat_lines errs))
   1.269 +    | Ambigs us =>
   1.270 +        (warn (); error ("Error: More than one term is type correct:\n" ^
   1.271 +          (cat_lines (map (Pretty.string_of o prt) us)))))
   1.272    end;
   1.273  
   1.274  
   1.275 +
   1.276  (** extend signature **)    (*exception ERROR*)
   1.277  
   1.278  (** signature extension functions **)  (*exception ERROR*)
   1.279 @@ -461,7 +451,7 @@
   1.280  
   1.281  fun ext_cnsts rd_const syn_only prmode (syn, tsig, ctab) raw_consts =
   1.282    let
   1.283 -    fun prep_const (c, ty, mx) = 
   1.284 +    fun prep_const (c, ty, mx) =
   1.285       (c, compress_type (Type.varifyT (Type.cert_typ tsig (Type.no_tvars ty))), mx)
   1.286         handle TYPE (msg, _, _)
   1.287           => (writeln msg; err_in_const (Syntax.const_name c mx));
     2.1 --- a/src/Pure/theory.ML	Thu Apr 17 18:45:43 1997 +0200
     2.2 +++ b/src/Pure/theory.ML	Thu Apr 17 18:46:58 1997 +0200
     2.3 @@ -169,7 +169,7 @@
     2.4  fun cert_axm sg (name, raw_tm) =
     2.5    let
     2.6      val (t, T, _) = Sign.certify_term sg raw_tm
     2.7 -      handle TYPE arg => error (Sign.exn_type_msg sg arg)
     2.8 +      handle TYPE (msg, _, _) => error msg
     2.9  	   | TERM (msg, _) => error msg;
    2.10    in
    2.11      assert (T = propT) "Term not of type prop";
     3.1 --- a/src/Pure/thm.ML	Thu Apr 17 18:45:43 1997 +0200
     3.2 +++ b/src/Pure/thm.ML	Thu Apr 17 18:46:58 1997 +0200
     3.3 @@ -260,7 +260,7 @@
     3.4      val (_, t', tye) =
     3.5            Sign.infer_types sign types sorts used freeze (ts, T');
     3.6      val ct = cterm_of sign t'
     3.7 -      handle TYPE arg => error (Sign.exn_type_msg sign arg)
     3.8 +      handle TYPE (msg, _, _) => error msg
     3.9             | TERM (msg, _) => error msg;
    3.10    in (ct, tye) end;
    3.11  
    3.12 @@ -271,18 +271,20 @@
    3.13    not practical.*)
    3.14  fun read_cterms sign (bs, Ts) =
    3.15    let
    3.16 -    val {tsig, syn, ...} = Sign.rep_sg sign
    3.17 -    fun read (b,T) =
    3.18 -        case Syntax.read syn T b of
    3.19 -            [t] => t
    3.20 -          | _   => error("Error or ambiguity in parsing of " ^ b)
    3.21 -    val (us,_) = Type.infer_types(tsig, Sign.const_type sign, 
    3.22 -                                  K None, K None, 
    3.23 -                                  [], true, 
    3.24 -                                  map (Sign.certify_typ sign) Ts, 
    3.25 -                                  ListPair.map read (bs,Ts))
    3.26 -  in  map (cterm_of sign) us  end
    3.27 -  handle TYPE arg => error (Sign.exn_type_msg sign arg)
    3.28 +    val {tsig, syn, ...} = Sign.rep_sg sign;
    3.29 +    fun read (b, T) =
    3.30 +      (case Syntax.read syn T b of
    3.31 +        [t] => t
    3.32 +      | _  => error ("Error or ambiguity in parsing of " ^ b));
    3.33 +
    3.34 +    val prt = setmp Syntax.show_brackets true (Sign.pretty_term sign);
    3.35 +    val prT = Sign.pretty_typ sign;
    3.36 +    val (us, _) =
    3.37 +      Type.infer_types prt prT tsig (Sign.const_type sign)
    3.38 +        (K None) (K None) [] true (map (Sign.certify_typ sign) Ts)
    3.39 +        (ListPair.map read (bs, Ts));
    3.40 +  in map (cterm_of sign) us end
    3.41 +  handle TYPE (msg, _, _) => error msg
    3.42         | TERM (msg, _) => error msg;
    3.43  
    3.44  
     4.1 --- a/src/Pure/type.ML	Thu Apr 17 18:45:43 1997 +0200
     4.2 +++ b/src/Pure/type.ML	Thu Apr 17 18:46:58 1997 +0200
     4.3 @@ -65,8 +65,9 @@
     4.4    val get_sort: type_sig -> (indexname -> sort option) -> (indexname * sort) list
     4.5      -> indexname -> sort
     4.6    val constrain: term -> typ -> term
     4.7 -  val infer_types: type_sig * (string -> typ option) * (indexname -> typ option)
     4.8 -    * (indexname -> sort option) * string list * bool * typ list * term list
     4.9 +  val infer_types: (term -> Pretty.T) -> (typ -> Pretty.T)
    4.10 +    -> type_sig -> (string -> typ option) -> (indexname -> typ option)
    4.11 +    -> (indexname -> sort option) -> string list -> bool -> typ list -> term list
    4.12      -> term list * (indexname * typ) list
    4.13  end;
    4.14  
    4.15 @@ -871,14 +872,14 @@
    4.16      "?" :: _ => true
    4.17    | _ => false);
    4.18  
    4.19 -fun infer_types (tsig, const_type, def_type, def_sort, used, freeze, pat_Ts, raw_ts) =
    4.20 +fun infer_types prt prT tsig const_type def_type def_sort used freeze pat_Ts raw_ts =
    4.21    let
    4.22      val TySg {classrel, arities, ...} = tsig;
    4.23      val pat_Ts' = map (cert_typ tsig) pat_Ts;
    4.24      val raw_ts' =
    4.25        map (decode_types tsig (is_some o const_type) def_type def_sort) raw_ts;
    4.26      val (ts, Ts, unifier) =
    4.27 -      TypeInfer.infer_types const_type classrel arities used freeze
    4.28 +      TypeInfer.infer_types prt prT const_type classrel arities used freeze
    4.29          q_is_param raw_ts' pat_Ts';
    4.30    in
    4.31      (ts, unifier)
     5.1 --- a/src/Pure/type_infer.ML	Thu Apr 17 18:45:43 1997 +0200
     5.2 +++ b/src/Pure/type_infer.ML	Thu Apr 17 18:46:58 1997 +0200
     5.3 @@ -7,7 +7,8 @@
     5.4  
     5.5  signature TYPE_INFER =
     5.6  sig
     5.7 -  val infer_types: (string -> typ option) -> Sorts.classrel -> Sorts.arities
     5.8 +  val infer_types: (term -> Pretty.T) -> (typ -> Pretty.T)
     5.9 +    -> (string -> typ option) -> Sorts.classrel -> Sorts.arities
    5.10      -> string list -> bool -> (indexname -> bool) -> term list -> typ list
    5.11      -> term list * typ list * (indexname * typ) list
    5.12  end;
    5.13 @@ -257,7 +258,7 @@
    5.14  
    5.15      fun not_in_sort x S' S =
    5.16        "Type variable " ^ x ^ "::" ^ Sorts.str_of_sort S' ^ " not in sort " ^
    5.17 -        Sorts.str_of_sort S;
    5.18 +        Sorts.str_of_sort S ^ ".";
    5.19  
    5.20      fun meet _ [] = ()
    5.21        | meet (Link (r as (ref (Param S')))) S =
    5.22 @@ -298,9 +299,10 @@
    5.23        | unif (Link (ref T)) U = unif T U
    5.24        | unif T (Link (ref U)) = unif T U
    5.25        | unif (PType (a, Ts)) (PType (b, Us)) =
    5.26 -          if a <> b then raise NO_UNIFIER ("Clash of " ^ a ^ ", " ^ b ^ "!")
    5.27 +          if a <> b then
    5.28 +            raise NO_UNIFIER ("Clash of types " ^ quote a ^ " and " ^ quote b ^ ".")
    5.29            else seq2 unif Ts Us
    5.30 -      | unif T U = if T = U then () else raise NO_UNIFIER "Unification failed!";
    5.31 +      | unif T U = if T = U then () else raise NO_UNIFIER "";
    5.32  
    5.33    in unif end;
    5.34  
    5.35 @@ -310,26 +312,63 @@
    5.36  
    5.37  (* infer *)                                     (*DESTRUCTIVE*)
    5.38  
    5.39 -fun infer classrel arities =
    5.40 +fun infer prt prT classrel arities =
    5.41    let
    5.42 -    val unif = unify classrel arities;
    5.43 +    (* errors *)
    5.44  
    5.45 -    fun err msg1 msg2 bs ts Ts =
    5.46 +    fun unif_failed msg =
    5.47 +      "Type unification failed" ^ (if msg = "" then "." else ": " ^ msg) ^ "\n";
    5.48 +
    5.49 +    val str_of = Pretty.string_of;
    5.50 +
    5.51 +    fun prep_output bs ts Ts =
    5.52        let
    5.53          val (Ts_bTs', ts') = typs_terms_of [] PTFree "??" (Ts @ map snd bs, ts);
    5.54          val len = length Ts;
    5.55          val Ts' = take (len, Ts_bTs');
    5.56          val xs = map Free (map fst bs ~~ drop (len, Ts_bTs'));
    5.57          val ts'' = map (fn t => subst_bounds (xs, t)) ts';
    5.58 -      in
    5.59 -        raise_type (msg1 ^ " " ^ msg2) Ts' ts''
    5.60 -      end;
    5.61 +      in (ts'', Ts') end;
    5.62 +
    5.63 +    fun err_loose i =
    5.64 +      raise_type ("Loose bound variable: B." ^ string_of_int i) [] [];
    5.65 +
    5.66 +    fun err_appl msg bs t T U_to_V u U =
    5.67 +      let
    5.68 +        val ([t', u'], [T', U_to_V', U']) = prep_output bs [t, u] [T, U_to_V, U];
    5.69 +        val text = cat_lines
    5.70 +         [unif_failed msg,
    5.71 +          "Type error in application:",
    5.72 +          "",
    5.73 +          str_of (Pretty.block [Pretty.str "operator:     ", Pretty.brk 1, prt t',
    5.74 +            Pretty.str " :: ", prT T']),
    5.75 +          str_of (Pretty.block [Pretty.str "expected type:", Pretty.brk 1, prT U_to_V']),
    5.76 +          "",
    5.77 +          str_of (Pretty.block [Pretty.str "operand:      ", Pretty.brk 1, prt u',
    5.78 +            Pretty.str " :: ", prT U']), ""];
    5.79 +      in raise_type text [T', U_to_V', U'] [t', u'] end;
    5.80 +
    5.81 +    fun err_constraint msg bs t T U =
    5.82 +      let
    5.83 +        val ([t'], [T', U']) = prep_output bs [t] [T, U];
    5.84 +        val text = cat_lines
    5.85 +         [unif_failed msg,
    5.86 +          "Cannot meet type constraint:",
    5.87 +          "",
    5.88 +          str_of (Pretty.block [Pretty.str "term:          ", Pretty.brk 1, prt t',
    5.89 +            Pretty.str " :: ", prT T']),
    5.90 +          str_of (Pretty.block [Pretty.str "expected type: ", Pretty.brk 1, prT U']), ""];
    5.91 +      in raise_type text [T', U'] [t'] end;
    5.92 +
    5.93 +
    5.94 +    (* main *)
    5.95 +
    5.96 +    val unif = unify classrel arities;
    5.97  
    5.98      fun inf _ (PConst (_, T)) = T
    5.99        | inf _ (PFree (_, T)) = T
   5.100        | inf _ (PVar (_, T)) = T
   5.101 -      | inf bs (PBound i) = snd (nth_elem (i, bs)
   5.102 -          handle LIST _ => raise_type "Loose bound variable" [] [Bound i])
   5.103 +      | inf bs (PBound i) = snd (nth_elem (i, bs) handle LIST _ => err_loose i)
   5.104        | inf bs (PAbs (x, T, t)) = PType ("fun", [T, inf ((x, T) :: bs) t])
   5.105        | inf bs (PAppl (t, u)) =
   5.106            let
   5.107 @@ -338,12 +377,11 @@
   5.108              val V = mk_param [];
   5.109              val U_to_V = PType ("fun", [U, V]);
   5.110              val _ = unif U_to_V T handle NO_UNIFIER msg =>
   5.111 -              err msg "Bad function application." bs [PAppl (t, u)] [U_to_V, U];
   5.112 +              err_appl msg bs t T U_to_V u U;
   5.113            in V end
   5.114        | inf bs (Constraint (t, U)) =
   5.115            let val T = inf bs t in
   5.116 -            unif T U handle NO_UNIFIER msg =>
   5.117 -              err msg "Cannot meet type constraint." bs [t] [T, U];
   5.118 +            unif T U handle NO_UNIFIER msg => err_constraint msg bs t T U;
   5.119              T
   5.120            end;
   5.121  
   5.122 @@ -352,7 +390,7 @@
   5.123  
   5.124  (* infer_types *)
   5.125  
   5.126 -fun infer_types const_type classrel arities used freeze is_param ts Ts =
   5.127 +fun infer_types prt prT const_type classrel arities used freeze is_param ts Ts =
   5.128    let
   5.129      (*convert to preterms/typs*)
   5.130      val (Tps, Ts') = pretyps_of (K true) ([], Ts);
   5.131 @@ -360,7 +398,7 @@
   5.132  
   5.133      (*run type inference*)
   5.134      val tTs' = ListPair.map Constraint (ts', Ts');
   5.135 -    val _ = seq (fn t => (infer classrel arities t; ())) tTs';
   5.136 +    val _ = seq (fn t => (infer prt prT classrel arities t; ())) tTs';
   5.137  
   5.138      (*collect result unifier*)
   5.139      fun ch_var (xi, Link (r as ref (Param S))) = (r := PTVar (xi, S); None)