mlton/elaborate/type-env.fun

   1 (* Copyright (C) 2009-2010,2012,2017 Matthew Fluet.
   2  * Copyright (C) 1999-2007 Henry Cejtin, Matthew Fluet, Suresh
   3  *    Jagannathan, and Stephen Weeks.
   4  * Copyright (C) 1997-2000 NEC Research Institute.
   5  *
   6  * MLton is released under a BSD-style license.
   7  * See the file MLton-LICENSE for details.
   8  *)
   9
  10 functor TypeEnv (S: TYPE_ENV_STRUCTS): TYPE_ENV =
  11 struct
  12
  13 open S
  14
  15 structure Layout =
  16    struct
  17       open Layout
  18       val bracket = fn l =>
  19          seq [str "[", l, str "]"]
  20    end
  21 local
  22    open Layout
  23 in
  24    val seq = seq
  25    val str = str
  26 end
  27
  28 local
  29    open LayoutPretty
  30 in
  31    val bracket = bracket
  32    val dontCare = dontCare
  33    val simple = simple
  34 end
  35
  36 local
  37    open Tycon
  38 in
  39    structure AdmitsEquality = AdmitsEquality
  40    structure Kind = Kind
  41 end
  42 structure Field = Record.Field
  43 structure Srecord = SortedRecord
  44 structure Set = DisjointSet
  45
  46 (*
  47  * Keep a clock that the elaborator ticks for each declaration.  Associate each
  48  * type with a time that indicates the earliest declaration at which the type
  49  * occurs.  The time is used for several things.
  50  *
  51  * 1. When we need to generalize a type, we can tell which unknowns appear
  52  *    only in the declaration under consideration, and can hence be generalized.
  53  *
  54  * 2. Similarly, for type variables, we can tell if they appear in an earlier
  55  *    declaration than the one in which they are to be bound, and hence can
  56  *    not be generalized.
  57  *
  58  * 3. For "FlexRecord" types, we can tell when it appears only in the declaration
  59  *    under consideration, and can hence be converted to a "GenFlexRecord" type
  60  *    which allows for generalization of fields not yet known to be in the
  61  *    flexRecord.
  62  *
  63  * 4. For type constructors, we can tell if they are used outside of the scope
  64  *    of their definition.  This handles the side conditions on rules 4, 17, and
  65  *    19.
  66  *)
  67
  68 structure Time:>
  69    sig
  70       type t
  71
  72       val <= : t * t -> bool
  73       val equals: t * t -> bool
  74       val layout: t -> Layout.t
  75       val max: t * t -> t
  76       val min: t * t -> t
  77       val now: unit -> t
  78       val region: t -> Region.t
  79       val tick: {region: Region.t} -> unit
  80       val zero: t
  81    end =
  82    struct
  83       datatype t = T of {clock: int,
  84                          region: Region.t}
  85
  86       local
  87          fun make f (T r) = f r
  88       in
  89          val clock = make #clock
  90          val region = make #region
  91       end
  92
  93       fun layout t =
  94          Layout.tuple [Int.layout (clock t),
  95                        Region.layout (region t)]
  96
  97       local
  98          fun make f (t, t') = f (clock t, clock t')
  99       in
 100          val equals = make Int.equals
 101          val op <= = make Int.<=
 102       end
 103       fun max (t, t') = if t <= t' then t' else t
 104       fun min (t, t') = if t <= t' then t else t'
 105
 106       val zero = T {clock = 0, region = Region.bogus}
 107
 108       local
 109          val current: t ref = ref zero
 110       in
 111          fun now () = !current
 112          fun tick {region} =
 113             current := T {clock = 1 + clock (!current),
 114                           region = region}
 115       end
 116
 117       val tick = Trace.trace ("TypeEnv.Time.tick", Layout.ignore, Unit.layout) tick
 118    end
 119
 120 structure Tyvar =
 121    struct
 122       open Tyvar
 123
 124       local
 125          val {get = info: Tyvar.t -> {isEquality: bool,
 126                                       time: Time.t},
 127               set = setInfo, ...} =
 128             Property.getSet
 129             (Tyvar.plist,
 130              Property.initRaise ("TypeEnv.Tyvar.info", Tyvar.layout))
 131          fun init (a, ie) =
 132             setInfo (a, {isEquality = ie,
 133                          time = Time.now ()})
 134       in
 135          local
 136             fun make f = f o info
 137          in
 138             val time = make #time
 139             val isEquality = make #isEquality
 140          end
 141          fun makeString (s, {equality}) =
 142             let
 143                val a = newString s
 144                val _ = init (a, equality)
 145             in
 146                a
 147             end
 148          fun makeNoname {equality} =
 149             let
 150                val a = newNoname ()
 151                val _ = init (a, equality)
 152             in
 153                a
 154             end
 155          fun makeLike a =
 156             let
 157                val a' = new a
 158                val _ = init (a', isEquality a)
 159             in
 160                a'
 161             end
 162       end
 163
 164       local
 165          fun makeLocalNames () =
 166             let
 167                val a = Char.toInt #"a"
 168                val z = Char.toInt #"z"
 169                val cnt = Counter.new a
 170                fun reset () = Counter.reset (cnt, a)
 171                fun next b =
 172                   let
 173                      val n = Counter.next cnt
 174                   in
 175                      Layout.str
 176                      (concat [if isEquality b then "''" else "'",
 177                               if n > z
 178                                  then concat ["a", Int.toString (n - z)]
 179                                  else Char.toString (Char.fromInt n)])
 180                   end
 181             in
 182                {next = next,
 183                 reset = reset}
 184             end
 185       in
 186          fun makeLayoutPretty () =
 187             let
 188                val {destroy, get = layoutPretty, set = setLayoutPretty, ...} =
 189                   Property.destGetSet (plist, Property.initFun Tyvar.layout)
 190                fun localInit bs =
 191                   let
 192                      val {next, ...} = makeLocalNames ()
 193                   in
 194                      Vector.foreach
 195                      (bs, fn b => setLayoutPretty (b, next b))
 196                   end
 197          in
 198             {destroy = destroy,
 199              layoutPretty = layoutPretty,
 200              localInit = localInit}
 201          end
 202
 203          fun makeLayoutPrettyLocal () =
 204             let
 205                val {next, reset} = makeLocalNames ()
 206                val {destroy, get = layoutPretty, ...} =
 207                   Property.destGet (plist, Property.initFun next)
 208             in
 209                {destroy = destroy,
 210                 layoutPretty = layoutPretty,
 211                 reset = fn () => (reset (); destroy ())}
 212             end
 213       end
 214    end
 215 structure TyvarExt = Tyvar
 216
 217 structure Tycon =
 218    struct
 219       open Tycon
 220
 221       local
 222          val {get = info: t -> {admitsEquality: AdmitsEquality.t ref,
 223                                 kind: Kind.t,
 224                                 prettyDefault: string,
 225                                 region: Region.t,
 226                                 time: Time.t},
 227               set = setInfo, ...} =
 228             Property.getSet
 229             (Tycon.plist,
 230              Property.initRaise ("TypeEnv.Tycon.info", Tycon.layout))
 231          fun init (c, a, k, pd, r) =
 232             setInfo (c, {admitsEquality = ref a,
 233                          kind = k,
 234                          prettyDefault = pd,
 235                          region = r,
 236                          time = Time.now ()})
 237          val _ =
 238             List.foreach
 239             (Tycon.prims, fn {tycon = c, admitsEquality = a, kind = k, name = lpd, ...} =>
 240              init (c, a, k, lpd, Region.bogus))
 241          val made: Tycon.t list ref = ref []
 242       in
 243          local
 244             fun make f = f o info
 245          in
 246             val admitsEquality = ! o make #admitsEquality
 247             val kind = make #kind
 248             val prettyDefault = make #prettyDefault
 249             val region = make #region
 250             val time = make #time
 251             fun setAdmitsEquality (t, ae) =
 252                (make #admitsEquality t) := ae
 253          end
 254          val layoutPrettyDefault = Layout.str o prettyDefault
 255          fun make {admitsEquality, kind, name,
 256                    prettyDefault, region} =
 257             let
 258                val tycon = Tycon.newString name
 259                val _ = init (tycon, admitsEquality, kind,
 260                              prettyDefault, region)
 261                val _ = List.push (made, tycon)
 262             in
 263                tycon
 264             end
 265          fun makeLike c =
 266             make {admitsEquality = admitsEquality c,
 267                   kind = kind c,
 268                   name = originalName c,
 269                   prettyDefault = prettyDefault c,
 270                   region = region c}
 271          fun scopeNew th =
 272             let
 273                val oldMade = !made
 274                val () = made := []
 275                val res = th ()
 276                val newMade = !made
 277                val () = made := oldMade
 278             in
 279                (res, newMade)
 280             end
 281       end
 282       fun makeBogus {name, kind, region} =
 283          make {admitsEquality = AdmitsEquality.Sometimes,
 284                kind = kind,
 285                name = name,
 286                prettyDefault = concat ["<", name, ">"],
 287                region = Option.fold (region, Region.bogus, #1)}
 288    end
 289
 290 structure Equality:>
 291    sig
 292       datatype t = False | True | Unknown
 293
 294       val and2: t * t -> t
 295       val andL: 'a list * ('a -> t) -> t
 296       val andV: 'a vector * ('a -> t) -> t
 297       val applyTycon: Tycon.t * t vector -> t
 298       val fromBool: bool -> t
 299       val join: t * t -> t
 300       val layout: t -> Layout.t
 301       val or2: t * t -> t
 302    end =
 303    struct
 304       datatype t = False | True | Unknown
 305
 306       fun layout e =
 307          case e of
 308             False => Layout.str "False"
 309           | True => Layout.str "True"
 310           | Unknown => Layout.str "Unknown"
 311
 312       fun and2 (e1, e2) =
 313          case (e1, e2) of
 314             (False, _) => False
 315           | (_, False) => False
 316           | (True, _) => e2
 317           | (_, True) => e1
 318           | (Unknown, Unknown) => Unknown
 319
 320       fun andL (xs, f) = List.fold (xs, True, fn (x, e) => and2 (f x, e))
 321       fun andV (xs, f) = Vector.fold (xs, True, fn (x, e) => and2 (f x, e))
 322
 323       fun or2 (e1, e2) =
 324          case (e1, e2) of
 325             (False, _) => e2
 326           | (_, False) => e1
 327           | (True, _) => True
 328           | (_, True) => True
 329           | (Unknown, Unknown) => Unknown
 330
 331       fun join (e1, e2) =
 332          case (e1, e2) of
 333             (Unknown, _) => e2
 334           | (_, Unknown) => e1
 335           | (False, False) => False
 336           | (True, True) => True
 337           | _ => Error.bug "TypeEnv.Equality.join"
 338
 339       fun applyTycon (c, es) =
 340          let
 341             datatype z = datatype AdmitsEquality.t
 342          in
 343             case Tycon.admitsEquality c of
 344                Always => True
 345              | Sometimes => andV (es, fn e => e)
 346              | Never => False
 347          end
 348
 349       fun fromBool b = if b then True else False
 350    end
 351
 352 structure Unknown =
 353    struct
 354       datatype t = T of {canGeneralize: bool,
 355                          id: int}
 356
 357       local
 358          fun make f (T r) = f r
 359       in
 360          val id = make #id
 361       end
 362
 363       fun layout (T {canGeneralize, id, ...}) =
 364          seq [str "Unknown ",
 365               Layout.record [("canGeneralize", Bool.layout canGeneralize),
 366                              ("id", Int.layout id)]]
 367
 368       fun layoutPretty _ = str "???"
 369
 370       fun equals (u, u') = id u = id u'
 371
 372       local
 373          val c = Counter.new 0
 374       in
 375          val newId = fn () => Counter.next c
 376       end
 377
 378       fun new {canGeneralize} =
 379          T {canGeneralize = canGeneralize,
 380             id = newId ()}
 381
 382       fun join (T r, T r'): t =
 383          T {canGeneralize = #canGeneralize r andalso #canGeneralize r',
 384             id = newId ()}
 385    end
 386
 387 (* Flexible record spine, i.e. a possibly extensible list of fields. *)
 388 structure Spine:
 389    sig
 390       type t
 391
 392       val canAddFields: t -> bool
 393       val equals: t * t -> bool
 394       val fields: t -> Field.t list
 395       (* ensureField checks if field is there.  If it is not, then ensureField
 396        * will add it unless no more fields are allowed in the spine.
 397        * It returns true iff it succeeds.
 398        *)
 399       val ensureField: t * Field.t -> bool
 400       val foldOverNew: t * (Field.t * 'a) list * 'b * (Field.t * 'b -> 'b) -> 'b
 401       val layout: t -> Layout.t
 402       val new: Field.t list -> t
 403       val noMoreFields: t -> unit
 404       val unify: t * t -> unit
 405    end =
 406    struct
 407       datatype t = T of {id: int,
 408                          body: {fields: Field.t list ref,
 409                                 more: bool ref} Set.t}
 410
 411       local
 412          val c = Counter.new 0
 413       in
 414          val newId = fn () => Counter.next c
 415       end
 416
 417       fun new fields = T {id = newId (),
 418                           body = Set.singleton {fields = ref fields,
 419                                                 more = ref true}}
 420
 421       fun equals (T {id = id1,...}, T {id = id2,...}) = id1 = id2
 422
 423       fun layout (T {body = s,...}) =
 424          let
 425             val {fields, more} = Set.! s
 426          in
 427             Layout.record [("fields", List.layout Field.layout (!fields)),
 428                            ("more", Bool.layout (!more))]
 429          end
 430
 431       fun canAddFields (T {body = s,...}) = ! (#more (Set.! s))
 432       fun fields (T {body = s,...}) = ! (#fields (Set.! s))
 433
 434       fun ensureFieldValue ({fields, more}, f) =
 435          List.contains (!fields, f, Field.equals)
 436          orelse (!more andalso (List.push (fields, f); true))
 437
 438       fun ensureField (T {body = s,...}, f) = ensureFieldValue (Set.! s, f)
 439
 440       fun noMoreFields (T {body = s,...}) = #more (Set.! s) := false
 441
 442       fun unify (T {body = s1,...}, T {body = s2,...}) =
 443          let
 444             val {fields = fs1, more = m1} = Set.! s1
 445             val {fields = fs2, more = m2} = Set.! s2
 446             val _ = Set.union (s1, s2)
 447             val fs = List.union (!fs1, !fs2, Field.equals)
 448             val m = !m1 andalso !m2
 449             val _ = Set.:= (s1, {fields = ref fs, more = ref m})
 450          in
 451             ()
 452          end
 453
 454       fun foldOverNew (spine: t, fs, ac, g) =
 455          List.fold
 456          (fields spine, ac, fn (f, ac) =>
 457           if List.exists (fs, fn (f', _) => Field.equals (f, f'))
 458              then ac
 459           else g (f, ac))
 460    end
 461
 462 structure Type =
 463    struct
 464       structure Overload =
 465          struct
 466             datatype t = Char | Int | Real | Word
 467
 468             val equals: t * t -> bool = op =
 469
 470             val toString =
 471                fn Char => "Char"
 472                 | Int => "Int"
 473                 | Real => "Real"
 474                 | Word => "Word"
 475
 476             val layout = Layout.str o toString
 477
 478             val matchesTycon: t * Tycon.t -> bool =
 479                fn (ov, c) =>
 480                case ov of
 481                   Char => Tycon.isCharX c
 482                 | Int => Tycon.isIntX c
 483                 | Real => Tycon.isRealX c
 484                 | Word => Tycon.isWordX c
 485
 486             val defaultTycon: t -> Tycon.t =
 487                fn Char => Tycon.defaultChar ()
 488                 | Int => Tycon.defaultInt ()
 489                 | Real => Tycon.defaultReal ()
 490                 | Word => Tycon.defaultWord ()
 491
 492            val admitsEquality: t -> Equality.t =
 493                fn Char => Equality.True
 494                 | Int => Equality.True
 495                 | Real => Equality.False
 496                 | Word => Equality.True
 497          end
 498
 499       (* Tuples of length <> 1 are always represented as records.
 500        * There will never be tuples of length one.
 501        *)
 502       datatype t = T of {equality: Equality.t ref,
 503                          plist: PropertyList.t,
 504                          time: Time.t ref,
 505                          ty: ty} Set.t
 506       and ty =
 507           Con of Tycon.t * t vector
 508         | FlexRecord of {fields: fields,
 509                          spine: Spine.t}
 510         (* GenFlexRecord only appears in type schemes.
 511          * It will never be unified.
 512          * The fields that are filled in after generalization are stored in
 513          * extra.
 514          *)
 515         | GenFlexRecord of genFlexRecord
 516         | Overload of Overload.t
 517         | Record of t Srecord.t
 518         | Unknown of Unknown.t
 519         | Var of Tyvar.t
 520       withtype fields = (Field.t * t) list
 521       and genFlexRecord =
 522          {extra: unit -> {field: Field.t,
 523                           tyvar: Tyvar.t} list,
 524           fields: (Field.t * t) list,
 525           spine: Spine.t}
 526
 527       local
 528          fun make f (T s) = f (Set.! s)
 529       in
 530          val equality = make #equality
 531          val plist: t -> PropertyList.t = make #plist
 532          val time: t -> Time.t ref = make #time
 533          val getTy: t -> ty = make #ty
 534       end
 535
 536       local
 537          open Layout
 538       in
 539          fun layoutFields fs =
 540             List.layout (Layout.tuple2 (Field.layout, layout)) fs
 541          and layout (T s) =
 542             let
 543                val {equality, time, ty, ...} = Set.! s
 544             in
 545                record
 546                [("time", Time.layout (!time)),
 547                 ("equality", Equality.layout (!equality)),
 548                 ("ty",
 549                  case ty of
 550                     Con (c, ts) =>
 551                        paren (align [seq [str "Con ", Tycon.layout c],
 552                                      Vector.layout layout ts])
 553                   | FlexRecord {fields, spine} =>
 554                        seq [str "Flex ",
 555                             record [("fields", layoutFields fields),
 556                                     ("spine", Spine.layout spine)]]
 557                   | GenFlexRecord {extra, fields, spine} =>
 558                        seq [str "GenFlex ",
 559                             record [("extra",
 560                                      List.layout
 561                                      (fn {field, tyvar} =>
 562                                       record [("field", Field.layout field),
 563                                               ("tyvar", Tyvar.layout tyvar)])
 564                                     (extra ())),
 565                                     ("fields", layoutFields fields),
 566                                     ("spine", Spine.layout spine)]]
 567                   | Overload ov => Overload.layout ov
 568                   | Record r => Srecord.layout {record = r,
 569                                                 separator = ": ",
 570                                                 extra = "",
 571                                                 layoutTuple = Vector.layout layout,
 572                                                 layoutElt = layout}
 573                   | Unknown u => Unknown.layout u
 574                   | Var a => paren (seq [str "Var ", Tyvar.layout a]))]
 575             end
 576       end
 577    end
 578
 579 structure Tycon =
 580    struct
 581       open Tycon
 582
 583       val {get = opaqueExpansion: t -> (Type.t vector -> Type.t) option,
 584            set = setOpaqueExpansion, ...} =
 585          Property.getSet (Tycon.plist, Property.initConst NONE)
 586
 587       val opaqueExpansion =
 588          Trace.trace
 589          ("TypeEnv.Tycon.opaqueExpansion", Tycon.layout, Layout.ignore)
 590          opaqueExpansion
 591
 592       val setOpaqueExpansion = fn (c, f) =>
 593          setOpaqueExpansion (c, SOME f)
 594    end
 595 structure TyconExt = Tycon
 596
 597 structure LayoutPretty =
 598    struct
 599       open LayoutPretty
 600       fun record (ds: (Field.t * bool * t) list, flexible: bool) =
 601          simple (case ds of
 602                     [] => if flexible then str "{...}" else str "{}"
 603                   | _ =>
 604                        seq [str "{",
 605                             Layout.mayAlign
 606                             (Layout.separateRight
 607                              (List.map
 608                               (QuickSort.sortList (ds, fn ((f, _, _), (f', _, _)) =>
 609                                                    Field.<= (f, f')),
 610                                fn (f, b, (l, _)) =>
 611                                let
 612                                   val f = Field.layout f
 613                                   val row = seq [f, str ": ", l]
 614                                   val row = if b then Layout.bracket row else row
 615                                in
 616                                   row
 617                                end),
 618                               ",")),
 619                             str (if flexible
 620                                     then ", ...}"
 621                                     else "}")])
 622       fun tuple (ls: t vector): t =
 623          Tycon.layoutAppPretty
 624          (Tycon.tuple, ls,
 625           {layoutPretty = fn _ =>
 626            Error.bug "TypeEnv.LayoutPretty.tuple: layoutPretty"})
 627    end
 628
 629 structure Type =
 630    struct
 631       open Type
 632
 633       fun makeHom {con, expandOpaque, flexRecord, genFlexRecord,
 634                    guard, overload, record, recursive, unknown, var} =
 635          let
 636             datatype status = Processing | Seen | Unseen
 637             val {destroy = destroyStatus, get = status, ...} =
 638                Property.destGet (plist, Property.initFun (fn _ => ref Unseen))
 639             val {get, destroy = destroyProp} =
 640                Property.destGet
 641                (plist,
 642                 Property.initRec
 643                 (fn (t, get) =>
 644                  let
 645                     val r = status t
 646                  in
 647                     case !r of
 648                        Seen => Error.bug "TypeEnv.Type.makeHom: impossible"
 649                      | Processing => recursive t
 650                      | Unseen =>
 651                           (case guard t of
 652                               NONE =>
 653                                  let
 654                                     val _ = r := Processing
 655                                     fun loopFields fields =
 656                                        List.revMap (fields, fn (f, t) => (f, get t))
 657                                     val res =
 658                                        case getTy t of
 659                                           Con (c, ts) =>
 660                                              let
 661                                                 fun no () =
 662                                                    con (t, c, Vector.map (ts, get))
 663                                                 fun yes () =
 664                                                    (case Tycon.opaqueExpansion c of
 665                                                        NONE => no ()
 666                                                      | SOME f => get (f ts))
 667                                              in
 668                                                 if expandOpaque then yes () else no ()
 669                                              end
 670                                         | FlexRecord {fields, spine} =>
 671                                              flexRecord
 672                                              (t, {fields = loopFields fields,
 673                                                   spine = spine})
 674                                         | GenFlexRecord {extra, fields, spine} =>
 675                                              genFlexRecord
 676                                              (t, {extra = extra,
 677                                                   fields = loopFields fields,
 678                                                   spine = spine})
 679                                         | Overload ov => overload (t, ov)
 680                                         | Record r => record (t, Srecord.map (r, get))
 681                                         | Unknown u => unknown (t, u)
 682                                         | Var a => var (t, a)
 683                                     val _ = r := Seen
 684                                  in
 685                                     res
 686                                  end
 687                             | SOME res => (r := Seen; res))
 688                  end))
 689             fun destroy () =
 690                (destroyStatus ()
 691                 ; destroyProp ())
 692          in
 693             {hom = get, destroy = destroy}
 694          end
 695
 696       fun hom (ty, z) =
 697          let
 698             val {hom, destroy} = makeHom z
 699          in
 700             Exn.finally (fn () => hom ty, destroy)
 701          end
 702
 703       fun makeLayoutPretty {expandOpaque,
 704                             layoutPrettyTycon,
 705                             layoutPrettyTyvar} :
 706          {destroy: unit -> unit,
 707           layoutPretty: t -> LayoutPretty.t} =
 708          let
 709             val layoutAppPretty = fn (c, ts) =>
 710                Tycon.layoutAppPretty
 711                (c, ts, {layoutPretty = layoutPrettyTycon})
 712             fun con (_, c, ts) = layoutAppPretty (c, ts)
 713             fun con0 c = layoutAppPretty (c, Vector.new0 ())
 714             fun flexRecord (_, {fields, spine}) =
 715                LayoutPretty.record
 716                (List.fold
 717                 (fields,
 718                  Spine.foldOverNew (spine, fields, [], fn (f, ac) =>
 719                                     (f, false, simple (str "#???"))
 720                                     :: ac),
 721                  fn ((f, t), ac) => (f, false, t) :: ac),
 722                 Spine.canAddFields spine)
 723             fun genFlexRecord (_, {extra, fields, spine}) =
 724                LayoutPretty.record
 725                (List.fold
 726                 (fields,
 727                  List.revMap (extra (), fn {field, tyvar} =>
 728                               (field, false, simple (layoutPrettyTyvar tyvar))),
 729                  fn ((f, t), ac) => (f, false, t) :: ac),
 730                 Spine.canAddFields spine)
 731             fun overload (_, ov) = con0 (Overload.defaultTycon ov)
 732             fun record (_, r) =
 733                case Srecord.detupleOpt r of
 734                   NONE =>
 735                      LayoutPretty.record
 736                      (Vector.toListMap
 737                       (Srecord.toVector r,
 738                        fn (f, t) => (f, false, t)),
 739                       false)
 740                 | SOME ts => LayoutPretty.tuple ts
 741             fun recursive _ = simple (str "<recur>")
 742             fun unknown (_, u) = simple (Unknown.layoutPretty u)
 743             fun var (_, a) = simple (layoutPrettyTyvar a)
 744             val {destroy, hom = layoutPretty} =
 745                makeHom {con = con,
 746                         expandOpaque = expandOpaque,
 747                         flexRecord = flexRecord,
 748                         genFlexRecord = genFlexRecord,
 749                         guard = fn _ => NONE,
 750                         overload = overload,
 751                         record = record,
 752                         recursive = recursive,
 753                         unknown = unknown,
 754                         var = var}
 755          in
 756             {destroy = destroy,
 757              layoutPretty = layoutPretty}
 758          end
 759
 760       fun layoutPretty (t, {expandOpaque, layoutPrettyTycon, layoutPrettyTyvar}) =
 761          let
 762             val {destroy, layoutPretty} =
 763                makeLayoutPretty {expandOpaque = expandOpaque,
 764                                  layoutPrettyTycon = layoutPrettyTycon,
 765                                  layoutPrettyTyvar = layoutPrettyTyvar}
 766             val res = layoutPretty t
 767             val () = destroy ()
 768          in
 769             res
 770          end
 771
 772       fun getEquality t =
 773          let
 774             (* guarded; only invoked if '!(Tycon.admitsEquality c) = Sometimes' *)
 775             fun con (_, c, es) = Equality.applyTycon (c, es)
 776             fun flexRecord (_, {fields: (Field.t * Equality.t) list, spine}) =
 777                if Spine.canAddFields spine
 778                   then Equality.Unknown
 779                   else Equality.andL (fields, #2)
 780             (* impossible; *)
 781             fun genFlexRecord _ = Error.bug "TypeEnv.Type.getEquality.genFlexRecord"
 782             (* guarded; an overload has known equality *)
 783             fun overload _ = Error.bug "TypeEnv.Type.getEquality.overload"
 784             fun record (_, r: Equality.t Srecord.t) =
 785                Equality.andV (Srecord.toVector r, #2)
 786             (* impossible *)
 787             fun recursive _ = Error.bug "TypeEnv.Type.getEquality.recursive"
 788             (* guarded; only invoked if '!(Type.equality t) = Unknown' *)
 789             fun unknown (_, _) = Equality.Unknown
 790             (* guarded; a tyvar has known equality *)
 791             fun var _ = Error.bug "TypeEnv.Type.getEquality.var"
 792             fun wrap (f, sel) arg =
 793                let
 794                   val res = f arg
 795                   val _ = equality (sel arg) := res
 796                in
 797                   res
 798                end
 799             fun guard t =
 800                let
 801                   val e = !(equality t)
 802                in
 803                   case e of
 804                      Equality.Unknown => NONE
 805                    | _ => SOME e
 806                end
 807          in
 808             hom (t, {con = wrap (con, #1),
 809                      expandOpaque = false,
 810                      flexRecord = wrap (flexRecord, #1),
 811                      genFlexRecord = genFlexRecord,
 812                      guard = guard,
 813                      overload = overload,
 814                      record = wrap (record, #1),
 815                      recursive = recursive,
 816                      unknown = unknown,
 817                      var = var})
 818          end
 819
 820       val getEquality =
 821          Trace.trace
 822          ("TypeEnv.Type.getEquality", layout, Equality.layout)
 823          getEquality
 824       val _ = getEquality
 825
 826       fun deConOpt t =
 827          case getTy t of
 828             Con x => SOME x
 829           | _ => NONE
 830
 831       fun deEta (t: t, tyvars: Tyvar.t vector): Tycon.t option =
 832          case deConOpt t of
 833             SOME (c, ts) =>
 834                if Vector.length ts = Vector.length tyvars
 835                   andalso Vector.foralli (ts, fn (i, t) =>
 836                                           case getTy t of
 837                                              Var a =>
 838                                                 Tyvar.equals
 839                                                 (a, Vector.sub (tyvars, i))
 840                                            | _ => false)
 841                   then SOME c
 842                else NONE
 843            | _ => NONE
 844
 845       fun make {equality, time, ty}: t =
 846          T (Set.singleton {equality = ref equality,
 847                            plist = PropertyList.new (),
 848                            time = ref time,
 849                            ty = ty})
 850
 851       fun newTy (ty: ty): t =
 852          let
 853             val (equality, time) =
 854                case ty of
 855                   Con (c, ts) =>
 856                      (Equality.applyTycon
 857                       (c, Vector.map (ts, ! o equality)),
 858                       Vector.fold
 859                       (ts, Tycon.time c, fn (t, t') =>
 860                        Time.max (!(time t), t')))
 861                 | GenFlexRecord _ =>
 862                      Error.bug "TypeEnv.Type.newTy: GenFlexRecord"
 863                 | FlexRecord _ =>
 864                      (Equality.Unknown,
 865                       Time.now ())
 866                 | Overload ov =>
 867                      (Overload.admitsEquality ov,
 868                       Time.zero)
 869                 | Record r =>
 870                      (Srecord.fold
 871                       (r, Equality.True, fn (t, e') =>
 872                        Equality.and2 (!(equality t), e')),
 873                       Srecord.fold
 874                       (r, Time.zero, fn (t, t') =>
 875                        Time.max (!(time t), t')))
 876                 | Unknown _ =>
 877                      Error.bug "TypeEnv.Type.newTy: Unknown"
 878                 | Var a =>
 879                      (Equality.fromBool (Tyvar.isEquality a),
 880                       Tyvar.time a)
 881          in
 882             make {equality = equality,
 883                   time = time,
 884                   ty = ty}
 885          end
 886
 887       fun setTy (T s, ty) =
 888          let
 889             val {equality, plist, time, ...} = Set.! s
 890          in
 891             Set.:= (s, {equality = equality,
 892                         plist = plist,
 893                         time = time,
 894                         ty = ty})
 895          end
 896
 897       fun unknownAux {canGeneralize, equality, time} =
 898          let
 899             val u = Unknown.new {canGeneralize = canGeneralize}
 900             val t = make {equality = equality,
 901                           time = time,
 902                           ty = Unknown u}
 903          in
 904             (u, t)
 905          end
 906       val unknown = #2 o unknownAux
 907
 908       fun new () =
 909          unknown
 910          {canGeneralize = true,
 911           equality = Equality.Unknown,
 912           time = Time.now ()}
 913
 914       val new = Trace.trace ("TypeEnv.Type.new", Unit.layout, layout) new
 915
 916       fun newFlex {fields, spine} =
 917          newTy (FlexRecord {fields = fields, spine = spine})
 918
 919       fun flexRecord record =
 920          let
 921             val v = Srecord.toVector record
 922             val spine = Spine.new (Vector.toListMap (v, #1))
 923             fun isResolved (): bool = not (Spine.canAddFields spine)
 924             val t = newFlex {fields = Vector.toList v,
 925                              spine = spine}
 926          in
 927             (t, isResolved)
 928          end
 929
 930       fun record r = newTy (Record r)
 931
 932       fun tuple ts =
 933          if 1 = Vector.length ts
 934             then Vector.first ts
 935          else newTy (Record (Srecord.tuple ts))
 936
 937       fun con (tycon, ts) =
 938          if Tycon.equals (tycon, Tycon.tuple)
 939             then tuple ts
 940          else newTy (Con (tycon, ts))
 941
 942       fun var a = newTy (Var a)
 943    end
 944
 945 structure Ops = TypeOps (structure Tycon = Tycon
 946                          open Type)
 947
 948 structure UnifyResult =
 949    struct
 950       datatype ('a, 'b) t =
 951          NotUnifiable of 'a
 952        | Unified of 'b
 953
 954       val layout =
 955          fn NotUnifiable _ => str "NotUnifiable"
 956           | Unified _ => str "Unified"
 957    end
 958
 959 structure Type =
 960    struct
 961       (* Order is important, since want specialized definitions in Type to
 962        * override general definitions in Ops.
 963        *)
 964       open Ops Type
 965
 966       val unit = tuple (Vector.new0 ())
 967
 968       fun isArrow t =
 969          case getTy t of
 970             Con (c, _) => Tycon.equals (c, Tycon.arrow)
 971           | _ => false
 972
 973       fun isBool t =
 974          case getTy t of
 975             Con (c, _) => Tycon.isBool c
 976           | _ => false
 977
 978       fun isCharX t =
 979          case getTy t of
 980             Con (c, _) => Tycon.isCharX c
 981           | Overload Overload.Char => true
 982           | _ => false
 983
 984       fun isCPointer t =
 985          case getTy t of
 986             Con (c, _) => Tycon.isCPointer c
 987           | _ => false
 988
 989       fun isInt t =
 990          case getTy t of
 991             Con (c, _) => Tycon.isIntX c
 992           | Overload Overload.Int => true
 993           | _ => false
 994
 995       fun isUnit t =
 996          case getTy t of
 997             Record r =>
 998                (case Srecord.detupleOpt r of
 999                    NONE => false
1000                  | SOME v => Vector.isEmpty v)
1001           | _ => false
1002
1003       fun isUnknown t =
1004          case getTy t of
1005             Unknown _ => true
1006           | _ => false
1007
1008       local
1009          fun make ov () = newTy (Overload ov)
1010          datatype z = datatype Overload.t
1011       in
1012          val unresolvedChar = make Char
1013          val unresolvedInt = make Int
1014          val unresolvedReal = make Real
1015          val unresolvedWord = make Word
1016       end
1017
1018       fun unresolvedString () = vector (unresolvedChar ())
1019
1020       val traceCanUnify =
1021          Trace.trace2
1022          ("TypeEnv.Type.canUnify", layout, layout, Bool.layout)
1023
1024       fun canUnify arg =
1025          traceCanUnify
1026          (fn (t, t') =>
1027           case (getTy t, getTy t') of
1028              (Unknown _,  _) => true
1029            | (_, Unknown _) => true
1030            | (Con (c, ts), t') => conAnd (c, ts, t')
1031            | (t', Con (c, ts)) => conAnd (c, ts, t')
1032            | (Overload o1, Overload o2) => Overload.equals (o1, o2)
1033            | (Record r, Record r') =>
1034                 let
1035                    val fs = Srecord.toVector r
1036                    val fs' = Srecord.toVector r'
1037                 in Vector.length fs = Vector.length fs'
1038                    andalso Vector.forall2 (fs, fs', fn ((f, t), (f', t')) =>
1039                                            Field.equals (f, f')
1040                                            andalso canUnify (t, t'))
1041                 end
1042            | (Var a, Var a') => Tyvar.equals (a, a')
1043            | _ => false) arg
1044       and conAnd (c, ts, t') =
1045          case t' of
1046             Con (c', ts') =>
1047                Tycon.equals (c, c')
1048                andalso Vector.forall2 (ts, ts', canUnify)
1049           | Overload ov =>
1050                Vector.isEmpty ts andalso Overload.matchesTycon (ov, c)
1051           | _ => false
1052
1053       (* checkEquality t checks that t is an equality type.  If t is
1054        * not an equality type, then checkEquality t returns:
1055        *  - a layout object highlighting violations in t
1056        *  - an alternate type, replacing violations in t with fresh
1057        *    equality unification variables and a layout object
1058        *    highlighting the fresh unification variables.
1059        *)
1060       fun checkEquality (t, {layoutPrettyTycon: Tycon.t -> Layout.t,
1061                              layoutPrettyTyvar: Tyvar.t -> Layout.t}) =
1062          let
1063             val layoutAppPretty = fn (c, ts) =>
1064                Tycon.layoutAppPretty
1065                (c, ts, {layoutPretty = layoutPrettyTycon})
1066             type ll = LayoutPretty.t * LayoutPretty.t
1067             local
1068                fun getLay sel (llo: ll option, _) =
1069                   Option.fold (llo, dontCare, sel o #1)
1070             in
1071                val getLay1 = getLay #1
1072                val getLay2 = getLay #2
1073             end
1074             fun getTy (_, ty) = ty
1075             (* guarded; only invoked if 'Tycon.admitsEquality c = Sometimes' *)
1076             fun con (_, c, rs) =
1077                if Vector.forall (rs, Option.isNone o #1)
1078                   then NONE
1079                   else SOME (layoutAppPretty
1080                              (c, Vector.map (rs, getLay1)),
1081                              layoutAppPretty
1082                              (c, Vector.map (rs, getLay2)),
1083                              Type.con
1084                              (c, Vector.map (rs, getTy)))
1085             fun doRecord (fls: (Field.t * ll) list,
1086                           extra: bool, mk: unit -> t) =
1087                if List.isEmpty fls
1088                   then NONE
1089                   else let
1090                           fun doit sel =
1091                              LayoutPretty.record
1092                              (List.map
1093                               (fls, fn (f, lll) =>
1094                                (f, false, sel lll)),
1095                               extra)
1096                        in
1097                           SOME (doit #1, doit #2, mk ())
1098                        end
1099             fun flexRecord (_, {fields, spine}) =
1100                doRecord (List.keepAllMap
1101                          (fields, fn (f, r) =>
1102                           Option.map (#1 r, fn ll => (f, ll))),
1103                          Spine.canAddFields spine,
1104                          fn () =>
1105                          let
1106                             val fields =
1107                                List.map (fields, fn (f, r) =>
1108                                          (f, getTy r))
1109                          in
1110                             Type.newFlex {fields = fields,
1111                                           spine = spine}
1112                          end)
1113             (* impossible *)
1114             fun genFlexRecord _ = Error.bug "TypeEnv.Type.checkEquality.genFlexRecord"
1115             (* guarded; an overload has known equality
1116              * only invoked if '!(Type.equality t) = False' *)
1117             fun overload (_, ov) =
1118                case ov of
1119                   Overload.Real =>
1120                      let
1121                         val ty =
1122                            Type.unknown {canGeneralize = true,
1123                                          equality = Equality.True,
1124                                          time = Time.now ()}
1125                      in
1126                         SOME (bracket (simple (str "real")),
1127                               bracket (simple (str "<equality>")),
1128                               ty)
1129                      end
1130                 | _ => Error.bug "TypeEnv.Type.checkEquality.overload"
1131             fun record (_, r) =
1132                case Srecord.detupleOpt r of
1133                   NONE =>
1134                      let
1135                         val fields = Srecord.toVector r
1136                         val fields' =
1137                            Vector.keepAllMap
1138                            (fields, fn (f, r) =>
1139                             Option.map (#1 r, fn ll => (f, ll)))
1140                      in
1141                         doRecord (Vector.toList fields',
1142                                   not (Vector.length fields = Vector.length fields'),
1143                                   fn () =>
1144                                   let
1145                                      val fields =
1146                                         Vector.map (fields, fn (f, r) =>
1147                                                     (f, getTy r))
1148                                      val fields = Srecord.fromVector fields
1149                                   in
1150                                      Type.record fields
1151                                   end)
1152                      end
1153                 | SOME rs =>
1154                      if Vector.forall (rs, Option.isNone o #1)
1155                         then NONE
1156                         else SOME (LayoutPretty.tuple (Vector.map (rs, getLay1)),
1157                                    LayoutPretty.tuple (Vector.map (rs, getLay2)),
1158                                    Type.tuple (Vector.map (rs, getTy)))
1159             (* impossible *)
1160             fun recursive _ = Error.bug "TypeEnv.Type.checkEquality.recursive"
1161             fun unknown (t, _) =
1162                case !(equality t) of
1163                   Equality.False =>
1164                      let
1165                         val ty =
1166                            Type.unknown {canGeneralize = true,
1167                                          equality = Equality.True,
1168                                          time = Time.now ()}
1169                      in
1170                         SOME (bracket (simple (str "<non-equality>")),
1171                               bracket (simple (str "<equality>")),
1172                               ty)
1173                      end
1174                 | Equality.True => NONE
1175                 | Equality.Unknown => NONE
1176             (* guarded; a tyvar has known equality
1177              * only invoked if '!(Type.equality t) = False' *)
1178             fun var (_, a) =
1179                if Tyvar.isEquality a
1180                   then Error.bug "TypeEnv.Type.checkEquality.var"
1181                   else let
1182                           val ty =
1183                              Type.unknown {canGeneralize = true,
1184                                            equality = Equality.True,
1185                                            time = Time.now ()}
1186                        in
1187                           SOME (bracket (simple (layoutPrettyTyvar a)),
1188                                 bracket (simple (str "<equality>")),
1189                                 ty)
1190                        end
1191             fun wrap (f, sel) arg =
1192                case f arg of
1193                   NONE =>
1194                      let
1195                         val t = sel arg
1196                      in
1197                         equality t := Equality.True
1198                         ; (NONE, t)
1199                      end
1200                 | SOME (l1, l2, t) =>
1201                      (SOME (l1, l2), t)
1202             (* Need extra guarding of Con, because proceeding with
1203              * hom/con would recursively force all Unknowns in type
1204              * args to Equality.True, even if tycon is
1205              * AdmitsEquality.Never. *)
1206             fun guard t =
1207                case !(equality t) of
1208                   Equality.True => SOME (NONE, t)
1209                 | _ => (case Type.getTy t of
1210                            Con (c, ts) =>
1211                               (case Tycon.admitsEquality c of
1212                                   AdmitsEquality.Always => SOME (NONE, t)
1213                                 | AdmitsEquality.Sometimes => NONE
1214                                 | AdmitsEquality.Never =>
1215                                      let
1216                                         val ty =
1217                                            Type.unknown {canGeneralize = true,
1218                                                          equality = Equality.True,
1219                                                          time = Time.now ()}
1220                                      in
1221                                         SOME (SOME ((bracket o layoutAppPretty)
1222                                                     (c, Vector.map (ts, fn _ => dontCare)),
1223                                                     bracket (simple (str "<equality>"))),
1224                                               ty)
1225                                      end)
1226                          | _ => NONE)
1227             val res : ll option * t =
1228                hom (t, {con = wrap (con, #1),
1229                         expandOpaque = false,
1230                         flexRecord = wrap (flexRecord, #1),
1231                         genFlexRecord = genFlexRecord,
1232                         guard = guard,
1233                         overload = wrap (overload, #1),
1234                         record = wrap (record, #1),
1235                         recursive = recursive,
1236                         unknown = wrap (unknown, #1),
1237                         var = wrap (var, #1)})
1238          in
1239             case res of
1240                (NONE, _) => NONE
1241              | (SOME (l1, l2), t) =>
1242                   SOME (l1, (t, l2))
1243          end
1244
1245       (* checkTime (t, bound) checks that all components of t have
1246        * times no larger than bound.  If t has components with time
1247        * larger than bound, then checkTime (t, bound) returns:
1248        *  - a layout object highlighting violations in t
1249        *  - an alternate type, replacing violations in t with fresh
1250        *    unification variables at time bound and a layout object
1251        *    highlighting the fresh unification variables.
1252        *  - a list of violating tycons
1253        *  - a list of violating tyvars
1254        *)
1255       fun makeCheckTime {layoutPrettyTycon: Tycon.t -> Layout.t,
1256                          layoutPrettyTyvar: Tyvar.t -> Layout.t} =
1257          let
1258             val layoutAppPretty = fn (c, ts) =>
1259                Tycon.layoutAppPretty
1260                (c, ts, {layoutPretty = layoutPrettyTycon})
1261             val times: Time.t list ref = ref []
1262             val tycons: Tycon.t list ref = ref []
1263             val tyvars: Tyvar.t list ref = ref []
1264             type lll = LayoutPretty.t * LayoutPretty.t * LayoutPretty.t
1265             local
1266                fun getLay sel (lllo: lll option, _) =
1267                   Option.fold (lllo, dontCare, sel o #1)
1268             in
1269                val getLay1 = getLay #1
1270                val getLay2 = getLay #2
1271                val getLay3 = getLay #3
1272             end
1273             fun getTy (_, ty) = ty
1274             fun con bound (_, c, rs) =
1275                if Time.<= (Tycon.time c, bound)
1276                   then if Vector.forall (rs, Option.isNone o #1)
1277                           then NONE
1278                           else SOME (layoutAppPretty
1279                                      (c, Vector.map (rs, getLay1)),
1280                                      layoutAppPretty
1281                                      (c, Vector.map (rs, getLay2)),
1282                                      layoutAppPretty
1283                                      (c, Vector.map (rs, getLay3)),
1284                                      Type.con
1285                                      (c, Vector.map (rs, getTy)))
1286                   else let
1287                           val (u, ty) =
1288                              Type.unknownAux {canGeneralize = true,
1289                                               equality = Equality.Unknown,
1290                                               time = bound}
1291                        in
1292                           List.push (times, bound)
1293                           ; List.push (tycons, c)
1294                           ; SOME ((bracket o layoutAppPretty)
1295                                   (c, Vector.map (rs, getLay2)),
1296                                   layoutAppPretty
1297                                   (c, Vector.map (rs, getLay2)),
1298                                   bracket (simple (Unknown.layoutPretty u)),
1299                                   ty)
1300                        end
1301             fun doRecord (fls: (Field.t * lll) list,
1302                           extra: bool, mk: unit -> t) =
1303                if List.isEmpty fls
1304                   then NONE
1305                   else let
1306                           fun doit sel =
1307                              LayoutPretty.record
1308                              (List.map
1309                               (fls, fn (f, lll) =>
1310                                (f, false, sel lll)),
1311                               extra)
1312                        in
1313                           SOME (doit #1, doit #2, doit #3, mk ())
1314                        end
1315             fun flexRecord (_, {fields, spine}) =
1316                doRecord (List.keepAllMap
1317                          (fields, fn (f, r) =>
1318                           Option.map (#1 r, fn lll => (f, lll))),
1319                          Spine.canAddFields spine,
1320                          fn () =>
1321                          let
1322                             val fields =
1323                                List.map (fields, fn (f, r) =>
1324                                          (f, getTy r))
1325                          in
1326                             Type.newFlex {fields = fields,
1327                                           spine = spine}
1328                          end)
1329             fun record (_, r) =
1330                case Srecord.detupleOpt r of
1331                   NONE =>
1332                      let
1333                         val fields = Srecord.toVector r
1334                         val fields' =
1335                            Vector.keepAllMap
1336                            (fields, fn (f, r) =>
1337                             Option.map (#1 r, fn lll => (f, lll)))
1338                      in
1339                         doRecord (Vector.toList fields',
1340                                   not (Vector.length fields = Vector.length fields'),
1341                                   fn () =>
1342                                   let
1343                                      val fields =
1344                                         Vector.map (fields, fn (f, r) =>
1345                                                     (f, getTy r))
1346                                      val fields = Srecord.fromVector fields
1347                                   in
1348                                      Type.record fields
1349                                   end)
1350                      end
1351                 | SOME rs =>
1352                      if Vector.forall (rs, Option.isNone o #1)
1353                         then NONE
1354                         else SOME (LayoutPretty.tuple (Vector.map (rs, getLay1)),
1355                                    LayoutPretty.tuple (Vector.map (rs, getLay2)),
1356                                    LayoutPretty.tuple (Vector.map (rs, getLay3)),
1357                                    Type.tuple (Vector.map (rs, getTy)))
1358             fun var bound (_, a) =
1359                if Time.<= (Tyvar.time a, bound)
1360                   then NONE
1361                   else let
1362                           val (u, ty) =
1363                              Type.unknownAux {canGeneralize = true,
1364                                               equality = Equality.Unknown,
1365                                               time = bound}
1366                        in
1367                           List.push (times, bound)
1368                           ; List.push (tyvars, a)
1369                           ; SOME (bracket (simple (layoutPrettyTyvar a)),
1370                                   simple (layoutPrettyTyvar a),
1371                                   bracket (simple (Unknown.layoutPretty u)),
1372                                   ty)
1373                        end
1374             fun genFlexRecord _ = Error.bug "TypeEnv.Type.checkTime.genFlexRecord"
1375             fun recursive _ = Error.bug "TypeEnv.Type.checkTime.recursive"
1376             fun checkTime (t, bound) =
1377                if Time.<= (!(time t), bound)
1378                   then NONE
1379                   else let
1380                           fun wrap (f, sel) arg =
1381                              case f arg of
1382                                 NONE =>
1383                                    let
1384                                       val t = sel arg
1385                                    in
1386                                       time t := bound
1387                                       ; (NONE, t)
1388                                    end
1389                               | SOME (l1, l2, l3, t) =>
1390                                    (time t := bound
1391                                     ; (SOME (l1, l2, l3), t))
1392                           fun guard t =
1393                              if Time.<= (!(time t), bound)
1394                                 then SOME (NONE, t)
1395                                 else NONE
1396                           val res : lll option * t =
1397                              hom (t, {con = wrap (con bound, #1),
1398                                       expandOpaque = false,
1399                                       flexRecord = wrap (flexRecord, #1),
1400                                       genFlexRecord = genFlexRecord,
1401                                       guard = guard,
1402                                       overload = wrap (fn _ => NONE, #1),
1403                                       record = wrap (record, #1),
1404                                       recursive = recursive,
1405                                       unknown = wrap (fn _ => NONE, #1),
1406                                       var = wrap (var bound, #1)})
1407                        in
1408                           case res of
1409                              (NONE, _) => NONE
1410                            | (SOME (l1, _, l3), t) =>
1411                                 SOME (l1, (t, l3))
1412                        end
1413             fun finishCheckTime () =
1414                {times = List.removeDuplicates (!times, Time.equals),
1415                 tycons = List.removeDuplicates (!tycons, Tycon.equals),
1416                 tyvars = List.removeDuplicates (!tyvars, Tyvar.equals)}
1417          in
1418             {checkTime = checkTime,
1419              finishCheckTime = finishCheckTime}
1420          end
1421
1422       datatype z = datatype UnifyResult.t
1423
1424       val traceUnify =
1425          Trace.trace2
1426          ("TypeEnv.Type.unify", layout, layout,
1427           UnifyResult.layout:
1428           (LayoutPretty.t * LayoutPretty.t, unit) UnifyResult.t -> Layout.t)
1429
1430       fun unify (t, t',
1431                  {layoutPretty: t -> LayoutPretty.t,
1432                   layoutPrettyTycon: Tycon.t -> Layout.t,
1433                   layoutPrettyTyvar: Tyvar.t -> Layout.t}) =
1434          let
1435             val layoutAppPretty = fn (c, ts) =>
1436                Tycon.layoutAppPretty
1437                (c, ts, {layoutPretty = layoutPrettyTycon})
1438             val checkEquality = fn t =>
1439                checkEquality (t, {layoutPrettyTycon = layoutPrettyTycon,
1440                                   layoutPrettyTyvar = layoutPrettyTyvar})
1441             val {checkTime, finishCheckTime} =
1442                makeCheckTime {layoutPrettyTycon = layoutPrettyTycon,
1443                               layoutPrettyTyvar = layoutPrettyTyvar}
1444             fun unify arg =
1445                traceUnify
1446                (fn (outer as T s, outer' as T s') =>
1447                 if Set.equals (s, s')
1448                    then Unified ()
1449                 else
1450                    let
1451                       fun notUnifiable (l: LayoutPretty.t, l': LayoutPretty.t) =
1452                          NotUnifiable (l, l')
1453                       fun notUnifiableBracket (l, l') =
1454                          notUnifiable (bracket l, bracket l')
1455                       fun flexToRecord (fields, spine) =
1456                          (Vector.fromList fields,
1457                           Spine.canAddFields spine)
1458                       fun rigidToRecord r =
1459                          (Srecord.toVector r,
1460                           false)
1461                       fun flexToFlexToRecord (fields, spine, equality, time, outer, spine') =
1462                          let
1463                             val () =
1464                                List.foreach
1465                                (Spine.fields spine', fn f' =>
1466                                 ignore (Spine.ensureField (spine, f')))
1467                             val fields =
1468                                Spine.foldOverNew
1469                                (spine, fields, fields, fn (f, fields) =>
1470                                 let
1471                                    val u =
1472                                       Type.unknown
1473                                       {canGeneralize = true,
1474                                        equality = Equality.or2 (equality, Equality.Unknown),
1475                                        time = time}
1476                                 in
1477                                    (f, u) :: fields
1478                                 end)
1479                             val _ = setTy (outer, FlexRecord {fields = fields, spine = spine})
1480                          in
1481                             flexToRecord (fields, spine)
1482                          end
1483                       fun flexToRigidToRecord (fields, spine, equality, time, outer, r') =
1484                          let
1485                             val () =
1486                                Vector.foreach
1487                                (Srecord.toVector r', fn (f', _) =>
1488                                 ignore (Spine.ensureField (spine, f')))
1489                             val () = Spine.noMoreFields spine
1490                             val fields =
1491                                Spine.foldOverNew
1492                                (spine, fields, fields, fn (f, fields) =>
1493                                 let
1494                                    val u =
1495                                       Type.unknown
1496                                       {canGeneralize = true,
1497                                        equality = Equality.or2 (equality, Equality.Unknown),
1498                                        time = time}
1499                                 in
1500                                    (f, u) :: fields
1501                                 end)
1502                             val r = Srecord.fromVector (Vector.fromList fields)
1503                             val _ = setTy (outer, Record r)
1504                          in
1505                             rigidToRecord r
1506                          end
1507                       fun oneFlex ({fields, spine}, equality, time, outer, r', swap) =
1508                          unifyRecords
1509                          (flexToRigidToRecord (fields, spine, equality, time, outer, r'),
1510                           rigidToRecord r',
1511                           fn () => Unified (Record r'),
1512                           notUnifiable o (fn (l, l') =>
1513                                           if swap
1514                                              then (l', l)
1515                                              else (l, l')))
1516                       fun genFlexError () =
1517                          Error.bug "TypeEnv.Type.unify: GenFlexRecord"
1518                       val {equality, time, ty = t, plist} = Set.! s
1519                       val {equality = equality', time = time', ty = t', ...} = Set.! s'
1520                       fun not () =
1521                          notUnifiableBracket (layoutPretty outer,
1522                                               layoutPretty outer')
1523                       fun unifys (ts, ts', yes, no) =
1524                          let
1525                             val us = Vector.map2 (ts, ts', unify)
1526                          in
1527                             if Vector.forall
1528                                (us, fn Unified _ => true | _ => false)
1529                                then yes ()
1530                             else
1531                                let
1532                                   val (ls, ls') =
1533                                      Vector.unzip
1534                                      (Vector.map
1535                                       (us, fn u =>
1536                                        case u of
1537                                           Unified _ => (dontCare, dontCare)
1538                                         | NotUnifiable (l, l') => (l, l')))
1539                                in
1540                                   no (ls, ls')
1541                                end
1542                          end
1543                       fun conAnd (c, ts, t, t', swap) =
1544                          let
1545                             fun maybe (z, z') =
1546                                if swap then (z', z) else (z, z')
1547                          in
1548                             case t of
1549                                Con (c', ts') =>
1550                                   if Tycon.equals (c, c')
1551                                      then
1552                                         if Vector.length ts <> Vector.length ts'
1553                                            then
1554                                               let
1555                                                  fun lay ts =
1556                                                     simple
1557                                                     (Layout.seq
1558                                                      [Layout.str
1559                                                       (concat ["<",
1560                                                                Int.toString
1561                                                                (Vector.length ts),
1562                                                                " args> "]),
1563                                                       Tycon.layout c])
1564                                               in
1565                                                  notUnifiableBracket
1566                                                  (maybe (lay ts, lay ts'))
1567                                               end
1568                                         else
1569                                            unifys
1570                                            (ts, ts',
1571                                             fn () => Unified t,
1572                                             fn (ls, ls') =>
1573                                             let
1574                                                fun lay ls = layoutAppPretty (c, ls)
1575                                             in
1576                                                notUnifiable
1577                                                (maybe (lay ls, lay ls'))
1578                                             end)
1579                                   else not ()
1580                              | Overload ov =>
1581                                   if Vector.isEmpty ts
1582                                      andalso Overload.matchesTycon (ov, c)
1583                                      then Unified t'
1584                                   else not ()
1585                              | _ => not ()
1586                          end
1587                       fun oneUnknown (u: Unknown.t,
1588                                       equality: Equality.t,
1589                                       time: Time.t,
1590                                       outer: t,
1591                                       t': Type.ty,
1592                                       outer': Type.t,
1593                                       swap: bool) =
1594                          let
1595                             (* This should fail if the unknown occurs in t. *)
1596                             fun con (_, _, ts) =
1597                                Vector.exists (ts, fn b => b)
1598                             fun doFields fields =
1599                                List.exists (fields, fn (_, b) => b)
1600                             fun flexRecord (_, {fields, spine = _}) =
1601                                doFields fields
1602                             fun record (_, r) = Srecord.exists (r, fn b => b)
1603                             fun unknown (_, u') = Unknown.equals (u, u')
1604                             fun no _ = false
1605                             val isCircular =
1606                                hom (outer',
1607                                     {con = con,
1608                                      expandOpaque = false,
1609                                      flexRecord = flexRecord,
1610                                      genFlexRecord = fn _ =>
1611                                      Error.bug "TypeEnv.Type.unify.oneUnknown: genFlexRecord",
1612                                      guard = fn _ => NONE,
1613                                      overload = no,
1614                                      record = record,
1615                                      recursive = fn _ =>
1616                                      Error.bug "TypeEnv.Type.unify.oneUnknown: recursive",
1617                                      unknown = unknown,
1618                                      var = no})
1619                          in
1620                             if isCircular
1621                                then not ()
1622                                else let
1623                                        fun err (l, (t'', l'')) =
1624                                           (setTy (outer, getTy t'')
1625                                            ; notUnifiable
1626                                              (if swap
1627                                                  then (l, l'')
1628                                                  else (l'', l)))
1629                                     in
1630                                        case equality of
1631                                           Equality.True =>
1632                                              (case checkEquality outer' of
1633                                                  NONE => Unified t'
1634                                                | SOME (l, (t'', l'')) =>
1635                                                     err (l, (t'', l'')))
1636                                         | _ =>
1637                                              (case checkTime (outer', time) of
1638                                                  NONE => Unified t'
1639                                                | SOME (l, (t'', l'')) =>
1640                                                     err (l, (t'', l'')))
1641                                     end
1642                          end
1643                       val res =
1644                          case (t, t') of
1645                             (Unknown r, Unknown r') =>
1646                                (case (!equality, !equality') of
1647                                    (Equality.True, Equality.False) =>
1648                                       notUnifiableBracket
1649                                       (simple (str "<equality>"),
1650                                        simple (str "<non-equality>"))
1651                                  | (Equality.False, Equality.True) =>
1652                                       notUnifiableBracket
1653                                       (simple (str "<non-equality>"),
1654                                        simple (str "<equality>"))
1655                                  | _ => Unified (Unknown (Unknown.join (r, r'))))
1656                           | (Unknown u, _) =>
1657                                oneUnknown (u, !equality, !time, outer, t', outer', false)
1658                           | (_, Unknown u') =>
1659                                oneUnknown (u', !equality', !time', outer', t, outer, true)
1660                           | (Con (c, ts), _) => conAnd (c, ts, t', t, false)
1661                           | (_, Con (c, ts)) => conAnd (c, ts, t, t', true)
1662                           | (FlexRecord f, Record r') =>
1663                                oneFlex (f, !equality, !time, outer, r', false)
1664                           | (Record r, FlexRecord f') =>
1665                                oneFlex (f', !equality', !time', outer', r, true)
1666                           | (FlexRecord {fields = fields, spine = spine},
1667                              FlexRecord {fields = fields', spine = spine'}) =>
1668                                let
1669                                   fun yes () =
1670                                      let
1671                                         val () = Spine.unify (spine, spine')
1672                                         val fields =
1673                                            List.fold
1674                                            (fields, fields', fn ((f, t), ac) =>
1675                                             if List.exists (fields', fn (f', _) =>
1676                                                             Field.equals (f, f'))
1677                                                then ac
1678                                                else (f, t) :: ac)
1679                                      in
1680                                         Unified (FlexRecord {fields = fields,
1681                                                              spine = spine})
1682                                      end
1683                                in
1684                                   unifyRecords
1685                                   (flexToFlexToRecord (fields, spine, !equality, !time, outer, spine'),
1686                                    flexToFlexToRecord (fields', spine', !equality', !time', outer', spine),
1687                                    yes, notUnifiable)
1688                                end
1689                           | (GenFlexRecord _, _) => genFlexError ()
1690                           | (_, GenFlexRecord _) => genFlexError ()
1691                           | (Overload ov1, Overload ov2) =>
1692                                if Overload.equals (ov1, ov2)
1693                                   then Unified t
1694                                else not ()
1695                           | (Record r, Record r') =>
1696                                (case (Srecord.detupleOpt r,
1697                                       Srecord.detupleOpt r') of
1698                                    (NONE, NONE) =>
1699                                       unifyRecords
1700                                       (rigidToRecord r, rigidToRecord r',
1701                                        fn () => Unified (Record r),
1702                                        notUnifiable)
1703                                  | (SOME ts, SOME ts') =>
1704                                       if Vector.length ts = Vector.length ts'
1705                                          then unifys
1706                                               (ts, ts',
1707                                                fn () => Unified (Record r),
1708                                                fn (ls, ls') =>
1709                                                notUnifiable
1710                                                (LayoutPretty.tuple ls,
1711                                                 LayoutPretty.tuple ls'))
1712                                          else not ()
1713                                  | _ => not ())
1714                           | (Var a, Var a') =>
1715                                if Tyvar.equals (a, a')
1716                                   then Unified t
1717                                   else not ()
1718                           | _ => not ()
1719                       val res =
1720                          case res of
1721                             NotUnifiable (l, l') =>
1722                                NotUnifiable (l, l')
1723                           | Unified ty =>
1724                                let
1725                                   val () = Set.union (s, s')
1726                                   val () = time := Time.min (!time, !time')
1727                                   val () = equality := Equality.join (!equality, !equality')
1728                                   val () =
1729                                      Set.:= (s, {equality = equality,
1730                                                  plist = plist,
1731                                                  time = time,
1732                                                  ty = ty})
1733                                in
1734                                   Unified ()
1735                                end
1736                    in
1737                       res
1738                    end) arg
1739             and unifyRecords ((fields: (Field.t * t) vector,
1740                                dots: bool),
1741                               (fields': (Field.t * t) vector,
1742                                dots': bool),
1743                               yes, no) =
1744                let
1745                   fun subset (fields, fields',
1746                               ac, dots, ac', dots',
1747                               skipBoth) =
1748                      Vector.fold
1749                      (fields, (ac, dots, ac', dots'),
1750                       fn ((f, t), (ac, dots, ac', dots')) =>
1751                       case Vector.peek (fields', fn (f', _) =>
1752                                         Field.equals (f, f')) of
1753                          NONE =>
1754                             ((f, true, dontCare) :: ac, dots, ac', dots')
1755                        | SOME (_, t') =>
1756                             if skipBoth
1757                                then (ac, dots, ac', dots')
1758                             else
1759                                case unify (t, t') of
1760                                   NotUnifiable (l, l') =>
1761                                      ((f, false, l) :: ac, dots,
1762                                       (f, false, l') :: ac', dots')
1763                                 | Unified _ => (ac, true, ac', true))
1764                   val (ac, dots, ac', dots') =
1765                      subset (fields, fields', [], dots, [], dots', false)
1766                   val (ac', dots', ac, dots) =
1767                      subset (fields', fields, ac', dots', ac, dots, true)
1768                in
1769                   case (ac, ac') of
1770                      ([], []) => yes ()
1771                    | _ => no (LayoutPretty.record (ac, dots),
1772                               LayoutPretty.record (ac', dots'))
1773                end
1774             val res = unify (t, t')
1775          in
1776             case res of
1777                NotUnifiable ((l, _), (l', _)) =>
1778                   let
1779                      val {times, tycons, tyvars} =
1780                         finishCheckTime ()
1781                      fun notes () =
1782                         if List.isEmpty tycons andalso List.isEmpty tyvars
1783                            then Layout.empty
1784                            else let
1785                                    fun doit (xs, lay) =
1786                                       List.insertionSort
1787                                       (List.map (xs, fn x => (x, lay x)),
1788                                        fn ((_, l1), (_, l2)) =>
1789                                        String.<= (Layout.toString l1,
1790                                                   Layout.toString l2))
1791                                    val tycons = doit (tycons, layoutPrettyTycon)
1792                                    val tyvars = doit (tyvars, layoutPrettyTyvar)
1793                                    val tys =
1794                                       List.map (tycons, #2)
1795                                       @ List.map (tyvars, #2)
1796                                 in
1797                                    Layout.align
1798                                    [seq [str "note: ",
1799                                          if List.length tys > 1
1800                                             then str "types would escape their scope: "
1801                                             else str "type would escape its scope: ",
1802                                          seq (Layout.separate (tys, ", "))],
1803                                     (Layout.align o List.map)
1804                                     (tycons, fn (c, _) =>
1805                                      seq [str "escape from: ",
1806                                           Region.layout (Tycon.region c)]),
1807                                     (Layout.align o List.map)
1808                                     (times, fn t =>
1809                                      seq [str "escape to: ",
1810                                           Region.layout (Time.region t)])]
1811                                 end
1812                   in
1813                      NotUnifiable (l, l',
1814                                    {notes = notes})
1815                   end
1816              | Unified () => Unified ()
1817          end
1818
1819       local
1820          val {get: Tycon.t -> (t * Tycon.t) option, set, ...} =
1821             Property.getSetOnce (Tycon.plist, Property.initConst NONE)
1822       in
1823          fun setSynonym (c, c') = set (c, SOME (con (c, Vector.new0 ()), c'))
1824          val synonym = get
1825       end
1826
1827       val () =
1828          List.foreach
1829          (CharSize.all, fn s =>
1830           setSynonym (Tycon.char s,
1831                       Tycon.word (WordSize.fromBits (CharSize.bits s))))
1832
1833       val () =
1834          List.foreach
1835          (IntSize.all, fn s =>
1836           setSynonym (Tycon.int s,
1837                       Tycon.word (WordSize.fromBits (IntSize.bits s))))
1838
1839       structure Overload =
1840          struct
1841             open Overload
1842
1843             val defaultType =
1844                fn Char => con (Tycon.defaultChar (), Vector.new0 ())
1845                 | Int => con (Tycon.defaultInt (), Vector.new0 ())
1846                 | Real => con (Tycon.defaultReal (), Vector.new0 ())
1847                 | Word => con (Tycon.defaultWord (), Vector.new0 ())
1848          end
1849
1850       fun 'a simpleHom {con: t * Tycon.t * 'a vector -> 'a,
1851                         expandOpaque: bool,
1852                         record: t * (Field.t * 'a) vector -> 'a,
1853                         replaceSynonyms: bool,
1854                         var: t * Tyvar.t -> 'a} =
1855          let
1856             val unit = con (unit, Tycon.tuple, Vector.new0 ())
1857             val unknown = unit
1858             fun sortFields (fields: (Field.t * 'a) list) =
1859                let
1860                   val a = Array.fromList fields
1861                   val () =
1862                      QuickSort.sortArray (a, fn ((f, _), (f', _)) =>
1863                                           Field.<= (f, f'))
1864                in
1865                   Array.toVector a
1866                end
1867             fun unsorted (t, fields: (Field.t * 'a) list) =
1868                let
1869                   val v = sortFields fields
1870                in
1871                   record (t, v)
1872                end
1873             fun genFlexRecord (t, {extra, fields, spine = _}) =
1874                unsorted (t,
1875                          List.fold
1876                          (extra (), fields, fn ({field, tyvar}, ac) =>
1877                           (field, var (Type.var tyvar, tyvar)) :: ac))
1878             fun flexRecord (t, {fields, spine}) =
1879                if Spine.canAddFields spine
1880                   then Error.bug "TypeEnv.Type.simpleHom: flexRecord"
1881                else unsorted (t,
1882                               Spine.foldOverNew
1883                               (spine, fields, fields, fn (f, ac) =>
1884                                (f, unit) :: ac))
1885             fun recursive _ = Error.bug "TypeEnv.Type.simpleHom.recursive"
1886             val con =
1887                if not replaceSynonyms
1888                   then con
1889                else
1890                   fn (t, c, ts) =>
1891                   let
1892                      val (t, c) =
1893                         case synonym c of
1894                            NONE => (t, c)
1895                          | SOME (t, c) => (t, c)
1896                   in
1897                      con (t, c, ts)
1898                   end
1899             fun overload (t', ov) =
1900                let
1901                   val t = Overload.defaultType ov
1902                   val _ = unify (t, t',
1903                                  {layoutPretty = fn _ =>
1904                                   Error.bug "TypeEnv.Type.simpleHom.overload: layoutPretty",
1905                                   layoutPrettyTycon = fn _ =>
1906                                   Error.bug "TypeEnv.Type.simpleHom.overload: layoutPrettyTycon",
1907                                   layoutPrettyTyvar = fn _ =>
1908                                   Error.bug "TypeEnv.Type.simpleHom.overload: layoutPrettyTyvar"})
1909                in
1910                   con (t, Overload.defaultTycon ov, Vector.new0 ())
1911                end
1912          in
1913             makeHom {con = con,
1914                      expandOpaque = expandOpaque,
1915                      flexRecord = flexRecord,
1916                      genFlexRecord = genFlexRecord,
1917                      guard = fn _ => NONE,
1918                      overload = overload,
1919                      record = fn (t, r) => record (t, Srecord.toVector r),
1920                      recursive = recursive,
1921                      unknown = fn _ => unknown,
1922                      var = var}
1923          end
1924    end
1925
1926 structure Scheme =
1927    struct
1928       datatype t =
1929          General of {bound: unit -> Tyvar.t vector,
1930                      canGeneralize: bool,
1931                      flexes: Type.genFlexRecord list,
1932                      tyvars: Tyvar.t vector,
1933                      ty: Type.t}
1934        | Mono of Type.t
1935
1936       val ty =
1937          fn General {ty, ...} => ty
1938           | Mono ty => ty
1939
1940       val dest =
1941          fn General {bound, ty, ...} => (bound (), ty)
1942           | Mono ty => (Vector.new0 (), ty)
1943
1944       val kind =
1945          fn General {bound, ...} => Kind.Arity (Vector.length (bound ()))
1946           | Mono _ => Kind.Arity 0
1947
1948       fun layout s =
1949          case s of
1950             Mono t => Type.layout t
1951           | General {canGeneralize, tyvars, ty, ...} =>
1952                Layout.record [("canGeneralize", Bool.layout canGeneralize),
1953                               ("tyvars", Vector.layout Tyvar.layout tyvars),
1954                               ("ty", Type.layout ty)]
1955
1956       fun make {canGeneralize, tyvars, ty} =
1957          if Vector.isEmpty tyvars
1958             then Mono ty
1959          else General {bound = fn () => tyvars,
1960                        canGeneralize = canGeneralize,
1961                        flexes = [],
1962                        tyvars = tyvars,
1963                        ty = ty}
1964
1965       val fromType = Mono
1966
1967       fun fromTycon (tycon: Tycon.t): t =
1968          let
1969             val kind = Tycon.kind tycon
1970             val arity =
1971                case kind of
1972                   Kind.Arity arity => arity
1973                 | Kind.Nary => Error.bug "TypeEnv.Scheme.fromTycon: Kind.Nary"
1974             val tyvars =
1975                Vector.tabulate
1976                (arity, fn _ =>
1977                 Tyvar.makeNoname {equality = false})
1978          in
1979             make
1980             {canGeneralize = true,
1981              ty = Type.con (tycon, Vector.map (tyvars, Type.var)),
1982              tyvars = tyvars}
1983          end
1984
1985       fun instantiateAux (t: t, subst) =
1986          case t of
1987             Mono ty => {args = fn () => Vector.new0 (),
1988                         instance = ty}
1989           | General {canGeneralize, flexes, tyvars, ty, ...} =>
1990                (case Type.deEta (ty, tyvars) of
1991                    SOME tycon =>
1992                       let
1993                          val types =
1994                             Vector.mapi
1995                             (tyvars, fn (i, a) =>
1996                              subst {canGeneralize = canGeneralize,
1997                                     equality = Tyvar.isEquality a,
1998                                     index = i})
1999                       in
2000                          {args = fn () => types,
2001                           instance = Type.con (tycon, types)}
2002                       end
2003                  | NONE =>
2004                let
2005                   open Type
2006                   val {destroy = destroyTyvarInst,
2007                        get = tyvarInst: Tyvar.t -> Type.t option,
2008                        set = setTyvarInst} =
2009                      Property.destGetSetOnce (Tyvar.plist,
2010                                               Property.initConst NONE)
2011                   val types =
2012                      Vector.mapi
2013                      (tyvars, fn (i, a) =>
2014                       let
2015                          val t = subst {canGeneralize = canGeneralize,
2016                                         equality = Tyvar.isEquality a,
2017                                         index = i}
2018                          val _ = setTyvarInst (a, SOME t)
2019                       in
2020                          t
2021                       end)
2022                   type z = {isNew: bool, ty: Type.t}
2023                   fun isNew {isNew = b, ty = _} = b
2024                   fun keep ty = {isNew = false, ty = ty}
2025                   fun con (ty, c, zs) =
2026                      if Vector.exists (zs, isNew)
2027                         then {isNew = true,
2028                               ty = Type.con (c, Vector.map (zs, #ty))}
2029                      else keep ty
2030                   val flexInsts = ref []
2031                   fun genFlexRecord (_, {extra = _, fields, spine}) =
2032                      let
2033                         val fields = List.revMap (fields, fn (f, t: z) =>
2034                                                   (f, #ty t))
2035                         val flex = newFlex {fields = fields,
2036                                             spine = spine}
2037                         val _ = List.push (flexInsts, {flex = flex,
2038                                                        spine = spine})
2039                      in
2040                         {isNew = true,
2041                          ty = flex}
2042                      end
2043                   fun record (t, r) =
2044                      if Srecord.exists (r, isNew)
2045                         then {isNew = true,
2046                               ty = Type.record (Srecord.map (r, #ty))}
2047                      else keep t
2048                   fun recursive _ =
2049                      (* If we get here, there has already been a type error
2050                       * in the user's program, so we return a new type to avoid
2051                       * compounding the error.
2052                       *)
2053                      {isNew = true,
2054                       ty = Type.new ()}
2055                   fun var (ty, a) =
2056                      case tyvarInst a of
2057                         NONE => {isNew = false, ty = ty}
2058                       | SOME ty => {isNew = true, ty = ty}
2059                   val {ty: Type.t, ...} =
2060                      Type.hom (ty, {con = con,
2061                                     expandOpaque = false,
2062                                     flexRecord = keep o #1,
2063                                     genFlexRecord = genFlexRecord,
2064                                     guard = fn _ => NONE,
2065                                     overload = keep o #1,
2066                                     record = record,
2067                                     recursive = recursive,
2068                                     unknown = keep o #1,
2069                                     var = var})
2070                   val _ = destroyTyvarInst ()
2071                   val flexInsts = !flexInsts
2072                   fun args (): Type.t vector =
2073                      Vector.fromList
2074                      (List.fold
2075                       (flexes, Vector.toList types,
2076                        fn ({fields, spine, ...}, ac) =>
2077                        let
2078                           fun done peek =
2079                              Spine.foldOverNew
2080                              (spine, fields, ac, fn (f, ac) =>
2081                               (case peek f of
2082                                   NONE => Type.unit
2083                                 | SOME t => t) :: ac)
2084                        in
2085                           case List.peek (flexInsts,
2086                                           fn {spine = spine', ...} =>
2087                                           Spine.equals (spine, spine')) of
2088                              NONE => done (fn _ => NONE)
2089                            | SOME {flex, ...} =>
2090                                 let
2091                                    fun peekFields (fields, f) =
2092                                       Option.map
2093                                       (List.peek (fields, fn (f', _) =>
2094                                                   Field.equals (f, f')),
2095                                        #2)
2096                                 in
2097                                    done
2098                                    (case Type.getTy flex of
2099                                       FlexRecord {fields, ...} =>
2100                                          (fn f => peekFields (fields, f))
2101                                     | GenFlexRecord {extra, fields, ...} =>
2102                                          (fn f =>
2103                                           case peekFields (fields, f) of
2104                                              NONE =>
2105                                                 Option.map
2106                                                 (List.peek
2107                                                  (extra (),
2108                                                   fn {field, ...} =>
2109                                                   Field.equals (f, field)),
2110                                                  Type.var o #tyvar)
2111                                            | SOME t => SOME t)
2112                                     | Record r =>
2113                                          (fn f => Srecord.peek (r, f))
2114                                     | _ => Error.bug "TypeEnv.instantiate': General:strange flexInst")
2115                                 end
2116                        end))
2117                in
2118                   {args = args,
2119                    instance = ty}
2120                end)
2121
2122       fun apply (s, ts) =
2123          #instance (instantiateAux (s, fn {index, ...} => Vector.sub (ts, index)))
2124
2125       fun instantiate s =
2126          instantiateAux
2127          (s, fn {canGeneralize, equality, ...} =>
2128           Type.unknown {canGeneralize = canGeneralize,
2129                         equality = if equality
2130                                       then Equality.True
2131                                       else Equality.Unknown,
2132                         time = Time.now ()})
2133
2134       val instantiate =
2135          Trace.trace ("TypeEnv.Scheme.instantiate", layout, Type.layout o #instance)
2136          instantiate
2137
2138       fun fresh s =
2139          let
2140             val (tyvars, _) = dest s
2141             val tyvars = Vector.map (tyvars, Tyvar.makeLike)
2142          in
2143             (tyvars, apply (s, (Vector.map (tyvars, Type.var))))
2144          end
2145
2146       fun freshEq s =
2147          let
2148             val (tyvars, _) = dest s
2149             val tyvars = Vector.map (tyvars, fn _ => Tyvar.makeNoname {equality = true})
2150          in
2151             (tyvars, apply (s, (Vector.map (tyvars, Type.var))))
2152          end
2153
2154       fun admitsEquality s =
2155          let
2156             val (_, ty) = freshEq s
2157          in
2158             case !(Type.equality ty) of
2159                Equality.False => false
2160              | Equality.True => true
2161              | Equality.Unknown => Error.bug "TypeEnv.Scheme.admitsEquality: Unknown"
2162          end
2163
2164       val admitsEquality =
2165          Trace.trace ("TypeEnv.Scheme.admitsEquality", layout, Bool.layout)
2166          admitsEquality
2167
2168       fun checkEquality (s, {layoutPrettyTycon}) =
2169          let
2170             fun layoutPrettyTyvar _ =
2171                Error.bug "TypeEnv.Scheme.checkEquality.layoutPrettyTyvar"
2172             val (_, ty) = freshEq s
2173          in
2174             Option.map
2175             (Type.checkEquality
2176              (ty, {layoutPrettyTycon = layoutPrettyTycon,
2177                    layoutPrettyTyvar = layoutPrettyTyvar}),
2178              fn ((l, _), _) => l)
2179          end
2180
2181       fun haveUnknowns s: bool =
2182          let
2183             fun con (_, _, bs) = Vector.exists (bs, fn b => b)
2184             fun no _ = false
2185             val {destroy, hom} =
2186                Type.makeHom
2187                {con = con,
2188                 expandOpaque = false,
2189                 flexRecord = fn (_, {fields, ...}) => List.exists (fields, #2),
2190                 genFlexRecord = (fn (_, {fields, ...}) =>
2191                                  List.exists (fields, #2)),
2192                 guard = fn _ => NONE,
2193                 overload = no,
2194                 record = fn (_, r) => Srecord.exists (r, fn b => b),
2195                 recursive = no,
2196                 unknown = fn _ => true,
2197                 var = no}
2198             val res = hom (ty s)
2199             val _ = destroy ()
2200          in
2201             res
2202          end
2203    end
2204
2205 fun 'a close region =
2206    let
2207       val beforeGen = Time.now ()
2208       val () = Time.tick region
2209    in
2210       fn (ensure,
2211           varTypes,
2212           {error: 'a * Layout.t * Tyvar.t list -> unit,
2213            layoutPrettyTycon,
2214            layoutPrettyTyvar}) =>
2215       let
2216          local
2217             fun checkTime (t, bound) =
2218                let
2219                   val {checkTime, finishCheckTime} =
2220                      Type.makeCheckTime {layoutPrettyTycon = layoutPrettyTycon,
2221                                          layoutPrettyTyvar = layoutPrettyTyvar}
2222                in
2223                   Option.map (checkTime (t, bound), fn z =>
2224                               (z, finishCheckTime ()))
2225                end
2226          in
2227             val varTypes =
2228                Vector.map
2229                (varTypes, fn ({isExpansive, ty, var}) =>
2230                 if not isExpansive
2231                    then {isExpansive = false,
2232                          ty = ty}
2233                    else (case checkTime (ty, beforeGen) of
2234                             NONE => {isExpansive = true,
2235                                      ty = ty}
2236                           | SOME (((l, _), _), {tyvars, ...}) =>
2237                                (error (var, l, tyvars)
2238                                 ; {isExpansive = false,
2239                                    ty = ty})))
2240          end
2241          val tyvars = Vector.toList ensure
2242          (* Convert all the unknown types bound at this level into tyvars.
2243           * Convert all the FlexRecords bound at this level into
2244           * GenFlexRecords.
2245           *)
2246          val (flexes, tyvars) =
2247             if Vector.forall
2248                (varTypes, fn {ty, ...} =>
2249                 Time.<= (!(Type.time ty), beforeGen))
2250                then ([], tyvars)
2251                else let
2252                        val flexes = ref []
2253                        val tyvars = ref tyvars
2254                        fun flexRecord (t, _) =
2255                           let
2256                              val (fields, spine) =
2257                                 case Type.getTy t of
2258                                    Type.FlexRecord {fields, spine} =>
2259                                       (fields, spine)
2260                                  | _ => Error.bug "TypeEnv.close.flexRecord: not FlexRecord"
2261                              fun newField f =
2262                                 {field = f,
2263                                  tyvar = Tyvar.makeNoname {equality = false}}
2264                              val extra =
2265                                 let
2266                                    val all = ref []
2267                                    val fields =
2268                                       List.map (fields, fn (f, _) => (f, ()))
2269                                 in
2270                                    fn () =>
2271                                    let
2272                                       val old = !all
2273                                       val fields =
2274                                          List.fold
2275                                          (old, fields, fn ({field, ...}, ac) =>
2276                                           (field, ()) :: ac)
2277                                       val new =
2278                                          Spine.foldOverNew
2279                                          (spine, fields, old, fn (f, ac) =>
2280                                           (newField f) :: ac)
2281                                       val () = all := new
2282                                    in
2283                                       new
2284                                    end
2285                                 end
2286                              val gfr = {extra = extra,
2287                                         fields = fields,
2288                                         spine = spine}
2289                              val _ = List.push (flexes, gfr)
2290                           in
2291                              Type.setTy
2292                              (t, Type.GenFlexRecord gfr)
2293                           end
2294                        fun unknown (t, Unknown.T {canGeneralize, ...}) =
2295                           if not canGeneralize
2296                              then ()
2297                              else let
2298                                      val equality = Type.equality t
2299                                      val a =
2300                                         Tyvar.makeNoname
2301                                         {equality =
2302                                          case !equality of
2303                                             Equality.False => false
2304                                           | Equality.True => true
2305                                           | Equality.Unknown =>
2306                                                (equality := Equality.False
2307                                                 ; false)}
2308                                      val _ = List.push (tyvars, a)
2309                                   in
2310                                      Type.setTy
2311                                      (t, Type.Var a)
2312                                   end
2313                        fun guard t =
2314                           if Time.<= (!(Type.time t), beforeGen)
2315                              then SOME ()
2316                              else NONE
2317                        val {destroy, hom} =
2318                           Type.makeHom
2319                           {con = fn _ => (),
2320                            expandOpaque = false,
2321                            flexRecord = flexRecord,
2322                            genFlexRecord = fn _ => (),
2323                            guard = guard,
2324                            overload = fn _ => (),
2325                            record = fn _ => (),
2326                            recursive = fn _ => (),
2327                            unknown = unknown,
2328                            var = fn _ => ()}
2329                        val _ = Vector.foreach (varTypes, hom o #ty)
2330                        val _ = destroy ()
2331                     in
2332                        (!flexes, !tyvars)
2333                     end
2334          (* For all fields that were added to the generalized flex records,
2335           * add a type variable.
2336           *)
2337          fun bound () =
2338             Vector.fromList
2339             (List.fold
2340              (flexes, tyvars, fn ({extra, fields, spine}, ac) =>
2341               let
2342                  val extra = extra ()
2343               in
2344                  Spine.foldOverNew
2345                  (spine, fields, ac, fn (f, ac) =>
2346                   case List.peek (extra, fn {field, ...} =>
2347                                   Field.equals (f, field)) of
2348                      NONE => Error.bug "TypeEnv.close.bound: GenFlex missing field"
2349                    | SOME {tyvar, ...} => tyvar :: ac)
2350               end))
2351          val schemes =
2352             Vector.map
2353             (varTypes, fn {isExpansive, ty} =>
2354              if isExpansive
2355                 then Scheme.Mono ty
2356              else Scheme.General {bound = bound,
2357                                   canGeneralize = true,
2358                                   flexes = flexes,
2359                                   tyvars = Vector.fromList tyvars,
2360                                   ty = ty})
2361       in
2362          {bound = bound,
2363           schemes = schemes}
2364       end
2365    end
2366
2367 structure Type =
2368    struct
2369       open Type
2370
2371       fun homConVar {con, expandOpaque, var} =
2372          let
2373             fun tuple (t, ts) =
2374                if 1 = Vector.length ts
2375                   then Vector.first ts
2376                else con (t, Tycon.tuple, ts)
2377          in
2378             simpleHom {con = con,
2379                        expandOpaque = expandOpaque,
2380                        record = fn (t, fs) => tuple (t, Vector.map (fs, #2)),
2381                        replaceSynonyms = true,
2382                        var = var}
2383          end
2384
2385       fun makeHom {con, expandOpaque, var} =
2386          homConVar {con = fn (_, c, ts) => con (c, ts),
2387                     expandOpaque = expandOpaque,
2388                     var = fn (_, a) => var a}
2389
2390       fun deRecord t =
2391          let
2392             val {hom, destroy} =
2393                simpleHom
2394                {con = fn (t, _, _) => (t, NONE),
2395                 expandOpaque = false,
2396                 record = fn (t, fs) => (t,
2397                                         SOME (Vector.map (fs, fn (f, (t, _)) =>
2398                                                           (f, t)))),
2399                 replaceSynonyms = true,
2400                 var = fn (t, _) => (t, NONE)}
2401             val res =
2402                case #2 (hom t) of
2403                   NONE => Error.bug "TypeEnv.Type.deRecord"
2404                 | SOME fs => fs
2405             val _ = destroy ()
2406          in
2407             res
2408          end
2409
2410       fun deTupleOpt t =
2411          let
2412             val {destroy, hom} =
2413                homConVar
2414                {con = fn (t, c, ts) => (t,
2415                                         if Tycon.equals (c, Tycon.tuple)
2416                                            then SOME (Vector.map (ts, #1))
2417                                         else NONE),
2418                 expandOpaque = false,
2419                 var = fn (t, _) => (t, NONE)}
2420             val res = #2 (hom t)
2421             val _ = destroy ()
2422          in
2423             res
2424          end
2425
2426       val deTupleOpt =
2427          Trace.trace ("TypeEnv.Type.deTupleOpt", layout,
2428                       Option.layout (Vector.layout layout))
2429          deTupleOpt
2430
2431       fun hom (t, {con, expandOpaque = e, record, replaceSynonyms = r,
2432                    var}) =
2433          let
2434             val {hom, destroy} =
2435                simpleHom {con = fn (_, c, v) => con (c, v),
2436                           expandOpaque = e,
2437                           record = fn (_, fs) => record (Srecord.fromVector fs),
2438                           replaceSynonyms = r,
2439                           var = fn (_, a) => var a}
2440             val res = hom t
2441             val _ = destroy ()
2442          in
2443             res
2444          end
2445
2446       fun copy t =
2447          hom (t, {con = Type.con,
2448                   expandOpaque = false,
2449                   record = Type.record,
2450                   replaceSynonyms = false,
2451                   var = Type.var})
2452
2453       val unify =
2454          fn (t1, t2, {error, layoutPretty, layoutPrettyTycon, layoutPrettyTyvar}) =>
2455          case unify (t1, t2, {layoutPretty = layoutPretty,
2456                               layoutPrettyTycon = layoutPrettyTycon,
2457                               layoutPrettyTyvar = layoutPrettyTyvar}) of
2458             NotUnifiable (l1, l2, extra) => error (l1, l2, extra)
2459           | Unified () => ()
2460
2461       val checkTime =
2462          fn (t, bound, {layoutPrettyTycon, layoutPrettyTyvar}) =>
2463          let
2464             val {checkTime, finishCheckTime} =
2465                makeCheckTime {layoutPrettyTycon = layoutPrettyTycon,
2466                               layoutPrettyTyvar = layoutPrettyTyvar}
2467          in
2468             Option.map
2469             (checkTime (t, bound), fn ((l, _), (ty, _)) =>
2470              (l, ty, let val {tycons, tyvars, ...} = finishCheckTime ()
2471                      in {tycons = tycons, tyvars = tyvars}
2472                      end))
2473          end
2474    end
2475
2476 end