xref: /seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/ParseTree/TYPECHECK_PARSETREE.sml

(*
    Copyright (c) 2013-2015 David C.J. Matthews

    This library is free software; you can redistribute it and/or
    modify it under the terms of the GNU Lesser General Public
    License version 2.1 as published by the Free Software Foundation.
    
    This library is distributed in the hope that it will be useful,
    but WITHOUT ANY WARRANTY; without even the implied warranty of
    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
    Lesser General Public License for more details.
    
    You should have received a copy of the GNU Lesser General Public
    License along with this library; if not, write to the Free Software
    Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA  02110-1301  USA
*)

(*
    Derived from the original parse-tree

    Copyright (c) 2000
        Cambridge University Technical Services Limited

    Further development:
    Copyright (c) 2000-13 David C.J. Matthews

    Title:      Parse Tree Structure and Operations.
    Author:     Dave Matthews, Cambridge University Computer Laboratory
    Copyright   Cambridge University 1985

*)


functor TYPECHECK_PARSETREE (

structure BASEPARSETREE : BaseParseTreeSig
structure PRINTTREE: PrintParsetreeSig
structure EXPORTTREE: ExportParsetreeSig
structure LEX : LEXSIG
structure CODETREE : CODETREESIG
structure STRUCTVALS : STRUCTVALSIG;
structure TYPETREE : TYPETREESIG
structure VALUEOPS : VALUEOPSSIG;
structure PRETTY : PRETTYSIG
structure COPIER: COPIERSIG
structure DATATYPEREP: DATATYPEREPSIG

structure UTILITIES :
sig
    type lexan;
    type location =
        { file: string, startLine: FixedInt.int, startPosition: FixedInt.int,
          endLine: FixedInt.int, endPosition: FixedInt.int }

    val noDuplicates: (string * 'a * 'a -> unit) -> 
                       { apply: (string * 'a -> unit) -> unit,
                         enter:  string * 'a -> unit,
                         lookup: string -> 'a option};

    val searchList: unit -> { apply: (string * 'a -> unit) -> unit,
                            enter:  string * 'a -> unit,
                            lookup: string -> 'a option };

    val checkForDots:  string * lexan * location -> unit;

    val splitString: string -> { first:string,second:string }

    structure Sharing:
    sig
        type lexan = lexan
    end
end

structure PRINTTABLE :
sig
    type typeConstrs
    type codetree

    val getOverloads: string -> (typeConstrs * codetree) list

    structure Sharing:
    sig
        type codetree = codetree
        and  typeConstrs = typeConstrs
    end
end;

structure MISC :
sig  
    exception InternalError of string; (* compiler error *)

    val quickSort : ('a -> 'a -> bool) -> 'a list -> 'a list;

    val lookupDefault :  ('a -> 'b option) -> ('a -> 'b option) -> 'a -> 'b option
end

sharing LEX.Sharing = TYPETREE.Sharing = STRUCTVALS.Sharing = COPIER.Sharing
       = VALUEOPS.Sharing = UTILITIES.Sharing = PRETTY.Sharing
       = CODETREE.Sharing = PRINTTABLE.Sharing = DATATYPEREP.Sharing
       = BASEPARSETREE.Sharing = PRINTTREE.Sharing = EXPORTTREE.Sharing

): TypeCheckParsetreeSig =
   
struct
    open MISC
    open LEX
    open CODETREE
    open STRUCTVALS
    open TYPETREE
    open VALUEOPS
    open UTILITIES
    open PRETTY
    open PRINTTABLE
    open DATATYPEREP
  
    open BASEPARSETREE
    open PRINTTREE
    open EXPORTTREE
  
    val emptyType            = EmptyType
    val badType              = BadType
  
   (* Second pass of ML parse tree. *)
   
    (* This is pass 2 of the compiler. It walks over the parse tree
       generated by pass 1 and looks up identifiers to match them to
       declarations. It performs the type checking. "makeTypeId" is used
       to construct unique identifiers for types depending on the context
       (i.e. in a signature, structure or functor). *)
    fun pass2 (v, makeTypeId, env, lex, sigTypeIdMap) =
    let
        (* Returns a function which can be passed to unify or apply to
           print a bit of context info. *)
        fun foundNear v () =
        let
            val errorDepth = errorDepth lex
        in
            displayParsetree (v, errorDepth)
        end

      (* A simpler error message routine for lookup_... where the message
         does not involve pretty-printing anything. *)
      fun giveError (v, lex, line)  =
        fn message => errorNear (lex, true, v, line, message);

      fun checkForBuiltIn (name, v, lex, lineno, isConstr) =
      (* ML97 does not allow the standard constructors to be rebound and does
         not allow "it" to become a constructor. *)
         if name = "true" orelse name = "false" orelse name = "nil"
         orelse name = "::" orelse name = "ref" orelse (isConstr andalso name = "it")
         then errorNear(lex, true, v, lineno,
                     "Rebinding or specifying \"" ^ name ^ "\" is illegal")
         else ()

        (* Turn a result from unifyTypes into a pretty structure so that it
           can be included in a message. *)
        fun unifyErrorReport(lex, typeEnv) = unifyTypesErrorReport(lex, typeEnv, typeEnv, "unify")

        (* Error message for incompatible types.  Displays both expressions and their types. *)
        fun typeMismatch (title, left, right, detail, lex : lexan, location, moreInfo) =
        let
            val message =
                PrettyBlock(3, true, [],
                    [
                        PrettyString title,
                        PrettyBreak(1, 0), left,
                        PrettyBreak(1, 0), right,
                        PrettyBreak(1, 0),
                        PrettyBlock(0, false, [],
                            [PrettyString "Reason:", PrettyBreak(1, 3), detail])
                    ])
        in
            reportError lex
            {
                location = location,
                hard = true,
                message = message,
                context = SOME (moreInfo ())
            }
        end;

        (* Error message for single expressions with the wrong type. e.g. "if" not followed
           by a "bool". *)
        fun typeWrong (title, value, detail, lex : lexan, location, moreInfo) =
        let
            val message =
                PrettyBlock(3, true, [],
                    [
                        PrettyString title,
                        PrettyBreak(1, 0), value,
                        PrettyBreak(1, 0),
                        PrettyBlock(0, false, [],
                            [ PrettyString "Reason:", PrettyBreak(1, 3), detail])
                    ])
        in
            reportError lex
            {
                location = location,
                hard = true,
                message = message,
                context = SOME (moreInfo ())
            }
        end;

        (* Display a value and its type as part of an error message. *)
        fun valTypeMessage (lex, typeEnv) (title, value, valType) =
        let
            val errorDepth = errorDepth lex
        in
            PrettyBlock(3, false, [],
                [
                    PrettyString title,
                    PrettyBreak(1, 0),
                    displayParsetree (value, errorDepth),
                    PrettyBreak(1, 0),
                    PrettyString ":",
                    PrettyBreak(1, 0),
                    display(valType, 10000 (* All of it *), typeEnv)
                ])
        end

        fun matchTypeMessage (lex, typeEnv) (title, match, valType) =
        let
            val errorDepth = errorDepth lex
        in
            PrettyBlock(3, false, [],
                [
                    PrettyString title,
                    PrettyBreak(1, 0),
                    displayMatch (match, errorDepth),
                    PrettyBreak(1, 0),
                    PrettyString ":",
                    PrettyBreak(1, 0),
                    display(valType, 10000 (* All of it *), typeEnv)
                ])
        end

        (* Old error message and unification functions.  These will eventually be
           removed.  *)
        fun matchError 
            (error: matchResult, lex : lexan, location : LEX.location, moreInfo : unit -> pretty, typeEnv) : unit =
            reportError lex
            {
                location = location,
                hard = true,
                message = unifyErrorReport(lex, typeEnv) error,
                context = SOME (moreInfo ())
           }

        fun unify (alpha, beta, lex, location, moreInfo, typeEnv) =
            case unifyTypes (alpha, beta) of
                NONE => ()
            |   SOME error =>
                    matchError (error, lex, location, moreInfo, typeEnv)

        fun apply (f, arg, lex, location, moreInfo, typeEnv) =
            case eventual f of
                FunctionType {arg=farg, result} =>
                (
                    unify (farg, arg, lex, location, moreInfo, typeEnv);
                    result
                )
            |   ef => (* Type variables etc. - Use general case. *)
                let  (* Make arg->'a, and unify with the function. *)
                    val resType  = mkTypeVar (generalisable, false, false, false)
                    val fType    = mkFunctionType (arg, resType)
      
                    (* This may involve more than just assigning the type to "ef". *)
                    val () = unify (ef, fType, lex, location, moreInfo, typeEnv);
                in
                    resType (* The result is the type variable unified to the result. *)
                end

        (* These cases currently use the "apply" or "unify" and may need to be improved in
           order to produce better messages.
           apply:
              Literals.  The conversion functions are applied to the string literal.  In effect this produces the set
              of overloadings of the literal.  This should never produce an error message.
              Constructors in patterns to their args.
              "case": the patterns are "applied" to the value to be tested.

           unify:
              Layered patterns, to set the variable. Also checks the pattern against any explicit type.
              Handlers: the handling patterns are unified against a function from exn -> the result type of the
              expression being handled.
         *)

    fun stringsOfSearchList { apply: (string * 'a -> unit) -> unit, ...} () =
    let
        val v = ref []
        val () = apply (fn (s, _) => v := s :: !v)
    in
        !v
    end

    fun assignValues (level, letDepth, env, near, v)  =
    let
        val typeEnv =
        {
            lookupType = fn s => case #lookupType env s of NONE => NONE | SOME t => SOME(t, NONE),
            lookupStruct = fn s => case #lookupStruct env s of NONE => NONE | SOME t => SOME(t, NONE)
        }
         (* Process each item of the sequence and return the type of the
            last item. A default item is returned if the list is empty. *)
        fun assignSeq(env, depth, l, isExp) =
        let
            fun applyList last []       = last
            |   applyList _ ((h, _) :: t) =
                let
                    val expT = assignValues(level, depth, env, v, h)
                    val _ =
                        if isExp andalso not (null t)
                        then (* It's not the last value and we're going to discard it *)
                        case checkDiscard(expT, lex) of
                            NONE => ()
                        |   SOME s => errorNear (lex, false, h, getLocation h, s)
                        else ()
                in
                    applyList expT t
                end
        in
            applyList badType l
        end

        (* Variables, constructors and fn are non-expansive.
           [] is a derived form of "nil" so must be included.
           Integer and string constants are also constructors but
           cannot involve imperative type variables. Constrained
           versions are also non-expansive.
           This has been extended and made more explicit in ML 97. *)
        fun nonExpansive (Fn _)   = true
        |   nonExpansive (Ident _) = true
        |   nonExpansive (List{elements = [], ...}) = true
        |   nonExpansive (List{elements, ...}) =
                List.foldl (fn (v, a) => a andalso nonExpansive v) true elements
        |   nonExpansive (Constraint {value, ...}) = nonExpansive value
        |   nonExpansive (Literal _) = true
        |   nonExpansive (Unit _) = true
        |   nonExpansive (TupleTree{fields, ...}) = 
                List.foldl (fn (v, a) => a andalso nonExpansive v) true fields
        |   nonExpansive (Labelled{recList, ...}) =
                List.foldl (fn ({valOrPat, ...}, a) => a andalso nonExpansive valOrPat)
                        true recList (* Every element must be non-expansive *)
        |   nonExpansive (Applic{f, arg, ...}) =
                isNonRefConstructor f andalso nonExpansive arg
        |   nonExpansive (Selector _) = true (* derived from fn {..} => ...*)
        |   nonExpansive (Parenthesised(p, _)) = nonExpansive p
        |   nonExpansive _       = false

        (* An application is non-expansive only if it is a, possibly
           constrained, constructor which is not ref. *)
        and isNonRefConstructor (Ident {value=ref v, ...}) =
            (* It is possible to rebind ref by way of datatype replication so we have
               to check the type here. *)
            let
                fun isRefConstructor t =
                    case eventual t of
                        FunctionType{result, ...} =>
                            (case eventual result of
                                TypeConstruction{constr, ...} =>
                                    sameTypeId (tcIdentifier constr, tcIdentifier refConstr)
                            |   _ => false)
                    |   _ => false
            in
                isConstructor v andalso not (isRefConstructor(valTypeOf v))
            end
        | isNonRefConstructor (Constraint {value, ...}) =
                isNonRefConstructor value
        | isNonRefConstructor (Parenthesised(p, _)) =
                isNonRefConstructor p
        | isNonRefConstructor _ = false

        (* Applies "assignValues" or "processPattern" to every element of a list and unifies the
           types. Returns a type variable if the list is empty.
           This is used for lists, function values (fn .. => ...),
           handlers and case expressions. *)
        fun assignList _ _ [] = mkTypeVar (generalisable, false, false, false)
        |   assignList (processValue: 'a->types, _, _) _ [single] = processValue single

        |   assignList (processValue: 'a->types, displayValue, typeMsg)
                            (errorMsg, itemName, separator, location, near) (tlist as hd :: tl) =
            let
                val firstType = processValue hd

                fun printList (doPrint: 'a*FixedInt.int->pretty) (c: 'a list, separator, depth): pretty list =
                    if depth <= 0 then [PrettyString "..."]
                    else
                    case c of
                        []      => []
                    |   [v]     => [doPrint (v, depth)]
                    |   (v::vs) =>
                            PrettyBlock (0, false, [],
                                [
                                    doPrint (v, depth),
                                    PrettyBreak
                                       (if separator = "," orelse separator = ";" orelse separator = "" then 0 else 1, 0),
                                    PrettyString separator
                                ]
                                ) ::
                            PrettyBreak (1, 0) ::
                            printList doPrint (vs, separator, depth - 1)

                fun applyList(ty, _, []) = ty
                |   applyList(ty, n, h::t) =
                    let
                        val typ = processValue h
                    in
                        case unifyTypes (ty, typ) of
                            NONE => applyList(ty, n+1, t)
                        |   SOME report =>
                            let
                                (* We have a type error but we don't know which is correct.
                                   The previous items must have produced a consistent type
                                   otherwise we'd already have reported an error but we
                                   can't identify exactly where the error occurred. *)
                                val errorDepth = errorDepth lex
                                val previousValsAndType =
                                    PrettyBlock(3, false, [],
                                        [
                                            PrettyString (
                                                if n = 1 then itemName ^ " 1:"
                                                else itemName ^ "s 1-" ^ Int.toString n ^ ":"),
                                            PrettyBreak(1, 0),
                                            PrettyBlock(0, false, [],
                                                printList (*displayParsetree*)displayValue (List.take(tlist, n),
                                                separator, errorDepth)),
                                            PrettyBreak(1, 0),
                                            PrettyString ":",
                                            PrettyBreak(1, 0),
                                            display(ty, 10000 (* All of it *), typeEnv)
                                        ])
                            in
                                typeMismatch(errorMsg,
                                    previousValsAndType,
                                    (*valTypeMessage*)typeMsg(lex, typeEnv) (concat[itemName, " ", Int.toString(n+1), ":"], h, typ),
                                    unifyErrorReport(lex, typeEnv) report, lex, location, foundNear near);
                                (* Continue with "bad" which suppresses further error messages
                                   and return "bad" as the result. *)
                                applyList(badType, n+1, t)
                            end
                    end
            in
                applyList(firstType, 1, tl)
            end

        fun ptAssignTypes (t, near) =
            assignTypes
                (t,
                fn (s, line) => 
                    lookupTyp 
                        ({lookupType = #lookupType env, lookupStruct = #lookupStruct env},
                        s, giveError (near, lex, line)),
                lex);

        (* Makes a type for an instance of an identifier. *)

        (* Get the current overload set for the function and return a new
           instance of the type containing the overload set. *)
        fun overloadType(Value{typeOf, access = Overloaded TypeDep, name, ...}, isConv) =
                #1 (generaliseOverload(typeOf, List.map #1 (getOverloads name), isConv))
        |   overloadType(Value{typeOf, ...}, _) =  #1 (generalise typeOf)

        fun instanceType (v as Value{access=Overloaded TypeDep, ...}) =
          (* Look up the current overloading for this function. *)
                overloadType(v, false)

        |   instanceType(Value{typeOf, ...}) = #1 (generalise typeOf)
            (* The types of constructors and variables are copied 
               to create new instances of type variables. *)

        fun processPattern(pat, enterResult, level, notConst, mkVar, isRec) =
        let
            val mapProcessPattern =
                map (fn x => processPattern(x, enterResult, level, notConst, mkVar, isRec));
        in
            case pat of
                Ident {name, value, expType, location, possible, ...} => (* Variable or nullary constructor. *)
                let
                    (* Look up the name. If it is a constructor then use it,
                        otherwise return `undefined'. If it is a qualified name,
                        i.e. it contains a full-stop, we assume it is a constructor
                        and give an error message if it does not exist. *)
                    (* In ML 97 recursive declarations such as val rec f = ...
                         override constructor status.  If this is a recursive declaration
                         we don't check for constructor status. *)
                    val names   = splitString name;
                    val nameVal =
                        if isRec
                        then undefinedValue
                        else if #first names = ""
                        then (* Not qualified - may be a variable. *)
                            getOpt (#lookupVal env name, undefinedValue) 
              
                        else (* Qualified - cannot be a variable. *)
                            lookupValue
                                ("Constructor",
                                {lookupVal= #lookupVal env, lookupStruct= #lookupStruct env},
                                name,
                                giveError (pat, lex, location))

                    (* Remember the possible names here. *)
                    val () = possible := #allValNames env

                    val instanceType = 
                        (* If the result is a constructor use it. *)
                        if isConstructor nameVal (* exceptions. *)
                        then if notConst
                        then
                        (
                            errorNear (lex, true, pat, location,
                                    "Identifier before `as' must not be a constructor.");
                            badType
                        )
                        else
                        (* Must be a nullary constructor otherwise it should
                           have been applied to something. *)
                        let
                            (* set this value in the record *)
                            val () = value := nameVal;
                            val isNullary =
                                case nameVal of
                                    Value{class=Constructor{nullary, ...}, ...} => nullary
                                |   Value{typeOf, ...} => (* exception *) not (isSome(getFnArgType typeOf))
                        in
                            if isNullary then instanceType nameVal
                            else
                            (
                                errorNear (lex, true, pat, location,
                                            "Constructor must be applied to an argument pattern.");
                                badType
                            )
                        end
      
                        (* If undefined or another variable, construct a new variable. *)
                        else
                        let
                            val props = [DeclaredAt location, SequenceNo (newBindingId lex)]
                            val var =  mkVar(name, mkTypeVar (level, false, false, false), props)
                        in
                            checkForDots (name, lex, location); (* Must not be qualified *)
                            (* Must not be "true", "false" etc. *)
                            checkForBuiltIn (name, v, lex, location, false);
                            enterResult (name, var);
                            value := var;
                            valTypeOf var (* and return its type *)
                        end;
                in
                    expType := instanceType; (* Record the instance type.*)
                    instanceType
                end
    
            |   Literal{converter, expType, location, ...} =>
                let
                    (* Find out the overloadings on this converter and
                       construct an instance of it.  The converters are
                       all functions from string to the result type. *)
                    val instanceType = overloadType(converter, true)
                    (* Apply the converter to string to get the type of the
                       literal. *)
                    val instance =
                        apply(instanceType, stringType, lex, location, foundNear pat, typeEnv)
                in
                    expType := instance; (* Record the instance type.*)
                    instance
                end

            |   Applic {f = con, arg, location, expType, ...} =>
                let
                    (* Apply the function to the argument and return the result. *)
                    (* Function must be a constructor. *)
                    val conType = 
                        case con of
                            Ident {name, value, location, expType, possible, ...} =>
                            let (* Look up the value and return the type. *)
                            
                                (* Remember the possible names here. *)
                                val () = possible := #allValNames env

                                val constrVal =
                                    lookupValue 
                                        ("Constructor",
                                        {lookupVal   = #lookupVal env, lookupStruct = #lookupStruct env},
                                        name, giveError (pat, lex, location));
                            in
                                if isConstructor constrVal
                                then
                                let
                                    val cType = instanceType constrVal
                                in
                                    value := constrVal;
                                    expType := cType; (* Record the instance type.*)
                                    cType
                                end
                                else (* Undeclared or a variable. *)
                                (
                                    if isUndefinedValue constrVal then ()
                                    else errorNear (lex, true, pat, location, name ^ " is not a constructor");
                                    badType
                                )
                            end
        
                        |   _ => (* con is not an Ident *)
                            (
                                errorNear (lex, true, pat, location,
                                    "Constructor in a pattern was not an identifier");
                                badType
                            )
    
                    val patType = processPattern(arg, enterResult, level, notConst, mkVar, isRec);
                    (* Apply to the pattern type. *)
                    val resultType = apply (conType, patType, lex, location, foundNear pat, typeEnv)
                in
                    expType := resultType; (* Record the instance type.*)
                    resultType
                end (* Applic *)

            |   TupleTree{fields, expType, ...} =>
                let
                    (* Construct the type obtained by mapping "processPattern"
                       onto each element of the tuple. *)
                    val tupleType = mkProductType (mapProcessPattern fields)
                in
                    expType := tupleType;
                    tupleType
                end

            |   Labelled {recList, frozen, expType, ...} =>
                let (* Process each item in the list. *)

                    fun mapLabels [] = []
                    |   mapLabels ({name, valOrPat, expType, ...}::T) =
                        (* Type is a label entry with the label name
                           and the type of the pattern. *)
                        let
                            val ty = processPattern(valOrPat, enterResult, level, notConst, mkVar, isRec)
                        in
                            expType := ty;
                            mkLabelEntry(name, ty) :: mapLabels T
                        end;
                    val patType = mkLabelled (sortLabels(mapLabels recList), frozen);
                in
                    expType := patType;
                    patType
                end

            |   (aList as List{elements, location, expType}) =>
                let
                    (* Applies "processPattern" to every element of a list and
                       unifies the types. Returns a type variable if the list
                       is empty *)
                    fun processElement elem =
                        processPattern(elem, enterResult, level, notConst, mkVar, isRec)
                    val elementType =
                        assignList (processElement, displayParsetree, valTypeMessage)
                            ("Elements in a list have different types.", "Item", ",", location, aList) elements
                    val resType =
                        if isBadType elementType
                        then badType
                        else mkTypeConstruction ("list", tsConstr listConstr, [elementType], [DeclaredAt inBasis])
                in
                    expType := resType;
                    resType
                end

            |   aConstraint as Constraint {value, given, location} =>
                let
                    val valType  = processPattern(value, enterResult, level, notConst, mkVar, isRec);
                    val theType = ptAssignTypes(given, pat);
                in
                    (* These must be unifiable. *)
                    case unifyTypes(valType, theType) of
                        NONE => () (* OK. *)
                    |   SOME report =>
                            typeMismatch("Type mismatch in type constraint.",
                                valTypeMessage (lex, typeEnv) ("Value:", value, valType),
                                PrettyBlock(0, false, [],
                                    [
                                        PrettyString "Constraint:",
                                        PrettyBreak(1, 0),
                                        display(theType, 10000 (* All of it *), typeEnv)
                                    ]),
                                unifyErrorReport (lex, typeEnv) report,
                                lex, location, foundNear aConstraint);
                    theType
                end

            |   Layered {var, pattern, location} =>
                let
                    (* Unify the variable and the pattern - At this stage that simply
                     involves assigning the type of the pattern to the variable,
                     but it may result in more unification when the variable is
                     used *)
              
                    (* The "variable" must be either id or id: ty but we have to
                     check that the id is not a constructor. *)
                    val varType = processPattern(var,     enterResult, level, true, mkVar, isRec);
                    val patType = processPattern(pattern, enterResult, level, notConst, mkVar, isRec)
                    val () = unify (varType, patType, lex, location, foundNear pat, typeEnv);
                in
                    varType
                end

            |   Unit _ => unitType

            |   WildCard _ => mkTypeVar (generalisable, false, false, false)

            |   Parenthesised(p, _) =>
                    processPattern(p, enterResult, level, notConst, mkVar, isRec)

            |   _ => (* not a legal pattern *)
                    badType

        end (* processPattern *)

        (* val assValues = assignValues level line env; *)
        and assValues near v =
          case v of
            Ident {name, value, expType, location, possible, ...} =>
            let
                val expValue =
                    lookupValue 
                        ("Value or constructor",
                            {lookupVal = #lookupVal env, lookupStruct = #lookupStruct env},
                            name, giveError (near, lex, location));
                (* Set the value and type found. *)
                val instanceType = instanceType expValue;
            in
                (* Include this reference in the list of local references. *)
                case expValue of
                    Value { references=SOME{localRef, ...}, ...} =>
                        localRef := location :: ! localRef
                |   _ => ();
                (* Include this type in the list of instance types. *)
                case expValue of
                    Value { instanceTypes=SOME instanceRef, ...} =>
                        instanceRef := instanceType :: ! instanceRef
                |   _ => ();
                expType := instanceType;
                value  := expValue;
                possible := #allValNames env;
                instanceType (* Result is the instance type. *)
            end

          | Literal{converter, expType, location, ...} =>
            let
                (* Find out the overloadings on this converter and
                   construct an instance of it.  The converters are
                   all functions from string to the result type. *)
                val instanceType = overloadType(converter, true)
                val instance =
                    apply(instanceType, stringType, lex, location, foundNear near, typeEnv)
            in
                expType := instance;
                instance
            end

          | Applic {f, arg, location, expType, ...} => 
            let
                (* Apply the function to the argument and return the result. *)
                val funType = assValues near f;
                val argType = assValues near arg;
                (* If this is not a constructor the expression is expansive.  We need to unify this
                   with a type-variable with local (non-generalisable) scope to force any type
                   variables to be monomorphic.  The reason for this is that if there are polymorphic
                   type variables remaining in identifiers in the next pass we treat the identifier as
                   polymorphic and wrap a function round it. *)
                val () =
                    if nonExpansive v
                    then ()
                    else (unifyTypes (funType, mkTypeVar(level, false, false, false)); ())
                (* Test to see if we have a function. *)
                val fType =
                    case eventual funType of
                        FunctionType {arg, result} => SOME(arg, result)
                    |   _ => (* May be a simple type variable. *)
                        let
                            val funResType = mkTypeVar (generalisable, false, false, false)
                            val funArgType = mkTypeVar (generalisable, false, false, false)
                            val fType    = mkFunctionType (funArgType, funResType)
                        in
                            case unifyTypes (fType, funType) of
                                NONE => SOME(funArgType, funResType)
                            |   SOME _ =>
                                (
                                    (* It's not a function. *)
                                    typeMismatch("Type error in function application.",
                                        valTypeMessage (lex, typeEnv) ("Function:", f, funType),
                                        valTypeMessage (lex, typeEnv) ("Argument:", arg, argType),
                                        PrettyString "Value being applied does not have a function type",
                                        lex, location, foundNear near);
                                    NONE
                                )
                        end

            in
                case fType of
                    NONE => badType (* Not a function *)
                |   SOME (fArg, fResult) =>
                    (
                        case unifyTypes (fArg, argType) of
                            NONE => ()
                        |   SOME report =>
                                typeMismatch("Type error in function application.",
                                    valTypeMessage (lex, typeEnv) ("Function:", f, funType),
                                    valTypeMessage (lex, typeEnv) ("Argument:", arg, argType),
                                    unifyErrorReport (lex, typeEnv) report, lex, location, foundNear near);
                        expType := fResult; (* Preserve for browsing. *)
                        fResult
                    )
            end

          | Cond {test, thenpt, elsept, location, ...} =>
            let
                (* The test must be bool, and the then and else parts must be the
                   same. The result is either of these two once they have been
                   unified. *)
                val testType = assValues v test;
                val thenType = assValues v thenpt;
                val elseType = assValues v elsept;
            in
                case unifyTypes(testType, boolType) of
                    NONE => ()
                |   SOME report =>
                        typeWrong("Condition in if-statement must have type bool.",
                            valTypeMessage (lex, typeEnv) ("If:", test, testType),
                            unifyErrorReport (lex, typeEnv) report, lex, location, foundNear v);

                case unifyTypes(thenType, elseType) of
                    NONE => thenType (* or equally elseType *)
                |   SOME report =>
                    (
                        typeMismatch("Type mismatch between then-part and else-part.",
                            valTypeMessage (lex, typeEnv) ("Then:", thenpt, thenType),
                            valTypeMessage (lex, typeEnv) ("Else:", elsept, elseType),
                            unifyErrorReport (lex, typeEnv) report, lex, location, foundNear v);
                        badType
                    )
            end

            |   TupleTree{fields, expType, ...} =>
                let
                    (* Construct the type obtained by mapping "assignValue" onto
                       each element of the tuple. *)
                    val tupleType = mkProductType (map (assValues near) fields)
                in
                    expType := tupleType;
                    tupleType
                end
          
          | Labelled {recList, frozen, expType, ...} =>
            let
                (* Process each item in the list. *)              
                fun labEntryToLabType {name, valOrPat, expType, ...} =
                let
                    val ty = assValues v valOrPat
                in
                    expType := ty;
                    {name = name, typeof = ty }
                end
            
              val expressionType =
                mkLabelled 
                  (sortLabels (map labEntryToLabType recList), frozen) (* should always be true *);
            in
                expType := expressionType;
                expressionType
            end

          | Selector {typeof, ...} =>
              typeof (* Already made. *)

          | ValDeclaration {dec, explicit, implicit, ...} =>
                (assValDeclaration (dec, explicit, implicit); badType (* Should never be used. *))

          | FunDeclaration fund =>
                (assFunDeclaration fund; badType (* Should never be used. *))

          | OpenDec{decs=ptl, variables, structures, typeconstrs, ...} =>
                let
                    (* Go down the list of names opening the structures. *)
                    (* We have to be careful because open A B is not the same as
                       open A; open B if A contains a structure called B. *)
                    (* We accumulate the values so that we can produce debugging
                       information if we need to.  Note: we have to be careful if
                       we have the same name in multiple structures. *)
                    val valTable = HashTable.hashMake 10
                    and typeTable = HashTable.hashMake 10
                    and structTable = HashTable.hashMake 10
    
                    (* First get the structures... *)
                    fun findStructure ({name, location, value, ...}: structureIdentForm) =
                    let
                        val foundStruct =
                            lookupStructure
                                ("Structure", {lookupStruct = #lookupStruct env}, name,
                                    giveError (v, lex, location))
                        val () = value := foundStruct (* Remember in case we export. *)
                    in
                        case foundStruct of
                            SOME str => SOME(str, location)
                        |   NONE => NONE
                    end
        
                    val strs = List.mapPartial findStructure ptl
                        
                    (* Value and substructure entries in a structure will generally have
                       "Formal" access which simply gives the offset of the entry within
                       the parent structure.  We need to convert these into "Select"
                       entries to capture the address of the base structure. *)
                    fun copyEntries (str as Struct{locations, signat = sigTbl, name=strName, ...}, varLoc) =
                    let
                        val openLocs =
                        (* If we have a declaration location for the structure set this as the structure
                           location.  Add in here as the "open location". *)
                            case List.find (fn DeclaredAt _ => true | _ => false) locations of
                                SOME (DeclaredAt loc) => [StructureAt loc, OpenedAt varLoc]
                            |   _ => [OpenedAt varLoc]

                        (* Open the structure.  Formal entries are turned into Selected entries. *)
                        val _ =
                            COPIER.openSignature 
                            (sigTbl,
                            {
                                enterType   =
                                fn (name, TypeConstrSet(ty, valConstrs)) =>
                                    let
                                        (* We also have to turn the value constructors into
                                           "selected" entries in case we use datatype
                                           replication. Unlike with "include" in signatures,
                                           there's no guarantee that the constructors will also
                                           be part of the value environment. They could have
                                           been redefined. *)
                                        val newTypeSet =
                                            TypeConstrSet(ty,
                                                List.map (fn c => mkSelectedVar (c, str, openLocs)) valConstrs)
                                    in
                                        HashTable.hashSet(typeTable, name, newTypeSet);
                                        #enterType env (name, newTypeSet)
                                    end,
                                enterStruct =
                                fn (name, strVal) =>
                                    let
                                        val selectedStruct = 
                                            makeSelectedStruct (strVal, str, openLocs);
                                    in
                                        HashTable.hashSet(structTable, name, selectedStruct);
                                        #enterStruct env (name, selectedStruct)
                                    end,
                                enterVal    =
                                fn (name, value) =>
                                    let
                                        val selectedVar = 
                                            mkSelectedVar (value, str, openLocs);
                                    in
                                        HashTable.hashSet(valTable, name, selectedVar);
                                        #enterVal env (name, selectedVar)
                                    end
                            },
                            (* Add the structure we're opening here to the types of
                               the values.  The name will be removed in messages if the type
                               constructor is in scope but if it has been redefined we can
                               get an identifiable name. *)
                            strName ^ ".");
                    in
                        ()
                    end
    
                    (* ...then put them into the name space. *)
                    val () = List.app copyEntries strs;
                in
                    variables := HashTable.fold (fn (_, v, t) => v :: t) [] valTable;
                    structures := HashTable.fold (fn (_, v, t) => v :: t) [] structTable;
                    typeconstrs := HashTable.fold (fn (_, v, t) => v :: t) [] typeTable;
                    badType (* Does not return a type *)
                end
    
          | TypeDeclaration(tlist, _) =>
            let (* This is either a type abbreviation in the core language, in a structure
                   or in a signature or it is a type specification in a signaure. *)
                fun messFn(name, _, new) = 
                    errorNear (lex, true, v, declaredAt(tcLocations new),
                        name ^ " has already been bound in this declaration");
               
                val newEnv = noDuplicates messFn;
              
                (* First match all the types on the right-hand sides. *)
                fun processTypeBody (TypeBind {decType = SOME decType, ...}) = ptAssignTypes(decType, v)
                |   processTypeBody _ = emptyType (* Specification. *)
                
                val resTypes = List.map processTypeBody tlist;
              
                (* Can now declare the new types. *)
                fun processType (TypeBind {name, typeVars, isEqtype, nameLoc, tcon=tcRef, ...}, decType) =
                let
                    (* Construct a type constructor which is an alias of the
                       right-hand side of the declaration.  If we are effectively
                       giving a new name to a type constructor we use the same type
                       identifier.  This is needed to check "well-formedness" in signatures. *)
                    val props = [DeclaredAt nameLoc, SequenceNo (newBindingId lex)]

                    val tcon =
                        if isEmpty decType
                        then (* Type specification *)
                        let
                            val description = { location = nameLoc, name = name, description = "" }
                        in
                            makeTypeConstructor (name, typeVars,
                                makeTypeId(isEqtype, false, (typeVars, EmptyType), description), props)
                        end
                        else case typeNameRebinding(typeVars, decType) of
                            SOME typeId =>
                                makeTypeConstructor (name,  typeVars,typeId, props)
                        |   NONE =>
                            let
                                val description = { location = nameLoc, name = name, description = "" }
                            in
                                makeTypeConstructor (name, typeVars,
                                    makeTypeId(isEqtype, false, (typeVars, decType), description), props)
                            end
                in
                    checkForDots  (name, lex, nameLoc); (* Must not be qualified *)
                    #enter newEnv (name, tcon); (* Check for duplicates. *)
                    tcRef := TypeConstrSet(tcon, []);
                    #enterType env  (name, TypeConstrSet(tcon, []))  (* Put in the surrounding scope. *)
                end
                   
                val () = ListPair.app processType (tlist, resTypes);
            in
                badType (* Does not return a type *)
            end
        
          | AbsDatatypeDeclaration absData => assAbsData absData

          | DatatypeReplication{oldType, newType, oldLoc, newLoc, ...} =>
                  (* Adds both the type and the constructors to the
                   current environment. *)
              let
                (* Look up the type constructor in the environment. *)
                val oldTypeCons: typeConstrSet =
                    lookupTyp 
                         ({lookupType = #lookupType env, lookupStruct = #lookupStruct env},
                          oldType,
                          giveError (near, lex, oldLoc))

                (* Copy the datatype, converting any Formal constructors to Selected. *)
                local
                    (* If the type name was qualified (e.g. S.t) we need to find the
                       value constructors from the same structure. *)
                    val {first = namePrefix, ...} = splitString oldType;
                    val baseStruct =
                        if namePrefix = ""
                        then NONE
                        else lookupStructure("Structure", {lookupStruct = #lookupStruct env},
                                    namePrefix, giveError (v, lex, oldLoc))
                    val TypeConstrSet(tcons, tcConstructors) = oldTypeCons
                    val newName = newType
                    val locations = [DeclaredAt newLoc, SequenceNo (newBindingId lex)]
                    (* Create a new constructor with the same unique ID. *)
                    val typeID = tcIdentifier tcons
                    val newTypeCons = makeTypeConstructor(newName, tcTypeVars tcons, typeID, locations)
    
                    (* Copy the value constructors. *)
                    fun copyAConstructor(Value{name=cName, typeOf, class, access, ...}) =
                        let
                            (* Copy the types of value constructors replacing
                               occurrences of the old type with the new one.
                               This is not strictly necessary but improves printing.
                               e.g. local datatype X = A | B in datatype Y = datatype X end;
                               A; prints  A: Y rather than A: X *)
                            fun copyTypeCons (tcon : typeConstrs) : typeConstrs =
                                if sameTypeId(tcIdentifier tcon, typeID)
                                then newTypeCons
                                else tcon;
                            fun copyTyp (t : types) : types =
                               copyType (t, fn x => x, (* Don't bother with type variables. *)
                                   copyTypeCons);
                            val newType = copyTyp typeOf;
                            val newAccess =
                                case (access, baseStruct) of
                                    (* If we are opening a structure we must have a base structure
                                       and we turn Formal entries into Selected.  If we are replicating
                                       a datatype within a signature the original constructors will
                                       be Formal. *)
                                    (Formal addr, SOME(Struct{access, ...})) => Selected{base=access, addr=addr}
                                |    (Formal _, NONE) => access
                                |    _ => access; (* Probably already a global. *)
                        in
                            Value{name=cName, typeOf=newType, class=class, access=newAccess, locations=locations,
                                  references = NONE, instanceTypes=NONE}
                        end

                in
                    val newValConstrs = map copyAConstructor tcConstructors
                    val newTypeCons = TypeConstrSet(newTypeCons, newValConstrs)
                end
            in
                (* This previously checked that it was a datatype but that's
                   not actually correct. *)
                (* Enter the value constrs in the environment. *)
                List.app (fn c => (#enterVal env) (valName c, c)) newValConstrs;
                (* Add this type constructor to the environment. *)
                (#enterType env) (newType, newTypeCons);
                badType (* Does not return a type *)
            end

          | (aList as List{elements, location, expType, ...}) =>
            let
                val elementType =
                    assignList(assValues v, displayParsetree, valTypeMessage)
                        ("Elements in a list have different types.", "Item", ",", location, aList) elements
                val resType =
                    if isBadType elementType
                    then badType
                    else mkTypeConstruction ("list", tsConstr listConstr, [elementType], [DeclaredAt inBasis])
            in
                expType := resType;
                resType
            end

          | Constraint {value, given, location} =>
            let
                val valType = assValues near value;
                val theType = ptAssignTypes(given, v)
            in
                (* These must be unifiable. *)
                case unifyTypes(valType, theType) of
                    NONE => () (* OK. *)
                |   SOME report =>
                        typeMismatch("Type mismatch in type constraint.",
                            valTypeMessage (lex, typeEnv) ("Value:", value, valType),
                            PrettyBlock(0, false, [],
                                [
                                    PrettyString "Constraint:",
                                    PrettyBreak(1, 0),
                                    display(theType, 10000 (* All of it *), typeEnv)
                                ]),
                            unifyErrorReport (lex, typeEnv) report,
                            lex, location, foundNear v);
                theType
            end

          | (aFun as Fn {matches, location, expType, ...}) =>  (* Must unify the types of each of the alternatives.*)
            let
                val resType =
                    assignList(assMatchTree aFun, displayMatch, matchTypeMessage)
                        ("Clauses in fn expression have different types.", "Clause", "|", location, aFun) matches
            in
                expType := resType;
                resType
            end

          | Unit _ =>
              unitType

          | Localdec {decs, body, isLocal, varsInBody, ...} =>
            let (* Local declarations or expressions. *)
              val newValEnv  = searchList();
              val newTypeEnv = searchList();
              val newStrEnv  = searchList();
              val newLetDepth = if isLocal then letDepth else letDepth+1;
              (* The environment for the local declarations. *)
              val localEnv =
                {
                   lookupVal     = lookupDefault (#lookup newValEnv)  (#lookupVal env),
                   lookupType    = lookupDefault (#lookup newTypeEnv) (#lookupType env),
                   lookupFix     = #lookupFix env,
                   (* This environment is needed if we open a 
                      structure which has sub-structures. *)
                   lookupStruct  = lookupDefault (#lookup newStrEnv) (#lookupStruct env),
                   lookupSig     = #lookupSig env,
                   lookupFunct   = #lookupFunct env,
                   lookupTvars   = #lookupTvars env,
                   enterVal      = #enter newValEnv,
                   enterType     = #enter newTypeEnv,
                  (* Fixity has already been dealt with in the parsing process.  The only reason
                     we deal with it here is to ensure that declarations are printed in the
                     correct order.  We simply need to make sure that local fixity declarations
                     are ignored. *)
                   enterFix      = fn _ => (),
                   enterStruct   = #enter newStrEnv,
                   enterSig      = #enterSig env,
                   enterFunct    = #enterFunct env,
                   allValNames   = fn () => (stringsOfSearchList newValEnv () @ #allValNames env ())
                };
        
              (* Process the local declarations and discard the result. *)
              val _ : types = assignSeq(localEnv, newLetDepth, decs, false)
        
              (* This is the environment used for the body of the declaration.
                 Declarations are added both to the local environment and to
                 the surrounding scope. *)
              val bodyEnv =
                { 
                  (* Look-ups come from the local environment *)
                  lookupVal     = #lookupVal localEnv,
                  lookupType    = #lookupType localEnv,
                  lookupFix     = #lookupFix localEnv,
                  lookupStruct  = #lookupStruct localEnv,
                  lookupSig     = #lookupSig localEnv,
                  lookupFunct   = #lookupFunct localEnv,
                  lookupTvars   = #lookupTvars localEnv,
                  enterVal      =
                    fn (pair as (_, v)) =>
                      (varsInBody := v :: ! varsInBody;
                       #enter newValEnv pair;
                       #enterVal env      pair),
                  enterType     =
                    fn pair =>
                      (#enter newTypeEnv pair;
                       #enterType env      pair),
                  enterFix      = #enterFix env,
                  enterStruct   =
                    fn pair =>
                      (#enter newStrEnv pair;
                       #enterStruct env   pair),
                  enterSig      = #enterSig env,
                  enterFunct    = #enterFunct env,
                  allValNames   = #allValNames localEnv
                };
              (* Now the body, returning its result if it is an expression. *)
                val resType = assignSeq(bodyEnv, newLetDepth, body, not isLocal)
            in
                resType
            end (* LocalDec *)

          | ExpSeq (ptl, _) =>
             (* A sequence of expressions separated by semicolons.
                Result is result of last expression. *)
              assignSeq (env, letDepth, ptl, true)

          | ExDeclaration(tlist, _) =>
            let
                fun messFn(name, _, line) =
                    errorNear (lex, true, v, line,
                        name ^ " has already been bound in this declaration");
         
                (* Construct an environment to check for duplicate declarations.
                   Include the declaration location as the value. *)
                val dupEnv = noDuplicates messFn;
  
                fun processException (ExBind {name, previous, ofType, value, nameLoc, ...}) =
                let
                    (* Fill in any types.  If there was no type given the exception has type exn
                       otherwise it has type ty->exn. *)
                    val oldType =
                        case ofType of
                            NONE => exnType
                        |   SOME typeof => mkFunctionType(ptAssignTypes(typeof, v), exnType)
                    val locations = [DeclaredAt nameLoc, SequenceNo (newBindingId lex)]
    
                    val exValue = 
                        case previous of 
                            EmptyTree => mkEx (name, oldType, locations) (* Generative binding. *)
                                
                        |   Ident {name = prevName, value = prevValue, location, expType, possible, ...} =>
                            let 
                                (* ex = ex' i.e. a non-generative binding? *)
                                (* Match up the previous exception. *)
                                val prev = 
                                    lookupValue 
                                        ("Exception",
                                            {lookupVal= #lookupVal env,
                                            lookupStruct= #lookupStruct env},
                                            prevName,
                                            giveError (v, lex, location))
                                val excType = valTypeOf prev
                            in
                                (* Check that it is an exception *)
                                case prev of
                                    Value{class=Exception, ...} => ()
                                |    _ => errorNear (lex, true, v, location, "(" ^ prevName ^ ") is not an exception.");
                                prevValue := prev; (* Set the value of the looked-up identifier. *)
                                expType := excType; (* And remember the type. *)
                                possible := #allValNames env;
                                (* The result is an exception with the same type. *)
                                mkEx (name, excType, locations)
                            end
                        | _ =>
                            raise InternalError "processException: badly-formed parse-tree"
                in
                    (* Save this value. *)
                    value := exValue;
        
                    (* In the check environment *)
                    #enter dupEnv (name, nameLoc);
        
                    (* Must not be qualified *)
                    checkForDots (name, lex, nameLoc) : unit;
                    (* Must not be "true", "false" etc. *)
                    checkForBuiltIn (name, v, lex, nameLoc, true) : unit;
        
                    (* Put this exception into the env *)
                    #enterVal env (name, exValue) 
                end
  
                val () = List.app processException tlist;
            in
                badType
            end (* ExDeclaration *)
        
          | Raise (pt, line) =>
            let
                val exType = assValues v pt
            in
                (* The exception value must have type exn. *)
                case unifyTypes(exType, exnType) of
                    NONE => ()
                |   SOME report =>
                        typeWrong("Exception to be raised must have type exn.",
                            valTypeMessage (lex, typeEnv) ("Raise:", pt, exType),
                            unifyErrorReport (lex, typeEnv) report, lex, line, foundNear v);
                (* Matches anything *)
                mkTypeVar (generalisable, false, false, false)
            end
  
        | (aHandler as HandleTree {exp, hrules, location, ...}) =>
            let
                (* If the expression returns type E
                 the handler must be exn -> E *)
                val expType = assValues aHandler exp;
                (* Unify the handler with a function from exn -> expType *)
                val clauses =
                    assignList(assMatchTree aHandler, displayMatch, matchTypeMessage)
                        ("Clauses in handler have different types.", "Clause", "|", location, aHandler) hrules
                (* The result type of the handlers must match the result type of the expression being
                   handled and the arguments must all have type exn. *)
                val () = 
                    unify (clauses, mkFunctionType (exnType, expType), lex, location, foundNear v, typeEnv);
            in
              expType (* Result is expType. *)
            end

          | While {test, body, location, ...} =>
            let
                val testType = assValues v test
            in
                (* Test must be bool. Result is unit *)
                case unifyTypes(testType, boolType) of
                    NONE => ()
                |   SOME report =>
                        typeWrong("Loop condition of while-expression must have type bool.",
                            valTypeMessage (lex, typeEnv) ("While:", test, testType),
                            unifyErrorReport (lex, typeEnv) report, lex, location, foundNear v);
                assValues v body; (* Result of body is discarded. *)
                unitType
            end

          | aCase as Case {test, match, location, expType, ...} =>
            let
                val funType =
                    assignList(assMatchTree aCase, displayMatch, matchTypeMessage)
                        ("Clauses in case have different types.", "Clause", "|", location, aCase) match;
                val argType = assValues aCase test;
                (* The matches constitute a function from the test type to
                   the result of the case statement, so we apply the match type
                   to the test. *)
                val resType = apply (funType, argType, lex, location, foundNear aCase, typeEnv)
            in
                expType := resType;
                resType
            end

          | anAndAlso as Andalso {first, second, location} =>
            let
                (* Both parts must be bool and the result is bool. *)
                fun mkTupleTree(fields, location) = TupleTree { fields=fields, location=location, expType = ref EmptyType }
                val pairArgs = mkTupleTree([first, second], location)
                val argTypes  = assValues anAndAlso pairArgs;
                val boolStarBool = mkProductType[boolType, boolType]
                val () =
                    case unifyTypes(argTypes, boolStarBool) of
                        NONE => ()
                    |   SOME report =>
                            typeWrong("Arguments of andalso must have type bool*bool.",
                                valTypeMessage (lex, typeEnv) ("Arguments:", pairArgs, argTypes),
                                unifyErrorReport (lex, typeEnv) report, lex, location, foundNear anAndAlso)
            in
                boolType
            end

          | anOrElse as Orelse {first, second, location} =>
            let
                (* Both parts must be bool and the result is bool. *)
                fun mkTupleTree(fields, location) = TupleTree { fields=fields, location=location, expType = ref EmptyType }
                val pairArgs = mkTupleTree([first, second], location)
                val argTypes  = assValues anOrElse pairArgs;
                val boolStarBool = mkProductType[boolType, boolType]
                val () =
                    case unifyTypes(argTypes, boolStarBool) of
                        NONE => ()
                    |   SOME report =>
                            typeWrong("Arguments of orelse must have type bool*bool.",
                                valTypeMessage (lex, typeEnv) ("Arguments:", pairArgs, argTypes),
                                unifyErrorReport (lex, typeEnv) report, lex, location, foundNear anOrElse)
            in
                boolType
            end

          | Directive { tlist, fix, ... } => 
                  (
                (* Infix declarations have already been processed by the parser.  We include
                   them here merely so that we get all declarations in the correct order. *)
                List.app (fn name => #enterFix env (name, FixStatus(name, fix))) tlist;
                badType
                )

          | WildCard _ => (* Should never occur in an expression. *)
                  raise InternalError "assignTypes: wildcard found"

          | Layered _ => 
                  raise InternalError "assignTypes: layered pattern found"

          | EmptyTree => 
                  raise InternalError "assignTypes: emptytree found"

          | Parenthesised(p, _) => assValues near p
                
            (* end of assValues *)

          and assMatchTree _ (MatchTree {vars, exp, resType, argType, ...}) =
            let 
              (* A match is a function from the pattern to the expression *)
              
              (* Process the pattern looking for variables. *)
        
               (* Construct a new environment for the variables. *)
              fun messFn(name, _, Value{locations, ...}) =  
                    errorNear (lex, true, v, declaredAt locations,
                        name ^ " has already been bound in this match");
              
              val newEnv   = noDuplicates messFn;
              val newLevel = level + 1;
              val decs     = processPattern(vars, #enter newEnv, newLevel, false, mkPattVar, false)
        
              (* The identifiers declared in the pattern are available in the
                 body of the function. *)
              val bodyEnv =
                {
                  lookupVal     = lookupDefault (#lookup newEnv) (#lookupVal env),
                  lookupType    = #lookupType env,
                  lookupFix     = #lookupFix env,
                  lookupStruct  = #lookupStruct env,
                  lookupSig     = #lookupSig env,
                  lookupFunct   = #lookupFunct env,
                  lookupTvars   = #lookupTvars env,
                  enterVal      = #enterVal env,
                  enterType     = #enterType env,
                  enterFix      = #enterFix env,
                  enterStruct   = #enterStruct env,
                  enterSig      = #enterSig env,
                  enterFunct    = #enterFunct env,
                  allValNames   =
                    fn () => (stringsOfSearchList newEnv () @ #allValNames env ())
                };
        
              (* Now the body. *)
              val expType = assignValues(newLevel, letDepth, bodyEnv, v, exp);
            in
              resType := expType;
              argType := decs;
              (* Result is a function from the type of the pattern to the type
                 of the body. This previously generalised the resulting type. Why? *)
              mkFunctionType (decs, expType)
            end (* MatchTree *)

        and assValDeclaration (valdecs: valbind list, explicit, implicit) =
        (* assignTypes for a val-declaration. *)
        let
            val newLevel = level + 1;
      
            (* Set the scope of explicit type variables. *)
            val () = #apply explicit(fn (_, tv) => setTvarLevel (tv, newLevel));

            (* For each implicit type variable associated with this value declaration,
               link it to any type variable with the same name in an outer
               scope. *)
            val () = 
                #apply implicit
                    (fn (name, tv) =>
                        case #lookupTvars env name of SOME v => linkTypeVars(v, tv) | NONE => setTvarLevel (tv, newLevel));
            (* If it isn't there set the level of the type variable. *)

            (* Construct a new environment for the variables. *)
            val newEnv =
                noDuplicates
                (fn(name, _, Value{locations, ...}) =>
                    errorNear (lex, true, v, declaredAt locations,
                        name ^ " has already been bound in this declaration"));

            (* This environment is those identifiers declared by recursive bindings *)
            val recEnv = searchList ();

            (* If this is a recursive declaration we will have to find all
               the variables declared by the patterns in each binding before
               we can look at the bodies of the bindings. For simplicity we
               process the patterns first even if this is not recursive but
               arrange for the variables to be added to the environment
               after rather than before processing the bodies. The result of
               processing the patterns is a list of their types. Each item
               in the list must be unified with the type of the
               corresponding body. *)

            (* Process the patterns. *)
            local
                fun doVal (ValBind {dec, isRecursive, variables, ...}) =
                    let
                        fun enterVals(pair as (_, value)) =
                        (
                            #enter newEnv pair;
                            if isRecursive then #enter recEnv pair else ();
                            variables := value :: ! variables
                        )

                        val patType =
                            processPattern(dec, enterVals, newLevel, false, mkValVar, isRecursive);
                    in
                        patType
                    end;
                
            in
                val decs = List.map doVal (valdecs)
            end

            (* Now the bodies. *)
            local
                (* Check that the types match by going down the list of value
                   bindings and the list of types produced from the patterns,
                   and matching corresponding types. *)
                fun checkTypes (patType, (ValBind {dec, exp, line, isRecursive, ...})) =
                    let
                        val newEnv =
                        { (* If this is recursive we find the recursive names
                             and others in the surrounding scope. *)
                            lookupVal     = 
                                if isRecursive
                                then lookupDefault (#lookup recEnv) (#lookupVal env)
                                else #lookupVal env,
                            lookupType    = #lookupType env,
                            lookupFix     = #lookupFix env,
                            lookupStruct  = #lookupStruct env,
                            lookupSig     = #lookupSig env,
                            lookupFunct   = #lookupFunct env,
                            (* Extend the environment of type variables. *)
                            lookupTvars   =
                                lookupDefault (#lookup explicit)
                                    (lookupDefault (#lookup implicit) (#lookupTvars env)),
                            enterVal      = #enterVal env,
                            enterType     = #enterType env,
                            enterFix      = #enterFix env,
                            enterStruct   = #enterStruct env,
                            enterSig      = #enterSig env,
                            enterFunct    = #enterFunct env,
                            allValNames   =
                                if isRecursive
                                then fn () => (stringsOfSearchList recEnv () @ #allValNames env ())
                                else #allValNames env
                        }

                        val expType = assignValues(newLevel, letDepth, newEnv, exp, exp);
            
                        val () =
                            case unifyTypes(patType, expType) of
                                NONE => () (* OK*)
                            |   SOME report =>
                                    typeMismatch("Pattern and expression have incompatible types.",
                                        valTypeMessage (lex, typeEnv) ("Pattern:", dec, patType),
                                        valTypeMessage (lex, typeEnv) ("Expression:", exp, expType),
                                        unifyErrorReport (lex, typeEnv) report, lex, line, foundNear v)
        
                        (* true if the expression is a possibly-constrained fn-expression.
                           It isn't clear whether a parenthesised expression is allowed here.
                           As often, the definition is informal.  On p8 of the ML97
                           definition it says "exp must be of the form fn match".  In ML90
                           it added "possibly constrained by one or more type expressions".
                           This is such a mess that I'm allowing both contraints and parentheses
                           here. *)
                        fun isConstrainedFn (Constraint {value, ...}) = isConstrainedFn value
                        |   isConstrainedFn (Fn _)  = true
                        |   isConstrainedFn (Parenthesised(p, _)) = isConstrainedFn p
                        |   isConstrainedFn _       = false;
                    in
                        (* Must check that the expression is of the form FN match. *)
                        (* N.B. the code generator assumes this is true. *)
                        if isRecursive andalso not (isConstrainedFn exp)
                        then errorNear (lex, true, v, line, 
                            "Recursive declaration is not of the form `fn match'")
                        else ()
                    end
            in
                val () = ListPair.app checkTypes (decs, valdecs)
            end

            (* Now allow generalisation on the variables being declared.
               For imperative type variables we have to know whether the
               expression is expansive. *)
            fun allowGen (d, (ValBind {exp, line, ...})) =
                (
                    allowGeneralisation 
                        (d, newLevel, nonExpansive exp, lex, line, foundNear v, typeEnv)
                ) (* allowGen *)
        in
            ListPair.appEq allowGen (decs, valdecs);
            (* And declare the new names into the surrounding environment. *)
            let
                fun enterDec(s, v as Value{instanceTypes, ...}) =
                (
                    valOf instanceTypes := []; (* Remove any recursive references. *)
                    #enterVal env (s, v)
                )
            in
                #apply newEnv enterDec
            end
        end (* assValDeclaration *)

        and assFunDeclaration {dec=tlist: fvalbind list, explicit, implicit, ...} =
        (* Assigntypes for a fun-declaration. *)
        let
            val funLevel = level + 1; (* Level for function names. *)
      
            (* Set the scope of explicit type variables. *)
            val () =
                #apply explicit(fn (_, tv) => setTvarLevel (tv, funLevel));

            (* For each implicit type variable associated with this value declaration,
               link it to any type variable with the same name in an outer
               scope. *)
            val () = 
                #apply implicit
                  (fn (name, tv) =>
                      case #lookupTvars env name of SOME v => linkTypeVars(v, tv) | NONE => setTvarLevel (tv, funLevel));
            (* If it isn't there set the level of the type variable. *)

            (* Construct a new environment for the variables. *)
            fun msgFn(name, _, Value{locations, ...}) = 
                errorNear (lex, true, v, declaredAt locations,
                    name ^ " has already been bound in this declaration");
           
            val newEnv = noDuplicates msgFn;
           
            (* Since this is a recursive declaration we must get the function
               names first. Because of the way they are parsed they are hidden
               as applications of the function to one or more patterns. There
               may be more than one clause in a function binding but each
               should declare the same function and have the same number of
               patterns. We need to know the number of patterns and the
               function name in the third pass so we save them in the
               function binding. *)

            local
                fun findNameAndPatts (FValBind {clauses = (FValClause {dec, line, ...}::_), numOfPatts, functVar, ...}) =
                let
                    (* Just look at the first clause for the moment. *)
                    val { ident = { name, location, ... }, ... } = dec;
                    (* Declare a new identifier with this name. *)
                    val locations = [DeclaredAt location, SequenceNo (newBindingId lex)]
                    val funVar =
                        mkValVar (name, mkTypeVar (funLevel, false, false, false), locations)

                    val arity = case dec of { args, ...} => List.length args
                    val () = numOfPatts := arity;
                    val () =
                        (* Put the results onto the function binding. *)
                        if arity = 0
                        then errorNear (lex, true, v, line,
                                "Clausal function does not have any parameters.")
                        else ()
                in
                    (* Must not be qualified *)
                    checkForDots (name, lex, line);
                    (* Must not be "true", "false" etc. but may be "it" *)
                    checkForBuiltIn (name, v, lex, line, false);
                    functVar := funVar; (* Save the variable. *)
                    (* Enter it in the environment. *)
                    #enter newEnv (name, funVar)
                end
                |   findNameAndPatts _ = raise InternalError "findNameAndPatts: badly-formed parse-tree";

            in
                val () = List.app findNameAndPatts tlist
            end;

            local
                (* Can now process the clausal functions in the environment 
                   of the function names and using the information about
                   function name and number of patterns we have saved. *)
                fun processBinding
                    (fvalBind as FValBind {clauses, functVar=ref functVar, argType, resultType, location, ...}) =
                let
                    (* Each fun binding in the declaration may consist of several
                       clauses. Each must have the same function name, the same
                       number of patterns and a unifiable type. *)
                    (* The type information is built up from the bottom so that if there are
                       errors we can report them in the most appropriate place.
                       Build a type to be used for the function.  This will later be unified
                       with the type that we've already created for the function variable. *)
                    val funType = mkTypeVar(generalisable, false, false, false)

                    fun processClause (clause as FValClause {dec, exp, line, ...}) =
                    let
                        val { ident = ident, args, constraint, ... } = dec

                        fun mkClausal(clauses, location) : fvalbind =
                           FValBind
                             { 
                               clauses    = clauses,
                               numOfPatts = ref 0,
                               functVar   = ref undefinedValue,
                               argType    = ref badType,
                               resultType = ref badType,
                               location   = location
                             }
    
                        fun mkFunDeclaration (dec, explicit, implicit, location) : parsetree =
                          FunDeclaration
                            {
                                dec=dec,
                                explicit = explicit,
                                implicit = implicit,
                                location = location
                            }

                        val clauseAsTree: parsetree =
                            (* This clause as a parsetree object for error messages. *)
                            mkFunDeclaration([mkClausal([clause], line)], explicit, implicit, line)
                        
                        val () = (* Set the type.  Only in case we look at the export tree. *)
                            #expType ident := valTypeOf functVar

                        fun messFn (name, _, Value{locations, ...}) =
                            errorNear (lex, true, clauseAsTree, declaredAt locations,
                                name ^ " has already been bound in this clause.");
                        (* Construct a new environment for the variables in the patts. *)
                        val varEnv = noDuplicates messFn;
                        val varLevel = funLevel + 1; (* Level for variables. *)

                        (* Process the patterns. *)
                        val argTypeList =
                            List.map (fn arg =>
                                        processPattern(arg, #enter varEnv, varLevel, false, mkPattVar, false))
                                args
                        (* This list is used for the type of the helper function. *)
                        val () = argType :=
                            (case argTypeList of
                                [] => badType (* error *)
                            |   [single] => single
                            |   multiple => mkProductType multiple)

                        (* The identifiers declared in the pattern are available in the
                           body of the function. Since it is recursive the function
                           names are also available. *)
                        val bodyEnv =
                        { 
                            lookupVal     = 
                                lookupDefault (#lookup varEnv)
                                    (lookupDefault (#lookup newEnv) (#lookupVal env)),
                            lookupType    = #lookupType env,
                            lookupFix     = #lookupFix env,
                            lookupStruct  = #lookupStruct env,
                            lookupSig     = #lookupSig env,
                            lookupFunct   = #lookupFunct env,
                            (* Extend the environment of type variables. *)
                            lookupTvars   =
                                lookupDefault (#lookup explicit)
                                    (lookupDefault (#lookup implicit) (#lookupTvars env)),
                            enterVal      = #enterVal env,
                            enterType     = #enterType env,
                            enterFix      = #enterFix env,
                            enterStruct   = #enterStruct env,
                            enterSig      = #enterSig env,
                            enterFunct    = #enterFunct env,
                            allValNames   =
                                fn () => (stringsOfSearchList varEnv () @
                                          stringsOfSearchList newEnv () @ #allValNames env ())
                        };
           
                        (* Now the body. *)
                        val expTyp = assignValues(varLevel, letDepth, bodyEnv, exp, exp);
                        (* Check the expression type against any explicit type constraint. *)
                        (* Return the explicit constraint if possible.  For the purposes of
                           type checking this is identical to "expTyp" but if there is a
                           type abbreviation this will be used when printing the result.
                           .e.g type t = int * int; fun f ((x, y):t): t = (y, x); *)
                        val typeOfBody =
                            case constraint of
                                NONE => expTyp
                            |   SOME given =>
                                let
                                    val theType = ptAssignTypes(given, v)
                                in
                                    case unifyTypes(expTyp, theType) of
                                        NONE => () (* OK. *)
                                    |   SOME report =>
                                            typeMismatch("Body of fun binding does not match type constraint.",
                                                valTypeMessage (lex, typeEnv) ("Expression:", exp, expTyp),
                                                PrettyBlock(0, false, [],
                                                    [
                                                        PrettyString "Constraint:",
                                                        PrettyBreak(1, 0),
                                                        display(theType, 10000 (* All *), typeEnv)
                                                    ]),
                                                unifyErrorReport (lex, typeEnv) report,
                                                lex, line, foundNear clauseAsTree);
                                    theType
                                end
                        (* Remember the result type for the debugger. Actually this
                           assigns the result type for each clause in the fun but
                           they'll all be the same. *)
                        val () = resultType := typeOfBody
                        (* The type of this clause is a function type. *)
                        val clauseType = List.foldr mkFunctionType typeOfBody argTypeList
                        (* Unify this with the type we're using for the other clauses. *)
                        val () =
                            case unifyTypes(clauseType, funType) of
                                NONE => () (* OK. *)
                            |   SOME report =>
                                    typeMismatch("Type of clause does not match the type of previous clauses.",
                                        valTypeMessage (lex, typeEnv) ("Clause:", clauseAsTree, clauseType),
                                        PrettyBlock(0, false, [],
                                            [
                                                PrettyString "Other clauses:",
                                                PrettyBreak(1, 0),
                                                display(funType, 10000 (* All *), typeEnv)
                                            ]),
                                        unifyErrorReport (lex, typeEnv) report,
                                        lex, line, foundNear clauseAsTree)
                    in (* body of processClause *)
                        ()
                    end
                in (* body of processFun *)
                    List.app processClause clauses;
                    (* If this function makes any recursive references move those references from the
                       local list to the recursive list.  In that way if we're looking for whether a
                       function is actually referenced we'll only include it if it's referenced outside
                       or from another referenced function. *)
                    let
                        fun moveRefs(FValBind{functVar=ref(Value{references,...}), ...}) =
                        let
                            val {localRef as ref locals, recursiveRef, ...} = valOf references
                            val callerName = valName functVar (* Name of referring function. *)
                        in
                            recursiveRef := List.map (fn r => (r, callerName)) locals @ !recursiveRef;
                            localRef := []
                        end
                    in
                        List.app moveRefs tlist
                    end;
                    (* Finally unify the function type with the type of the function variable.  If the
                       variable has not yet been used that will simply set its type but if it has been
                       used recursively it may have been given an incompatible type. *)
                    case unifyTypes(funType, valTypeOf functVar) of
                        NONE => () (* OK. *)
                    |   SOME report =>
                        let
                            fun mkFunDeclaration (dec, explicit, implicit, location) : parsetree =
                              FunDeclaration
                                {
                                    dec=dec,
                                    explicit = explicit,
                                    implicit = implicit,
                                    location = location
                                }

                            fun mkIdent (name, loc) : parsetree = 
                              Ident
                                {
                                  name   = name,
                                  expType = ref EmptyType,
                                  value  = ref undefinedValue,
                                  location = loc,
                                  possible = ref(fn () => [])
                                }
 
                            val fvalAsTree = mkFunDeclaration([fvalBind], explicit, implicit, location)
                        in
                            typeMismatch("Type of function does not match type of recursive application.",
                                valTypeMessage (lex, typeEnv) ("Function:", fvalAsTree, funType),
                                valTypeMessage (lex, typeEnv)
                                    ("Variable:", mkIdent(valName functVar, location), valTypeOf functVar),
                                unifyErrorReport (lex, typeEnv) report,
                                lex, location, foundNear fvalAsTree)
                        end
                end
            in
                val () = List.app processBinding tlist
            end;

        in
            (* Now declare the new names into the surrounding environment,
               releasing the copy flags on the type variables. All fun
               bindings are non-expansive. *)
            List.app
                (fn(FValBind{
                    functVar as ref(var as Value{typeOf, locations, name, instanceTypes, ...}), ...}) =>
                (
                    (* Generalise the types.  allowGeneralisation side-effects the type variables,
                       replaces any that can be generalised by general variables. *)
                    allowGeneralisation(typeOf, funLevel, true, lex, declaredAt locations, foundNear v, typeEnv);
                    (* Remove any recursive references.  This really isn't right. *)
                    valOf instanceTypes := [];
                    #enterVal env (name, var);
                    functVar := var
                )) tlist
        end (* assFunDeclaration *)

        and assAbsData({typelist=typeList, withtypes, declist, equalityStatus, isAbsType=isAbs, ...}) =
        let
            (* A type declaration causes a type to be entered in the type
               environment, together with some constructors. *)
            fun messFn (name, _, TypeConstrSet(new, _)) = 
                errorNear (lex, true, v, declaredAt(tcLocations new),
                   name ^ " has already been bound in this declaration");

            val localTypeEnv = noDuplicates messFn;
      
            (* datatype and abstype declarations are both recursive so we can
               enter the type names into the environment during a first pass,
               and then process the value constructors during a second. *)
            fun enterType(typeConstr, typeName) =
            (
                checkForDots  (typeName, lex, declaredAt(tcLocations(tsConstr typeConstr))); (* Must not be qualified *)
                #enter localTypeEnv (typeName, typeConstr) (* Check for duplicates. *)
            );
       
            (* Make the type constructors and put them in a list. *)
            fun enterTcon (DatatypeBind {name, tcon, typeVars, nameLoc, ...}) =
            let
                (* Make a new ID.  If this is within a let declaration we always make
                   a free ID because it is purely local and can't be exported. *)
                val description = { location = nameLoc, name = name, description = "" }
                val arity = length typeVars
            
                val newId =
                    if letDepth = 0
                    then makeTypeId(false, true, (typeVars, EmptyType), description)
                    else makeFreeIdEqUpdate (arity, Local{addr = ref ~1, level = ref baseLevel}, false, description)
                val locations = [DeclaredAt nameLoc, SequenceNo (newBindingId lex)]
                val tc = makeTypeConstructor(name, typeVars, newId, locations)
            in
                tcon := TypeConstrSet(tc, []);
                enterType(TypeConstrSet(tc, []), name);
                tc
            end
      
            val listOfTypes = map enterTcon typeList;

            local
                fun lookup(s, line) =
                    lookupTyp 
                        ({lookupType = lookupDefault(#lookup localTypeEnv) (#lookupType env),
                            lookupStruct = #lookupStruct env},
                        s, giveError (v, lex, line))
            in
                fun localAssignTypes decType = assignTypes (decType, lookup, lex)
            end

            (* First match all the types on the right-hand sides using the
               datatypes and the existing bindings. *)
            local
                fun processType (TypeBind {decType = SOME decType, ...}) = localAssignTypes decType
                |   processType _ = emptyType
            in
                val decTypes = List.map processType withtypes
            end;

            (* Can now enter the `withtypes'. *)
            fun enterWithType (TypeBind {name, typeVars, nameLoc, tcon=tcRef, ...}, decType) =
            let
                val description = { location = nameLoc, name = name, description = "" }
                (* Construct a type constructor which is an alias of the
                   right-hand side of the declaration. *)
                val locations = [DeclaredAt nameLoc, SequenceNo (newBindingId lex)]
                val tcon =
                    makeTypeConstructor (name, typeVars,
                        makeTypeId(false, false, (typeVars, decType), description), locations)
                val tset = TypeConstrSet(tcon, [])
            in
                tcRef := tset;
                enterType(tset, name); (* Checks for duplicates. *)
                #enterType env (name, tset) (* Put in the global environment. *)
            end

            val () = ListPair.app enterWithType (withtypes, decTypes);
        
            (* For the constructors *)
            fun messFn (name, _, Value{locations, ...}) =
                errorNear (lex, true, v, declaredAt locations,
                    name ^ " has already been used as a constructor in this type");
      
            val consEnv = noDuplicates messFn;
            val abstypeEnv = searchList ();
    
            (* Now process the types and generate the constructors. *)
            fun genValueConstrs (DatatypeBind {name, typeVars, constrs, nameLoc, tcon, ...}, typ) =
            let
                val numOfConstrs = length constrs;
                val typeVarsAsTypes = List.map TypeVar typeVars
        
                (* The new constructor applied to the type variables (if any) *)
                val locations = [DeclaredAt nameLoc, SequenceNo (newBindingId lex)]
                val resultType = mkTypeConstruction (name, typ, typeVarsAsTypes, locations)

                (* Sort the constructors by name.  This simplifies matching with
                   datatypes in signatures. *)
                fun leq {constrName=xname: string, ...} {constrName=yname, ...} = xname < yname;
                val sortedConstrs = quickSort leq constrs;

                fun processConstr ({constrName=name, constrArg, idLocn, constrVal, ...}) =
                let
                    val (constrType, isNullary) =
                        case constrArg of
                            NONE => (resultType, true)
                        |   SOME argtype =>
                                (mkFunctionType (localAssignTypes argtype, resultType), false)
                    val locations = [DeclaredAt idLocn, SequenceNo (newBindingId lex)]
                    val cons =
                        makeValueConstr (name, constrType, isNullary, numOfConstrs, Local{addr = ref ~1, level = ref baseLevel},
                                         locations)
        
                    (* Name must not be qualified *)
                    val () = checkForDots (name, lex, idLocn);
                    (* Must not be "true", "false" etc. *)
                    val () = checkForBuiltIn (name, v, lex, idLocn, true) : unit;
          
                    (* Put into the environment. *)
                    val () = #enter consEnv (name, cons)
                    
                    (* Link it in case we export the tree. *)
                    val () = constrVal := cons
                in    
                    cons
                end (* processConstr *)
                val tset = TypeConstrSet (typ, List.map processConstr sortedConstrs)
            in
                (* If this is an abstype enter the version with the constructors into
                   a local environment and a version without the constructors into the
                   global environment.  If it is a datatype enter the version with
                   constructors in the global environment. *)
                if isAbs
                then (#enter abstypeEnv (name, tset); #enterType env (name, TypeConstrSet(typ, [])))
                else #enterType env (name, tset);
                tcon := tset;
                tset
            end (* genValueConstrs *)
      
            val listOfTypeSets = ListPair.map genValueConstrs (typeList, listOfTypes);

            (* Third pass - Check to see if equality testing is allowed for
               these types. *)
            val () = computeDatatypeEqualities(listOfTypeSets, sigTypeIdMap);

            (* If this is a datatype declaration the value constructors should be
               entered in the surrounding scope, otherwise (abstract type
               declaration) we evaluate the declarations in an environment
               containing the value constructors, but the value constructors
               themselves do not appear in the surrounding scope. *)
            val () =
                if not isAbs
                then #apply consEnv (#enterVal env)
                else
                let   (* Abstract type *)
                    (* The declarations have to be evaluated in an environment in
                       which the constructors have been declared. When an identifier
                       is looked up it may:
                       (a) be one of these new declarations, or else
                       (b) be a constructor from the type declarations, or else
                       (c) be outside the abstract type declaration.
                       New declarations are entered in the local environment so that
                       they can be found under (a) and in the surrounding environment
                       where they will be available after this declaration. *)
                    val decEnv =
                    let
                        val localEnv = searchList ();
                        fun enterValFn pair = (#enter localEnv pair; #enterVal env pair);
                        val lookupValFn = 
                            lookupDefault (#lookup localEnv)
                                (lookupDefault (#lookup consEnv) (#lookupVal env))
                        fun allValNames () = (stringsOfSearchList localEnv () @ stringsOfSearchList consEnv () @ #allValNames env ())
                        (* We also have to do something similar with types.  This is really
                           only for perverse cases where there is a datatype replication
                           inside the abstype. *)
                        fun enterTypeFn pair = (#enter abstypeEnv pair; #enterType env pair);
                        val lookupTypeFn = 
                            lookupDefault (#lookup abstypeEnv) (#lookupType env)
                    in
                        { 
                            lookupVal     = lookupValFn,
                            lookupType    = lookupTypeFn,
                            lookupFix     = #lookupFix env,
                            lookupStruct  = #lookupStruct env,
                            lookupSig     = #lookupSig env,
                            lookupFunct   = #lookupFunct env,
                            lookupTvars   = #lookupTvars env,
                            enterVal      = enterValFn,
                            enterType     = enterTypeFn,
                            enterFix      = #enterFix env,
                            enterStruct   = #enterStruct env,
                            enterSig      = #enterSig env,
                            enterFunct    = #enterFunct env,
                            allValNames   = allValNames
                        }
                    end;
  
                in
                    (* Process the declarations, discarding the result. *)
                    assignSeq (decEnv, letDepth, declist, false);
                    (* Turn off equality outside the with..end block.  This is required by the
                       "Abs" function defined in section 4.9 of the ML Definition.
                       We need to record the equality status, though, because we need
                       to reinstate this for code-generation. *)
                    equalityStatus := List.map tcEquality listOfTypes;
                    List.app(fn tc => tcSetEquality (tc, false)) listOfTypes;
                    ()
                end;
        in
            badType (* Does not return a type *)
        end (* assAbsData *)
    in 
        assValues near v
    end (* assignValues *);

      val Env gEnv = env
      
      val env = 
          {
            lookupVal     = #lookupVal gEnv,
            lookupType    = #lookupType gEnv,
            lookupFix     = #lookupFix gEnv,
            lookupStruct  = #lookupStruct gEnv,
            lookupSig     = #lookupSig gEnv,
            lookupFunct   = #lookupFunct gEnv,
            lookupTvars   = fn _ => NONE,
            enterVal      = #enterVal gEnv,
            enterType     = #enterType gEnv,
            enterFix      = #enterFix gEnv,
            enterStruct   = #enterStruct gEnv,
            enterSig      = #enterSig gEnv,
            enterFunct    = #enterFunct gEnv,
            allValNames   = #allValNames gEnv
          };
    in
      assignValues(1, 0, env, v, v)
    end (* pass2 *);

    (* Before code-generation perform an extra pass through the tree to remove
       unnecessary polymorphism.  The type-checking computes a most general
       type for a value, typically a function, but it is frequently used in
       situations where a less general type would suffice. *)
    (* Note: if the less general type involves a local datatype this isn't
       done to avoid a possible bug with datatypes defined after the
       function. *)
    fun setLeastGeneralTypes(p: parsetree, _: lexan) =
    let
        (* Because of mutual recursion we need to process the set of variables
           produced by a fun-declaration or a val rec declaration as a group.
           We also process no-recursive val bindings here for simplicity.  *)
        fun processVariableSet(variables: values list) =
        let
            (* Two polymorphic values that are involved in mutual recursion will have
               the same type variable in both values.  When we produce the least
               general type we have to consider all the types that may be used for
               those variables. Unfortunately, because of flexible records we need
               to repeat the unification we did in the previous pass. *)
            local
                fun getTypeVarsAndInstance (Value{typeOf, instanceTypes, ...}, vars) =
                let
                    val instances = ! (valOf instanceTypes)
                    fun getPolyVars typ =
                    let
                        val (copied, tyVars) = generalise typeOf
                        (* Unify the types.  If there's an error we return a fresh set of the type
                           variables which gives the most general type.
                           There shouldn't be an error but there is one
                           circumstance at least where we can get an error here.  If we have a functor
                           declaration followed by an application of the functor in the same "program"
                           we can set an entry in instanceTypes of a Value used in the functor declaration
                           to an instance in the functor application because the instanceTypes value is
                           inherited into the functor signature if there's no explicit signature.
                           We really need to handle this properly and not inherit the instanceTypes
                           value in that case.  Test116 shows this. *)
                    in
                        if isSome(unifyTypes(copied, typ))
                        then #2 (generalise typeOf)
                        else tyVars (* Return the type vars instantiated to the instance types. *)
                    end
                    (* This returns a list, one entry for each instance, of a list of the
                       type variables for that instance. *)
                    val instanceVarLists = List.map getPolyVars instances
                    (* Transpose that list so we get a list, one entry for each type variable,
                       of all the instance types that are possible. *)
                    fun transpose ([]::_) = []
                    |   transpose (args as _::_) = (List.map hd args) :: transpose (List.map tl args)
                    |   transpose [] = []
                    val instanceVars = transpose instanceVarLists
                    (* Get the original type variables. *)
                    val originalVars = getPolyTypeVars(typeOf, fn _ => NONE)
                    (* Look to see if we already have some of the original vars in the list.
                       If we have we use the same ref for each var and merge the instance types. *)
                    fun mergeVars(ovar, iTypes) =
                        case List.find (fn (tv, _) => sameTv(tv, ovar)) vars of
                            NONE => (ovar, ref iTypes)
                        |   SOME(matched as (_, otherRef)) =>
                                ( otherRef := iTypes @ ! otherRef; matched)
                    val mergedList = ListPair.map mergeVars (originalVars, instanceVars) @ vars
                in
                    mergedList
                end
            in
                (* Get a list of the original type variables each with a reference containing
                   the shared list of instance types. *)
                val typeVarMap = List.foldl getTypeVarsAndInstance [] variables
            end
            local
                fun reduceTypes(tv, ref types) =
                    (* Although tv is a type variable it could occur as the least general type.
                       Unify takes care of that. *)
                    if isSome(unifyTypes(TypeVar tv, leastGeneral(List.map #value types)))
                    then raise InternalError "reduceTypes: Unable to set type vars"
                    else ()
            in
                val () = List.app reduceTypes typeVarMap
            end
        in
            ()
        end

        fun leastGenExp(ValDeclaration{dec, ...}) =
            (
                (* Val declarations may be recursive or non-recursive.  In the case of
                   recursive declarations we need to handle these in the same way as
                   fun-declarations. *)
                (* Gather all the variables and process them as a group.  There can't be
                   any dependencies between them except for mutual recursion. *)
                processVariableSet
                        (List.foldl (fn (ValBind{variables=ref variables, ...}, vars) => variables @ vars) [] dec);
                List.app (fn ValBind{exp, ...} => leastGenExp exp) dec
            )

        |   leastGenExp(FunDeclaration{dec, ...}) =
            (
                (* First process the outer declarations. *)
                processVariableSet(List.map(fn FValBind{functVar=ref var, ...} => var) dec);
                (* Then process the inner declarations.  Setting the outer type may have set the
                   instance types within the bodies. *)
                let
                    fun processClause(FValClause{exp, ...}) = leastGenExp exp
                    fun processBind(FValBind{clauses, ...}) = List.app processClause clauses
                in
                    List.app processBind dec
                end
            )

        |   leastGenExp(Localdec{decs, body, ...}) =
            (
                (* Process the body expressions in order but the declarations must be done in
                   reverse order after the body. *)
                List.app (leastGenExp o #1) body;
                List.foldr (fn ((p, _), ()) => leastGenExp p) () decs
            )

        |   leastGenExp(AbsDatatypeDeclaration { declist, ... }) =
                (* Declarations in reverse order *)
                List.foldr (fn ((p, _), ()) => leastGenExp p) () declist

            (* All the rest of these just involve processing sub-expressions. *)
        |   leastGenExp(Applic{f, arg, ...}) = (leastGenExp f; leastGenExp arg)

        |   leastGenExp(Cond{test, thenpt, elsept, ...}) =
                (leastGenExp test; leastGenExp thenpt; leastGenExp elsept)

        |   leastGenExp(TupleTree{fields, ...}) = List.app leastGenExp fields

        |   leastGenExp(Constraint{value, ...}) = leastGenExp value

        |   leastGenExp(Fn {matches, ...}) = List.app (fn MatchTree{exp, ...} => leastGenExp exp) matches

        |   leastGenExp(ExpSeq(ptl, _)) = List.app (leastGenExp o #1) ptl

        |   leastGenExp(HandleTree{exp, hrules, ...}) =
                (leastGenExp exp; List.app (fn MatchTree{exp, ...} => leastGenExp exp) hrules)

        |   leastGenExp(While{test, body, ...}) = (leastGenExp test; leastGenExp body)

        |   leastGenExp(Case{test, match, ...}) =
                (leastGenExp test; List.app (fn MatchTree{exp, ...} => leastGenExp exp) match)

        |   leastGenExp(Andalso {first, second, ...}) = (leastGenExp first; leastGenExp second)

        |   leastGenExp(Orelse{first, second, ...}) = (leastGenExp first; leastGenExp second)

        |   leastGenExp(Labelled{recList, ...}) = List.app (leastGenExp o #valOrPat) recList

        |   leastGenExp(List{elements, ...}) = List.app leastGenExp elements

        |   leastGenExp(Parenthesised(p, _)) = leastGenExp p

        |   leastGenExp _ = ()

    in
        leastGenExp p
    end

    (* Types that can be shared. *)
    structure Sharing =
    struct
        type lexan      = lexan
        and  pretty     = pretty
        and  codetree   = codetree
        and  codeBinding = codeBinding
        and  types      = types
        and  values     = values
        and  typeId     = typeId
        and  structVals = structVals
        and  typeConstrs= typeConstrs
        and  typeVarForm=typeVarForm
        and  env        = env
        and  fixStatus  = fixStatus
        and  structureIdentForm = structureIdentForm
        and  typeParsetree = typeParsetree
        and  parsetree  = parsetree
        and  valbind    = valbind
        and  fvalbind   = fvalbind
        and  fvalclause = fvalclause
        and  typebind   = typebind
        and  datatypebind=datatypebind
        and  exbind     = exbind
        and  labelRecEntry=labelRecEntry
        and  ptProperties = ptProperties
        and  matchtree   = matchtree
        and  typeVarMap = typeVarMap
        and  level = level
    end

end (* PARSETREE *);