+fun ununify (tAll as (t, _)) =
+ case t of
+ TUnif (_, ref (SOME t)) => ununify t
+ | _ => tAll
+
+fun normalize_error err =
+ case err of
+ WrongType (s, e, t1, t2, ueo) =>
+ WrongType (s, e, ununify t1, ununify t2, ueo)
+ | WrongForm (s1, s2, e, t, ueo) =>
+ WrongForm (s1, s2, e, ununify t, ueo)
+ | UnboundVariable _ => err
+ | WrongPred _ => err
+
+fun describe_type_error loc te =
+ let
+ val te = normalize_error te
+ in
+ describe_type_error' loc te;
+ Option.app (fn s => (print "Hint Monster says:\n";
+ print s;
+ print "\n"))
+ (hint te)
+ end
+