(*
    Original Poly version:
    Title:      Operations on type structures.
    Author:     Dave Matthews, Cambridge University Computer Laboratory
    Copyright   Cambridge University 1985

    ML translation and other changes:
    Copyright (c) 2000
        Cambridge University Technical Services Limited

    Further development:
    Copyright (c) 2000-9, 2012-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
*)

functor TYPE_TREE (
    structure LEX : LEXSIG
    structure STRUCTVALS : STRUCTVALSIG;
    structure PRETTY : PRETTYSIG
    structure CODETREE : CODETREESIG where type machineWord = Address.machineWord
    structure EXPORTTREE: EXPORTTREESIG;
    structure DEBUG: DEBUGSIG

    structure UTILITIES :
    sig
        val mapTable: ('a * 'a -> bool) ->
                       {enter: 'a * 'b -> unit, lookup: 'a -> 'b option}
        val splitString:   string -> { first:string, second:string }
    end;

    structure MISC :
    sig
        exception InternalError of string;
  
        val lookupDefault : ('a -> 'b option) -> ('a -> 'b option) -> 'a -> 'b option
    end;

    sharing LEX.Sharing = PRETTY.Sharing = EXPORTTREE.Sharing = STRUCTVALS.Sharing
          = CODETREE.Sharing

) :  TYPETREESIG =

(*****************************************************************************)
(*                  TYPETREE functor body                                    *)
(*****************************************************************************)
struct
  open MISC;
  open PRETTY;
  
  open STRUCTVALS;
  open LEX;
  open UTILITIES;
  open CODETREE;
  open EXPORTTREE
  
  val badType : types = BadType;
  
  (* added 16/4/96 SPF *)
  fun sameTypeVar (TypeVar x, TypeVar y) = sameTv (x, y)
    | sameTypeVar _                      = false;

  
  fun isTypeVar          (TypeVar          _) = true
    | isTypeVar          _ = false;
     
  fun isFunctionType     (FunctionType     _) = true
    | isFunctionType     _ = false;

  fun isEmpty             EmptyType           = true
    | isEmpty            _ = false;
    
  fun isBadType           BadType             = true
    | isBadType          _ = false;

  val emptyType            = EmptyType;

  fun typesTypeVar          (TypeVar          x) = x 
    | typesTypeVar          _ = raise Match;
    
  fun typesFunctionType     (FunctionType     x) = x
     | typesFunctionType     _ = raise Match;

    (* This is really left over from an old definition. *)
    fun tcEquivalent(TypeConstrs{identifier = TypeId {idKind = TypeFn(_, result), ...}, ...}) = result
    |   tcEquivalent _ = raise InternalError "tcEquivalent: Not a type function"

  (* A type construction is the application of a type constructor to
     a sequence of types to yield a type. A construction may have a nil
     list if it is a single type identifier such as ``int''. *)
  
  (* When a type constructor is encountered in the first pass this entry 
     is put in. Subsequently a type constructor entry will be assigned to
     it so that the types can be checked. *)

