improved type checking errors;
authorwenzelm
Wed Jul 09 16:54:17 1997 +0200 (1997-07-09)
changeset 351024d235feeb2a
parent 3509 db03a42120bf
child 3511 da4dd8b7ced4
improved type checking errors;
src/Pure/type_infer.ML
     1.1 --- a/src/Pure/type_infer.ML	Wed Jul 09 16:53:53 1997 +0200
     1.2 +++ b/src/Pure/type_infer.ML	Wed Jul 09 16:54:17 1997 +0200
     1.3 @@ -333,20 +333,22 @@
     1.4      fun err_loose i =
     1.5        raise_type ("Loose bound variable: B." ^ string_of_int i) [] [];
     1.6  
     1.7 -    fun err_appl msg bs t T U_to_V u U =
     1.8 +    fun err_appl msg bs t T u U =
     1.9        let
    1.10 -        val ([t', u'], [T', U_to_V', U']) = prep_output bs [t, u] [T, U_to_V, U];
    1.11 +        val ([t', u'], [T', U']) = prep_output bs [t, u] [T, U];
    1.12 +        val why =
    1.13 +          (case T' of
    1.14 +            Type ("fun", _) => "Incompatible operand type."
    1.15 +          | _ => "Operator not of function type.");
    1.16          val text = cat_lines
    1.17           [unif_failed msg,
    1.18 -          "Type error in application:",
    1.19 +          "Type error in application: " ^ why,
    1.20            "",
    1.21 -          str_of (Pretty.block [Pretty.str "operator:", Pretty.brk 2, prt t',
    1.22 +          str_of (Pretty.block [Pretty.str "Operator:", Pretty.brk 2, prt t',
    1.23              Pretty.str " :: ", prT T']),
    1.24 -          str_of (Pretty.block [Pretty.str "expected:", Pretty.brk 2, prT U_to_V']),
    1.25 -          "",
    1.26 -          str_of (Pretty.block [Pretty.str "operand:", Pretty.brk 3, prt u',
    1.27 +          str_of (Pretty.block [Pretty.str "Operand:", Pretty.brk 3, prt u',
    1.28              Pretty.str " :: ", prT U']), ""];
    1.29 -      in raise_type text [T', U_to_V', U'] [t', u'] end;
    1.30 +      in raise_type text [T', U'] [t', u'] end;
    1.31  
    1.32      fun err_constraint msg bs t T U =
    1.33        let
    1.34 @@ -355,9 +357,9 @@
    1.35           [unif_failed msg,
    1.36            "Cannot meet type constraint:",
    1.37            "",
    1.38 -          str_of (Pretty.block [Pretty.str "term:", Pretty.brk 2, prt t',
    1.39 +          str_of (Pretty.block [Pretty.str "Term:", Pretty.brk 2, prt t',
    1.40              Pretty.str " :: ", prT T']),
    1.41 -          str_of (Pretty.block [Pretty.str "type:", Pretty.brk 2, prT U']), ""];
    1.42 +          str_of (Pretty.block [Pretty.str "Type:", Pretty.brk 2, prT U']), ""];
    1.43        in raise_type text [T', U'] [t'] end;
    1.44  
    1.45  
    1.46 @@ -376,8 +378,7 @@
    1.47              val U = inf bs u;
    1.48              val V = mk_param [];
    1.49              val U_to_V = PType ("fun", [U, V]);
    1.50 -            val _ = unif U_to_V T handle NO_UNIFIER msg =>
    1.51 -              err_appl msg bs t T U_to_V u U;
    1.52 +            val _ = unif U_to_V T handle NO_UNIFIER msg => err_appl msg bs t T u U;
    1.53            in V end
    1.54        | inf bs (Constraint (t, U)) =
    1.55            let val T = inf bs t in