comparison src/elab_err.sml @ 1582:dfb38a333816

Harmonize have/need terminology in error messages; display canceled record summaries on errors
author Adam Chlipala <adam@chlipala.net>
date Thu, 27 Oct 2011 08:36:31 -0400
parents 001638622c4f
children c37d8341940a
comparison
equal deleted inserted replaced
1581:1ced338f691a 1582:dfb38a333816
125 125
126 fun cunifyError env err = 126 fun cunifyError env err =
127 case err of 127 case err of
128 CKind (k1, k2, kerr) => 128 CKind (k1, k2, kerr) =>
129 (eprefaces "Kind unification failure" 129 (eprefaces "Kind unification failure"
130 [("Kind 1", p_kind env k1), 130 [("Have", p_kind env k1),
131 ("Kind 2", p_kind env k2)]; 131 ("Need", p_kind env k2)];
132 kunifyError env kerr) 132 kunifyError env kerr)
133 | COccursCheckFailed (c1, c2) => 133 | COccursCheckFailed (c1, c2) =>
134 eprefaces "Constructor occurs check failed" 134 eprefaces "Constructor occurs check failed"
135 [("Con 1", p_con env c1), 135 [("Have", p_con env c1),
136 ("Con 2", p_con env c2)] 136 ("Need", p_con env c2)]
137 | CIncompatible (c1, c2) => 137 | CIncompatible (c1, c2) =>
138 eprefaces "Incompatible constructors" 138 eprefaces "Incompatible constructors"
139 [("Con 1", p_con env c1), 139 [("Have", p_con env c1),
140 ("Con 2", p_con env c2)] 140 ("Need", p_con env c2)]
141 | CExplicitness (c1, c2) => 141 | CExplicitness (c1, c2) =>
142 eprefaces "Differing constructor function explicitness" 142 eprefaces "Differing constructor function explicitness"
143 [("Con 1", p_con env c1), 143 [("Have", p_con env c1),
144 ("Con 2", p_con env c2)] 144 ("Need", p_con env c2)]
145 | CKindof (k, c, expected) => 145 | CKindof (k, c, expected) =>
146 eprefaces ("Unexpected kind for kindof calculation (expecting " ^ expected ^ ")") 146 eprefaces ("Unexpected kind for kindof calculation (expecting " ^ expected ^ ")")
147 [("Kind", p_kind env k), 147 [("Kind", p_kind env k),
148 ("Con", p_con env c)] 148 ("Con", p_con env c)]
149 | CRecordFailure (c1, c2, fo) => 149 | CRecordFailure (c1, c2, fo) =>
150 (eprefaces "Can't unify record constructors" 150 (eprefaces "Can't unify record constructors"
151 (("Summary 1", p_con env c1) 151 (("Have", p_con env c1)
152 :: ("Summary 2", p_con env c2) 152 :: ("Need", p_con env c2)
153 :: (case fo of 153 :: (case fo of
154 NONE => [] 154 NONE => []
155 | SOME (nm, t1, t2, _) => 155 | SOME (nm, t1, t2, _) =>
156 [("Field", p_con env nm), 156 [("Field", p_con env nm),
157 ("Value 1", p_con env t1), 157 ("Value 1", p_con env t1),
208 (ErrorMsg.errorAt (#2 e) ("Expression is not a " ^ variety); 208 (ErrorMsg.errorAt (#2 e) ("Expression is not a " ^ variety);
209 eprefaces' [("Expression", p_exp env e), 209 eprefaces' [("Expression", p_exp env e),
210 ("Type", p_con env t)]) 210 ("Type", p_con env t)])
211 | IncompatibleCons (c1, c2) => 211 | IncompatibleCons (c1, c2) =>
212 (ErrorMsg.errorAt (#2 c1) "Incompatible constructors"; 212 (ErrorMsg.errorAt (#2 c1) "Incompatible constructors";
213 eprefaces' [("Con 1", p_con env c1), 213 eprefaces' [("Have", p_con env c1),
214 ("Con 2", p_con env c2)]) 214 ("Need", p_con env c2)])
215 | DuplicatePatternVariable (loc, s) => 215 | DuplicatePatternVariable (loc, s) =>
216 ErrorMsg.errorAt loc ("Duplicate pattern variable " ^ s) 216 ErrorMsg.errorAt loc ("Duplicate pattern variable " ^ s)
217 | PatUnify (p, c1, c2, uerr) => 217 | PatUnify (p, c1, c2, uerr) =>
218 (ErrorMsg.errorAt (#2 p) "Unification failure for pattern"; 218 (ErrorMsg.errorAt (#2 p) "Unification failure for pattern";
219 eprefaces' [("Pattern", p_pat env p), 219 eprefaces' [("Pattern", p_pat env p),