Mercurial > urweb

comparison src/elab_err.sml @ 1303:c7b9a33c26c8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Hopeful fix for the Great Unification Bug
author Adam Chlipala <adam@chlipala.net>
date Sun, 10 Oct 2010 14:41:03 -0400
parents 26197c957ad6
children 3a845f2ce9e9
comparison
equal deleted inserted replaced
1302:d008c4c43a0a 1303:c7b9a33c26c8
1 (* Copyright (c) 2008, Adam Chlipala 1 (* Copyright (c) 2008-2010, Adam Chlipala
2 * All rights reserved. 2 * All rights reserved.
3 * 3 *
4 * Redistribution and use in source and binary forms, with or without 4 * Redistribution and use in source and binary forms, with or without
5 * modification, are permitted provided that the following conditions are met: 5 * modification, are permitted provided that the following conditions are met:
6 * 6 *
110 | ProjMismatch (c, k) => 110 | ProjMismatch (c, k) =>
111 (ErrorMsg.errorAt (#2 c) "Projection from non-tuple constructor"; 111 (ErrorMsg.errorAt (#2 c) "Projection from non-tuple constructor";
112 eprefaces' [("Constructor", p_con env c), 112 eprefaces' [("Constructor", p_con env c),
113 ("Kind", p_kind env k)]) 113 ("Kind", p_kind env k)])
114 114
115
116 datatype cunify_error = 115 datatype cunify_error =
117 CKind of kind * kind * kunify_error 116 CKind of kind * kind * kunify_error
118 | COccursCheckFailed of con * con 117 | COccursCheckFailed of con * con
119 | CIncompatible of con * con 118 | CIncompatible of con * con
120 | CExplicitness of con * con 119 | CExplicitness of con * con
121 | CKindof of kind * con * string 120 | CKindof of kind * con * string
122 | CRecordFailure of con * con * (con * con * con) option 121 | CRecordFailure of con * con * (con * con * con) option
122 | TooLifty of ErrorMsg.span * ErrorMsg.span
123 | TooUnify of con * con
123 124
124 fun cunifyError env err = 125 fun cunifyError env err =
125 case err of 126 case err of
126 CKind (k1, k2, kerr) => 127 CKind (k1, k2, kerr) =>
127 (eprefaces "Kind unification failure" 128 (eprefaces "Kind unification failure"
152 NONE => [] 153 NONE => []
153 | SOME (nm, t1, t2) => 154 | SOME (nm, t1, t2) =>
154 [("Field", p_con env nm), 155 [("Field", p_con env nm),
155 ("Value 1", p_con env t1), 156 ("Value 1", p_con env t1),
156 ("Value 2", p_con env t2)])) 157 ("Value 2", p_con env t2)]))
158 | TooLifty (loc1, loc2) =>
159 (ErrorMsg.errorAt loc1 "Can't unify two unification variables that both have suspended liftings";
160 eprefaces' [("Other location", Print.PD.string (ErrorMsg.spanToString loc2))])
161 | TooUnify (c1, c2) =>
162 (ErrorMsg.errorAt (#2 c1) "Substitution in constructor is blocked by a too-deep unification variable";
163 eprefaces' [("Replacement", p_con env c1),
164 ("Body", p_con env c2)])
157 165
158 datatype exp_error = 166 datatype exp_error =
159 UnboundExp of ErrorMsg.span * string 167 UnboundExp of ErrorMsg.span * string
160 | UnboundStrInExp of ErrorMsg.span * string 168 | UnboundStrInExp of ErrorMsg.span * string
161 | Unify of exp * con * con * cunify_error 169 | Unify of exp * con * con * cunify_error