adam@1719: (* Copyright (c) 2008-2010, 2012, Adam Chlipala
adamc@329:  * All rights reserved.
adamc@329:  *
adamc@329:  * Redistribution and use in source and binary forms, with or without
adamc@329:  * modification, are permitted provided that the following conditions are met:
adamc@329:  *
adamc@329:  * - Redistributions of source code must retain the above copyright notice,
adamc@329:  *   this list of conditions and the following disclaimer.
adamc@329:  * - Redistributions in binary form must reproduce the above copyright notice,
adamc@329:  *   this list of conditions and the following disclaimer in the documentation
adamc@329:  *   and/or other materials provided with the distribution.
adamc@329:  * - The names of contributors may not be used to endorse or promote products
adamc@329:  *   derived from this software without specific prior written permission.
adamc@329:  *
adamc@329:  * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
adamc@329:  * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
adamc@329:  * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
adamc@329:  * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
adamc@329:  * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR 
adamc@329:  * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
adamc@329:  * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
adamc@329:  * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
adamc@329:  * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
adamc@329:  * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
adamc@329:  * POSSIBILITY OF SUCH DAMAGE.
adamc@329:  *)
adamc@329: 
adamc@329: structure ElabErr :> ELAB_ERR = struct
adamc@329: 
adamc@329: structure L = Source
adamc@329: open Elab
adamc@329: 
adamc@329: structure E = ElabEnv
adamc@329: structure U = ElabUtil
adamc@329: 
adamc@329: open Print
adamc@329: structure P = ElabPrint
adamc@329: 
adamc@329: val p_kind = P.p_kind
adamc@623:              
adamc@623: datatype kind_error =
adamc@623:          UnboundKind of ErrorMsg.span * string
adamc@623: 
adamc@623: fun kindError env err =
adamc@623:     case err of
adamc@623:         UnboundKind (loc, s) =>
adamc@623:         ErrorMsg.errorAt loc ("Unbound kind variable " ^ s)
adamc@329: 
adamc@329: datatype kunify_error =
adamc@329:          KOccursCheckFailed of kind * kind
adamc@329:        | KIncompatible of kind * kind
adam@1639:        | KScope of kind * kind
adamc@329: 
adamc@623: fun kunifyError env err =
adamc@329:     case err of
adamc@329:         KOccursCheckFailed (k1, k2) =>
adamc@329:         eprefaces "Kind occurs check failed"
adamc@623:         [("Kind 1", p_kind env k1),
adamc@623:          ("Kind 2", p_kind env k2)]
adamc@329:       | KIncompatible (k1, k2) =>
adamc@329:         eprefaces "Incompatible kinds"
adamc@623:         [("Kind 1", p_kind env k1),
adamc@623:          ("Kind 2", p_kind env k2)]
adam@1639:       | KScope (k1, k2) =>
adam@1639:         eprefaces "Scoping prevents kind unification"
adam@1639:         [("Kind 1", p_kind env k1),
adam@1639:          ("Kind 2", p_kind env k2)]
adamc@329: 
adam@1714: fun p_con env c = P.p_con env (ElabOps.reduceCon env c)
adamc@329: 
adamc@329: datatype con_error =
adamc@329:          UnboundCon of ErrorMsg.span * string
adamc@329:        | UnboundDatatype of ErrorMsg.span * string
adamc@329:        | UnboundStrInCon of ErrorMsg.span * string
adam@1719:        | WrongKind of con * kind * kind * E.env * kunify_error
adamc@329:        | DuplicateField of ErrorMsg.span * string
adamc@329:        | ProjBounds of con * int
adamc@329:        | ProjMismatch of con * kind
adamc@329: 
adamc@329: fun conError env err =
adamc@329:     case err of
adamc@329:         UnboundCon (loc, s) =>
adamc@329:         ErrorMsg.errorAt loc ("Unbound constructor variable " ^ s)
adamc@329:       | UnboundDatatype (loc, s) =>
adamc@329:         ErrorMsg.errorAt loc ("Unbound datatype " ^ s)
adamc@329:       | UnboundStrInCon (loc, s) =>
adamc@329:         ErrorMsg.errorAt loc ("Unbound structure " ^ s)
adam@1719:       | WrongKind (c, k1, k2, env', kerr) =>
adamc@329:         (ErrorMsg.errorAt (#2 c) "Wrong kind";
adamc@329:          eprefaces' [("Constructor", p_con env c),
adamc@623:                      ("Have kind", p_kind env k1),
adamc@623:                      ("Need kind", p_kind env k2)];
adam@1719:          kunifyError env' kerr)
adamc@329:       | DuplicateField (loc, s) =>
adamc@329:         ErrorMsg.errorAt loc ("Duplicate record field " ^ s)
adamc@329:       | ProjBounds (c, n) =>
adamc@329:         (ErrorMsg.errorAt (#2 c) "Out of bounds constructor projection";
adamc@329:          eprefaces' [("Constructor", p_con env c),
adamc@329:                      ("Index", Print.PD.string (Int.toString n))])
adamc@329:       | ProjMismatch (c, k) =>
adamc@329:         (ErrorMsg.errorAt (#2 c) "Projection from non-tuple constructor";
adamc@329:          eprefaces' [("Constructor", p_con env c),
adamc@623:                      ("Kind", p_kind env k)])
adamc@329: 
adamc@329: datatype cunify_error =
adam@1719:          CKind of kind * kind * E.env * kunify_error
adamc@329:        | COccursCheckFailed of con * con
adamc@329:        | CIncompatible of con * con
adamc@329:        | CExplicitness of con * con
adamc@413:        | CKindof of kind * con * string
adam@1719:        | CRecordFailure of con * con * (con * con * con * (E.env * cunify_error) option) option
adam@1303:        | TooLifty of ErrorMsg.span * ErrorMsg.span
adam@1303:        | TooUnify of con * con
adam@1306:        | TooDeep
adam@1639:        | CScope of con * con
adamc@329: 
adam@1719: fun cunifyError env err : unit =
adamc@329:     case err of
adam@1719:         CKind (k1, k2, env', kerr) =>
adamc@329:         (eprefaces "Kind unification failure"
adam@1582:                    [("Have", p_kind env k1),
adam@1582:                     ("Need", p_kind env k2)];
adam@1719:          kunifyError env' kerr)
adamc@329:       | COccursCheckFailed (c1, c2) =>
adamc@329:         eprefaces "Constructor occurs check failed"
adam@1582:                   [("Have", p_con env c1),
adam@1582:                    ("Need", p_con env c2)]
adamc@329:       | CIncompatible (c1, c2) =>
adamc@329:         eprefaces "Incompatible constructors"
adam@1582:                   [("Have", p_con env c1),
adam@1582:                    ("Need", p_con env c2)]
adamc@329:       | CExplicitness (c1, c2) =>
adamc@329:         eprefaces "Differing constructor function explicitness"
adam@1582:                   [("Have", p_con env c1),
adam@1582:                    ("Need", p_con env c2)]
adamc@413:       | CKindof (k, c, expected) =>
adamc@413:         eprefaces ("Unexpected kind for kindof calculation (expecting " ^ expected ^ ")")
adamc@623:                   [("Kind", p_kind env k),
adamc@329:                    ("Con", p_con env c)]
adamc@1071:       | CRecordFailure (c1, c2, fo) =>
adam@1359:         (eprefaces "Can't unify record constructors"
adam@1582:                    (("Have", p_con env c1)
adam@1582:                     :: ("Need", p_con env c2)
adam@1359:                     :: (case fo of
adam@1359:                             NONE => []
adam@1359:                           | SOME (nm, t1, t2, _) =>
adam@1359:                             [("Field", p_con env nm),
adam@1359:                              ("Value 1", p_con env t1),
adam@1359:                              ("Value 2", p_con env t2)]));
adam@1359:          case fo of
adam@1719:              SOME (_, _, _, SOME (env', err')) => cunifyError env' err'
adam@1359:            | _ => ())
adam@1303:       | TooLifty (loc1, loc2) =>
adam@1303:         (ErrorMsg.errorAt loc1 "Can't unify two unification variables that both have suspended liftings";
adam@1303:          eprefaces' [("Other location", Print.PD.string (ErrorMsg.spanToString loc2))])
adam@1303:       | TooUnify (c1, c2) =>
adam@1303:         (ErrorMsg.errorAt (#2 c1) "Substitution in constructor is blocked by a too-deep unification variable";
adam@1303:          eprefaces' [("Replacement", p_con env c1),
adam@1303:                      ("Body", p_con env c2)])
adam@1306:       | TooDeep => ErrorMsg.error "Can't reverse-engineer unification variable lifting"
adam@1639:       | CScope (c1, c2) =>
adam@1639:         eprefaces "Scoping prevents constructor unification"
adam@1639:                   [("Have", p_con env c1),
adam@1639:                    ("Need", p_con env c2)]
adamc@329: 
adamc@329: datatype exp_error =
adamc@329:        UnboundExp of ErrorMsg.span * string
adamc@329:      | UnboundStrInExp of ErrorMsg.span * string
adam@1719:      | Unify of exp * con * con * E.env * cunify_error
adamc@339:      | Unif of string * ErrorMsg.span * con
adamc@329:      | WrongForm of string * exp * con
adamc@329:      | IncompatibleCons of con * con
adamc@329:      | DuplicatePatternVariable of ErrorMsg.span * string
adam@1719:      | PatUnify of pat * con * con * E.env * cunify_error
adamc@329:      | UnboundConstructor of ErrorMsg.span * string list * string
adamc@329:      | PatHasArg of ErrorMsg.span
adamc@329:      | PatHasNoArg of ErrorMsg.span
adamc@819:      | Inexhaustive of ErrorMsg.span * pat
adamc@329:      | DuplicatePatField of ErrorMsg.span * string
adamc@329:      | Unresolvable of ErrorMsg.span * con
adamc@329:      | OutOfContext of ErrorMsg.span * (exp * con) option
adamc@329:      | IllegalRec of string * exp
adamc@329: 
adam@1714: val simplExp = U.Exp.mapB {kind = fn _ => fn k => k,
adam@1714:                            con = fn env => fn c => #1 (ElabOps.reduceCon env (c, ErrorMsg.dummySpan)),
adam@1714:                            exp = fn _ => fn e => e,
adam@1714:                            bind = fn (env, U.Exp.RelC (x, k)) => E.pushCRel env x k
adam@1714:                                    | (env, U.Exp.NamedC (x, n, k, co)) => E.pushCNamedAs env x n k co
adam@1714:                                    | (env, _) => env}
adam@1714: 
adam@1714: fun p_exp env e = P.p_exp env (simplExp env e)
adamc@329: val p_pat = P.p_pat
adamc@329: 
adamc@329: fun expError env err =
adamc@329:     case err of
adamc@329:         UnboundExp (loc, s) =>
adamc@329:         ErrorMsg.errorAt loc ("Unbound expression variable " ^ s)
adamc@329:       | UnboundStrInExp (loc, s) =>
adamc@329:         ErrorMsg.errorAt loc ("Unbound structure " ^ s)
adam@1719:       | Unify (e, c1, c2, env', uerr) =>
adamc@329:         (ErrorMsg.errorAt (#2 e) "Unification failure";
adamc@329:          eprefaces' [("Expression", p_exp env e),
adamc@329:                      ("Have con", p_con env c1),
adamc@329:                      ("Need con", p_con env c2)];
adam@1719:          cunifyError env' uerr)
adamc@339:       | Unif (action, loc, c) =>
adamc@339:         (ErrorMsg.errorAt loc ("Unification variable blocks " ^ action);
adamc@329:          eprefaces' [("Con", p_con env c)])
adamc@329:       | WrongForm (variety, e, t) =>
adamc@329:         (ErrorMsg.errorAt (#2 e) ("Expression is not a " ^ variety);
adamc@329:          eprefaces' [("Expression", p_exp env e),
adamc@329:                      ("Type", p_con env t)])
adamc@329:       | IncompatibleCons (c1, c2) =>
adamc@329:         (ErrorMsg.errorAt (#2 c1) "Incompatible constructors";
adam@1582:          eprefaces' [("Have", p_con env c1),
adam@1582:                      ("Need", p_con env c2)])
adamc@329:       | DuplicatePatternVariable (loc, s) =>
adamc@329:         ErrorMsg.errorAt loc ("Duplicate pattern variable " ^ s)
adam@1719:       | PatUnify (p, c1, c2, env', uerr) =>
adamc@329:         (ErrorMsg.errorAt (#2 p) "Unification failure for pattern";
adamc@329:          eprefaces' [("Pattern", p_pat env p),
adamc@329:                      ("Have con", p_con env c1),
adamc@329:                      ("Need con", p_con env c2)];
adam@1719:          cunifyError env' uerr)
adamc@329:       | UnboundConstructor (loc, ms, s) =>
adamc@329:         ErrorMsg.errorAt loc ("Unbound constructor " ^ String.concatWith "." (ms @ [s]) ^ " in pattern")
adamc@329:       | PatHasArg loc =>
adamc@329:         ErrorMsg.errorAt loc "Constructor expects no argument but is used with argument"
adamc@329:       | PatHasNoArg loc =>
adamc@329:         ErrorMsg.errorAt loc "Constructor expects argument but is used with no argument"
adamc@819:       | Inexhaustive (loc, p) =>
adamc@819:         (ErrorMsg.errorAt loc "Inexhaustive 'case'";
adamc@819:          eprefaces' [("Missed case", p_pat env p)])
adamc@329:       | DuplicatePatField (loc, s) =>
adamc@329:         ErrorMsg.errorAt loc ("Duplicate record field " ^ s ^ " in pattern")
adamc@329:       | OutOfContext (loc, co) =>
adamc@329:         (ErrorMsg.errorAt loc "Type class wildcard occurs out of context";
adamc@329:          Option.app (fn (e, c) => eprefaces' [("Function", p_exp env e),
adamc@329:                                               ("Type", p_con env c)]) co)
adamc@329:       | Unresolvable (loc, c) =>
adamc@329:         (ErrorMsg.errorAt loc "Can't resolve type class instance";
adamc@850:          eprefaces' [("Class constraint", p_con env c)(*,
adamc@711:                      ("Class database", p_list (fn (c, rules) =>
adamc@711:                                                    box [P.p_con env c,
adamc@711:                                                         PD.string ":",
adamc@711:                                                         space,
adamc@711:                                                         p_list (fn (c, e) =>
adamc@711:                                                                    box [p_exp env e,
adamc@711:                                                                         PD.string ":",
adamc@711:                                                                         space,
adamc@711:                                                                         P.p_con env c]) rules])
adamc@850:                                         (E.listClasses env))*)])
adamc@329:       | IllegalRec (x, e) =>
adamc@329:         (ErrorMsg.errorAt (#2 e) "Illegal 'val rec' righthand side (must be a function abstraction)";
adamc@329:          eprefaces' [("Variable", PD.string x),
adamc@329:                      ("Expression", p_exp env e)])
adamc@329: 
adamc@329: 
adamc@329: datatype decl_error =
adamc@329:          KunifsRemain of decl list
adamc@329:        | CunifsRemain of decl list
adamc@329:        | Nonpositive of decl
adamc@329: 
adamc@329: fun lspan [] = ErrorMsg.dummySpan
adamc@329:   | lspan ((_, loc) :: _) = loc
adamc@329: 
adam@1584: val baseLen = 2000
adam@1584: 
adam@1584: fun p_decl env d =
adam@1584:     let
adam@1584:         val fname = OS.FileSys.tmpName ()
adam@1584:         val out' = TextIO.openOut fname
adam@1584:         val out = Print.openOut {dst = out', wid = 80}
adam@1584: 
adam@1584:         fun readFromFile () =
adam@1584:             let
adam@1584:                 val inf = TextIO.openIn fname
adam@1584: 
adam@1584:                 fun loop acc =
adam@1584:                     case TextIO.inputLine inf of
adam@1584:                         NONE => String.concat (rev acc)
adam@1584:                       | SOME line => loop (line :: acc)
adam@1584:             in
adam@1584:                 loop []
adam@1584:                 before TextIO.closeIn inf
adam@1584:             end
adam@1584:     in
adam@1584:         Print.fprint out (P.p_decl env d);
adam@1584:         TextIO.closeOut out';
adam@1584:         let
adam@1584:             val content = readFromFile ()
adam@1584:         in
adam@1584:             OS.FileSys.remove fname;
adam@1584:             Print.PD.string (if size content <= baseLen then
adam@1584:                                  content
adam@1584:                              else
adam@1584:                                  let
adam@1584:                                      val (befor, after) = Substring.position "<UNIF:" (Substring.full content)
adam@1584:                                  in
adam@1584:                                      if Substring.isEmpty after then
adam@1584:                                          raise Fail "No unification variables in rendering"
adam@1584:                                      else
adam@1584:                                          Substring.concat [Substring.full "\n.....\n",
adam@1584:                                                            if Substring.size befor <= baseLen then
adam@1584:                                                                befor
adam@1584:                                                            else
adam@1584:                                                                Substring.slice (befor, Substring.size befor - baseLen, SOME baseLen),
adam@1584:                                                            if Substring.size after <= baseLen then
adam@1584:                                                                after
adam@1584:                                                            else
adam@1584:                                                                Substring.slice (after, 0, SOME baseLen),
adam@1584:                                                            Substring.full "\n.....\n"]
adam@1584:                                  end)
adam@1584:         end
adam@1584:     end
adamc@329: 
adamc@329: fun declError env err =
adamc@329:     case err of
adamc@329:         KunifsRemain ds =>
adam@1521:         (ErrorMsg.errorAt (lspan ds) "Some kind unification variables are undetermined in declaration\n(look for them as \"<UNIF:...>\")";
adamc@329:          eprefaces' [("Decl", p_list_sep PD.newline (p_decl env) ds)])
adamc@329:       | CunifsRemain ds =>
adam@1521:         (ErrorMsg.errorAt (lspan ds) "Some constructor unification variables are undetermined in declaration\n(look for them as \"<UNIF:...>\")";
adamc@329:          eprefaces' [("Decl", p_list_sep PD.newline (p_decl env) ds)])
adamc@329:       | Nonpositive d =>
adamc@329:         (ErrorMsg.errorAt (#2 d) "Non-strictly-positive datatype declaration (could allow non-termination)";
adamc@329:          eprefaces' [("Decl", p_decl env d)])
adamc@329: 
adamc@329: datatype sgn_error =
adamc@329:          UnboundSgn of ErrorMsg.span * string
adamc@1000:        | UnmatchedSgi of ErrorMsg.span * sgn_item
adam@1719:        | SgiWrongKind of ErrorMsg.span * sgn_item * kind * sgn_item * kind * E.env * kunify_error
adam@1719:        | SgiWrongCon of ErrorMsg.span * sgn_item * con * sgn_item * con * E.env * cunify_error
adamc@1000:        | SgiMismatchedDatatypes of ErrorMsg.span * sgn_item * sgn_item
adam@1719:                                    * (con * con * E.env * cunify_error) option
adamc@1000:        | SgnWrongForm of ErrorMsg.span * sgn * sgn
adamc@329:        | UnWhereable of sgn * string
adam@1719:        | WhereWrongKind of kind * kind * E.env * kunify_error
adamc@329:        | NotIncludable of sgn
adamc@329:        | DuplicateCon of ErrorMsg.span * string
adamc@329:        | DuplicateVal of ErrorMsg.span * string
adamc@329:        | DuplicateSgn of ErrorMsg.span * string
adamc@329:        | DuplicateStr of ErrorMsg.span * string
adamc@329:        | NotConstraintsable of sgn
adamc@329: 
adamc@329: val p_sgn_item = P.p_sgn_item
adamc@329: val p_sgn = P.p_sgn
adamc@329: 
adamc@329: fun sgnError env err =
adamc@329:     case err of
adamc@329:         UnboundSgn (loc, s) =>
adamc@329:         ErrorMsg.errorAt loc ("Unbound signature variable " ^ s)
adamc@1000:       | UnmatchedSgi (loc, sgi) =>
adamc@329:         (ErrorMsg.errorAt loc "Unmatched signature item";
adamc@329:          eprefaces' [("Item", p_sgn_item env sgi)])
adam@1719:       | SgiWrongKind (loc, sgi1, k1, sgi2, k2, env', kerr) =>
adamc@1000:         (ErrorMsg.errorAt loc "Kind unification failure in signature matching:";
adamc@329:          eprefaces' [("Have", p_sgn_item env sgi1),
adamc@329:                      ("Need", p_sgn_item env sgi2),
adamc@623:                      ("Kind 1", p_kind env k1),
adamc@623:                      ("Kind 2", p_kind env k2)];
adam@1719:          kunifyError env' kerr)
adam@1719:       | SgiWrongCon (loc, sgi1, c1, sgi2, c2, env', cerr) =>
adamc@1000:         (ErrorMsg.errorAt loc "Constructor unification failure in signature matching:";
adamc@329:          eprefaces' [("Have", p_sgn_item env sgi1),
adamc@329:                      ("Need", p_sgn_item env sgi2),
adamc@329:                      ("Con 1", p_con env c1),
adamc@329:                      ("Con 2", p_con env c2)];
adam@1719:          cunifyError env' cerr)
adamc@1000:       | SgiMismatchedDatatypes (loc, sgi1, sgi2, cerro) =>
adamc@1000:         (ErrorMsg.errorAt loc "Mismatched 'datatype' specifications:";
adamc@329:          eprefaces' [("Have", p_sgn_item env sgi1),
adamc@329:                      ("Need", p_sgn_item env sgi2)];
adam@1719:          Option.app (fn (c1, c2, env', ue) =>
adamc@329:                         (eprefaces "Unification error"
adam@1719:                                    [("Con 1", p_con env' c1),
adam@1719:                                     ("Con 2", p_con env' c2)];
adam@1719:                          cunifyError env' ue)) cerro)
adamc@1000:       | SgnWrongForm (loc, sgn1, sgn2) =>
adamc@1000:         (ErrorMsg.errorAt loc "Incompatible signatures:";
adamc@329:          eprefaces' [("Sig 1", p_sgn env sgn1),
adamc@329:                      ("Sig 2", p_sgn env sgn2)])
adamc@329:       | UnWhereable (sgn, x) =>
adamc@329:         (ErrorMsg.errorAt (#2 sgn) "Unavailable field for 'where'";
adamc@329:          eprefaces' [("Signature", p_sgn env sgn),
adamc@329:                      ("Field", PD.string x)])
adam@1719:       | WhereWrongKind (k1, k2, env', kerr) =>
adamc@329:         (ErrorMsg.errorAt (#2 k1) "Wrong kind for 'where'";
adamc@623:          eprefaces' [("Have", p_kind env k1),
adamc@623:                      ("Need", p_kind env k2)];
adam@1719:          kunifyError env' kerr)
adamc@329:       | NotIncludable sgn =>
adamc@329:         (ErrorMsg.errorAt (#2 sgn) "Invalid signature to 'include'";
adamc@329:          eprefaces' [("Signature", p_sgn env sgn)])
adamc@329:       | DuplicateCon (loc, s) =>
adamc@329:         ErrorMsg.errorAt loc ("Duplicate constructor " ^ s ^ " in signature")
adamc@329:       | DuplicateVal (loc, s) =>
adamc@329:         ErrorMsg.errorAt loc ("Duplicate value " ^ s ^ " in signature")
adamc@329:       | DuplicateSgn (loc, s) =>
adamc@329:         ErrorMsg.errorAt loc ("Duplicate signature " ^ s ^ " in signature")
adamc@329:       | DuplicateStr (loc, s) =>
adamc@329:         ErrorMsg.errorAt loc ("Duplicate structure " ^ s ^ " in signature")
adamc@329:       | NotConstraintsable sgn =>
adamc@329:         (ErrorMsg.errorAt (#2 sgn) "Invalid signature for 'open constraints'";
adamc@329:          eprefaces' [("Signature", p_sgn env sgn)])
adamc@329: 
adamc@329: datatype str_error =
adamc@329:          UnboundStr of ErrorMsg.span * string
adamc@329:        | NotFunctor of sgn
adamc@329:        | FunctorRebind of ErrorMsg.span
adamc@329:        | UnOpenable of sgn
adam@1719:        | NotType of ErrorMsg.span * kind * (kind * kind * E.env * kunify_error)
adamc@329:        | DuplicateConstructor of string * ErrorMsg.span
adamc@329:        | NotDatatype of ErrorMsg.span
adamc@329: 
adamc@329: fun strError env err =
adamc@329:     case err of
adamc@329:         UnboundStr (loc, s) =>
adamc@329:         ErrorMsg.errorAt loc ("Unbound structure variable " ^ s)
adamc@329:       | NotFunctor sgn =>
adamc@329:         (ErrorMsg.errorAt (#2 sgn) "Application of non-functor";
adamc@329:          eprefaces' [("Signature", p_sgn env sgn)])
adamc@329:       | FunctorRebind loc =>
adamc@329:         ErrorMsg.errorAt loc "Attempt to rebind functor"
adamc@329:       | UnOpenable sgn =>
adamc@329:         (ErrorMsg.errorAt (#2 sgn) "Un-openable structure";
adamc@329:          eprefaces' [("Signature", p_sgn env sgn)])
adam@1719:       | NotType (loc, k, (k1, k2, env', ue)) =>
adamc@706:         (ErrorMsg.errorAt loc "'val' type kind is not 'Type'";
adamc@623:          eprefaces' [("Kind", p_kind env k),
adamc@623:                      ("Subkind 1", p_kind env k1),
adamc@623:                      ("Subkind 2", p_kind env k2)];
adam@1719:          kunifyError env' ue)
adamc@329:       | DuplicateConstructor (x, loc) =>
adamc@329:         ErrorMsg.errorAt loc ("Duplicate datatype constructor " ^ x)
adamc@329:       | NotDatatype loc =>
adamc@329:         ErrorMsg.errorAt loc "Trying to import non-datatype as a datatype"
adamc@329: 
adamc@329: end