-datatype unification_error =
- UnifyPred of pred * pred
- | UnifyTyp of typ * typ
- | UnifyOccurs of string * typ
-
-exception Unify of unification_error
-
-datatype type_error =
- WrongType of string * exp * typ * typ * unification_error option
- | WrongForm of string * string * exp * typ * unification_error option
- | UnboundVariable of string
- | WrongPred of string * pred * pred
-
-fun preface (s, d) = printd (PD.hovBox (PD.PPS.Rel 0,
- [PD.string s, PD.space 1, d]))
-
-fun describe_unification_error t ue =
- case ue of
- UnifyPred (p1, p2) =>
- (print "Reason: Incompatible contexts.\n";
- preface ("Have:", p_pred p1);
- preface ("Need:", p_pred p2))
- | UnifyTyp (t1, t2) =>
- if eqTy (t, t1) then
- ()
- else
- (print "Reason: Incompatible types.\n";
- preface ("Have:", p_typ t1);
- preface ("Need:", p_typ t2))
- | UnifyOccurs (name, t') =>
- if eqTy (t, t') then
- ()
- else
- (print "Reason: Occurs check failed for ";
- print name;
- print " in:\n";
- printd (p_typ t))
-
-fun describe_type_error loc te =
- case te of
- WrongType (place, e, t1, t2, ueo) =>
- (ErrorMsg.error (SOME loc) (place ^ " has wrong type.");
- preface (" Expression:", p_exp e);
- preface ("Actual type:", p_typ t1);
- preface ("Needed type:", p_typ t2);
- Option.app (describe_unification_error t1) ueo)
- | WrongForm (place, form, e, t, ueo) =>
- (ErrorMsg.error (SOME loc) (place ^ " has a non-" ^ form ^ " type.");
- preface ("Expression:", p_exp e);
- preface (" Type:", p_typ t);
- Option.app (describe_unification_error t) ueo)
- | UnboundVariable name =>
- ErrorMsg.error (SOME loc) ("Unbound variable " ^ name ^ ".\n")
- | WrongPred (place, p1, p2) =>
- (ErrorMsg.error (SOME loc) ("Context incompatibility for " ^ place ^ ".");
- preface ("Have:", p_pred p1);
- preface ("Need:", p_pred p2))
-