Mercurial > urweb

annotate src/elab_err.sml @ 2043:e762c96fffb7

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Small tweak to ordering of unification rules, to support better record matching
author Adam Chlipala <adam@chlipala.net>
date Tue, 29 Jul 2014 14:38:50 -0400
parents 799be3911ce3
children
rev   line source
adam@1719 1 (* Copyright (c) 2008-2010, 2012, Adam Chlipala
adamc@329 2 * All rights reserved.
adamc@329 3 *
adamc@329 4 * Redistribution and use in source and binary forms, with or without
adamc@329 5 * modification, are permitted provided that the following conditions are met:
adamc@329 6 *
adamc@329 7 * - Redistributions of source code must retain the above copyright notice,
adamc@329 8 * this list of conditions and the following disclaimer.
adamc@329 9 * - Redistributions in binary form must reproduce the above copyright notice,
adamc@329 10 * this list of conditions and the following disclaimer in the documentation
adamc@329 11 * and/or other materials provided with the distribution.
adamc@329 12 * - The names of contributors may not be used to endorse or promote products
adamc@329 13 * derived from this software without specific prior written permission.
adamc@329 14 *
adamc@329 15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
adamc@329 16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
adamc@329 17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
adamc@329 18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
adamc@329 19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
adamc@329 20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
adamc@329 21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
adamc@329 22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
adamc@329 23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
adamc@329 24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
adamc@329 25 * POSSIBILITY OF SUCH DAMAGE.
adamc@329 26 *)
adamc@329 27
adamc@329 28 structure ElabErr :> ELAB_ERR = struct
adamc@329 29
adamc@329 30 structure L = Source
adamc@329 31 open Elab
adamc@329 32
adamc@329 33 structure E = ElabEnv
adamc@329 34 structure U = ElabUtil
adamc@329 35
adamc@329 36 open Print
adamc@329 37 structure P = ElabPrint
adamc@329 38
adamc@329 39 val p_kind = P.p_kind
adamc@623 40
adamc@623 41 datatype kind_error =
adamc@623 42 UnboundKind of ErrorMsg.span * string
adamc@623 43
adamc@623 44 fun kindError env err =
adamc@623 45 case err of
adamc@623 46 UnboundKind (loc, s) =>
adamc@623 47 ErrorMsg.errorAt loc ("Unbound kind variable " ^ s)
adamc@329 48
adamc@329 49 datatype kunify_error =
adamc@329 50 KOccursCheckFailed of kind * kind
adamc@329 51 | KIncompatible of kind * kind
adam@1639 52 | KScope of kind * kind
adamc@329 53
adamc@623 54 fun kunifyError env err =
adamc@329 55 case err of
adamc@329 56 KOccursCheckFailed (k1, k2) =>
adamc@329 57 eprefaces "Kind occurs check failed"
adamc@623 58 [("Kind 1", p_kind env k1),
adamc@623 59 ("Kind 2", p_kind env k2)]
adamc@329 60 | KIncompatible (k1, k2) =>
adamc@329 61 eprefaces "Incompatible kinds"
adamc@623 62 [("Kind 1", p_kind env k1),
adamc@623 63 ("Kind 2", p_kind env k2)]
adam@1639 64 | KScope (k1, k2) =>
adam@1639 65 eprefaces "Scoping prevents kind unification"
adam@1639 66 [("Kind 1", p_kind env k1),
adam@1639 67 ("Kind 2", p_kind env k2)]
adamc@329 68
adam@1714 69 fun p_con env c = P.p_con env (ElabOps.reduceCon env c)
adamc@329 70
adamc@329 71 datatype con_error =
adamc@329 72 UnboundCon of ErrorMsg.span * string
adamc@329 73 | UnboundDatatype of ErrorMsg.span * string
adamc@329 74 | UnboundStrInCon of ErrorMsg.span * string
adam@1719 75 | WrongKind of con * kind * kind * E.env * kunify_error
adamc@329 76 | DuplicateField of ErrorMsg.span * string
adamc@329 77 | ProjBounds of con * int
adamc@329 78 | ProjMismatch of con * kind
adamc@329 79
adamc@329 80 fun conError env err =
adamc@329 81 case err of
adamc@329 82 UnboundCon (loc, s) =>
adamc@329 83 ErrorMsg.errorAt loc ("Unbound constructor variable " ^ s)
adamc@329 84 | UnboundDatatype (loc, s) =>
adamc@329 85 ErrorMsg.errorAt loc ("Unbound datatype " ^ s)
adamc@329 86 | UnboundStrInCon (loc, s) =>
adamc@329 87 ErrorMsg.errorAt loc ("Unbound structure " ^ s)
adam@1719 88 | WrongKind (c, k1, k2, env', kerr) =>
adamc@329 89 (ErrorMsg.errorAt (#2 c) "Wrong kind";
adamc@329 90 eprefaces' [("Constructor", p_con env c),
adamc@623 91 ("Have kind", p_kind env k1),
adamc@623 92 ("Need kind", p_kind env k2)];
adam@1719 93 kunifyError env' kerr)
adamc@329 94 | DuplicateField (loc, s) =>
adamc@329 95 ErrorMsg.errorAt loc ("Duplicate record field " ^ s)
adamc@329 96 | ProjBounds (c, n) =>
adamc@329 97 (ErrorMsg.errorAt (#2 c) "Out of bounds constructor projection";
adamc@329 98 eprefaces' [("Constructor", p_con env c),
adamc@329 99 ("Index", Print.PD.string (Int.toString n))])
adamc@329 100 | ProjMismatch (c, k) =>
adamc@329 101 (ErrorMsg.errorAt (#2 c) "Projection from non-tuple constructor";
adamc@329 102 eprefaces' [("Constructor", p_con env c),
adamc@623 103 ("Kind", p_kind env k)])
adamc@329 104
adamc@329 105 datatype cunify_error =
adam@1719 106 CKind of kind * kind * E.env * kunify_error
adamc@329 107 | COccursCheckFailed of con * con
adamc@329 108 | CIncompatible of con * con
adamc@329 109 | CExplicitness of con * con
adamc@413 110 | CKindof of kind * con * string
adam@1719 111 | CRecordFailure of con * con * (con * con * con * (E.env * cunify_error) option) option
adam@1303 112 | TooLifty of ErrorMsg.span * ErrorMsg.span
adam@1303 113 | TooUnify of con * con
adam@1306 114 | TooDeep
adam@1639 115 | CScope of con * con
adamc@329 116
adam@1719 117 fun cunifyError env err : unit =
adamc@329 118 case err of
adam@1719 119 CKind (k1, k2, env', kerr) =>
adamc@329 120 (eprefaces "Kind unification failure"
adam@1582 121 [("Have", p_kind env k1),
adam@1582 122 ("Need", p_kind env k2)];
adam@1719 123 kunifyError env' kerr)
adamc@329 124 | COccursCheckFailed (c1, c2) =>
adamc@329 125 eprefaces "Constructor occurs check failed"
adam@1582 126 [("Have", p_con env c1),
adam@1582 127 ("Need", p_con env c2)]
adamc@329 128 | CIncompatible (c1, c2) =>
adamc@329 129 eprefaces "Incompatible constructors"
adam@1582 130 [("Have", p_con env c1),
adam@1582 131 ("Need", p_con env c2)]
adamc@329 132 | CExplicitness (c1, c2) =>
adamc@329 133 eprefaces "Differing constructor function explicitness"
adam@1582 134 [("Have", p_con env c1),
adam@1582 135 ("Need", p_con env c2)]
adamc@413 136 | CKindof (k, c, expected) =>
adamc@413 137 eprefaces ("Unexpected kind for kindof calculation (expecting " ^ expected ^ ")")
adamc@623 138 [("Kind", p_kind env k),
adamc@329 139 ("Con", p_con env c)]
adamc@1071 140 | CRecordFailure (c1, c2, fo) =>
adam@1359 141 (eprefaces "Can't unify record constructors"
adam@1582 142 (("Have", p_con env c1)
adam@1582 143 :: ("Need", p_con env c2)
adam@1359 144 :: (case fo of
adam@1359 145 NONE => []
adam@1359 146 | SOME (nm, t1, t2, _) =>
adam@1359 147 [("Field", p_con env nm),
adam@1359 148 ("Value 1", p_con env t1),
adam@1359 149 ("Value 2", p_con env t2)]));
adam@1359 150 case fo of
adam@1719 151 SOME (_, _, _, SOME (env', err')) => cunifyError env' err'
adam@1359 152 | _ => ())
adam@1303 153 | TooLifty (loc1, loc2) =>
adam@1303 154 (ErrorMsg.errorAt loc1 "Can't unify two unification variables that both have suspended liftings";
adam@1303 155 eprefaces' [("Other location", Print.PD.string (ErrorMsg.spanToString loc2))])
adam@1303 156 | TooUnify (c1, c2) =>
adam@1303 157 (ErrorMsg.errorAt (#2 c1) "Substitution in constructor is blocked by a too-deep unification variable";
adam@1303 158 eprefaces' [("Replacement", p_con env c1),
adam@1303 159 ("Body", p_con env c2)])
adam@1306 160 | TooDeep => ErrorMsg.error "Can't reverse-engineer unification variable lifting"
adam@1639 161 | CScope (c1, c2) =>
adam@1639 162 eprefaces "Scoping prevents constructor unification"
adam@1639 163 [("Have", p_con env c1),
adam@1639 164 ("Need", p_con env c2)]
adamc@329 165
adamc@329 166 datatype exp_error =
adamc@329 167 UnboundExp of ErrorMsg.span * string
adamc@329 168 | UnboundStrInExp of ErrorMsg.span * string
adam@1719 169 | Unify of exp * con * con * E.env * cunify_error
adamc@339 170 | Unif of string * ErrorMsg.span * con
adamc@329 171 | WrongForm of string * exp * con
adamc@329 172 | IncompatibleCons of con * con
adamc@329 173 | DuplicatePatternVariable of ErrorMsg.span * string
adam@1719 174 | PatUnify of pat * con * con * E.env * cunify_error
adamc@329 175 | UnboundConstructor of ErrorMsg.span * string list * string
adamc@329 176 | PatHasArg of ErrorMsg.span
adamc@329 177 | PatHasNoArg of ErrorMsg.span
adamc@819 178 | Inexhaustive of ErrorMsg.span * pat
adamc@329 179 | DuplicatePatField of ErrorMsg.span * string
adamc@329 180 | Unresolvable of ErrorMsg.span * con
adamc@329 181 | OutOfContext of ErrorMsg.span * (exp * con) option
adamc@329 182 | IllegalRec of string * exp
adam@2009 183 | IllegalFlex of Source.exp
adamc@329 184
adam@1714 185 val simplExp = U.Exp.mapB {kind = fn _ => fn k => k,
adam@1714 186 con = fn env => fn c => #1 (ElabOps.reduceCon env (c, ErrorMsg.dummySpan)),
adam@1714 187 exp = fn _ => fn e => e,
adam@1714 188 bind = fn (env, U.Exp.RelC (x, k)) => E.pushCRel env x k
adam@1714 189 | (env, U.Exp.NamedC (x, n, k, co)) => E.pushCNamedAs env x n k co
adam@1714 190 | (env, _) => env}
adam@1714 191
adam@1714 192 fun p_exp env e = P.p_exp env (simplExp env e)
adamc@329 193 val p_pat = P.p_pat
adamc@329 194
adamc@329 195 fun expError env err =
adamc@329 196 case err of
adamc@329 197 UnboundExp (loc, s) =>
adamc@329 198 ErrorMsg.errorAt loc ("Unbound expression variable " ^ s)
adamc@329 199 | UnboundStrInExp (loc, s) =>
adamc@329 200 ErrorMsg.errorAt loc ("Unbound structure " ^ s)
adam@1719 201 | Unify (e, c1, c2, env', uerr) =>
adamc@329 202 (ErrorMsg.errorAt (#2 e) "Unification failure";
adamc@329 203 eprefaces' [("Expression", p_exp env e),
adamc@329 204 ("Have con", p_con env c1),
adamc@329 205 ("Need con", p_con env c2)];
adam@1719 206 cunifyError env' uerr)
adamc@339 207 | Unif (action, loc, c) =>
adamc@339 208 (ErrorMsg.errorAt loc ("Unification variable blocks " ^ action);
adamc@329 209 eprefaces' [("Con", p_con env c)])
adamc@329 210 | WrongForm (variety, e, t) =>
adamc@329 211 (ErrorMsg.errorAt (#2 e) ("Expression is not a " ^ variety);
adamc@329 212 eprefaces' [("Expression", p_exp env e),
adamc@329 213 ("Type", p_con env t)])
adamc@329 214 | IncompatibleCons (c1, c2) =>
adamc@329 215 (ErrorMsg.errorAt (#2 c1) "Incompatible constructors";
adam@1582 216 eprefaces' [("Have", p_con env c1),
adam@1582 217 ("Need", p_con env c2)])
adamc@329 218 | DuplicatePatternVariable (loc, s) =>
adamc@329 219 ErrorMsg.errorAt loc ("Duplicate pattern variable " ^ s)
adam@1719 220 | PatUnify (p, c1, c2, env', uerr) =>
adamc@329 221 (ErrorMsg.errorAt (#2 p) "Unification failure for pattern";
adamc@329 222 eprefaces' [("Pattern", p_pat env p),
adamc@329 223 ("Have con", p_con env c1),
adamc@329 224 ("Need con", p_con env c2)];
adam@1719 225 cunifyError env' uerr)
adamc@329 226 | UnboundConstructor (loc, ms, s) =>
adamc@329 227 ErrorMsg.errorAt loc ("Unbound constructor " ^ String.concatWith "." (ms @ [s]) ^ " in pattern")
adamc@329 228 | PatHasArg loc =>
adamc@329 229 ErrorMsg.errorAt loc "Constructor expects no argument but is used with argument"
adamc@329 230 | PatHasNoArg loc =>
adamc@329 231 ErrorMsg.errorAt loc "Constructor expects argument but is used with no argument"
adamc@819 232 | Inexhaustive (loc, p) =>
adamc@819 233 (ErrorMsg.errorAt loc "Inexhaustive 'case'";
adamc@819 234 eprefaces' [("Missed case", p_pat env p)])
adamc@329 235 | DuplicatePatField (loc, s) =>
adamc@329 236 ErrorMsg.errorAt loc ("Duplicate record field " ^ s ^ " in pattern")
adamc@329 237 | OutOfContext (loc, co) =>
adamc@329 238 (ErrorMsg.errorAt loc "Type class wildcard occurs out of context";
adamc@329 239 Option.app (fn (e, c) => eprefaces' [("Function", p_exp env e),
adamc@329 240 ("Type", p_con env c)]) co)
adamc@329 241 | Unresolvable (loc, c) =>
adamc@329 242 (ErrorMsg.errorAt loc "Can't resolve type class instance";
adam@1742 243 eprefaces' ([("Class constraint", p_con env c)]
adam@1742 244 @ (case E.resolveFailureCause () of
adam@1742 245 NONE => []
adam@1778 246 | SOME c' => [("Reduced to unresolvable", p_con env c')]))(*;
adam@1778 247 app (fn (c, rs) => (eprefaces' [("CLASS", p_con env c)];
adam@1778 248 app (fn (c, e) => eprefaces' [("RULE", p_con env c),
adam@1778 249 ("IMPL", p_exp env e)]) rs))
adam@1778 250 (E.listClasses env)*))
adamc@329 251 | IllegalRec (x, e) =>
adamc@329 252 (ErrorMsg.errorAt (#2 e) "Illegal 'val rec' righthand side (must be a function abstraction)";
adamc@329 253 eprefaces' [("Variable", PD.string x),
adamc@329 254 ("Expression", p_exp env e)])
adam@2009 255 | IllegalFlex e =>
adam@2009 256 (ErrorMsg.errorAt (#2 e) "Flex record syntax (\"...\") only allowed in patterns";
adam@2009 257 eprefaces' [("Expression", SourcePrint.p_exp e)])
adamc@329 258
adamc@329 259
adamc@329 260 datatype decl_error =
adamc@329 261 KunifsRemain of decl list
adamc@329 262 | CunifsRemain of decl list
adamc@329 263 | Nonpositive of decl
adamc@329 264
adamc@329 265 fun lspan [] = ErrorMsg.dummySpan
adamc@329 266 | lspan ((_, loc) :: _) = loc
adamc@329 267
adam@1584 268 val baseLen = 2000
adam@1584 269
adam@1584 270 fun p_decl env d =
adam@1584 271 let
adam@1584 272 val fname = OS.FileSys.tmpName ()
adam@1584 273 val out' = TextIO.openOut fname
adam@1584 274 val out = Print.openOut {dst = out', wid = 80}
adam@1584 275
adam@1584 276 fun readFromFile () =
adam@1584 277 let
adam@1584 278 val inf = TextIO.openIn fname
adam@1584 279
adam@1584 280 fun loop acc =
adam@1584 281 case TextIO.inputLine inf of
adam@1584 282 NONE => String.concat (rev acc)
adam@1584 283 | SOME line => loop (line :: acc)
adam@1584 284 in
adam@1584 285 loop []
adam@1584 286 before TextIO.closeIn inf
adam@1584 287 end
adam@1584 288 in
adam@1584 289 Print.fprint out (P.p_decl env d);
adam@1584 290 TextIO.closeOut out';
adam@1584 291 let
adam@1584 292 val content = readFromFile ()
adam@1584 293 in
adam@1584 294 OS.FileSys.remove fname;
adam@1584 295 Print.PD.string (if size content <= baseLen then
adam@1584 296 content
adam@1584 297 else
adam@1584 298 let
adam@1584 299 val (befor, after) = Substring.position "<UNIF:" (Substring.full content)
adam@1584 300 in
adam@1584 301 if Substring.isEmpty after then
adam@1584 302 raise Fail "No unification variables in rendering"
adam@1584 303 else
adam@1584 304 Substring.concat [Substring.full "\n.....\n",
adam@1584 305 if Substring.size befor <= baseLen then
adam@1584 306 befor
adam@1584 307 else
adam@1584 308 Substring.slice (befor, Substring.size befor - baseLen, SOME baseLen),
adam@1584 309 if Substring.size after <= baseLen then
adam@1584 310 after
adam@1584 311 else
adam@1584 312 Substring.slice (after, 0, SOME baseLen),
adam@1584 313 Substring.full "\n.....\n"]
adam@1584 314 end)
adam@1584 315 end
adam@1584 316 end
adamc@329 317
adamc@329 318 fun declError env err =
adamc@329 319 case err of
adamc@329 320 KunifsRemain ds =>
adam@1521 321 (ErrorMsg.errorAt (lspan ds) "Some kind unification variables are undetermined in declaration\n(look for them as \"<UNIF:...>\")";
adamc@329 322 eprefaces' [("Decl", p_list_sep PD.newline (p_decl env) ds)])
adamc@329 323 | CunifsRemain ds =>
adam@1521 324 (ErrorMsg.errorAt (lspan ds) "Some constructor unification variables are undetermined in declaration\n(look for them as \"<UNIF:...>\")";
adamc@329 325 eprefaces' [("Decl", p_list_sep PD.newline (p_decl env) ds)])
adamc@329 326 | Nonpositive d =>
adamc@329 327 (ErrorMsg.errorAt (#2 d) "Non-strictly-positive datatype declaration (could allow non-termination)";
adamc@329 328 eprefaces' [("Decl", p_decl env d)])
adamc@329 329
adamc@329 330 datatype sgn_error =
adamc@329 331 UnboundSgn of ErrorMsg.span * string
adamc@1000 332 | UnmatchedSgi of ErrorMsg.span * sgn_item
adam@1719 333 | SgiWrongKind of ErrorMsg.span * sgn_item * kind * sgn_item * kind * E.env * kunify_error
adam@1719 334 | SgiWrongCon of ErrorMsg.span * sgn_item * con * sgn_item * con * E.env * cunify_error
adamc@1000 335 | SgiMismatchedDatatypes of ErrorMsg.span * sgn_item * sgn_item
adam@1719 336 * (con * con * E.env * cunify_error) option
adamc@1000 337 | SgnWrongForm of ErrorMsg.span * sgn * sgn
adamc@329 338 | UnWhereable of sgn * string
adam@1719 339 | WhereWrongKind of kind * kind * E.env * kunify_error
adamc@329 340 | NotIncludable of sgn
adamc@329 341 | DuplicateCon of ErrorMsg.span * string
adamc@329 342 | DuplicateVal of ErrorMsg.span * string
adamc@329 343 | DuplicateSgn of ErrorMsg.span * string
adamc@329 344 | DuplicateStr of ErrorMsg.span * string
adamc@329 345 | NotConstraintsable of sgn
adamc@329 346
adamc@329 347 val p_sgn_item = P.p_sgn_item
adamc@329 348 val p_sgn = P.p_sgn
adamc@329 349
adamc@329 350 fun sgnError env err =
adamc@329 351 case err of
adamc@329 352 UnboundSgn (loc, s) =>
adamc@329 353 ErrorMsg.errorAt loc ("Unbound signature variable " ^ s)
adamc@1000 354 | UnmatchedSgi (loc, sgi) =>
adamc@329 355 (ErrorMsg.errorAt loc "Unmatched signature item";
adamc@329 356 eprefaces' [("Item", p_sgn_item env sgi)])
adam@1719 357 | SgiWrongKind (loc, sgi1, k1, sgi2, k2, env', kerr) =>
adamc@1000 358 (ErrorMsg.errorAt loc "Kind unification failure in signature matching:";
adamc@329 359 eprefaces' [("Have", p_sgn_item env sgi1),
adamc@329 360 ("Need", p_sgn_item env sgi2),
adamc@623 361 ("Kind 1", p_kind env k1),
adamc@623 362 ("Kind 2", p_kind env k2)];
adam@1719 363 kunifyError env' kerr)
adam@1719 364 | SgiWrongCon (loc, sgi1, c1, sgi2, c2, env', cerr) =>
adamc@1000 365 (ErrorMsg.errorAt loc "Constructor unification failure in signature matching:";
adamc@329 366 eprefaces' [("Have", p_sgn_item env sgi1),
adamc@329 367 ("Need", p_sgn_item env sgi2),
adamc@329 368 ("Con 1", p_con env c1),
adamc@329 369 ("Con 2", p_con env c2)];
adam@1719 370 cunifyError env' cerr)
adamc@1000 371 | SgiMismatchedDatatypes (loc, sgi1, sgi2, cerro) =>
adamc@1000 372 (ErrorMsg.errorAt loc "Mismatched 'datatype' specifications:";
adamc@329 373 eprefaces' [("Have", p_sgn_item env sgi1),
adamc@329 374 ("Need", p_sgn_item env sgi2)];
adam@1719 375 Option.app (fn (c1, c2, env', ue) =>
adamc@329 376 (eprefaces "Unification error"
adam@1719 377 [("Con 1", p_con env' c1),
adam@1719 378 ("Con 2", p_con env' c2)];
adam@1719 379 cunifyError env' ue)) cerro)
adamc@1000 380 | SgnWrongForm (loc, sgn1, sgn2) =>
adamc@1000 381 (ErrorMsg.errorAt loc "Incompatible signatures:";
adamc@329 382 eprefaces' [("Sig 1", p_sgn env sgn1),
adamc@329 383 ("Sig 2", p_sgn env sgn2)])
adamc@329 384 | UnWhereable (sgn, x) =>
adamc@329 385 (ErrorMsg.errorAt (#2 sgn) "Unavailable field for 'where'";
adamc@329 386 eprefaces' [("Signature", p_sgn env sgn),
adamc@329 387 ("Field", PD.string x)])
adam@1719 388 | WhereWrongKind (k1, k2, env', kerr) =>
adamc@329 389 (ErrorMsg.errorAt (#2 k1) "Wrong kind for 'where'";
adamc@623 390 eprefaces' [("Have", p_kind env k1),
adamc@623 391 ("Need", p_kind env k2)];
adam@1719 392 kunifyError env' kerr)
adamc@329 393 | NotIncludable sgn =>
adamc@329 394 (ErrorMsg.errorAt (#2 sgn) "Invalid signature to 'include'";
adamc@329 395 eprefaces' [("Signature", p_sgn env sgn)])
adamc@329 396 | DuplicateCon (loc, s) =>
adamc@329 397 ErrorMsg.errorAt loc ("Duplicate constructor " ^ s ^ " in signature")
adamc@329 398 | DuplicateVal (loc, s) =>
adamc@329 399 ErrorMsg.errorAt loc ("Duplicate value " ^ s ^ " in signature")
adamc@329 400 | DuplicateSgn (loc, s) =>
adamc@329 401 ErrorMsg.errorAt loc ("Duplicate signature " ^ s ^ " in signature")
adamc@329 402 | DuplicateStr (loc, s) =>
adamc@329 403 ErrorMsg.errorAt loc ("Duplicate structure " ^ s ^ " in signature")
adamc@329 404 | NotConstraintsable sgn =>
adamc@329 405 (ErrorMsg.errorAt (#2 sgn) "Invalid signature for 'open constraints'";
adamc@329 406 eprefaces' [("Signature", p_sgn env sgn)])
adamc@329 407
adamc@329 408 datatype str_error =
adamc@329 409 UnboundStr of ErrorMsg.span * string
adamc@329 410 | NotFunctor of sgn
adamc@329 411 | FunctorRebind of ErrorMsg.span
adamc@329 412 | UnOpenable of sgn
adam@1719 413 | NotType of ErrorMsg.span * kind * (kind * kind * E.env * kunify_error)
adamc@329 414 | DuplicateConstructor of string * ErrorMsg.span
adamc@329 415 | NotDatatype of ErrorMsg.span
adamc@329 416
adamc@329 417 fun strError env err =
adamc@329 418 case err of
adamc@329 419 UnboundStr (loc, s) =>
adamc@329 420 ErrorMsg.errorAt loc ("Unbound structure variable " ^ s)
adamc@329 421 | NotFunctor sgn =>
adamc@329 422 (ErrorMsg.errorAt (#2 sgn) "Application of non-functor";
adamc@329 423 eprefaces' [("Signature", p_sgn env sgn)])
adamc@329 424 | FunctorRebind loc =>
adamc@329 425 ErrorMsg.errorAt loc "Attempt to rebind functor"
adamc@329 426 | UnOpenable sgn =>
adamc@329 427 (ErrorMsg.errorAt (#2 sgn) "Un-openable structure";
adamc@329 428 eprefaces' [("Signature", p_sgn env sgn)])
adam@1719 429 | NotType (loc, k, (k1, k2, env', ue)) =>
adamc@706 430 (ErrorMsg.errorAt loc "'val' type kind is not 'Type'";
adamc@623 431 eprefaces' [("Kind", p_kind env k),
adamc@623 432 ("Subkind 1", p_kind env k1),
adamc@623 433 ("Subkind 2", p_kind env k2)];
adam@1719 434 kunifyError env' ue)
adamc@329 435 | DuplicateConstructor (x, loc) =>
adamc@329 436 ErrorMsg.errorAt loc ("Duplicate datatype constructor " ^ x)
adamc@329 437 | NotDatatype loc =>
adamc@329 438 ErrorMsg.errorAt loc "Trying to import non-datatype as a datatype"
adamc@329 439
adamc@329 440 end