1structure typecheck_error =
2struct
3  datatype tcheck_error =
4           ConstrainFail of Term.term * Type.hol_type * string
5         | AppFail of Term.term * Term.term * string
6         | OvlNoType of string * Type.hol_type
7         | OvlTooMany
8         | OvlFail
9         | Misc of string
10
11  type error = tcheck_error * locn.locn
12  fun errorMsg tc =
13    case tc of
14        ConstrainFail (_,_,msg) => msg
15      | AppFail (_,_,msg) => msg
16      | OvlNoType(s,_) =>
17        ("Couldn't infer type for overloaded name "^s)
18      | OvlFail => "Overloading constraints were unsatisfiable"
19      | OvlTooMany =>
20          "There was more than one resolution of overloaded constants"
21      | Misc s => s
22
23  local
24    open Feedback
25  in
26  fun mkExn (tc, loc) =
27    mk_HOL_ERRloc "Preterm" "type-analysis" loc (errorMsg tc)
28
29  end (* local *)
30
31
32end (* struct *)
33