(*************)

    fun mkTypeVar (level, equality, nonunifiable, printable) = 
        TypeVar (makeTv {value=emptyType, level=level, equality=equality,
                         nonunifiable=nonunifiable, printable=printable});

    fun mkTypeConstruction (name, typc, args, locations) =
        TypeConstruction {name = name, constr = typc,
                          args = args, locations = locations}

    local
        (* Turn a tuple into a record of the form {1=.., 2=... }*)
        fun maptoRecord ([], _) = []
          | maptoRecord (H::T, i) = 
                {name=Int.toString i, typeof=H} :: maptoRecord (T,i+1)
    in
        fun mkProductType (typel: types list) =
        let
            val fields = maptoRecord (typel, 1)
        in
            LabelledType {recList = fields, fullList = FieldList(List.map #name fields, true)}
        end
    end

  fun mkFunctionType (arg, result) = 
      FunctionType {arg = arg, result = result};

  fun mkOverloadSet [constr] =
    (* If there is just a single constructor in the set we make
       a type construction from it. *)
        mkTypeConstruction(tcName constr, constr, nil, [])
   | mkOverloadSet constrs = 
    let
        (* Make a type variable and point this at the overload set
           so we can narrow down the overloading. *)
        val var = mkTypeVar (generalisable, false, false, false)
        val set = OverloadSet {typeset=constrs};
    in
        tvSetValue (typesTypeVar var, set);
        var
    end

    fun mkLabelled (l, frozen) = 
    let
        val final = FieldList(map #name l, frozen)
        val lab =
            LabelledType {recList = l,
                          fullList = if frozen then final else FlexibleList(ref final) }
    in
        if frozen
        then lab
        else
        let
           (* Use a type variable so that the record can be expanded.
              This also provides a model (equality etc). for any fields that
              are added later. *)
            val var = mkTypeVar (generalisable, false, false, false)
            val () =
                if isTypeVar var
                then tvSetValue (typesTypeVar var, lab)
                else ();
        in
            var
        end
    end

    (* Must remove leading zeros because the labels are compared by
       string comparison. *)
    fun mkLabelEntry (name, t) = 
    let
        fun stripZeros s = 
            if size s <= 1  orelse String.str(String.sub(s, 0)) <> "0" 
            then s
            else stripZeros (String.substring(s, 1, size s-1));
    in
        {name = stripZeros name, typeof = t}
    end;

    (* Functions to construct the run-time representations of type constructor values,
       type values and value constructors.  These are all tuples and centralising the
       code here avoids having the offsets as integers at various places.
       Monotype constructor and type values are almost the same except that
       type values have the printer entry as the function whereas monotype
       constructors have the print entry as a ref pointing to the function,
       allowing addPrettyPrint to set a printer for the type.  The entries
       for polytypes are functions that take the type values as arguments
       and return the corresponding values. *)
    structure TypeValue =
    struct
        val equalityOffset = 0
        and printerOffset = 1
        and boxnessOffset = 2
        and sizeOffset = 3

        local
            (* Values used to represent boxness. *)
            val boxedRepNever  = 0w1   (* Never boxed, always tagged e.g. bool *)
            and boxedRepAlways = 0w2   (* Always boxed, never tagged e.g. function types *)
            and boxedRepEither = 0w3   (* Either boxed or tagged e.g. (arbitrary precision) int *)
            fun make n = mkConst(Address.toMachineWord n)
            fun isCode n =
                mkInlproc(
                    mkEval(rtsFunction RuntimeCalls.POLY_SYS_word_eq, [mkLoadArgument 0, make n]),
                    1, "test-box", [], 0)
        in
            val boxedNever  = make boxedRepNever
            and boxedAlways = make boxedRepAlways
            and boxedEither = make boxedRepEither
            (* Test for boxedness.  This must be applied to the value extracted from
               the "boxedness" field after applying to any base type arguments in
               the case of a polytype constructor. *)
            val isBoxedNever  = isCode boxedRepNever
            and isBoxedAlways = isCode boxedRepAlways
            and isBoxedEither = isCode boxedRepEither
        end

        (* Sizes are always a single word. *)
        val singleWord = mkConst(Address.toMachineWord 0w1)

        fun extractEquality idCode = mkInd(equalityOffset, idCode)
        and extractPrinter idCode = mkInd(printerOffset, idCode)
        and extractBoxed idCode = mkInd(boxnessOffset, idCode)
        and extractSize idCode = mkInd(sizeOffset, idCode)

        fun createTypeValue{eqCode, printCode, boxedCode, sizeCode} =
            mkTuple[eqCode, printCode, boxedCode, sizeCode]
    end

    (* Value constructors are represented by tuples, either pairs for nullary constructors
       or triples for constructors with arguments.  For nullary functions the "injection"
       function is actually the value itself.  If this is a polytype all the entries are
       functions that take the type values for the base types as arguments. *)
    structure ValueConstructor =
    struct
        val testerOffset = 0
        val injectorOffset = 1
        val projectorOffset = 2

        fun extractTest constrCode = mkInd(testerOffset, constrCode)
        and extractInjection constrCode = mkInd(injectorOffset, constrCode)
        and extractProjection constrCode = mkInd(projectorOffset, constrCode)

        fun createValueConstr{testMatch, injectValue, projectValue} = mkTuple[testMatch, injectValue, projectValue]
        fun createNullaryConstr{ testMatch, constrValue } = mkTuple[testMatch, constrValue]
    end

    (* Eqtypes with built-in equality functions.  The printer functions are all replaced in the basis. *)
    local
        open Address PRETTY RuntimeCalls TypeValue
        fun defaultMonoTypePrinter _ = PrettyString "?"
        fun defaultPolyTypePrinter _ _ = PrettyString "?"

        fun eqAndPrintCode (eqCode, nArgs, boxed) =
        let
            val code =
                if nArgs = 0
                then createTypeValue{
                        eqCode=eqCode,
                        printCode=mkConst (toMachineWord (ref defaultMonoTypePrinter)),
                        boxedCode = boxed,
                        sizeCode = singleWord
                        }
                else createTypeValue{
                        eqCode=mkInlproc(eqCode, nArgs, "eq-helper()", [], 0),
                        printCode=mkConst (toMachineWord (ref defaultPolyTypePrinter)),
                        boxedCode = mkInlproc(boxed, nArgs, "boxed-helper()", [], 0),
                        sizeCode = mkInlproc(singleWord, nArgs, "size-helper()", [], 0)
                        }
        in
            Global (genCode(code, [], 0) ())
        end

        fun makeConstr(name, eqFun, boxed) =
            makeTypeConstructor (name,
                makeFreeId(0, eqAndPrintCode(eqFun, 0, boxed), true, basisDescription name),
                [DeclaredAt inBasis])
        (* wordEq is used both for tagged words and for pointer equality *)
        val wordEq = CODETREE.rtsFunction POLY_SYS_word_eq

        (* Strings can be either tagged single characters or vectors whose first word is
           the length. *)
        local
            val stringEquality =
                mkInlproc(
                    mkCor( (* Either they're equal... *)
                        mkEval(wordEq, [mkLoadArgument 0, mkLoadArgument 1]),
                        (* ... or they're both long and ...*)
                        mkCand(
                            mkCand(
                                mkEval(rtsFunction POLY_SYS_not_bool,
                                    [mkEval(rtsFunction POLY_SYS_is_short, [mkLoadArgument 0])]),
                                mkEval(rtsFunction POLY_SYS_not_bool,
                                    [mkEval(rtsFunction POLY_SYS_is_short, [mkLoadArgument 1])])
                            ),
                            (* ... their contents are equal.  Because the first word contains the
                               length if we include this in the test we will have tested the length
                               as well and will stop immediately if the lengths are different. *)
                            mkEval(rtsFunction POLY_SYS_bytevec_eq,
                                [mkLoadArgument 0, CodeZero, mkLoadArgument 1, CodeZero,
                                    mkEval(rtsFunction POLY_SYS_plus_word,
                                        [
                                            mkConst(toMachineWord wordSize),
                                            (* Use argument 1 here rather than 0.  We could use either but this works
                                               better when we're using equality for pattern matching since it
                                               gets the length of the constant string.  It also works better
                                               for the, to me, more natural ordering of variable=constant. *)
                                            mkEval(rtsFunction POLY_SYS_string_length, [mkLoadArgument 1])
                                        ])
                                ])
                        )
                    ),
                    2, "stringEquality", [], 0)
        in
            val stringEquality = genCode(stringEquality, [], 0) ()
        end
    in
        val intConstr    = makeConstr("int",    CODETREE.rtsFunction POLY_SYS_equala, boxedEither) (* Need arbitrary precision equality *)
        val charConstr   = makeConstr("char",   wordEq, boxedNever) (* Always short *)
        val stringConstr = makeConstr("string", stringEquality, boxedEither (* Single chars are unboxed. *))
        val wordConstr   = makeConstr("word",   wordEq, boxedNever)

        (* Ref is a datatype with a single constructor.  The constructor is added in INITIALISE.
           Equality is special for "'a ref", "'a array" and "'a Array2.array".  They permit equality
           even if the 'a is not an eqType. *)
        val refConstr =
            makeTypeConstructor 
                ("ref",
                makeFreeId(1, eqAndPrintCode(wordEq, 1, boxedAlways), true, basisDescription "ref"),
                [DeclaredAt inBasis]);
        val arrayConstr =
            makeTypeConstructor 
                ("array",
                makeFreeId(1, eqAndPrintCode(wordEq, 1, boxedAlways), true, basisDescription "Array.array"),
                [DeclaredAt inBasis]);
        val array2Constr =
            makeTypeConstructor 
                ("array",
                makeFreeId(1, eqAndPrintCode(wordEq, 1, boxedAlways), true, basisDescription "Array2.array"),
                [DeclaredAt inBasis]);
        val byteArrayConstr =
            makeTypeConstructor 
                ("byteArray",
                makeFreeId(0, eqAndPrintCode(wordEq, 0, boxedAlways), true, basisDescription "byteArray"),
                [DeclaredAt inBasis]);
        (* Bool is a datatype.  The constructors are added in INITIALISE. *)
        val boolConstr =
            makeTypeConstructor 
                ("bool", makeFreeId(0, eqAndPrintCode(wordEq, 0, boxedNever), true, basisDescription "bool"),
                [DeclaredAt inBasis]);
    end

    (* These polytypes allow equality even if the type argument is not an equality type. *)
    fun isPointerEqType id =
        sameTypeId (id, tcIdentifier refConstr) orelse
        sameTypeId (id, tcIdentifier arrayConstr) orelse
        sameTypeId (id, tcIdentifier array2Constr) orelse
        sameTypeId (id, tcIdentifier byteArrayConstr)

    (* Non-eqtypes *)
    local
        open Address PRETTY TypeValue

        fun makeType(name, descr, boxed) =
        let
            fun defaultPrinter _ = PrettyString "?"
            val code =
                createTypeValue{
                    eqCode=CodeZero (* No equality. *),
                    printCode=mkConst (toMachineWord (ref defaultPrinter)),
                    boxedCode=boxed,
                    sizeCode=singleWord
                }
        in
            makeTypeConstructor (
                name, makeFreeId(0, Global (genCode(code, [], 0) ()), false, descr),
                [DeclaredAt inBasis])
        end
    in
        val realConstr   = makeType("real", basisDescription "real", boxedAlways(* Currently*)); (* Not an eqtype in ML97. *)
        val exnConstr    = makeType("exn", basisDescription "exn", boxedAlways);
        (* "undefConstr" is used as a place-holder during parsing for the actual type constructor.
           If the type constructor is not found this may appear in an error message. *)
        val undefConstr  =
            makeType("undefined", { location = inBasis, description = "Undefined", name = "undefined" }, boxedEither);
    end

    (* The unit type is equivalent to the empty record. *)
    val unitConstr   =
        makeTypeConstructor ("unit",
            makeTypeFunction({ location = inBasis, description = "unit", name = "unit" },
            ([], LabelledType {recList = [], fullList = FieldList([], true)})),
            [DeclaredAt inBasis]);


  (* Type identifiers bound to standard type constructors. *)
   
  val unitType = mkTypeConstruction ("unit", unitConstr, [], []);
   
  val intType    = mkTypeConstruction ("int",     intConstr,    [], []);
  val realType   = mkTypeConstruction ("real",    realConstr,   [], []);
  val charType   = mkTypeConstruction ("char",    charConstr,   [], []);
  val stringType = mkTypeConstruction ("string",  stringConstr, [], []);
  val boolType   = mkTypeConstruction ("bool",    boolConstr,   [], []);
  val exnType    = mkTypeConstruction ("exn",     exnConstr,    [], []);
  val wordType   = mkTypeConstruction ("word",    wordConstr,   [], []);
          
    fun isUndefined cons = sameTypeId (tcIdentifier cons, tcIdentifier undefConstr);
    val isUndefinedTypeConstr = isUndefined

    (* Test if a type is the undefined constructor. *)
    fun isUndefinedType(TypeConstruction{constr, ...}) = isUndefined constr
    |   isUndefinedType _ = false

    (* Similar to alphabetic ordering except that shorter labels come before longer ones.
       This has the advantage that numerical labels are compared by their numerical order
       i.e. 1 < 2 < 10 whereas alphabetic ordering puts "1" < "10" < "2". *)
    fun compareLabels (a : string, b : string) : int = 
    if size a = size b 
    then if a = b then 0 else if a < b then ~1 else 1
    else if size a < size b then ~1 else 1;

    (* Sort using the label ordering.
       A simple sort routine - particularly if the list is already sorted. *)
    fun sortLabels [] = []
    |   sortLabels (s::rest) =
    let
        fun enter s _    [] = [s]
          | enter s name (l as ( (h as {name=hname, ...}) :: t)) =
        let
            val comp = compareLabels (name, hname);
        in
            if comp <= 0 then s :: l else h :: enter s name t
        end;
    in  
        enter s (#name s) (sortLabels rest)
    end

  (* Chains down a list of type variables returning the type they are
     bound to. As a side-effect it also points all the type variables
     at this type to reduce the need for future chaining and to free
     unused type variables. Normally a type variable points to at most
     one other, which then points to "empty". However if we have unified
     two type variables by pointing one at the other, there may be type
     variables which pointed to the first and which cannot be found and
     redirected at the second until they themselves are examined. *)
     
    fun eventual (t as (TypeVar tv)) : types =
    let
        (* Note - don't change the level/copy information - the only type
           variable with this correct is the one at the end of the list. *)
        val oldVal = tvValue tv
        val newVal = eventual oldVal;   (* Search that *)
    in
        (* Update the type variable to point to the last in the chain.
         We don't do this if the value hasn't changed.  The reason for
         that was that assignment to refs in the database in the old
         persistent store system was very expensive and we wanted to avoid
         unnecessary assignments.  This special case could probably be removed. *)
        if PolyML.pointerEq(oldVal, newVal)
        then ()
        else tvSetValue (tv, newVal); (* Put it on *)
        case newVal of
            EmptyType => t (* Not bound to anything - return the type variable *)
        |   LabelledType (r as { recList, fullList }) =>
            if List.length recList = List.length(recordFields r)
            then (* All the generic fields are present so we don't need to do anything. *)
                if recordIsFrozen r then newVal else t
            else (* We need to add fields from the generic. *)
            let
                (* Add any fields from the generic that aren't present in this instance. *)
                fun createNewField name =
                        { name = name,
                          (* The new type variable has to be created with the same properties
                             as if we had first generalised it from the generic and then
                             unified with this instance.
                             The level is inherited from the instance since the generic
                             will always have level = generalisable.  Nonunifiable must be false. *)
                            typeof = mkTypeVar (tvLevel tv, tvEquality tv, false, tvPrintity tv)}

                fun addToInstance([], []) = []
                |   addToInstance(generic :: geRest, []) = createNewField generic :: addToInstance(geRest, [])
                |   addToInstance([], instance) = instance
                        (* This case can occur if we are producing an error message because of
                           a type-incorrect program so we just ignore it. *)
                |   addToInstance(generic :: geRest, inst as instance :: iRest) =
                    let
                        val order = compareLabels (generic, #name instance);
                    in
                        if order = 0 (* Equal *)
                        then instance :: addToInstance(geRest, iRest)
                        else if order < 0 (* generic name < instance name *)
                        then createNewField generic :: addToInstance(geRest, inst)
                        else (* This is another case that can occur with type-incorrect code. *)
                            instance :: addToInstance(generic :: geRest, iRest)
                    end

                val newList = addToInstance(recordFields r, recList)
                val newRecord =
                    LabelledType {recList = newList, fullList = fullList}
            in
                tvSetValue(tv, newRecord);
                if recordIsFrozen r then newRecord else t
            end
 
        |   OverloadSet _ => t (* Return the set of types. *)

        |   _ => newVal (* Return the type it is bound to *)
    end
    
    | eventual t (* not a type variable *) = t;


    (* Apply a function to every element of a type. *)
    fun foldType f =
    let
        fun foldT typ v =
        let
            val t   = eventual typ;
            val res = f t v; (* Process this entry. *)
        in
            case t of
                TypeVar tv => foldT (tvValue tv) res

            |   TypeConstruction {args, ...} => (* Then process the arguments. *)
                    List.foldr (fn (t, v) => foldT t v) res args
           
            |   FunctionType {arg, result} => foldT arg (foldT result res)
    
            |   LabelledType {recList,...} =>
                    List.foldr (fn ({ typeof, ... }, v) => foldT typeof v) res recList

            |   BadType => res
         
            |   EmptyType => res
          
            |   OverloadSet _ => res
        end
    in
        foldT
    end;

    (* Checks to see whether a labelled record is in the form of
     a product i.e. 1=, 2=   We only need this for prettyprinting.
     Zero-length records (i.e. unit) and singleton records are not
     considered as tuples. *)
    fun isProductType(LabelledType(r as {recList=recList as _::_::_, ...})) =
    let
        fun isRec [] _ = true
         |  isRec ({name, ...} :: l) n =
                name = Int.toString n andalso isRec l (n+1)
    in
        recordIsFrozen r andalso isRec recList 1
    end
    | isProductType _ = false;


    (* Test to see is a type constructor is in an overload set. *)
    fun isInSet(tcons: typeConstrs, (H::T): typeConstrs list) =
            sameTypeId (tcIdentifier tcons, tcIdentifier H) orelse isInSet(tcons, T)
    |   isInSet(_, []: typeConstrs list) = false

    (* Returns the preferred overload if there is one. *)
    fun preferredOverload typeset =
        if isInSet(intConstr, typeset)
        then SOME intConstr
        else if isInSet(realConstr, typeset)
        then SOME realConstr
        else if isInSet(wordConstr, typeset)
        then SOME wordConstr
        else if isInSet(charConstr, typeset)
        then SOME charConstr
        else if isInSet(stringConstr, typeset)
        then SOME stringConstr
        else NONE


    fun equalTypeIds(x, y) =
    let
        (* True if two types are equal. *)
        fun equalTypes (TypeConstruction{constr=xVal, args=xArgs, ...},
                        TypeConstruction{constr=yVal, args=yArgs, ...}) =
            equalTypeIds(tcIdentifier xVal, tcIdentifier yVal)
                andalso equalTypeLists (xArgs, yArgs)
    
        | equalTypes (FunctionType x, FunctionType y) = 
            equalTypes (#arg x, #arg y)   andalso 
            equalTypes (#result x, #result y)
                 
        | equalTypes (LabelledType x, LabelledType y) =
            recordIsFrozen x andalso recordIsFrozen y andalso  
            equalRecordLists (#recList x, #recList y)

        | equalTypes (TypeVar x, TypeVar y)  = sameTv (x, y)

        | equalTypes (EmptyType, EmptyType) = true

        | equalTypes _ = false
                              
        and equalTypeLists ([], [])    = true
        |   equalTypeLists (x::xs, y::ys) =
               equalTypes(x, y) andalso equalTypeLists (xs, ys)
        |   equalTypeLists _           = false

        and equalRecordLists ([],        [])    = true
        |   equalRecordLists (x::xs, y::ys) =
               #name x = #name y andalso 
               equalTypes(#typeof x, #typeof y) andalso equalRecordLists (xs, ys)
        |   equalRecordLists _             = false
    in
        case (x, y) of
            (TypeId{idKind=TypeFn(_, xEquiv), ...}, TypeId{idKind=TypeFn(_, yEquiv), ...}) =>
                equalTypes(xEquiv, yEquiv)
        |   _ => sameTypeId(x, y) 
    end

    (* See if the types are the same. This is a bit of a fudge, but saves carrying
       around a flag saying whether the structures were copied. This is only an
       optimisation. If the values are different it will not go wrong. *)
    val identical : types * types -> bool = PolyML.pointerEq
    and identicalConstr : typeConstrs * typeConstrs -> bool = PolyML.pointerEq
    and identicalList : 'a list * 'a list -> bool = PolyML.pointerEq

    (* Copy a type, avoiding copying type structures unnecessarily.
       Used to make new type variables for all distinct type variables when
       generalising polymorphic functions, and to make new type stamps for
       type constructors when generalising signatures. *)
    fun copyType (at, copyTypeVar, copyTypeConstr) =
    let
        fun copyList [] = []
        |   copyList (l as (h :: t)) =
        let
            val h' = copyType (h, copyTypeVar, copyTypeConstr);
            val t' = copyList t;
        in
            if identical (h', h) andalso identicalList (t', t)
            then l
            else h' :: t'
        end  (* copyList *);

        fun copyRecordList [] = []
        |   copyRecordList (l as ({name, typeof} :: t)) =
        let
            val typeof' = copyType (typeof, copyTypeVar, copyTypeConstr);
            val t' = copyRecordList t;
        in
            if identical (typeof', typeof) andalso identicalList (t', t)
            then l
            else {name=name, typeof=typeof'} :: t'
        end  (* copyList *);

        val atyp = eventual at;
    in
        case atyp of
            TypeVar _ =>  (* Unbound type variable, flexible record or overloading. *)
                copyTypeVar atyp
    
        |   TypeConstruction {constr, args, locations, ...} => 
            let
                val copiedArgs   = copyList args;
                val copiedConstr = copyTypeConstr constr;
                (* Use the name from the copied constructor.  This will normally
                   be the same as the original EXCEPT in the case where we are
                   using copyType to generate copies of the value constructors of
                   replicated datatypes. *)
                val copiedName = tcName copiedConstr
            in
                if identicalList (copiedArgs, args) andalso
                    identicalConstr (copiedConstr, constr)
                then atyp 
                else (* Must copy it. *) 
                    mkTypeConstruction (copiedName, copiedConstr, copiedArgs, locations)
            end 
           
        |   FunctionType {arg, result} => 
            let
                val copiedArg  = copyType (arg,    copyTypeVar, copyTypeConstr);
                val copiedRes  = copyType (result, copyTypeVar, copyTypeConstr);
            in
                if identical (copiedArg, arg) andalso 
                    identical (copiedRes, result)
                then atyp 
                else FunctionType {arg = copiedArg, result = copiedRes}
            end 
              
        |   LabelledType {recList, fullList} =>
                (* Rigid labelled records only.  Flexible ones are treated as type vars. *)
            let
                val copiedList = copyRecordList recList
            in
                if identicalList (copiedList, recList)
                then atyp 
                else LabelledType {recList = copiedList, fullList = fullList}
            end
                        
        |   EmptyType =>
                EmptyType

        |   BadType =>
                BadType
        
        |   OverloadSet _ =>
                raise InternalError "copyType: OverloadSet found"

    end (* copyType *);

    (* Copy a type constructor if it is Bound and in the required range.  If this refers to a type
       function copies that as well. Does not copy value constructors. *)
    fun copyTypeConstrWithCache (tcon, typeMap, _, mungeName, cache) =
        case tcIdentifier tcon of
            TypeId{idKind = TypeFn(args, equiv), description, access, ...} =>
            let
                val copiedEquiv =
                    copyType(equiv, fn x => x,
                        fn tcon =>
                            copyTypeConstrWithCache (tcon, typeMap, fn x => x, mungeName, cache))
            in
                if identical (equiv, copiedEquiv)
                then tcon (* Type is identical and we don't want to change the name. *)
                else (* How do we find a type function? *)
                    makeTypeConstructor (mungeName(tcName tcon),
                        TypeId {
                            access = access, description = description, idKind = TypeFn(args, copiedEquiv)},
                            tcLocations tcon)

            end

       |    id =>
            (
                case typeMap id of
                    NONE =>
                    (
                        (*print(concat[tcName tcon, " not copied\n"]);*)
                        tcon (* No change *)
                    )
                |   SOME newId =>
                    let
                        val name = #second(splitString (tcName tcon))
                        (* We must only match here if they're really the same. *)
                        fun cacheMatch tc =
                            equalTypeIds(tcIdentifier tc, newId)
                                andalso #second(splitString(tcName tc)) = name
                    in
                        case List.find cacheMatch cache of
                            SOME tc =>
                            (
                                (*print(concat[tcName tcon, " copied as ", tcName tc, "\n"]);*)
                                tc (* Use the entry from the cache. *)
                            )
                        |   NONE =>
                            (* Either a hidden identifier or alternatively this can happen as part of
                               the matching process.
                               When matching a structure to a signature we first match up the type
                               constructors then copy the type of each value replacing bound type IDs
                               with the actual IDs as part of the checking process.
                               We will return SOME newId but we don't have a
                               cache so return NONE for List.find. *)
                            let
                                val newName = mungeName(tcName tcon)
                            in
                                (*print(concat[tcName tcon, " not cached\n"]);*)
                                makeTypeConstructor(newName, newId, tcLocations tcon)
                            end
                    end
            )

    (* Exported version. *)
    fun copyTypeConstr (tcon, typeMap, copyTypeVar, mungeName) =
        copyTypeConstrWithCache(tcon, typeMap, copyTypeVar, mungeName, [])

    (* Compose typeID maps.  If the first map returns a Bound id we apply the second otherwise
       just return the result of the first. *)
    fun composeMaps(m1, m2) n =
    let
        fun map2 (TypeId{idKind=Bound{ offset, ...}, ...}) = m2 offset

        |   map2 (id as TypeId{idKind=Free _, ...}) = id

        |   map2 (TypeId{idKind=TypeFn(args, equiv), access, description, ...}) =
            let
                fun copyId(TypeId{idKind=Free _, ...}) = NONE
                |   copyId id = SOME(map2 id)
                (* If it's a type function e.g. this was a "where type" we have to apply the
                   map to any type identifiers in the type. *)
                val copiedEquiv =
                    copyType(equiv, fn x => x,
                        fn tcon => copyTypeConstr (tcon, copyId, fn x => x, fn y => y))
            in
                TypeId{idKind = TypeFn(args, copiedEquiv), access=access, description=description}
            end
    in
        map2(m1 n)
    end

    (* Basic procedure to print a type structure. *)
    type printTypeEnv =
        { lookupType: string -> (typeConstrSet * (int->typeId) option) option,
          lookupStruct: string -> (structVals * (int->typeId) option) option}

    val emptyTypeEnv = { lookupType = fn _ => NONE, lookupStruct = fn _ => NONE }

    (* Test whether two type constructors are the same after mapping.
       This is used to try to find the correct "path" to a type constructor
       when printing. *)
    fun eqTypeConstrs(xTypeCons, xMap, yTypeCons, yMap) =
    let
        fun id x = x
        fun copyId (SOME mapTypeId) (TypeId{idKind=Bound{ offset, ...}, ...}) = SOME(mapTypeId offset)
        |   copyId _ _ = NONE
        val mappedX = copyTypeConstr(xTypeCons, copyId xMap, id, id)
        and mappedY = copyTypeConstr(yTypeCons, copyId yMap, id, id)
    in
        equalTypeIds(tcIdentifier mappedX, tcIdentifier mappedY)
    end

    (* prints a block of items *)
    fun tDisp (t : types, depth : int, typeVarName : typeVarForm -> string, env: printTypeEnv,
               sigMap: (int->typeId)option) : pretty =
    let
        (* prints a block of items *)
        fun dispP (t : types, depth : int) : pretty =
        let
            (* prints a block of items *)
            fun parenthesise depth t =
            if depth <= 1
            then PrettyString "..."
            else
                PrettyBlock (0, false, [],
                    [
                        PrettyString "(",
                        dispP (t, depth - 1),
                        PrettyString ")"
                    ]);
    
            (* prints a sequence of items *)
            fun prettyList [] _ _: pretty list = []

            |   prettyList [H] depth separator =
                let
                    val v = eventual H;
                in
                    if separator = "*" andalso
                        (isFunctionType v orelse isProductType v)
                    then (* Must bracket the expression *) [parenthesise depth v]
                    else [dispP (v, depth)]
                end

            |   prettyList (H :: T) depth separator =
                if depth <= 0
                then [PrettyString "..."]
                else
                let
                    val v = eventual H;
                in
                    PrettyBlock (0, false, [],
                        [(if separator = "*" andalso
                           (isFunctionType v orelse isProductType v)
                        then (* Must bracket the expression *) parenthesise depth v
                        else dispP (v, depth)),
                        PrettyBreak (if separator = "," then 0 else 1, 0),
                        PrettyString separator
                        ]) ::
                    PrettyBreak (1, 0) ::
                    prettyList T (depth - 1) separator
                end;
        
            val typ = eventual t; (* Find the real type structure *)
        in 
            case typ of
                TypeVar tyVar =>
                let
                    val tyVal : types = tvValue tyVar;
                in
                    case tyVal of
                        EmptyType => PrettyString (typeVarName tyVar)
                    |   _         => dispP (tyVal, depth)
                end
      
                (* Type construction. *)
            |   TypeConstruction {args, name, constr=typeConstructor, ...} =>
                let
                    val constrName = (* Use the type constructor name unless we're had an error. *)
                        if isUndefined typeConstructor then name else tcName typeConstructor

                    (* There are three possible cases: we may not find any type with the
                       name, we may look up the name and find the type or we may look up the
                       name and find a different type. *)
                    datatype isFound = NotFound | FoundMatch | FoundNotMatch
                    
                    (* If we're printing a value that refers to a type constructor we
                       want to print the correct amount of any structure prefix for the
                       current context. *)
                    fun findType (_, []) = NotFound
                    |   findType ({ lookupType, ... }, [typeName]) =
                        (
                            (* This must be the name of a type. *)
                            case lookupType typeName of
                                SOME (t, map) =>
                                    if eqTypeConstrs(typeConstructor, sigMap, tsConstr t, map)
                                    then FoundMatch else FoundNotMatch
                            |   NONE => NotFound
                        )
                    |   findType ({ lookupStruct, ... }, structName :: tail) =
                        (
                            (* This must be the name of a structure.  Does it contain our type? *)
                            case lookupStruct structName of
                                SOME(Struct { signat, ...}, map) =>
                                    let
                                        val Signatures { tab, typeIdMap, ...} = signat
                                        val Env { lookupType, lookupStruct, ...} = makeEnv tab
                                        val newMap =
                                            case map of
                                                SOME map => composeMaps(typeIdMap, map)
                                            |   NONE => typeIdMap
                                        fun subLookupType s =
                                            case lookupType s of NONE => NONE | SOME t => SOME(t, SOME newMap)
                                        fun subLookupStruct s =
                                            case lookupStruct s of NONE => NONE | SOME t => SOME(t, SOME newMap)
                                    in
                                        findType({lookupType=subLookupType, lookupStruct=subLookupStruct}, tail)
                                    end
                            |   NONE => NotFound
                        )

                    (* See if we have this type in the current environment or in some structure in
                       the current environment.  The name we have may be a full structure path. *)
                    fun nameToList ("", l) = (l, NotFound) (* Not there. *)
                    |   nameToList (s, l) = 
                        let
                            val { first, second } = splitString s
                            val currentList = second :: l
                        in
                            case findType(env, currentList) of
                                FoundMatch => (currentList, FoundMatch)
                            |   FoundNotMatch =>
                                (
                                    case nameToList(first, currentList) of
                                        result as (_, FoundMatch) => result
                                    |   (l, _) => (l, FoundNotMatch)
                                )
                            |   NotFound => nameToList(first, currentList)
                        end
                    (* Try the type constructor name first.  This is usually accurate.  If not
                       fall back to the type identifier.  This may be needed in rarer cases. *)
                    val names =
                        case nameToList(constrName, []) of
                            (names, FoundMatch) => names (* Found the type constructor name. *)
                        |   (names, f) =>
                            let
                                (* Try the type identifier name. *)
                                val TypeId { description = { name=idName, ...}, ...} =
                                    case (sigMap, tcIdentifier typeConstructor) of
                                    (SOME map, TypeId{idKind=Bound{offset, ...}, ...}) => map offset
                                |   (_, id) => id
                                (* Only add "?" if we actually found a type with the required
                                   name but it wasn't the right one.  This allows us to print a
                                   sensible result where the type has been shadowed but doesn't
                                   affect situations such as where we create a unique type name
                                   for a free type variable. *)
                                fun addQuery n =
                                    case f of FoundNotMatch => "?" :: n | _ => n
                            in
                                if idName = "" then addQuery names
                                else
                                case nameToList(idName, []) of
                                    (idNames, FoundMatch) => idNames
                                |   (_, _) => addQuery names (* Print it as "?.t".  This isn't ideal but will help in
                                                              situations where we have redefined "t". *)
                            end
                    val newName = String.concatWith "." names
                    (* Get the declaration position for the type constructor. *)
                    val constrContext =
                        if isUndefined typeConstructor then []
                        else
                        (
                            case List.find(fn DeclaredAt _ => true | _ => false) (tcLocations typeConstructor) of
                                SOME(DeclaredAt loc) => [ContextLocation loc]
                            |   _ => []
                        )
                    val constructorEntry = 
                        PrettyBlock(0, false, constrContext, [PrettyString newName(*constrName*)])
                in
                    case args of
                        [] => constructorEntry
                    |   args as hd :: tl =>
                        let
                            val argVal = eventual hd;
                        in
                            PrettyBlock (0, false, [],
                            [
                                (* If we have just a single argument and it's just a type constructor
                                   or a construction we don't need to parenthesise it. *)
                                if null tl andalso not (isProductType argVal orelse isFunctionType argVal)
                                then dispP (argVal, depth - 1)
                                else if depth <= 1
                                then PrettyString "..."
                                else PrettyBlock(0, false, [],
                                         [PrettyString "(", PrettyBreak (0, 0)]
                                         @ prettyList args (depth - 1) ","
                                         @ [PrettyBreak (0, 0), PrettyString ")"]
                                     ),
                                PrettyBreak(1, 0),
                                constructorEntry (* The constructor. *)
                            ])
                        end
                end
        
            |   FunctionType {arg, result} =>
                if depth <= 0
                then PrettyString "..."
                else (* print out in infix notation *)
                let
                    val evArg = eventual arg;
                in
                    PrettyBlock (0, false, [],
                        [
                        (* If the argument is a function it must be printed as (a-> b)->.. *)
                        if isFunctionType evArg 
                        then parenthesise depth evArg
                        else dispP (evArg, depth - 1),
                        PrettyBreak(1, 2),
                        PrettyString "->",
                        PrettyBreak (1, 2),
                        dispP (result, depth - 1)
                        ])
                end
                     
            |   LabelledType (r as {recList, ...}) =>
                if depth <= 0
                then PrettyString "..."
                else if isProductType typ
                then (* Print as a product *)
                    PrettyBlock (0, false, [], (* Print them as t1 * t2 * t3 .... *)
                        prettyList (map (fn {typeof, ...} => typeof) recList) depth "*")
                else (* Print as a record *)
                let
                    (* The ordering on fields is designed to allow mixing of tuples and
                       records (e.g. #1).  It puts shorter names before longer so that
                       #11 comes after #2 and before #100.  For named records it does
                       not make for easy reading so we sort those alphabetically when
                       printing. *)
                    val sortedRecList =
                        Misc.quickSort(fn {name = a, ...} => fn {name = b, ...} => a <= b) recList
                in
                    PrettyBlock (2, false, [],
                        PrettyString "{" ::
                        (let
                            fun pRec [] _ = []
                              | pRec ({name, typeof} :: T) depth =
                                if depth <= 0 then [PrettyString "..."]
                                else
                                    [
                                    PrettyBlock(0, false, [],
                                        [
                                            PrettyBlock(0, false, [],
                                                [
                                                PrettyString (name ^ ":"),
                                                PrettyBreak(1, 0),
                                                dispP(typeof, depth - 1)
                                                ] @
                                                (if null T then [] else [PrettyBreak (0, 0), PrettyString ","])
                                            )
                                        ]@
                                        (if null T then [] else PrettyBreak (1, 0) :: pRec T (depth-1))
                                        )
                                    ]
                        in
                            pRec sortedRecList (depth - 1)
                        end) @
                        [ PrettyString (if recordIsFrozen r then "}" else case recList of [] =>   "...}" | _  => ", ...}")]
                        )
                end

            |   OverloadSet {typeset = []} => PrettyString "no type"

            |   OverloadSet {typeset = tconslist} =>
                (* This typically arises when printing error messages in the second pass because
                   the third pass will select a single type e.g. int where possible.  To
                   simplify the messages select a single type if possible. *)
                (
                    case preferredOverload tconslist of
                        SOME tcons => dispP(mkTypeConstruction (tcName tcons, tcons,[], []), depth)
                    |   NONE =>
                      (* Just print the type constructors separated by / *)
                    let
                        fun constrLocation tcons =
                            case List.find(fn DeclaredAt _ => true | _ => false) (tcLocations tcons) of
                                SOME(DeclaredAt loc) => [ContextLocation loc]
                            |   _ => []
                        (* Type constructor with context. *)
                        fun tconsItem tcons =
                            PrettyBlock(0, false, constrLocation tcons, [PrettyString(tcName tcons)])

                        fun printTCcons [] = []
                          | printTCcons [tcons] = [tconsItem tcons]
                          | printTCcons (tcons::rest) =
                                tconsItem tcons :: PrettyBreak (0, 0) ::
                                PrettyString "/" :: printTCcons rest
                    in
                        PrettyBlock (0, false, [], printTCcons tconslist)
                    end
                )

            |   EmptyType => PrettyString "no type"
            
            |   BadType => PrettyString "bad"
        end (* dispP *)
    in
        dispP (t, depth)
    end (* tDisp *);

  (* Generate unique type-variable names. *)

    fun varNameSequence () : typeVarForm -> string = 
    (* We need to ensure that every distinct type variable has a distinct name.
       Each new type variable is given a name starting at "'a" and going on
       through the alphabet. *)
    let
        datatype names = Names of {name: string, entry: typeVarForm}
        val nameNum    = ref ~1
        val gNameList  = ref [] (* List of names *)
    in
        (* If the type is already there return the name we have given it
           otherwise make a new name and put it in the list. *)
        fn var =>
            case List.find (fn (Names {entry,...}) => sameTv (entry, var)) (!gNameList) of
                NONE =>  (* Not on the list - make a new name *)
                let
                    fun name num = (if num >= 26 then name (num div 26 - 1) else "")
                          ^ String.str (Char.chr (num mod 26 + Char.ord #"a"))
                    val () = nameNum := !nameNum + 1
                    val n = (if tvEquality var then "''" else "'") ^ name(!nameNum)
                    (* Should explicit type variables be distinguished? *)
                in
                    gNameList := Names{name=n, entry=var} :: !gNameList;
                    n
                end
           |    SOME (Names {name,...}) => name
    end (* varNameSequence *)
  

    (* Create the type variables on the fly. *)
    fun tcTypeVars tc =
        List.tabulate(tcArity tc,
            fn _ => makeTv{value=EmptyType, level=generalisable, nonunifiable=false,
                         equality=false, printable=false})

    (* Print a type (as a block of items) *)
    fun displayWithMap (t : types, depth : int, env, sigMap) =
        tDisp (t, depth, varNameSequence (), env, sigMap)
    and display (t : types, depth : int, env) =
        tDisp (t, depth, varNameSequence (), env, NONE)

    (* Print out zero, one or more type variables (unblocked) *)
    fun printTypeVars([], _, _) = [] (* No type vars i.e. monotype *)
 
    |   printTypeVars([oneVar], depth, typeV) = (* Single type var. *)
        [
            tDisp (TypeVar oneVar, depth, typeV, emptyTypeEnv, NONE), 
            PrettyBreak (1, 0)
        ]

    |   printTypeVars(vars, depth, typeV) =
        (* Must parenthesise them. *)
        if depth <= 1 then [PrettyString "..."]
        else
        [
            PrettyBlock(0, false, [],
                PrettyString "(" ::
                PrettyBreak(0, 0) ::
                (let
                    fun pVars vars depth: pretty list = 
                        if depth <= 0 then [PrettyString "..."]
                        else if null vars then []
                        else
                        [
                            tDisp (TypeVar(hd vars), depth, typeV, emptyTypeEnv, NONE),
                            PrettyBreak (0, 0)
                        ] @
                        (if null (tl vars) then []
                         else PrettyString "," :: PrettyBreak (1, 0) :: pVars (tl vars) (depth - 1)
                        )
                in
                    pVars vars depth
                end) @ [PrettyString ")"]
            ),
            PrettyBreak (1, 0)
        ]
  
  
    (* Version used in parsetree. *)
    fun displayTypeVariables (vars : typeVarForm list, depth : int) =
      printTypeVars (vars, depth, varNameSequence ())
    
 
    (* Parse tree for types.  This is used to represent types in the source. *)
    datatype typeParsetree =
        ParseTypeConstruction of
            { name: string, args: typeParsetree list,
              location: location, nameLoc: location, argLoc: location,
              (* foundConstructor is set to the constructor when it has been
                 looked up.  This allows us to get the location where it was
                 declared if we export the parse-tree. *)
              foundConstructor: typeConstrs ref }
    |   ParseTypeProduct of
            { fields: typeParsetree list, location: location }
    |   ParseTypeFunction of
            { argType: typeParsetree, resultType: typeParsetree, location: location }
    |   ParseTypeLabelled of
            { fields: ((string * location) * typeParsetree * location) list,
              frozen: bool, location: location }
    |   ParseTypeId of { types: typeVarForm, location: location }
    |   ParseTypeBad (* Place holder for errors. *)

    fun typeFromTypeParse(
            ParseTypeConstruction{ args, name, location, foundConstructor = ref constr, ...}) =
        let
            val argTypes = List.map typeFromTypeParse args
        in
            TypeConstruction {name = name, constr = constr,
                              args = argTypes, locations = [DeclaredAt location]}
        end

    |   typeFromTypeParse(ParseTypeProduct{ fields, ...}) =
            mkProductType(List.map typeFromTypeParse fields)
    
    |   typeFromTypeParse(ParseTypeFunction{ argType, resultType, ...}) =
            mkFunctionType(typeFromTypeParse argType, typeFromTypeParse resultType)
    
    |   typeFromTypeParse(ParseTypeLabelled{ fields, frozen, ...}) =
        let
            fun makeField((name, _), t, _) = mkLabelEntry(name, typeFromTypeParse t)        
        in
            mkLabelled(sortLabels(List.map makeField fields), frozen)
        end
    
    |   typeFromTypeParse(ParseTypeId{ types, ...}) = TypeVar types
    
    |   typeFromTypeParse(ParseTypeBad) = BadType
    
    fun makeParseTypeConstruction((constrName, nameLoc), (args, argLoc), location) =
        ParseTypeConstruction{
            name = constrName, nameLoc = nameLoc, args = args, argLoc = argLoc,
            location = location, foundConstructor = ref undefConstr }

    fun makeParseTypeProduct(recList, location) =
        ParseTypeProduct{ fields = recList, location = location }

    fun makeParseTypeFunction(arg, result, location) =
        ParseTypeFunction{ argType = arg, resultType = result, location = location }

    fun makeParseTypeLabelled(recList, frozen, location) =
        ParseTypeLabelled{ fields = recList, frozen = frozen, location = location }

    fun makeParseTypeId(types, location) =
        ParseTypeId{ types = types, location = location }

    fun unitTree location = ParseTypeLabelled{ fields = [], frozen = true, location = location }

    (* Build an export tree from the parse tree. *)
    fun typeExportTree(navigation, p: typeParsetree) =
    let        
        val typeof = typeFromTypeParse p

        (* Common properties for navigation and printing. *)
        val commonProps =
            PTprint(fn d => display(typeof, d, emptyTypeEnv)) ::
            PTtype typeof ::
            exportNavigationProps navigation

        fun asParent () = typeExportTree(navigation, p)
        
    in
        case p of
            ParseTypeConstruction{ location, nameLoc, args, argLoc, ...} =>
            let
                (* If the constructor has been bound return the declaration location.
                   We have to attach the declaration location in the right place if
                   this is a polytype e.g. if we have "int list" here we will have
                   the location for "list" which is the second item not the first. *)
                val (name, decLoc) =
                    case typeof of
                        TypeConstruction { constr, name, ...} =>
                            if isUndefined constr
                            then (name, [])
                            else (name, mapLocationProps(tcLocations constr))
                    |   _ => ("", []) (* Error? *)
                val navNameAndArgs =
                (* Separate cases for nullary, unary and higher type constructions. *)
                    case args of
                        [] => decLoc (* Singleton e.g. int *)
                    |   [oneArg] =>
                        let (* Single arg e.g. int list. *)
                            (* Navigate between the type constructor and the argument.
                               Since the arguments come before the constructor we go there first. *)
                            fun getArg () =
                                typeExportTree({parent=SOME asParent, previous=NONE, next=SOME getName}, oneArg)
                            and getName () =
                                getStringAsTree({parent=SOME asParent, previous=SOME getArg, next=NONE},
                                            name, nameLoc, decLoc)
                        in
                            [PTfirstChild getArg]
                        end
                    |   args =>
                        let (* Multiple arguments e.g. (int, string) pair *)
                            fun getArgs () =
                                (argLoc,
                                    exportList(typeExportTree, SOME getArgs) args @
                                        exportNavigationProps{parent=SOME asParent, previous=NONE, next=SOME getName})
                            and getName () =
                                getStringAsTree({parent=SOME asParent, previous=SOME getArgs, next=NONE},
                                            name, nameLoc, decLoc)
                        in
                            [PTfirstChild getArgs]
                        end
            in
                (location, navNameAndArgs @ commonProps)
            end

        |   ParseTypeProduct{ location, fields, ...} =>
                (location, exportList(typeExportTree, SOME asParent) fields @ commonProps)

        |   ParseTypeFunction{ location, argType, resultType, ...} =>
                (location, exportList(typeExportTree, SOME asParent) [argType, resultType] @ commonProps)

        |   ParseTypeLabelled{ location, fields, ...} =>
            let
                fun exportField(navigation, label as ((name, nameLoc), t, fullLoc)) =
                    let
                        (* The first position is the label, the second the type *)
                        fun asParent () = exportField (navigation, label)
                        fun getLab () =
                            getStringAsTree({parent=SOME asParent, next=SOME getType, previous=NONE},
                                name, nameLoc, [PTtype(typeFromTypeParse t)])
                        and getType () =
                            typeExportTree({parent=SOME asParent, previous=SOME getLab, next=NONE}, t)
                    in
                        (fullLoc, PTfirstChild getLab :: exportNavigationProps navigation)
                    end
            in
                (location, exportList(exportField, SOME asParent) fields @ commonProps)
            end

        |   ParseTypeId{ location, ...} =>
                (location, commonProps)

        |   ParseTypeBad =>
                (nullLocation, commonProps)
    end

    fun displayTypeParse(types, depth, env) = display(typeFromTypeParse types, depth, env)

    (* Associates type constructors from the environment with type identifiers
       (NOT type variables) *)
    fun assignTypes (tp : typeParsetree,  lookupType : string * location -> typeConstrSet, lex : lexan) =
    let
        fun typeFromTypeParse(ParseTypeConstruction{ args, name, location, foundConstructor, ...}) =
            let
                (* Assign constructor, then the parameters. *)
                val TypeConstrSet(constructor, _) = lookupType (name, location)
                val () =
                    (* Check that it has the correct arity. *)
                    if not (isUndefined constructor)
                    then
                    let
                        val arity : int = tcArity constructor;
                        val num   : int = length args;
                    in
                        if arity <> num
                        then (* Give an error message *)
                        errorMessage (lex, location,
                            String.concat["Type constructor (", tcName constructor,
                                ") requires ", Int.toString arity, " type(s) not ",
                                Int.toString num])
                        else foundConstructor := constructor
                    end
                    else ()
                val argTypes = List.map typeFromTypeParse args
            in
                TypeConstruction {name = name, constr = constructor,
                                  args = argTypes, locations = [DeclaredAt location]}
            end

        |   typeFromTypeParse(ParseTypeProduct{ fields, ...}) =
                mkProductType(List.map typeFromTypeParse fields)
    
        |   typeFromTypeParse(ParseTypeFunction{ argType, resultType, ...}) =
                mkFunctionType(typeFromTypeParse argType, typeFromTypeParse resultType)
    
        |   typeFromTypeParse(ParseTypeLabelled{ fields, frozen, ...}) =
            let
                fun makeField((name, _), t, _) = mkLabelEntry(name, typeFromTypeParse t)        
            in
                mkLabelled(sortLabels(List.map makeField fields), frozen)
            end
    
        |   typeFromTypeParse(ParseTypeId{ types, ...}) = TypeVar types
    
        |   typeFromTypeParse(ParseTypeBad) = BadType
    in
        typeFromTypeParse tp
    end;

    (* When we have finished processing a list of patterns we need to check
       that the record is now frozen. *)
    fun recordNotFrozen (TypeVar t) : bool = (* Follow the chain *) recordNotFrozen (tvValue t)
    |   recordNotFrozen (LabelledType r) = not(recordIsFrozen r)
    |   recordNotFrozen _ = false (* record or type alias *);

    datatype generalMatch = Matched of {old: typeVarForm, new: types};

    fun generaliseTypes (atyp : types, checkTv: typeVarForm->types option) = 
    let
        val madeList = ref [] (* List of tyVars. *);

        fun tvs atyp =
        let
            val tyVar = typesTypeVar atyp;
        in
            case List.find(fn Matched{old, ...} => sameTv (old, tyVar)) (!madeList) of
                SOME(Matched{new, ...}) => new
            |   NONE =>
                (
                case checkTv tyVar of
                    SOME found => found
                |   NONE =>
                    let  (* Not on the list - make a new name *)
                        (* Make a unifiable type variable even if the original
                           is nonunifiable. *)
                        val n : types = 
                            mkTypeVar (generalisable, tvEquality tyVar, false, tvPrintity tyVar)
                    in
                        (* Set the new variable to have the same value as the
                           existing.  That is only really needed if we have an
                           overload set. *)
                        tvSetValue (typesTypeVar n, tvValue tyVar);
                        madeList := Matched {old = tyVar, new = n} :: !madeList;
                        n
                    end
                )
        end

        fun copyTypeVar (atyp as TypeVar tyVar) =
            if tvLevel tyVar <> generalisable
            then atyp (* Not generalisable. *)
            else (* Unbound, overload set or flexible record *)
            let
                val newTv = tvs atyp
            in
                (* If we have a type variable pointing to a flexible record we have to
                   copy the type pointed at by the variable. *)
                case tvValue tyVar of
                    valu as LabelledType _ =>
                        tvSetValue (typesTypeVar newTv, copyType (valu, copyTypeVar, fn t => t))
                |   _ => ();
                newTv
            end
        | copyTypeVar atyp = atyp
        
        val copied =
            (* Only process type variables. Return type constructors unchanged. *)
            copyType (atyp, copyTypeVar, fn t => t (*copyTCons*))
    in
        (copied, ! madeList)
    end (* generaliseTypes *);

    (* Exported wrapper for generaliseTypes. *)
    fun generalise atyp =
    let
        val (t, newMatch) = generaliseTypes (atyp, fn _ => NONE)
        fun makeResult(Matched{new, old}) =
            {value=new, equality=tvEquality old, printity=tvPrintity old}
    in
        (t, List.map makeResult newMatch)
    end;

    (* Return the original polymorphic type variables. *)
    fun getPolyTypeVars(atyp, map) =
    let
        val (_, newMatch) = generaliseTypes (atyp, map)
    in
        List.map (fn(Matched{old, ...}) => old) newMatch
    end;
    
    fun generaliseWithMap(atyp, map) =
    let
        val (t, newMatch) = generaliseTypes (atyp, map)
        fun makeResult(Matched{new, old}) =
            {value=new, equality=tvEquality old, printity=tvPrintity old}
    in
        (t, List.map makeResult newMatch)
    end
  
   (* Find the argument type which gives this result when the constructor
      is applied. If we have, for example, a value of type int list and
      we have discovered that this is a "::" node we have to work back by
      comparing the type of "::" ('a * 'a list -> 'a list) to find the
      argument of the constructor (int * int list) and hence how to print it.
     (Actually "list" is treated specially). *)
    fun constructorResult (FunctionType{arg, result=TypeConstruction{args, ...}}, typeArgs) =
        let
            val matches = ListPair.zip(List.map typesTypeVar args, typeArgs)
            fun getArg tv =
                case List.find(fn (atv, _) => sameTv(tv, atv)) matches of
                    SOME (_, ty) => SOME ty
                |   NONE => NONE
        in
            #1 (generaliseTypes(arg, getArg))
        end
    | constructorResult _ = raise InternalError "Not a function type"

    (* If we have a type construction which is an alias for another type
       we construct the alias by first instantiating all the type variables
       and then copying the type. *)
    fun makeEquivalent (atyp, args) =
        case tcIdentifier atyp of
            TypeId{idKind=TypeFn(typeArgs, typeResult), ...} =>
            let
                val matches = ListPair.zip(typeArgs, args)
                fun getArg tv =
                    case List.find(fn (atv, _) => sameTv(tv, atv)) matches of
                        SOME (_, ty) => SOME ty
                    |   NONE => NONE
            in
                #1 (generaliseTypes(typeResult, getArg))
            end

        |   TypeId _ => raise InternalError "makeEquivalent: Not a type function"

    (* Look for the occurrence of locally declared datatypes in the type of a value. *)
    fun checkForEscapingDatatypes(ty: types, errorFn: string->unit) : unit =
    let
        fun checkTypes (typ: types) (ok: bool) : bool =
        case typ of
            TypeConstruction {constr, args, ...} =>
                if tcIsAbbreviation constr
                then (* May be an alias for a type that contains a local datatype. *)
                    foldType checkTypes (makeEquivalent (constr, args)) ok
                else if ok
                then
                (
                    case tcIdentifier constr of
                        TypeId{access=Local{addr, ...}, ...} =>
                            if !addr < 0
                            then 
                            (
                                errorFn("Type of expression contains local datatype (" ^ tcName constr
                                        ^") outside its definition.");
                                false
                            )
                            else true
                    |   _ => true (* Could we have a "selected" entry with a local datatype? *)
                )
                else false
        |   _ => ok
    in
        foldType checkTypes ty true;
        ()
    end

  (* This 3-valued logic is used because in a few cases we may not be sure
     if equality testing is allowed. If we have 2 mutually recursive datatypes
     t = x of s | ... and s = z of t we would first examine "t", find that
     it uses "s", look at "s", find that refers back to "t". To avoid
     infinite recursion we return the result that equality "maybe"
     allowed for "t" and hence for "s". However we may find that the
     other constructors for "t" do not allow equality and so equality
     will not be allowed for "s" either. *)
     
  datatype tri = Yes (* 3-valued logic *)
               | No
               | Maybe;


  (* Returns a flag saying if equality testing is allowed for values of
     the given type. "equality" is used both to generate the code for
     a specific call of equality e.g.  (a, b, c) = f(x), and to generate
     the equality operation for a type when it is declared. In the latter
     case type variables may be parameters which will be filled in later e.g.
     type 'a list = nil | op :: of ('a * 'a list). "search"
     is a function which looks up constructors in mutually recursive type
     declarations. "lookupTypeVar" deals with type variables. If they
     represent parameters to a type declaration equality 
     checking will be allowed. If we are unifying this type to an equality
     type variable they  will be unified to new equality type variables.
     Otherwise equality is not allowed. *)
    
    fun equality (ty, search, lookupTypeVar) : tri =
    let
        (* Can't use foldT because it is not monotonic
           (equality on ref 'a is allowed). *)
        (* Returns Yes only if equality testing is allowed for all types
           in the list. *)
        fun eqForList ([],    soFar) = soFar
          | eqForList (x::xs, soFar) = 
            case equality (x, search, lookupTypeVar) of
               No    => No
             | Maybe => eqForList (xs, Maybe)
             | Yes   => eqForList (xs, soFar);
    in
        case eventual ty of
            TypeVar tyVar => (* The type variable may point to a flexible record or
                          an overload set or it may be the end of the chain.
                          If this is a labelled record we have to make sure that
                          any fields we add also admit equality.
                          lookupTypeVar makes the type variable an equality type
                          so that any new fields are checked for equality but
                          we also have to call "equality" to check the existing
                          fields. *)
                if tvEquality tyVar then Yes
                else
                    (
                    case tvValue tyVar of
                        lab as LabelledType _ =>
                            (
                            case lookupTypeVar tyVar of
                                No => No
                              | _ => equality (lab, search, lookupTypeVar)
                            )
                     | _ => lookupTypeVar tyVar
                    )
   
        |   FunctionType {...} => No  (* No equality on function types! *)
    
        |   TypeConstruction {constr, args, ...} =>
            if isUndefined constr
            then No

            else if tcIsAbbreviation constr
            then (* May be an alias for a type that allows equality. *)
                equality (makeEquivalent (constr, args), search, lookupTypeVar)

            (* ref - Equality is permitted on refs of all types *)
            (* The Definition of Standard ML says that ref is the ONLY type
               constructor which is treated in this way.  The standard basis
               library says that other mutable types such as array should
               also work this way. *)
            else if isPointerEqType(tcIdentifier constr)
            then Yes

            (* Others apart from ref and real *)
            else if tcEquality constr (* Equality allowed. *)
            then eqForList (args, Yes) (* Must be allowed for all the args *)
      
            else
            let (* Not an alias. - Look it up. *)
                val s = search (tcIdentifier constr);
            in 
                if s = No then No else eqForList (args, s)
            end (* TypeConstruction *)
         
        |   LabelledType {recList, ...} => (* Record equality if all subtypes are (ignore frozen!) *)
                (* TODO: Avoid copying the list? *)
                eqForList (map (fn{typeof, ...}=>typeof) recList, Yes)

        |   OverloadSet _ =>
                (* This should not happen because all overload sets should be pointed
                   to by type variables and so should be handled in the TypeVar case. *)
                raise InternalError "equality - Overloadset found"

        |   BadType => No

        |   EmptyType => No (* shouldn't occur *)
    end

  (* When a datatype is declared we test to see if equality is allowed. The
     types are mutually recursive so value constructors of one type may
     take arguments involving values of any of the others. *)
     
    fun computeDatatypeEqualities(types: typeConstrSet list, boundIdEq) =
    let
        datatype state =
          Processed of tri              (* Already processed or processing. *)
        | NotSeen   of typeConstrSet list (* Value is list of constrs. *);
    
        (* This table tells us, for each type constructor, whether it definitely
           admits equality, definitely does not or whether we have yet to look
           at it. *)

        fun isProcessed (Processed _) = true | isProcessed _ = false;
    
        fun stateProcessed (Processed x) = x | stateProcessed _ = raise Match;
        fun stateNotSeen   (NotSeen   x) = x | stateNotSeen   _ = raise Match;
    
        val {enter:typeId * state -> unit,lookup} = mapTable sameTypeId;

        (* Look at each of the constructors in the list. Equality testing is
           only allowed if it is allowed for each of the alternatives. *)
        fun constrEq _           []       soFar = soFar (* end of list - all o.k. *)
        |   constrEq constructor (h :: t) soFar =
            (* The constructor may be a constant e.g.
               datatype 'a list = nil | ... or  a function e.g.
               datatype 'a list = ... cons of 'a * 'a list. *)
            if not (isFunctionType (valTypeOf h)) (* Constant *)
            then constrEq constructor t soFar (* Go on to the next. *)
      
            else
            let
                (* Function - look at the argument type. *)
                (* Equality is allowed for any type-variable.  The only type variables
                   allowed are parameters to the datatype so if we have a type variable
                   then equality is allowed for this datatype.  *)
                val eq = 
                    equality (#arg (typesFunctionType (valTypeOf h)),
                        genEquality, fn _ => Yes);
            in
                if eq = No
                then (* Not allowed. *) No
                else (* O.k. - go on to the next. *)
                    constrEq constructor t (if eq = Maybe then Maybe else soFar)
            end (* constrEq *)

        (* This procedure checks to see if equality is allowed for this datatype. *)
        and genEquality constructorId =
        let 
            (* Look it up to see if we have already done it. It may fail because
               we may have constructors that do not admit equality. *)
            val thisState =
                case (lookup constructorId, constructorId) of
                    (SOME inList, _) => inList
                |   (NONE, TypeId{idKind = Bound{offset, ...}, ...}) =>
                        Processed(if boundIdEq offset then Yes else No)
                |   _ => Processed No
        in
            if isProcessed thisState
            then stateProcessed thisState (* Have either done it already or are currently doing it. *)
            else (* notSeen - look at it now. *)
            let
                (* Equality is allowed for this datatype only if all of them admit it.
                   There are various other alternatives but this is what the standard says.
                   If the "name" is rigid (free) we must not grant equality if it is not 
                   already there although that is not an error. *)
                (* Set the state to "Maybe". This prevents infinite recursion. *)
                val () = enter (constructorId, Processed Maybe);
                val eq =
                    List.foldl 
                        (fn (cons, t) => 
                        if t = No
                        then No
                        else constrEq cons (tsConstructors cons) t)
                        Yes
                        (stateNotSeen thisState);
            in
                (* Set the state we have found if it is "yes" or "no".  If it is
                   maybe we have a recursive reference which appears to admit
                   equality, but may not. E.g. if we have
                             datatype t = A of s | B of int->int  and  s = C of t
                   if we start processing "t" we will go on to "s" and do that
                   before returning to "t". It is only later we find that "t" does
                   not admit equality. If we get "Maybe" as the final result when
                   all the recursion has been unwound we can set the result to
                   "yes", but any intermediate "Maybe"s have to be done again. *)
                enter (constructorId, if eq = Maybe then thisState else Processed eq);
                eq
            end
        end (* genEquality *);
    in
        (* If we have an eqtype we set it to true, otherwise we set all of them
           to "notSeen" with the constructor as value. *)
        List.app 
            (fn dec as TypeConstrSet(decCons, _) => 
            let  (* If we have two datatypes which share we may already have
                    one in the table.  We have to link them together. *)
                val tclist =
                    case lookup (tcIdentifier decCons) of
                        NONE => [dec]
                    |   SOME l =>
                        let
                            val others = stateNotSeen l
                            val newList = dec :: others;
                        in
                            (* If any of these are already equality types (i.e. share with an eqtype)
                               then they all must be. *)
                            if tcEquality decCons orelse tcEquality (tsConstr(hd others))
                            then List.app (fn d => tcSetEquality (tsConstr d, true)) newList
                            else ();
                            newList
                        end
            in
                enter (tcIdentifier decCons, NotSeen tclist)
            end) types;

        (* Apply genEquality to each element of the list. *)
        List.app
            (fn TypeConstrSet(constructor, _) => 
            let
                val constructorId = tcIdentifier constructor;
                val eqForCons     = genEquality constructorId;
            in
                (* If the result is "Maybe" it involves a recursive reference, but
                   the rest of the type allows equality. The type admits equality. *)
                if eqForCons = No
                then () (* Equality not allowed *)
                else
                ( (* Turn on equality. *)
                    enter (constructorId, Processed Yes);
                    tcSetEquality (constructor, true)
                )
            end) types
    end (* computeDatatypeEqualities *);
    
    datatype matchResult =
        SimpleError of types * types * string
    |   TypeConstructorError of types * types * typeConstrs * typeConstrs

    (* Type matching algorithm for both unification and signature matching. *)
    (* The mapping has now been moved out of here.  Instead when signature matching the
       target signature is copied before this is called which means that this
       process is now symmetric.  There may be some redundant tests left in here. *)
    fun unifyTypes(Atype : types, Btype : types) : matchResult option =
    let
        (* Get the result in here.  This isn't very ML-like but it greatly
           simplifies converting the code. *)
        val matchResult: matchResult option ref = ref NONE
        fun matchError error = (* Only report one error. *)
            case matchResult of ref (SOME _) => () | r => r := SOME error
        fun cantMatch(alpha, beta, text) = matchError(SimpleError(alpha, beta, text))
  
    fun match (Atype : types, Btype : types) : unit =
    let (* Check two records/tuples and return the combined type. *)
      fun unifyRecords (rA as {recList=typAlist, fullList = gA},
                        rB as {recList=typBlist, fullList = gB},
                        typA : types, typB : types) : types =
      let        
        val typAFrozen = recordIsFrozen rA
        and typBFrozen = recordIsFrozen rB

        fun matchLabelled ([], []) = []
          
             (* Something left in bList - this is fine if typeA is not frozen.
                e.g.  (a: s, b: t) will match (a: s, ...) but not just (a:s). *)
        |   matchLabelled ([], bList as {name=bName, ...} :: _) =
            ( 
                if typAFrozen
                then cantMatch (typA, typB, "(Field " ^ bName ^ " missing)")
                else ();
                bList (* return the remainder of the list *)
            )

        |   matchLabelled (aList as {name=aName, ...} :: _, []) = (* Something left in bList *)
            ( 
                if typBFrozen
                then cantMatch (typA, typB, "(Field " ^ aName ^ " missing)")
                else ();
                aList (* the rest of aList *)
            )
        
        |   matchLabelled (aList as ((aVal as {name=aName,typeof=aType})::aRest),
                           bList as ((bVal as {name=bName,typeof=bType})::bRest)) =
            (* both not nil - look at the names. *)
            let
                val order = compareLabels (aName, bName);
            in
                if order = 0 (* equal *)
                then (* same name - must be unifiable types *)
                ( (* The result is (either) one of these with the rest of the list. *)
                    match (aType, bType);
                    aVal :: matchLabelled (aRest, bRest)
                )
                else if order < 0 (* aName < bName *)
                then (* The entries in each list are in order so this means that this
                       entry is not in bList. If the typeB is frozen this is an error. *)
                    if typBFrozen (* Continue with the entry removed. *)
                then (cantMatch (typA, typB, "(Field " ^ aName ^ " missing)"); aList)
                else aVal :: matchLabelled (aRest, bList)
                else (* aName > bName *)
                    if typAFrozen
                then (cantMatch (typA, typB, "(Field " ^ bName ^ " missing)"); bList)
                else bVal :: matchLabelled (aList, bRest)
             end (* not nil *);
 
        (* Return the combined list. Only actually used if both are flexible. *)
        val result =
            if typAFrozen andalso typBFrozen andalso List.length typAlist <> List.length typBlist
            then (* Don't attempt to unify the fields if we have the wrong number of items.
                    If we've added or removed an item from a tuple e.g. a function with
                    multiple arguments, it's more useful to know this than to get unification
                    errors on fields that don't match. *)
               (cantMatch (typA, typB, "(Different number of fields)"); [])
            else matchLabelled (typAlist, typBlist)

        fun lastFlex(FlexibleList(ref(r as FlexibleList _))) = lastFlex r
        |   lastFlex(FlexibleList r) = SOME r
        |   lastFlex(FieldList _) = NONE

      in
        if typAFrozen
        then (if typBFrozen then () else valOf(lastFlex gB) := gA; typA)
        else if typBFrozen
        then (valOf(lastFlex gA) := gB; typB)
        else
        let
            (* We may have these linked already in which case we shouldn't do anything. *)
            val lastA = valOf(lastFlex gA) and lastB = valOf(lastFlex gB)
        in
            if lastA = lastB
            then ()
            else
            let
                val genericFields = FieldList(map #name result, false)
            in
                (* If these are both flexible we have link all the generics together
                   so that if we freeze any one of them they all get frozen. *)
                lastA := genericFields;
                lastB := FlexibleList lastA
            end;
            LabelledType {recList = result, fullList = gA}
        end
      end (* unifyRecords *);

    (* Sets a type variable to a value. - Checks that the type variable
       we are assigning does not occur in the expression we are about to
       assign to it. Such cases can occur if we have infinitely-typed
       expressions such as fun a. a::a where a has type 'a list list ...
       Also propagates the level information of the type variable.
       Now also deals with flexible records. *)
    fun assign (var, t) =
    let
      (* Mapped over the type to be assigned. *)
      (* Returns "false" if it is safe to make the assignment. Sorts out
         imperative type variables and propagates level information.
         N.B. It does not propagate equality status. The reason is that
         if we are unifying ''a with '_b ref, the '_b does NOT become
         an equality type var. In all other cases it would. *)
        fun occursCheckFails _ true = true

        |   occursCheckFails ty false =
            let
                val t = eventual ty
            in
                case t of
                    TypeVar tvar =>
                    let
                        (* The level is the minimum of the two, and if we are unifying with
                           an equality type variable we must make this into one. *)
                        val minLev = Int.min (tvLevel var, tvLevel tvar);
                    in
                        if tvLevel tvar <> minLev
                        then 
                            (* If it is nonunifiable we cannot make its level larger. *)
                            if tvNonUnifiable tvar
                            then cantMatch (Atype, Btype, "(Type variable is free in surrounding scope)")
                        else
                        let
                            (* Must make a new type var with the right properties *)
                            (* This type variable may be a flexible record, in which
                               case we have to save the record and put it on the new
                               type variable. foldType will apply checkForLoops to the
                               record. *)
                            val newTv = mkTypeVar (minLev, tvEquality tvar, false, tvPrintity tvar)
                        in
                            tvSetValue (typesTypeVar newTv, tvValue tvar);
                            tvSetValue (tvar, newTv)
                        end
                        else ();
                        sameTv (tvar, var) (* Safe if vars are different. *)
                    end

                |   TypeConstruction {args, constr, ...} =>
                        (* If this is a type abbreviation we have to expand this before processing
                           any arguments.  We mustn't process arguments that are not actually used. *)
                        if tcIsAbbreviation constr
                        then occursCheckFails(makeEquivalent (constr, args)) false
                        else List.foldr (fn (t, v) => occursCheckFails t v) false args

                |   FunctionType {arg, result} =>
                        occursCheckFails arg false orelse occursCheckFails result false

                |   LabelledType {recList,...} =>
                        List.foldr (fn ({ typeof, ... }, v) => occursCheckFails typeof v) false recList

                |   _ => false

            end


      val varVal = tvValue var (* Current value of the variable to be set. *)

      local
        (* We need to process any type abbreviations before applying the occurs check.
           The type we're assigning could boil down to the same type variable we're
           trying to assign.  This doesn't breach the occurs check. *)
         fun followVarsAndTypeFunctions t =
            case eventual t of
                ev as TypeConstruction{constr, args, ...} =>
                if tcIsAbbreviation constr
                then followVarsAndTypeFunctions(makeEquivalent (constr, args))
                else ev
            |   ev => ev
      in
        val finalType = followVarsAndTypeFunctions t
      end
      
      (* We may actually have the same type variable after any type abbreviations
         have been followed. *)
      val reallyTheSame =
            case finalType of
                TypeVar tv => sameTv (tv, var)
            |   _ => false

    in (* start of "assign" *)
        case varVal of
            LabelledType _ =>
            (* Flexible record. Check that the records are compatible. *)
                match (varVal, t)
          | OverloadSet _ =>
             (* OverloadSet.  Check that the sets match.  This is only in the
                case where t is something other than an overload set since
                we remove the overload set from a variable when unifying two
                sets. *)
                match (varVal, t)
          | _ => ();
 
        if reallyTheSame
        then () (* Don't apply the occurs check or check for non-unifiable. *)

        (* If this type variable was put in explicitly then it can't be
           assigned to something else. (We have already checked for the
           type variables being the same). *)
        else if tvNonUnifiable var
        then cantMatch (Atype, Btype, "(Cannot unify with explicit type variable)")

        else if occursCheckFails finalType false
        then cantMatch (Atype, Btype, "(Type variable to be unified occurs in type)")

        else let (* Occurs check succeeded. *)
        fun canMkEqTv (tvar : typeVarForm) : tri = 
          (* Turn it into an equality type var. *)
          if tvEquality tvar then Yes 
          (* If it is nonunifiable we cannot make it into an equality type var. *)
          else if tvNonUnifiable tvar then No
          else (* Must make a new type var with the right properties *)
          let  (* This type variable may be a flexible record or an overload set,
                  in which case we have to save the record and put it on the
                  new type variable.
                  We have to do both because we have to ensure that the existing
                  fields in the flexible record admit equality and ALSO that any
                  additional fields we may add by unification with other records
                  also admit equality. *)
            val newTv = mkTypeVar (tvLevel tvar, true, false, tvPrintity tvar)
            val oldValue = tvValue tvar
          in
            tvSetValue (tvar, newTv);
            (* If this is an overloaded type we must remove any types that
               don't admit equality. *)
            case oldValue of
               OverloadSet{typeset} =>
                    let
                    (* Remove any types which do not admit equality. *)
                       fun filter [] = []
                        |  filter (h::t) =
                                if tcEquality h then h :: filter t else filter t
                    in
                        case filter typeset of
                            [] => No
                          | [constr] =>
                            ( (* Turn a singleton into a type construction. *)
                            tvSetValue (typesTypeVar newTv,
                                mkTypeConstruction(tcName constr, constr, nil, []));
                            Yes
                            )
                          | newset =>
                            (
                            tvSetValue (typesTypeVar newTv, OverloadSet{typeset=newset});
                            Yes
                            )
                    end
              | _ => (* Labelled record or unbound variable. *)
                (
                tvSetValue (typesTypeVar newTv, oldValue);
                Yes
                )
          end;
      
       in
          (* If we are unifying a type with an equality type variable
             we must ensure that equality is allowed for that type. This
             will turn most type variables into equality type vars. *)
          if tvEquality var andalso equality (t, fn _ => No, canMkEqTv) = No
          then cantMatch (Atype, Btype, "(Requires equality type)")
              (* TODO: This can result in an unhelpful message if var is bound
                 to a flexible record since there is no indication in the
                 printed type that the flexible record is an equality type.
                 It would be improved if we set the value to be EmptyType.
                 At least then the type variable would be printed which would
                 be an equality type.
                 --- Adding the "Requires equality type" should improve things. *)
          else ();
          (* Propagate the "printity" status.  This is probably not complete
             but doesn't matter too much since this is a Poly extension. *)
          if tvPrintity var
          then
          let
            fun makePrintity(TypeVar tv) _ =
            (
                if tvPrintity tv then ()
                else case tvValue tv of
                    (* If it's an overload set we don't need to do anything. This will
                       eventually be a monotype. *)
                    OverloadSet _ => ()
                |   oldValue =>
                    let (* Labelled record or unbound variable. *)
                        val newTv = mkTypeVar (tvLevel tv, tvEquality tv, tvNonUnifiable tv, true)
                    in
                        tvSetValue(tv, newTv);
                        (* Put this on the chain if it's a labelled record. *)
                        tvSetValue (typesTypeVar newTv, oldValue)
                    end
            )

            |   makePrintity _ _ = ()
          in
            foldType makePrintity t ()
          end
          else ();
         (* Actually make the assignment. It doesn't matter if var is 
            a labelled record, because t will be either a fixed record
            or a combination of the fields of var and t.  Likewise if
            var was previously an overload set this may replace the set
            by a single type construction. *)
         (* If we have had an error don't make the assignment.  At the very least
            it could prevent us producing useful error information and it could
            also result in unnecessary consequential errors. *)
         case !matchResult of
            NONE => tvSetValue (var, t)
         |  SOME _ => ()
       end
     end (* assign *);

    (* First find see if typeA and typeB are unified to anything
       already, and get the end of a list of "flexibles".  *)

    val tA = eventual Atype
    and tB = eventual Btype

    in (* start of "match" *)
    if isUndefinedType tA orelse isUndefinedType tB
    then () (* If either of these was an undefined type constructor don't try to match. 
               TODO: There are further tests below for this which are now redundant. *)
    else
    case (tA, tB) of
        (BadType, _) => () (* If either is an error don't try to match *)
      | (_, BadType) => ()

      | (TypeVar typeAVar, TypeVar typeBVar) =>
            (* Unbound type variable, flexible record or overload set. *)
            let
                (* Even if this is a one-way match we can allow type variables
                   in the typeA to be instantiated to anything in the typeB. *)
                val typeAVal = tvValue typeAVar;
                (* We have two unbound type variables or flex. records. *)
            in
                if sameTv (typeAVar, typeBVar) (* same type variable? *)
                then ()
                else (* no - assign one to the other *)
                    if tvNonUnifiable typeAVar
                    (* If we have a nonunifiable type variable we want to assign
                       the typeB to  it. If the typeB is nonunifiable as well we
                       will get an error message. *)
                then assign (typeBVar, tA)
                else
                let 
                    (* If they are both flexible records we first set the typeB
                       to the union of the records, and then set the typeA to
                       that. In that way we propagate properties such as
                       equality and level between the two variables. *)
                    val typBVal = tvValue typeBVar
                in
                    case (typeAVal, typBVal) of
                        (LabelledType recA, LabelledType recB) =>
                        (
                          (* Turn these back into simple type variables to save
                             checking the combined record against the originals
                             when we make the assignment.
                             (Would be safe but redundant). *)
                          tvSetValue (typeBVar, emptyType);
                          tvSetValue (typeAVar, emptyType);
                          assign (typeBVar,
                                  unifyRecords (recA, recB, typeAVal, typBVal));
                          assign (typeAVar, tB)
                        )
                     | (OverloadSet{typeset=setA}, OverloadSet{typeset=setB}) =>
                        let
                            (* The lists aren't ordered so we just have to go
                               through by hand. *)
                            fun intersect(_, []) = []
                              | intersect(a, H::T) =
                                    if isInSet(H, a) then H::intersect(a, T) else intersect(a, T)
                            val newSet = intersect(setA, setB)
                        in
                            case newSet of
                                [] => cantMatch (Atype, Btype, "(Incompatible overloadings)")
                             | _ =>
                                (
                                  tvSetValue (typeBVar, emptyType);
                                  tvSetValue (typeAVar, emptyType);
                                  (* I've changed this from OverloadSet{typeset=newset}
                                     to use mkOverloadSet.  The main reason was that it
                                     fixed a bug which resulted from a violation of the
                                     assumption that "equality" would not be passed an
                                     overload set except when pointed to by a type variable.
                                     It also removed the need for a separate test for
                                     singleton sets since mkOverloadSet deals with them.
                                     DCJM 1/9/00. *)
                                  assign (typeBVar, mkOverloadSet newSet);
                                  assign (typeAVar, tB)
                                )
                        end
                     | (EmptyType, _) => (* A is not a record or an overload set. *)
                         assign (typeAVar, tB)
                     | (_, EmptyType) => (* A is a record but B isn't *)
                            assign (typeBVar, tA) (* typeB is ordinary type var. *)
                     | _ => (* Bad combination of labelled record and overload set *)
                        cantMatch (Atype, Btype, "(Incompatible types)")
                end
          end

      | (TypeVar typeAVar, _) =>
            (* typeB is not a type variable so set typeA to typeB.*)
            (* Be careful if this is a non-unifiable type variable being matched to
               the special case of the identity type-construction. *)
        (
            if tvNonUnifiable typeAVar orelse (case tvValue typeAVar of OverloadSet _ => true | _ => false)
            then
                (
                case tB of
                    TypeConstruction {constr, args, ...} =>
                        if isUndefined constr orelse not (tcIsAbbreviation constr)
                        then
                            (
                            case tB of
                                TypeConstruction {constr, args, ...} =>
                                    if isUndefined constr orelse not (tcIsAbbreviation constr)
                                    then assign (typeAVar, tB)
                                    else match(tA, eventual (makeEquivalent (constr, args)))
                            | _ => assign (typeAVar, tB)
                            )
                        else match(tA, eventual (makeEquivalent (constr, args)))

                |  _ => assign (typeAVar, tB)
                )
            else assign (typeAVar, tB)
        )
         
      | (_, TypeVar typeBVar) => (* and typeA is not *)
        (
            (* We have to check for the special case of the identity type-construction. *)
            if tvNonUnifiable typeBVar orelse (case tvValue typeBVar of OverloadSet _ => true | _ => false)
            then
                (
                case tA of
                    TypeConstruction {constr, args, ...} =>
                        if isUndefined constr orelse not (tcIsAbbreviation constr)
                        then
                            (
                            case tB of
                                TypeVar tv =>
                                  (* This will fail if we are matching a signature because the
                                     typeB will be non-unifiable. *)
                                    assign (tv, tA) (* set typeB to typeA *)
                              | typB => match (tA, typB)
                            )
                        else match(eventual (makeEquivalent (constr, args)), tB)
                |  _ =>
                    (
                    case tB of
                        TypeVar tv =>
                          (* This will fail if we are matching a signature because the
                             typeB will be non-unifiable. *)
                            assign (tv, tA) (* set typeB to typeA *)
                      | typB => match (tA, typB)
                    )
                )
            else
                (
                case tB of
                    TypeVar tv =>
                      (* This will fail if we are matching a signature because the
                         typeB will be non-unifiable. *)
                        assign (tv, tA) (* set typeB to typeA *)
                  | typB => match (tA, typB)
                )
        )
              
      | (TypeConstruction({constr = tACons, args=tAargs, ...}), 
         TypeConstruction ({constr = tBCons, args=tBargs, ...})) =>
            (
                (* We may have a number of possibilities here.
                 a) If tA is an alias we simply expand it out and recurse (even
                 if tB is the same alias). e.g. if we have string t where
                 type 'a t = int*'a we expand string t into int*string and
                 try to unify that.
                 b) map it and see if the result is an alias. -- NOW REMOVED
                 c) If tB is a type construction and it is an alias we expand
                 that e.g. unifying "int list" and "int t" where type
                 'a t = 'a list (particularly common in signature/structure
                 matching.)
                 d) Finally we try to unify the stamps and the arguments. *)
                if isUndefined tACons orelse isUndefined tBCons
                then () (* If we've had an undefined type constructor don't try to check further. *)
                else if tcIsAbbreviation tACons
                (* Candidate is an alias - expand it. *)
                then match (makeEquivalent (tACons, tAargs), tB)
                else if tcIsAbbreviation tBCons
                then match (tA, makeEquivalent (tBCons, tBargs))
                else if tcIsAbbreviation tBCons (* If the typeB is an alias it must be expanded. *)
                then match (tA, makeEquivalent (tBCons, tBargs))
                else if sameTypeId (tcIdentifier tACons, tcIdentifier tBCons)
                then
                let (* Same type constructor - do the arguments match? *)
                    fun matchLists []      []    = ()
                      | matchLists (a::al) (b::bl) =
                      (  
                        match (a, b);
                        matchLists al bl
                      )
                      | matchLists _ _ = (* This should only happen as a result of
                                            a different error. *)
                            cantMatch (Atype, Btype, "(Different numbers of arguments)")
                in
                        matchLists tAargs tBargs
                end

                (* When we have different type constructors, especially two with the same name,
                   we try to produce more information. *)
                else matchError(TypeConstructorError(tA, tB, tACons, tBCons))
            )

      | (OverloadSet {typeset}, TypeConstruction {constr=tBCons, args=tBargs, ...}) =>
        (* The candidate is an overloaded type and the target is a type
           construction. *)
        (
            if not (isUndefined tBCons orelse not (tcIsAbbreviation tBCons))
            then match (tA, makeEquivalent (tBCons, tBargs))
            else if isUndefined tBCons
            then ()
            else if tcIsAbbreviation tBCons
            then match (tA, makeEquivalent (tBCons, tBargs))
            else (* See if the target type is among those in the overload set. *)
                if null tBargs (* Must be a nullary type constructor. *)
                    andalso isInSet(tBCons, typeset)
            then () (* ok. *)
                (* Overload sets arise primarily with literals such as "1" and it's
                   most likely that the error is a mismatch between int and another
                   type rather than that the user assumed that the literal was
                   overloaded on a type it actually wasn't. *)
            else
            case preferredOverload typeset of
                NONE => cantMatch (tA, tB, "(Different type constructors)")
            |   SOME prefType =>
                matchError(
                    TypeConstructorError(
                        mkTypeConstruction (tcName prefType, prefType,[], []),
                        tB, prefType, tBCons))
        )

      | (TypeConstruction {constr=tACons, args=tAargs, ...}, OverloadSet {typeset}) =>
        (
            if not (isUndefined tACons orelse not (tcIsAbbreviation tACons))
            then match (makeEquivalent (tACons, tAargs), tB)
            (* We should never find an overload set as the target for a signature
               match but it is perfectly possible for tB to be an overload set
               when unifying two types.  *)
            else if null tAargs andalso isInSet(tACons, typeset)
            then () (* ok. *)
            else
            case preferredOverload typeset of
                NONE => cantMatch (tA, tB, "(Different type constructors)")
            |   SOME prefType =>
                matchError(
                    TypeConstructorError(
                        tA, mkTypeConstruction (tcName prefType, prefType,[], []),
                        tACons, prefType))
        )

      |  (OverloadSet _ , OverloadSet _) => raise InternalError "Unification: OverloadSet/OverloadSet"
      (* (OverloadSet , OverloadSet) should not occur because that should be
         handled in the (TypeVar, TypeVar) case. *)
        
      | (TypeConstruction({constr = tACons, args=tAargs, ...}), _) =>
            if not (isUndefined tACons orelse not (tcIsAbbreviation tACons))
            (* Candidate is an alias - expand it. *)
            then match (makeEquivalent (tACons, tAargs), tB)
            else (* typB not a construction (but typeA is) *)
                cantMatch (tA, tB, "(Incompatible types)")
        
      | (_, TypeConstruction {constr=tBCons, args=tBargs, ...}) => (* and typeA is not. *)
        (* May have a type equivalence e.g. "string t" matches int*string if  type
           'a t = int * 'a . Alternatively we may be matching a structure to a signature
           where the signature says "type t" and the structure contains "type 
           t = int->int" (say). We need to set the type in the signature to int->int. *)
            if not (isUndefined tBCons orelse not (tcIsAbbreviation tBCons))
            then match (tA, makeEquivalent (tBCons, tBargs))
            else if isUndefined tBCons
            then ()
            else if tcIsAbbreviation tBCons
            then match (tA, makeEquivalent (tBCons, tBargs))
            else cantMatch (tB, tA, "(Incompatible types)")

         
      | (FunctionType {arg=typAarg, result=typAres, ...},
         FunctionType {arg=typBarg, result=typBres, ...}) =>
        ( (* must be unifiable functions *)
            (* In principle it doesn't matter whether we unify arguments or
               results first but it could affect the error messages.  Is this
               the best way to do it? *)
            match (typAarg, typBarg);
            match (typAres, typBres)
        )

      | (EmptyType, EmptyType) => ()
            (* This occurs only with exceptions - empty means no argument *)
    
      | (LabelledType recA, LabelledType recB) =>
          (* Unify the records, but discard the result because at least one of the
             records is frozen. *)
            (unifyRecords (recA, recB, tA, tB); ())
            
      | _ => cantMatch (tA, tB, "(Incompatible types)")

    end (* match *)

    in
        match (Atype, Btype);
        ! matchResult
    end; (* unifyTypes *)

    (* Turn a result from matchTypes into a pretty structure so that it
       can be included in a message. *)
    fun unifyTypesErrorReport (_, alphaTypeEnv, betaTypeEnv, what) =
    let
        fun reportError(SimpleError(alpha: types, beta: types, reason)) =
            (* This previously used a single type variable sequence for
               both types.  It may be that this is needed to make
               sensible error messages. *)
            PrettyBlock(3, false, [],
                [
                    PrettyString ("Can't " ^ what (* "match" if a signature, "unify" if core lang. *)),
                    PrettyBreak (1, 0),
                    display (alpha, 1000 (* As deep as necessary *), alphaTypeEnv),
                    PrettyBreak (1, 0),
                    PrettyString "to",
                    PrettyBreak (1, 0),
                    display (beta, 1000 (* As deep as necessary *), betaTypeEnv),
                    PrettyBreak (1, 0),
                    PrettyString reason                        
                ])

        |   reportError(TypeConstructorError(alpha: types, beta: types, alphaCons, betaCons)) =
            let
                fun expandedTypeConstr(ty, tyEnv, tyCons) =
                let
                    fun lastPart name = #second(splitString name)

                    (* Print the type which includes the type constructor name with as
                       much additional information as we can. *)
                    fun printWithDesc{ location, name, description } =
                        PrettyBlock(3, false, [],
                            [ display (ty, 1000, tyEnv) ]
                            @ (if lastPart name = lastPart(tcName tyCons) then []
                               else
                                [
                                    PrettyBreak(1, 0),
                                    PrettyString "=",
                                    PrettyBreak(1, 0),
                                    PrettyBlock(0, false, [ContextLocation location], [PrettyString name])
                                ]
                              )
                            @ (if description = "" then []
                               else
                                [
                                    PrettyBreak(1, 0),
                                    PrettyBlock(0, false, [ContextLocation location],
                                        [PrettyString ("(*" ^ description ^ "*)")])
                                ]
                              )
                            )
                in
                    case tcIdentifier tyCons of
                        TypeId { description, ...} => printWithDesc description
                end
            in
                PrettyBlock(3, false, [],
                    [
                        PrettyString ("Can't " ^ what (* "match" if a signature, "unify" if core lang. *)),
                        PrettyBreak (1, 0),
                        expandedTypeConstr(alpha, alphaTypeEnv, alphaCons),
                        PrettyBreak (1, 0),
                        PrettyString (if what = "unify" then "with" else "to"),
                        PrettyBreak (1, 0),
                        expandedTypeConstr(beta, betaTypeEnv, betaCons),
                        PrettyBreak (1, 0),
                        PrettyString "(Different type constructors)"                        
                    ])
            end
            
    in
        reportError
    end

  (* Given a function type returns the first argument if the
     function takes a tuple otherwise returns the only argument.
     Extended to include the case where the argument is not a function
     in order to work properly for overloaded literals. *)
  fun firstArg(FunctionType{arg=
        LabelledType { recList = {typeof, ...} ::_, ...}, ...}) =
            eventual typeof
   |  firstArg(FunctionType{arg, ...}) = eventual arg
   |  firstArg t = t

    (* Returns an instance of an overloaded function using the supplied
       list of type constructors for the overloading. *)
    fun generaliseOverload(t, constrs, isConverter) =
    let
        (* Returns the result type of a function. *)
        fun getResult(FunctionType{result, ...}) = eventual result
        |   getResult _ = raise InternalError "getResult - not a function";

        val arg = if isConverter then getResult t else firstArg t
    in
        case arg of
            TypeVar tv =>
            let
                (* The argument should be a type variable, possibly set to
                   an empty overload set.  This should be replaced by
                   the current overload set in the copied function type. *)
                val newSet = mkOverloadSet constrs
                val (t, _) = generaliseTypes(t, fn old => if sameTv(old, tv) then SOME newSet else NONE)
            in
                (t, [newSet])
            end
          | _ => raise InternalError "generaliseOverload - arg is not a type var"
    end
    (* Prints out a type constructor e.g. type 'a fred = 'a * 'a
       or datatype 'a joe = bill of 'a list | mary of 'a * int or
       simply type 'a abs if the type is abstract. *)
    fun displayTypeConstrsWithMap (
        TypeConstrSet(
            TypeConstrs{identifier=TypeId{idKind=TypeFn(args, result), ...}, name, ...}, []), depth, typeEnv, sigMap) =
         (* Type function *)
        if depth <= 0 
        then PrettyString "..."
        else
        let
            val typeV = varNameSequence () (* Local sequence for this binding. *)
        in
            PrettyBlock (3, false, [],
                PrettyString "type" ::
                PrettyBreak (1, 0) ::
                printTypeVars (args, depth, typeV) @
                [
                    PrettyString (#second(splitString name)),
                    PrettyBreak(1, 0),
                    PrettyString "=",
                    PrettyBreak(1, 0),
                    tDisp(result, depth-1, typeV, typeEnv, sigMap)
                ]
                )
        end

    |   displayTypeConstrsWithMap (TypeConstrSet(tCons, [] (* No constructors *)), depth, _, _) =
        (* Abstract type or type in a signature. *)
        if depth <= 0 
        then PrettyString "..."
        else PrettyBlock (3, false, [],
            PrettyString (
                if tcEquality tCons then "eqtype" else "type") ::
            PrettyBreak (1, 0) ::
            printTypeVars (tcTypeVars tCons, depth, varNameSequence ()) @
            [PrettyString (#second(splitString(tcName tCons)))]
            )

    |   displayTypeConstrsWithMap (TypeConstrSet(tCons as TypeConstrs{name, locations, ...}, tcConstructors), depth, typeEnv, sigMap) =
            (* It has constructors - datatype declaration *)
        if depth <= 0 
        then PrettyString "..."
        else
        let
            val typeV = varNameSequence ()
            (* Construct a ('a, 'b, 'c) tyCons construction for the result types
               of each of the constructors. *)
            val typeVars = tcTypeVars tCons
            val typeResult = mkTypeConstruction(name, tCons, map TypeVar typeVars, locations)

            (* Print a single constructor (blocked) *)
            fun pValConstr (first, name, typeOf, depth) =
            let
                val (t, _) = generalise typeOf
                val firstBreak = PrettyBreak (1, if first then 2 else 0)
            in
                case t of
                    FunctionType { arg, result} =>
                    let
                        (* Constructor with an argument.  The constructor "type" is the argument.
                           We have to unify the result type of the function with the
                           ('a, 'b, 'c) tyCons type so that we get the correct type variables
                           in the argument.  We just print the argument of the function. *)
                        val _ = unifyTypes(result, typeResult)
                    in
                        [
                            firstBreak,
                            PrettyBlock (0, false, [],
                                PrettyBlock (0, false, [],
                                (if first then PrettyBreak (0, 2)
                                 else PrettyBlock (0, false, [], [PrettyString "|", PrettyBreak(1, 2)]) 
                                 ) ::
                                 (if depth <= 0 then [PrettyString "..."]
                                 else [ PrettyString name, PrettyBreak (1, 4), PrettyString "of"])
                            ) ::
                            (if depth > 0
                            then
                            [
                                PrettyBreak (1, 4),
                                (* print the type as a single block of output *)
                                tDisp (arg, depth - 1, typeV, typeEnv, sigMap)
                            ]
                            else [])
                            )
                        ]
                    end

                |   _ =>
                    [
                        firstBreak,
                        PrettyBlock (0, false, [],
                            [if first then PrettyBreak (0, 2)
                            else PrettyBlock (0, false, [], [PrettyString "|", PrettyBreak(1, 2)]),
                            PrettyString (if depth <= 0 then "..." else name)]
                        )
                    ]
            end
          
            (* Print a sequence of constructors (unblocked) *)
            fun pValConstrRest ([],     _    ): pretty list = []
            |   pValConstrRest (H :: T, depth): pretty list =
                if depth < 0 then []           
                else pValConstr (false, valName H, valTypeOf H, depth) @
                        pValConstrRest (T, depth - 1)
           
            fun pValConstrList ([],     _    ) = PrettyString "" (* shouldn't occur *)    
            |   pValConstrList (H :: T, depth) =
                    PrettyBlock (2, true, [],
                        pValConstr (true, valName H, valTypeOf H, depth) @
                        pValConstrRest (T, depth - 1)
                    )

            in
                PrettyBlock(0, false, [],
                    [
                        PrettyBlock(0, false, [],
                                PrettyString "datatype" ::
                                PrettyBreak (1, 2) ::
                                printTypeVars (typeVars, depth, typeV) @
                                [ PrettyString(#second(splitString(tcName tCons))), PrettyBreak(1, 0), PrettyString "=" ]
                        ),
                        pValConstrList (tcConstructors, depth - 1)
                    ]
                )
            end (* displayTypeConstrsWithMap *)

    fun displayTypeConstrs (tCons : typeConstrSet, depth : int, typeEnv) : pretty =
        displayTypeConstrsWithMap(tCons, depth, typeEnv, NONE)

    (* Return a type constructor from an overload.  If there are
       several (i.e. the overloading has not resolved to a single type)
       it returns the "best".  This is called in the third pass so it
       should never be called if there is not at least one type that
       is possible. *)
    fun typeConstrFromOverload(f, _) =
    let
    fun prefType(TypeVar tvar) =
            ( (* If we still have an overload set that's because it has
                 not reduced to a single type.  In ML 97 we default to
                 int, real, word, char or string in that order.  This
                 works correctly for overloading literals so long as
                 the literal conversion functions are correctly installed. *)
            case tvValue tvar of
                OverloadSet{typeset} =>
                    let
                        (* If we accept this type we have to freeze the
                            overloading to this type.
                            I'm not happy about doing this here but it
                            seems the easiest solution. *)
                        fun freezeType tcons =
                            (
                            tvSetValue(tvar,
                                mkTypeConstruction(tcName tcons, tcons, [], []));
                            tcons
                            )
                    in
                        case preferredOverload typeset of
                            SOME tycons => freezeType tycons
                        |   NONE => raise InternalError "typeConstrFromOverload: No matching type"
                    end
              | _ => raise InternalError "typeConstrFromOverload: No matching type" (* Unbound or flexible record. *)
            )
     |  prefType(TypeConstruction{constr, args, ...}) =
            if not (tcIsAbbreviation constr)
            then constr (* Generally args will be nil in this case but
                           in the special case of looking for an equality
                           function for 'a ref or 'a array it may not be.  *)
            else prefType (makeEquivalent (constr, args))
     |  prefType _ = raise InternalError "typeConstrFromOverload: No matching type"
    in
        prefType(firstArg(eventual f))
    end;

    (* Return the result type of a function.  Also used to test if the value is
       a function type. *)
    fun getFnArgType t =
    case eventual t of
        FunctionType {arg, ... } => SOME arg
    |   _ => NONE
    

  (* Assigns type variables to variables with generalisation permitted
     if their level is at least that of the current level.
     In ML90 mode this produced an error message for any top-level
     free imperative type variables.  We don't do that in ML97 because
     it is possible that another declaration may "freeze" the type variable
     before the composite expression reaches the top level. *)
  fun allowGeneralisation (t, level, nonExpansive, lex, location, moreInfo, typeEnv) =
    let
        fun giveError(s1: string, s2: string) =
        let
            (* Use a single sequence. *)
            val vars : typeVarForm -> string = varNameSequence ();
            open DEBUG
            val parameters = debugParams lex
            val errorDepth = getParameter errorDepthTag parameters
        in
            reportError lex
            {
                hard = true,
                location = location,
                message =
                    PrettyBlock (3, false, [],
                        [
                            PrettyString s1,
                            PrettyBreak (1, 0),
                            tDisp (t, errorDepth, vars, typeEnv, NONE),
                            PrettyBreak (1, 0),
                            PrettyString s2
                        ]
                    ),
                context = SOME(moreInfo ())
            }
        end

        local
            open DEBUG
            val parameters = debugParams lex
        in
            val checkOverloadFlex = getParameter narrowOverloadFlexRecordTag parameters
        end

        fun general t (genArgs as (showError, nonExpansive)) =
            case eventual t of
                TypeVar tvar =>
                let
                    val argSet =
                        if tvLevel tvar >= level andalso tvLevel tvar <> generalisable
                            andalso (case tvValue tvar of OverloadSet _ => false | _ => true)
                        then
                        let
                            (* Make a new generisable type variable, except that type
                               variables in an expansive context cannot be generalised.
                               We also don't generalise if this is an overload set.
                               The reason for that is that it allows us to get overloading
                               information from the surrounding context.
                               e.g. let fun f x y = x+y in f 2.0 end.  An alternative
                               would be take the default type (in this case int).
                               DCJM 1/9/00. *)
                            val nonCopiable = not nonExpansive
                            val newLevel =
                               if nonCopiable then level-1 else generalisable (* copiable *);

                            val isOk =
                                (* If the type variable has top-level scope then we have
                                   a free type variable.  We only want to generate this
                                   message once even if we have multiple type variables.*)
                                (* If the type variable is non-unifiable and the expression is
                                   expansive then we have an error since this will have to
                                   be a monotype.  *)
                                if tvNonUnifiable tvar andalso nonCopiable andalso showError
                                then
                                    (
                                    giveError("Type", "includes a free type variable");
                                    false
                                    )
                                else showError;
                            val newVal =
                                 mkTypeVar 
                                   (newLevel, tvEquality tvar,
                                    if nonCopiable then (tvNonUnifiable tvar) else false,
                                    tvPrintity tvar)
                        in
                            (* If an explicit type variable is going out of scope we can
                               generalise it, except if it is nonunifiable. *)
                            (* It may be a flexible record so we have to transfer the
                               record to the new variable. *)
                            tvSetValue (typesTypeVar newVal, tvValue tvar);
                            tvSetValue (tvar, newVal);
                            (isOk, nonExpansive)
                        end
                        else genArgs
                in
                    (* If we are using the "narrow" context for overloading and
                       flexible records we should apply this here.  Otherwise it is
                       dealt with in the next pass when we have the full program context. *)
                    case (checkOverloadFlex, tvValue tvar) of
                        (true, LabelledType _) => giveError("Type", "is an unresolved flexible record")
                    |   (true, OverloadSet {typeset, ...}) =>
                        (   (* Set this to the "preferred" type.  Typically this is "int" but for overloaded literals
                               (e.g. 0w0) it could be something else. *)
                            case preferredOverload typeset of
                                SOME tycons =>
                                    tvSetValue(tvar,
                                        mkTypeConstruction(tcName tycons, tycons, [], []))
                            |   NONE => raise InternalError "general: No matching type"
                        )
                    |   _ => ();
                    general (tvValue tvar) argSet (* Process any flexible record. *)
                end
           
            |   TypeConstruction {args, constr, ...} =>
                    (* There is a pathological case here.  If we have a type equivalence
                       which contains type variables that do not occur on the RHS
                       (e.g. type 'a t = int) then we generalise over them even with an
                       expansive expression.  This is because the semantics treats type
                       abbreviations as type functions and so any type variables that
                       are eliminated by the function application do not appear in the
                       "type" that the semantics applies to the expression. *)
                    if tcIsAbbreviation constr
                    then
                    let
                        val (r1, _) = general(makeEquivalent (constr, args)) genArgs
                        (* Process any arguments that have not been processed in the equivalent. *)
                        val (r2, _) = List.foldr (fn (t, v) => general t v) (r1, true) args
                    in
                        (r2, nonExpansive)
                    end
                    else List.foldr (fn (t, v) => general t v) genArgs args

            |   FunctionType {arg, result} => general arg (general result genArgs)

            |   LabelledType {recList,...} =>
                    List.foldr (fn ({ typeof, ... }, v) => general typeof v) genArgs recList

            |   _ => genArgs
    in
        general t (true, nonExpansive);
        ()
    end (*  end allowGeneralisation *);

  (* Check for free type variables at the top level.  Added for ML97.  This replaces the
     test in allowGeneralisation above and is applied to all top-level
     values including those in structures and functors.  *)
  (* I've changed this from giving an error message, which prevented the
     code from evaluating, to giving a warning and setting the type
     variables to unique type variables.  That allows, for example,
     fun f x = raise x; f Subscript; to work.  DCJM 8/3/01. *)
  fun checkForFreeTypeVariables(valName: string, ty: types, lex: lexan, printAndEqCode) : unit =
  let
    (* Generate new names for the type constructors. *)
    val count = ref 0
    fun genName num =
        (if num >= 26 then genName (num div 26 - 1) else "")
        ^ String.str (Char.chr (num mod 26 + Char.ord #"a"));

    fun checkTypes (TypeVar tvar) () =
        if isEmpty(tvValue tvar) andalso tvLevel tvar = 1
        then (* The type variable is unbound (specifically, not
                an overload set) and it is not generic i.e. it
                must have come from an expansive expression. *)
            let
                val name = "_" ^ genName(!count)
                val _ = count := !count + 1;
                val declLoc = location lex (* Not correct but OK for the moment. *)
                val declDescription =
                    { location = declLoc, name = name, description = "Constructed from a free type variable." }
                val tCons =
                    makeTypeConstructor (name,
                        makeFreeId(0, Global(printAndEqCode()), tvEquality tvar, declDescription),
                        [DeclaredAt declLoc]);
                val newVal = mkTypeConstruction(name, tCons, [], [])
            in
                warningMessage(lex, location lex, 
                    concat["The type of (", valName,
                        ") contains a free type variable. Setting it to a unique monotype."]);
                tvSetValue (tvar, newVal)
            end
        else ()
     |  checkTypes _ () = ()

  in
      foldType checkTypes ty ();
    ()
  end

    (* Returns true if a type constructor permits equality. *)
    
    fun permitsEquality constr =
        if tcIsAbbreviation constr
        then typePermitsEquality(
                mkTypeConstruction (tcName constr, constr, List.map TypeVar (tcTypeVars constr), []))
        else tcEquality constr
   
    and typePermitsEquality ty = equality (ty, fn _ => No, fn _ => Yes) <> No

    (* See if a type abbreviation or "where type" has the form type t = s or
       type 'a t = 'a s etc and so is simply giving a new name to the type
       constructor.  If it is it then checks that the type constructor used
       (s in this example) is just a simple type name. *)
    fun typeNameRebinding(typeArgs, typeResult): typeId option =
    let
        fun eqTypeVar(TypeVar ta, tb) = sameTv (ta, tb)
        |   eqTypeVar _ = false
    in
        case typeResult of
            TypeConstruction {constr, args, ... } =>
                if not (ListPair.allEq eqTypeVar(args, typeArgs))
                then NONE
                else
                (
                    case tcIdentifier constr of
                        TypeId{idKind=TypeFn _, ...} => NONE
                    |   tId => SOME tId

                )
        |   _ => NONE
    end

  (* Returns the number of the entry in the list. Used to find out the
     location of fields in a labelled record for expressions and pattern
     matching. Assumes that the label appears in the list somewhere. *)
     
  fun entryNumber (label, LabelledType{recList, ...}) =
    let (* Count up the list. *)
      fun entry ({name, ...}::l) n =
        if name = label then n else entry l (n + 1)
       |  entry [] _ = raise Match
    in
      entry recList 0
    end
      
   | entryNumber (label, TypeVar tvar) =
        entryNumber (label, tvValue tvar)
      
   | entryNumber (label, TypeConstruction{constr, ...}) = (* Type alias *)
        entryNumber (label, tcEquivalent constr)
      
   | entryNumber _ =
        raise InternalError "entryNumber - not a record"

  (* Size of a labelled record. *)

  fun recordWidth (LabelledType{recList, ...}) =
        length recList
      
   | recordWidth (TypeVar tvar) =
        recordWidth (tvValue tvar)
      
   | recordWidth (TypeConstruction{constr, ...}) = (* Type alias *)
        recordWidth (tcEquivalent constr)
      
   | recordWidth _ =
        raise InternalError "entryNumber - not a record"

    fun recordFieldMap f (LabelledType{recList, ...}) = List.map (f o (fn {typeof, ...} => typeof)) recList
    |   recordFieldMap f (TypeVar tvar) = recordFieldMap f (tvValue tvar)
    |   recordFieldMap f (TypeConstruction{constr, ...}) = recordFieldMap f (tcEquivalent constr)
    |   recordFieldMap _ _ = raise InternalError "entryNumber - not a record"

    (* Unify two type variables which would otherwise be non-unifiable.
       Used when we have found a local type variable with the same name
       as a global one. *)
    fun linkTypeVars (a, b) =
    let
        val ta = typesTypeVar (eventual(TypeVar a)); (* Must both be type vars. *)
        val tb = typesTypeVar (eventual(TypeVar b));
    in  (* Set the one with the higher level to point to the one with the
         lower, so that the effective level is the lower. *)
        if (tvLevel ta) > (tvLevel tb)
        then tvSetValue (ta, TypeVar b)
        else tvSetValue (tb, TypeVar a)
    end;

    (* Set its level by setting it to a new type variable. *)
    fun setTvarLevel (typ, level) =
    let
        val tv = typesTypeVar (eventual(TypeVar typ)); (* Must be type var. *)
    in
        tvSetValue (tv, mkTypeVar (level, tvEquality tv, true, tvPrintity tv))
    end;

    (* Construct the least general type from a list of types.  This is used after
       type checking to try to remove polymorphism from local values.  It takes
       the list of actual uses of the value, usually a function, and removes
       any unnecessary polymorphism.  This is particularly the case if the
       function involves a flexible record, where the unspecified fields are
       treated as polymorphic, but where the function is actually applied
       to a records which are monomorphic. *)
    fun leastGeneral [] = EmptyType (* Never used? *)

    (* Don't use this at the moment - see the comment on TypeVar below.
       Also the comment on TypeConstruction for local datatypes. *)
(*    |   leastGeneral [oneType] = oneType *)(* Just one - this is it. *)

    |   leastGeneral(firstType::otherTypes): types =
    let
        fun canonical (typ as TypeVar tyVar) =
            (
                case tvValue tyVar of
                    EmptyType => typ
                |   OverloadSet _ =>
                    let
                        val constr = typeConstrFromOverload(typ, false)
                    in
                        mkTypeConstruction(tcName constr, constr, [], [])
                    end
                |   t => canonical t
            )
        |   canonical (typ as TypeConstruction { constr, args, ...}) =
                if tcIsAbbreviation constr (* Handle type abbreviations directly *)
                then canonical(makeEquivalent (constr, args))
                else typ
        |   canonical typ = typ

        (* Take the head of the each argument list and extract the least general.
           Then process the tail.  It's an error if each element of the list
           does not contain the same number of items. *)
        fun leastArgs ([]::_) = []
        |   leastArgs (args as _::_) =
                leastGeneral(List.map hd args) :: leastArgs (List.map tl args)
        |   leastArgs _ = raise Empty

    in
        case canonical firstType of
            (*typ as *)TypeVar _(*tv*) =>
            let
                (*fun sameTypeVar(TypeVar tv1) = sameTv(tv, tv1) | sameTypeVar _ = false*)
            in
                (* If they are all the same type variable return that otherwise return
                   a new generalisable type variable.  They may all be equal if we always
                   apply this function to a value whose type is a polymorphic type in the
                   function that contains all these uses. *)
                (* Temporarily, at least, create a new type var in this case.  If we have a polymorphic
                   function that is only used inside another polymorphic function but isn't declared
                   inside it, if we use the caller's type variable here the call won't be recognised
                   as polymorphic. *)
                (*if List.all sameTypeVar otherTypes then typ else*) mkTypeVar(generalisable, false, false, false)
            end
    
        |   TypeConstruction{ constr, args, name, locations, ...}  =>
            (
                (* There is a potential problem if the datatype is local including if it was
                   constructed in a functor.  Almost always it will have been declared after
                   the polymorphic function but if it happens not to have been we could set
                   a polymorphic function to a type that doesn't exist yet.  To avoid this
                   we don't allow a local datatype here and instead fall back to the
                   polymorphic case. *)
                case tcIdentifier constr of
                    thisConstrId as TypeId{access=Global _, ...} =>
                    let
                        val argLength = List.length args
                        (* This matches if it is an application of the same type constructor. *)
                        fun getTypeConstrs(TypeConstruction{constr, args, ...}) =
                                if sameTypeId(thisConstrId, tcIdentifier constr) andalso
                                        List.length args = argLength
                                then SOME args else NONE
                        |   getTypeConstrs _ = NONE
                        val allArgs = List.mapPartial (getTypeConstrs o canonical) otherTypes
                    in
                        if List.length allArgs = List.length otherTypes
                        then TypeConstruction{constr=constr, name=name, locations=locations,
                                             args = leastArgs(args :: allArgs)}
                        else (* At least one of these wasn't the same type constructor. *)
                            mkTypeVar(generalisable, false, false, false)
                    end
                |   _ => mkTypeVar(generalisable, false, false, false)
            )

        |   FunctionType{ arg, result } =>
            let
                fun getFuns(FunctionType{arg, result}) = SOME(arg, result)
                |   getFuns _ = NONE
                val argResults = List.mapPartial (getFuns o canonical) otherTypes
            in
                if List.length argResults = List.length otherTypes
                then
                let
                    val (args, results) = ListPair.unzip argResults
                in
                    FunctionType{arg=leastGeneral(arg::args), result = leastGeneral(result::results)}
                end
                else (* At least one of these wasn't a function. *)
                    mkTypeVar(generalisable, false, false, false)
            end
  
        |   LabelledType (r as {recList=firstRec, fullList}) =>
            if recordIsFrozen r
            then
            let
                (* This matches if all the field names are the same.  Extract the types. *)
                fun nameMatch({name=name1: string, ...}, {name=name2, ...}) = name1 = name2
                fun getRecords(LabelledType{recList, ...}) =
                        if ListPair.allEq nameMatch (firstRec, recList) 
                        then SOME(List.map #typeof recList) else NONE
                |   getRecords _ = NONE
                val argResults = List.mapPartial (getRecords o canonical) otherTypes
            in
                if List.length argResults = List.length otherTypes
                then
                let
                    (* Use the names from the first record (they all are the same) to
                       build a new record. *)
                    val argTypes = leastArgs(List.map #typeof firstRec :: argResults)
                    fun recreateRecord({name, ...}, types) = {name=name, typeof=types}
                    val newList = ListPair.map recreateRecord(firstRec, argTypes)
                in
                    LabelledType{recList=newList, fullList=fullList }
                end
                else (* At least one of these wasn't a record. *)
                    mkTypeVar(generalisable, false, false, false)
            end
            else (* At this stage the record should be frozen if the program is
                    correct but if it isn't we could have a flexible record which
                    we report elsewhere. *)
                mkTypeVar(generalisable, false, false, false)

        |   _ => (* May arise if there's been an error. *) mkTypeVar(generalisable, false, false, false)
    end

    (* Test if this is floating point i.e. the "real" type. We could include
       abbreviations of real as well but it's probably not worth it. *)
    fun isFloatingPt t =
        case eventual t of
            TypeConstruction{args=[], constr, ...} =>
                sameTypeId (tcIdentifier constr, tcIdentifier realConstr)
        |   OverloadSet {typeset, ...} =>
                (
                    case preferredOverload typeset of
                        SOME t => sameTypeId (tcIdentifier t, tcIdentifier realConstr)
                    |   NONE => false
                )
        |   _ => false

    fun checkDiscard(t: types, lex: lexan): string option =
    let
        open DEBUG
        val checkLevel = getParameter reportDiscardedValuesTag (debugParams lex)

        fun isUnit(LabelledType{recList=[], ...}) = true (* Unit is actually an empty record *)
        |   isUnit(TypeConstruction{
                    constr as TypeConstrs{identifier=TypeId{idKind=TypeFn _, ...}, ...},
                    args, ...}) =
                isUnit(makeEquivalent(constr, args))
        |   isUnit(TypeVar _) = true (* Allow unbound type vars *)
        |   isUnit _ = false
        
        fun isAFunction(FunctionType _) = true
        |   isAFunction(TypeConstruction{
                    constr as TypeConstrs{identifier=TypeId{idKind=TypeFn _, ...}, ...},
                    args, ...}) =
                isAFunction(makeEquivalent(constr, args))
        |   isAFunction _ = false
    in
        case checkLevel of
            1 => if isAFunction (eventual t) then SOME "A function value is being discarded." else NONE
        |   2 => if isUnit (eventual t) then NONE else SOME "A non unit value is being discarded."
        |   _ => NONE
    end

    structure Sharing =
    struct
        type types      = types
        and  values     = values
        and  typeId     = typeId
        and  structVals = structVals
        and  typeConstrs= typeConstrs
        and  typeConstrSet=typeConstrSet
        and  typeParsetree = typeParsetree
        and  locationProp = locationProp
        and  pretty     = pretty
        and  lexan      = lexan
        and  ptProperties = ptProperties
        and  typeVarForm = typeVarForm
        and  codetree   = codetree
        and  matchResult = matchResult
        and  generalMatch = generalMatch
    end
end (* TYPETREE *);