Mercurial > urweb

comparison src/elab_err.sml @ 1359:e525ad571e15

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Recursive record unification errors, for more detail
author Adam Chlipala <adam@chlipala.net>
date Thu, 23 Dec 2010 11:23:31 -0500
parents 3a845f2ce9e9
children 001638622c4f
comparison
equal deleted inserted replaced
1358:32c8a3509369 1359:e525ad571e15
116 CKind of kind * kind * kunify_error 116 CKind of kind * kind * kunify_error
117 | COccursCheckFailed of con * con 117 | COccursCheckFailed of con * con
118 | CIncompatible of con * con 118 | CIncompatible of con * con
119 | CExplicitness of con * con 119 | CExplicitness of con * con
120 | CKindof of kind * con * string 120 | CKindof of kind * con * string
121 | CRecordFailure of con * con * (con * con * con) option 121 | CRecordFailure of con * con * (con * con * con * cunify_error option) option
122 | TooLifty of ErrorMsg.span * ErrorMsg.span 122 | TooLifty of ErrorMsg.span * ErrorMsg.span
123 | TooUnify of con * con 123 | TooUnify of con * con
124 | TooDeep 124 | TooDeep
125 125
126 fun cunifyError env err = 126 fun cunifyError env err =
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 (("Summary 1", p_con env c1)
152 :: ("Summary 2", p_con env c2) 152 :: ("Summary 2", 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),
158 ("Value 2", p_con env t2)])) 158 ("Value 2", p_con env t2)]));
159 case fo of
160 SOME (_, _, _, SOME err') => cunifyError env err'
161 | _ => ())
159 | TooLifty (loc1, loc2) => 162 | TooLifty (loc1, loc2) =>
160 (ErrorMsg.errorAt loc1 "Can't unify two unification variables that both have suspended liftings"; 163 (ErrorMsg.errorAt loc1 "Can't unify two unification variables that both have suspended liftings";
161 eprefaces' [("Other location", Print.PD.string (ErrorMsg.spanToString loc2))]) 164 eprefaces' [("Other location", Print.PD.string (ErrorMsg.spanToString loc2))])
162 | TooUnify (c1, c2) => 165 | TooUnify (c1, c2) =>
163 (ErrorMsg.errorAt (#2 c1) "Substitution in constructor is blocked by a too-deep unification variable"; 166 (ErrorMsg.errorAt (#2 c1) "Substitution in constructor is blocked by a too-deep unification variable";