SpadTypeTree.spad

)abbrev domain STRULE SpadTypeRule
SpadTypeRule() : Exports == Implementation where
)include SpadTypeDefs.inc

  Exports ==> CoercibleTo(PF) with
    construct : (List(N), N) -> %

    elt : (%, "formulas") -> List(N)
    elt : (%, "solution") -> N

    references : % -> List(NR)
    references : List(%) -> List(NR)

  Implementation ==> add
    import Logger('Rule)

    Rep := Record(m_formulas : List(N), m_solution : N)

    construct (fs, s) == [fs, s]$Rep

    elt (x, "formulas") == x.m_formulas
    elt (x, "solution") == x.m_solution

    references (x : %) : List(NR) ==
      [(f :: NR) for f in x.m_formulas | nodeRef? f]

    references (lx : List(%)) : List(NR) ==
      empty? lx => []
      -- PARSER BUG? Parens are required around reduce expression.
      removeDuplicates("concat"/[references x for x in lx])

    coerce x ==
      pfs : List(PF) := []

      for f in x.m_formulas repeat
        pf :=
          condExpr? f =>
            ce := f :: CE
            spaces(["if" :: PF, ce.cond :: PF,
                    "then" :: PF, ce.truebr :: PF,
                    "else" :: PF, ce.falsebr :: PF])
          aggregate? f =>
            paren sepBy("; " :: PF, [n :: PF for n in f :: List(N)])
          f :: PF
        pfs := [pf, :pfs]

      brace reverse pfs

)abbrev domain STNODE SpadTypeNode
SpadTypeNode() : Exports == Implementation where
)include SpadTypeDefs.inc

  Exports ==> CoercibleTo(PF) with
    construct : (PI, PI, N) -> %

    elt : (%, "index") -> NR
    elt : (%, "node") -> N
    elt : (%, "rules") -> List(TR)
    elt : (%, "type") -> N
    elt : (%, "env") -> ENV

    setelt! : (%, "rules", List(TR)) -> List(TR)
    setelt! : (%, "type", N) -> N
    setelt! : (%, "node", N) -> N
    setelt! : (%, "env", ENV) -> ENV

    pending? : % -> Boolean
    done? : % -> Boolean
    done! : % -> %
    killed? : % -> Boolean
    kill! : % -> %
    poisoned? : % -> Boolean
    poison! : % -> %

    references : % -> List(NR)

    nodeRef : % -> N
    typeRef : % -> N

  Implementation ==> add
    import SpadNode
    import Printer
    import SpadTypeUnifier
    import SpadNodeFactory
    import SpadNodeTools

    Rep := Record(m_index : NR,
                  m_node : N,
                  m_rules : List(TR),
                  m_type : N,
                  m_env : ENV,
                  m_state : Union("finished", "pending", "poisoned", "killed"))

    construct (i, j, n) ==
      [[i, j]$NR, n, [], null, new(), "pending"]$Rep

    elt (x, "index") == x.m_index
    elt (x, "node") == x.m_node
    elt (x, "rules") == x.m_rules
    elt (x, "type") == x.m_type
    elt (x, "env") == x.m_env

    setelt! (x, "node", n) ==
      x.m_node := n
    setelt! (x, "rules", r) ==
      x.m_rules := r
    setelt! (x, "type", ts) ==
      x.m_type := ts
    setelt! (x, "env", env) ==
      x.m_env := env

    pending? x == x.m_state case "pending"
    done? x == x.m_state case "finished"
    done! x == (x.m_state := "finished"; x)
    killed? x == x.m_state case "killed"
    kill! x == (x.m_state := "killed"; x)
    poisoned? x == x.m_state case "poisoned"
    poison! x == (x.m_state := "poisoned"; x)

    references x ==
      references x.m_rules

    nodeRef x ==
      nodeNodeRef(x.m_index.major :: PI, x.m_index.minor :: PI)

    typeRef x ==
      nodeTypeVar(x.m_index.major :: PI, x.m_index.minor :: PI)

    onelineOf (n : N) : PF ==
      condExpr? n =>
        c := n :: CE
        fs : List(PF) :=
          ["if" :: PF, c.cond :: PF, "then" :: PF, c.truebr :: PF]
        if not null? c.falsebr then
          fs := [:fs, "else" :: PF, c.falsebr :: PF]
        spaces fs
      function? n =>
        f := n :: FN
        f.name case Symbol =>
          fargs := [arg :: PF for arg in f.args]
          rtype : List(PF) :=
            null? f.type => []
            [":" :: PF, f.type :: PF]
          spaces([f.name :: Symbol :: PF, paren fargs, :rtype,
                  "==" :: PF, f.body :: PF])
        n :: PF
      functor? n =>
        ft := n :: FT
        spaces([ft.name :: PF, paren [arg :: PF for arg in ft.args],
                ":" :: PF, ft.type :: PF, "==" :: PF, ft.extends :: PF,
                "add" :: PF, ft.capsule :: PF])

      loop? n =>
        lp := n :: LP
        il := [i :: PF for i in lp.itors]
        gl := [spaces ["if" :: PF, g :: PF] for g in lp.guards]
        loopBody := lp.body :: PF
        lp.kind case "loop" =>
          loopExpr : List(PF) :=
            if empty? il then
              loopCond := sepBy(" and " :: PF, [g :: PF for g in lp.guards])
              ["while" :: PF, loopCond]
            else
              [:il, :gl]
          spaces [:loopExpr, "repeat" :: PF, loopBody]
        lp.kind case "collect" =>
          bracket spaces [loopBody, :concat(il, gl)]
        lp.kind case "repeat" =>
          spaces ["repeat" :: PF, loopBody]
      aggregate? n =>
        ns := [i :: PF for i in n :: List(N)]
        #ns > 1 => paren sepBy(", " :: PF, ns)
        first ns
      n :: PF

    coerce x ==
      state : PF :=
        x.m_state case "finished" => green(" (+)" :: PF)
        x.m_state case "pending" => red(" (-)" :: PF)
        x.m_state case "poisoned" => bold yellow(" (x)" :: PF)
        white(" (_)" :: PF)
      prefix := hconcat [right(6, x.m_index:: PF), state]
      t := bold (x.m_type :: PF)
      if typeVar? x.m_type then
        t := red t
      if null? x.m_type then
        t := bold yellow("%none" :: PF)
      t := indent(11, t)
      not empty? x.m_rules =>
        rs := sepBy(" | " :: PF, [onelineOf rule.solution for rule in x.m_rules])
        spaces([prefix, bold cyan(rs), "is" :: PF, t])
      n := stripOrigin x.m_node
      aggregate? n =>
        pile([spaces [prefix, bold blue(nodeRef(x) :: PF), "is" :: PF], t])
      recordType? n or unionType? n or mappingType? n =>
        spaces [prefix, blue(n :: PF)]
      pn :=
        apply? n or typeDecl? n or symbol? n or import? n =>
          -- leaves that influence environment contents
          magenta(n :: PF)
        case? n or typeIs? n or typeHas? n or value? n =>
          -- leaves that yield a value
          blue(n :: PF)
        typeVar? n => 
          bold cyan(n :: PF)
        nodeRef? n =>
          bold blue(n :: PF)
        bold yellow(onelineOf(n))
      spaces [prefix, pn, ":" :: PF, t]

)abbrev category STTCAT SpadTypeTreeCategory
SpadTypeTreeCategory() : Category == Definition where
)include SpadTypeDefs.inc

  Definition ==> CoercibleTo(PF) with
    registerNode! : (%, TN) -> Void
    unregisterNode! : (%, TN, N) -> Void

)abbrev package STNARR SpadTypeNodeArray
SpadTypeNodeArray(TT : SpadTypeTreeCategory) : Exports == Implementation where
)include SpadTypeDefs.inc

  Exports ==> CoercibleTo(PF) with
    construct : (TT, PI) -> %

    root : % -> TN
    node : (%, PI) -> TN
    members : % -> List(TN)
    addNode! : (%, N) -> TN
    addNode! : (%, N, ENV) -> TN
    poisonNode! : (%, TN) -> Void
    bindNode! : (%, TN, N) -> Void
    killNode! : (%, TN) -> Void
    rewriteNodes! : (%, TV, N) -> Void

    listTypeVars : % -> List(TV)
    listPostOrder : % -> List(TN)

  Implementation ==> add
    Rep := Record(m_tree : TT,
                  m_major : PI,
                  m_nodes : FlexibleArray(TN))

    import SpadNode
    import SpadNodeFactory
    import SpadNodeTools
    import SpadTypeUnifier
    import Printer
    import Logger('TNArray)

    construct (tree, major) ==
      [tree, major, [[]]]

    root x ==
      x.m_nodes.1

    node (x, i) ==
      x.m_nodes.i

    members x ==
      members x.m_nodes

    addNode! (x, n, env) ==
      tn := addNode!(x, n)
      tn.env := env
      tn

    addNode! (x, n) ==
      i := (#(x.m_nodes) + 1) :: PI
      tn := [x.m_major, i, n]
      tn.type := typeVar(x.m_major, i)
      concat!(x.m_nodes, tn)
      registerNode!(x.m_tree, tn)
      tn

    poisonNode! (x : %, tn : TN) ==
      info ["Poisoning" :: PF, tn.index :: PF, "node!" :: PF]
      -- leave node's type as is for error reporting
      poison! tn

    bindNode! (x : %, tn : TN, t : N) ==
      info ["Binding" :: PF, tn.index :: PF, "node type to" :: PF, t :: PF]
      if typeVar? tn.type then
        unregisterNode!(x.m_tree, tn, t)
      else
        tn.type := t

    killNode! (x : %, tn : TN) ==
      info ["Killing" :: PF, tn.index :: PF, "node!" :: PF]
      if typeVar? tn.type then
        unregisterNode!(x.m_tree, tn, undefinedType)
      else
        tn.type := undefinedType
      kill! tn

    needsRewrite? : (TN, TV) -> Boolean
    needsRewrite? (tn, tv) ==
      occurs?(tv, tn.type) or (typeDecl? tn.node and occurs?(tv, tn.node))

    -- rewrite all nodes with type that contains given variable
    rewriteNodes! (x, tv, term) ==
      for n in entries x.m_nodes | needsRewrite?(n, tv) repeat
        n.type := substitute(n.type, tv, term)
        if typeDecl? n.node then
          n.node := substitute(n.node, tv, term)
        debug (["Rewrote" :: PF, n.index :: PF, "with" :: PF,
                brace spaces [tv :: PF, "=>" :: PF, term :: PF]])

    listTypeVars x ==
      [n.type :: TV for n in entries x.m_nodes | typeVar? n.type]

    walkPostOrder(x : %, tn : TN) : List(TN) ==
      lst : List(List(TN)) := [[tn]]
      for nr in reverse references(tn) repeat
        if nr.major = tn.index.major then
          lst := [walkPostOrder(x, (x.m_nodes)(nr.minor)), :lst]
      "concat"/lst

    listPostOrder x ==
      walkPostOrder(x, x.m_nodes.1)

    coerce (x : %) : PF ==
      indent(2, vconcat [n :: PF for n in members x.m_nodes | not killed? n])

)abbrev package STTREE SpadTypeTree
SpadTypeTree() : Exports == Implementation where
  CTX ==> %
  TVS ==> List(Record(key : TV, entry : List(N)))

)include SpadTypeDefs.inc

  Exports ==> SpadTypeTreeCategory with
    construct : () -> %

    coerce : % -> N

    root : % -> TNA
    members : % -> List(TNA)
    listPostOrder : (%, PI) -> List(TN)

    node : (%, PI) -> TN
    node : (%, PI, PI) -> TN
    node : (%, NR) -> TN
    addNode! : (%, N) -> TN
    addNode! : (%, N, ENV) -> TN
    hasUnknownType? : (%, TN) -> Boolean
    hasUndefinedType? : (%, TN) -> Boolean
    typeOf : (%, TN) -> List(N)
    extendTypeOf! : (%, TN, List(N)) -> Void
    setTypeOf! : (%, TN, List(N)) -> Boolean

    addSubTree! : % -> Void
    leaveSubTree! : % -> Void

    poisonNode! : (%, TN) -> Void
    bindNode! : (%, TN, N) -> Void
    killNode! : (%, TN) -> Void

    limitTypeVar! : (%, TV, List(N)) -> Boolean
    limitTypeVar! : (%, SUBS) -> Boolean
    limitNodeType! : (%, TN, List(N)) -> Boolean

    nodeSubType! : (%, TN, TN) -> Boolean
    nodeSubTypeOf! : (%, TN, List(N)) -> Boolean
    nodesTypeMatch! : (%, TN, TN) -> Boolean 

    rewriteIfInferred! : (%, TN) -> Boolean

  Implementation ==> add
    import SpadNode
    import SpadNodeFactory
    import SpadNodeTools
    import SpadTypeUnifier
    import SpadTypeNode
    import SpadTypeNodeArray(%)
    import Printer
    import Logger('TTree)
    import Stack(TNA)

    rewriteTypeVars! : (%, TV, N) -> Void
    removeAlias! : (%, TV, N) -> Void
    rewriteNodes! : (%, TV, N) -> Void

    Rep := Record(m_nodes : FlexibleArray(TNA),
                  m_current : Stack(TNA),
                  m_typevars : AssociationList(TV, List(N)))

    construct () ==
      [flexibleArray [], [[]], [[]]]

    coerce (x : %) : N ==
      root(root(x)).node

    root x ==
      x.m_nodes.1

    members x ==
      members x.m_nodes

    node (x : %, i : PI) : TN ==
      node(top x.m_current, i)

    node (x : %, i : PI, j : PI) : TN ==
      node((x.m_nodes)(i), j)

    node (x : %, nr : NR) : TN ==
      node((x.m_nodes)(nr.major), nr.minor :: PI)

    listPostOrder (x : %, i : PI) : List(TN) ==
      listPostOrder (x.m_nodes.i)

    unknownType? (terms : List(N)) : Boolean ==
      #terms = 1 and null?(first terms)

    undefinedType? (terms : List(N)) : Boolean ==
      #terms = 1 and undefinedType?(first terms)

    poisonType? (terms : List(N)) : Boolean ==
      #terms = 1 and undefinedType?(first terms)

    aliasType? (terms : List(N)) : Boolean ==
      #terms = 1 and typeVar?(first terms)

    addNode! (x : %, n : N) : TN ==
      addNode! (top x.m_current, n)

    addNode! (x : %, n : N, env : ENV) : TN ==
      addNode! (top x.m_current, n, env)

    poisonNode! (x : %, tn : TN) ==
      poisonNode!((x.m_nodes)(tn.index.major), tn)

    bindNode! (x : %, tn : TN, n : N) ==
      bindNode!((x.m_nodes)(tn.index.major), tn, n)

    killNode! (x : %, tn : TN) ==
      killNode!((x.m_nodes)(tn.index.major), tn)

    registerNode! (x : %, tn : TN) : Void ==
      (x.m_typevars)(tn.type :: TV) := [null]

    unregisterNode! (x : %, tn : TN, final : N) : Void ==
      tv := tn.type :: TV
      rewriteTypeVars! (x, tv, final)
      rewriteNodes!(x, tv, final)
      remove!(tv, x.m_typevars)

    -- checks if type attached to the node has form "%a[?]"
    hasUnknownType? (x : %, tn : TN) : Boolean ==
      not typeVar? tn.type => false
      unknownType? (x.m_typevars)(tn.type :: TV)

    hasUndefinedType? (x : %, tn : TN) : Boolean ==
      not typeVar? tn.type =>
        tn.type = undefinedType
      undefinedType? (x.m_typevars)(tn.type :: TV)

    typeOf (x : %, n : TN) : List(N) ==
      not typeVar? n.type => [n.type] 
      tl := (x.m_typevars)(n.type :: TV)
      unknownType? tl => [n.type]
      tl

    extendTypeOf! (x : %, tn : TN, terms : List(N)) : Void ==
      if typeVar? tn.type then
        tv := tn.type :: TV
        unknownType? (x.m_typevars)(tv) =>
          (x.m_typevars)(tv) := terms
        (x.m_typevars)(tv) := removeDuplicates concat((x.m_typevars)(tv), terms)

    setTypeOf! (x : %, tn : TN, terms : List(N)) : Boolean ==
      typeVar? tn.type =>
        (x.m_typevars)(tn.type :: TV) := terms
        true
      #terms ~= 1 or isSubType(terms.1, tn.type) case "false" =>
        warn ["Cannot set the type of" :: PF, tn.index :: PF, "node!" :: PF]
        warn pile(
          ["Types not equal:" :: PF,
           bold red("old:" :: PF),
           indent(2, tn.type :: PF),
           bold red("new:" :: PF), 
           indent(2, vconcat [t :: PF for t in terms])])
        false
      tn.type := terms.1
      true

    addSubTree! x ==
      subtree := [x, (#(x.m_nodes) + 1) :: PI]
      concat!(x.m_nodes, subtree)
      push!(subtree, x.m_current)

    leaveSubTree! x ==
      pop!(x.m_current)
      void()

    rewriteTypeVars! (x : %, var : TV, term : N) : Void ==
      debug(["Rewriting" :: PF, bold(var :: PF), "to" :: PF, bold(term :: PF),
             "in all type variables." :: PF])
      for tv in members(x.m_typevars)@TVS repeat
        unknownType? tv.entry => "iterate"
        poisonType? tv.entry => "iterate"
        ts : List(N) := []
        for t in tv.entry repeat
          t := substitute(t, var, term)
          -- Remove duplicates.
          member?(t, ts) => "iterate"
          -- Avoid ill-formed types (for now only unions).
          null? t => "iterate"
          ts := [t, :ts]
        tv.entry := reverse ts

    -- rewrite all nodes with type that contains given variable
    rewriteNodes! (x : %, var : TV, term : N) : Void ==
      for tna in members x.m_nodes repeat
        rewriteNodes!(tna, var, term)

    rewriteIfInferred! (x : %, n : TN) : Boolean ==
      not typeVar? n.type => false
      tv := n.type :: TV
      terms := (x.m_typevars)(tv)
      #terms ~= 1 => false
      unknownType? terms => false
      term := first terms
      typeVar? term =>
        removeAlias!(x, tv, term)
        true
      unbound? term => false
      rewriteTypeVars!(x, tv, term)
      debug ["Removing" :: PF, bold(tv :: PF), "type variable." :: PF]
      remove!(tv, x.m_typevars)
      info (["Type inferred for node" :: PF, n.index :: PF,
             ":" :: PF, bold(term :: PF)])
      rewriteNodes!(x, tv, term)
      true

    removeAlias! (x : %, tv : TV, alias : N) : Void ==
      tv = (alias :: TV) => void() -- BUG? Handle degenerate case!
      debug ["Removing alias:" :: PF, tv :: PF, "=>" :: PF, alias :: PF]
      rewriteTypeVars!(x, tv, alias)
      rewriteNodes!(x, tv, alias)
      remove!(tv, x.m_typevars)

    limitTypeVar! (x : %, tv : TV, terms : List(N)) : Boolean ==
      debug(["Modyfing" :: PF, bold(tv :: PF), "type variable with" :: PF,
             bracket [bold(t :: PF) for t in terms]])
      -- 1) typevars(%x) = [?]
      ts := (x.m_typevars)(tv)
      unknownType? ts =>
        -- a) %x = %y => alias removal
        -- b) %x = [t1, t2, t3, ...]
        if aliasType? terms
          then removeAlias!(x, tv, first terms)
          else (x.m_typevars)(tv) := terms
        true
      -- 2) typevars(%x) = [s1, s2, s3, ...], %x = [t1, t2, t3, ...]
      -- Unify proposed values with already stored in the variable
      -- store only matching ones (without performing substitutions).
      ms := findMatches(ts, terms)
      not empty? ms.terms =>
        (x.m_typevars)(tv) := ms.terms
        true
      -- 3) no matching types? let's check if we tried to replace
      --    supertype with subtype.
      for t in ts repeat
        for s in terms repeat
          not isSubType(s, t) case "false" => return true
      -- 4) we could've tried to replace subtype with supertype.
      sl : List(N) := []
      for t in ts repeat
        for s in terms repeat
          isSubType(t, s) case "false" => "iterate"
          sl := [s, :sl]
      empty? sl => false
      (x.m_typevars)(tv) := sl
      true

    limitTypeVar! (x : %, subs : SUBS) : Boolean ==
      empty? subs => true
      "and"/[limitTypeVar!(x, s.key, s.entry) for s in entries subs]

    flattenTypeOf (x : %, tn : TN) : List(N) ==
      visited : Set(TV) := empty()
      queue : Queue(N) := [typeOf(x, tn)]
      types : List(N) := []

      while not empty? queue repeat
        t := dequeue! queue
        typeVar? t =>
          member?(t :: TV, visited) => "iterate"
          types := concat(types, (x.m_typevars)(t :: TV))
        types := concat(types, t)

      removeDuplicates types

    nodesTypeMatch! (x : %, ln : TN, rn : TN) : Boolean ==
      info(["Types of" :: PF, bold(ln.index :: PF), "and" :: PF, 
            bold(rn.index :: PF), "must match." :: PF])
      -- %a[?] ~ %b[?]
      hasUnknownType?(x, ln) and hasUnknownType?(x, rn) =>
        ures := unifyType(ln.type, rn.type)
        ures case "failed" => false
        limitTypeVar!(x, ures :: SUBS)
      -- %a[?] ~ (%b[t1, t2, ...] | T)
      hasUnknownType?(x, ln) and not hasUnknownType?(x, rn) =>
        limitTypeVar!(x, ln.type :: TV, [rn.type])
      -- (%a[t1, t2, ...] | T) ~ %b[?]
      not hasUnknownType?(x, ln) and hasUnknownType?(x, rn) =>
        limitTypeVar!(x, rn.type :: TV, [ln.type])
      -- (%a[t1, t2, ...] | T) ~ (%b[s1, s2, ...] | S)
      ms := findMatches(typeOf(x, ln), typeOf(x, rn))
      empty? ms.terms => false
      if not aliasType? ms.terms then
        setTypeOf!(x, ln, ms.terms)
        setTypeOf!(x, rn, ms.terms)
      limitTypeVar!(x, ms.subs)

    limitNodeType! (x : %, n : TN, types : List(N)) : Boolean ==
      debug(["Limit type of" :: PF, bold(n.index :: PF), "to" :: PF,
             bracket [t :: PF for t in types]])
      -- %a[?] ~ [s1, s2, ...]
      hasUnknownType?(x, n) =>
        limitTypeVar!(x, n.type :: TV, types)
      -- (%a[t1, t2, ...] | T) ~ [s1, s2, ...]
      undefinedType? types => true
      ms := findMatches(typeOf(x, n), types)
      empty? ms.terms => false
      if not aliasType? ms.terms then
        setTypeOf!(x, n, ms.terms)
      limitTypeVar!(x, ms.subs)

    -- With limited knowledge this routine tries to constraint types in given
    -- nodes to pairs which are (possibly) in subtyping relation.
    nodeSubType! (x : %, sn : TN, tn : TN) : Boolean ==
      info(["Node" :: PF, bold(sn.index :: PF), "has subtype of" :: PF,
            bold(tn.index :: PF), "node." :: PF])
      -- In both cases we can assume nothing...
      -- a) {%s[s1, s2, ...] | S} <: {%t[?]}
      -- b) {%s[?]} <: {%t[t1, t2, ...] | T}
      hasUnknownType?(x, sn) or hasUnknownType?(x, tn) => true
      -- We're left with: {%s[s1, s2, ...] | S} <: {%t[t1, t2, ...] | T}
      -- In %s and %t there are usually some type variables. We could
      -- start normalizing terms to find out what's their exact structure, but
      -- I don't know how to deal with them yet. 
      -- With terms of known structure we can deal quite well.
      sl : List(N) := []
      tl : List(N) := []
      for s in typeOf(x, sn) repeat
        for t in typeOf(x, tn) repeat
          isSubType(s, t) case "false" => "iterate"
          sl := [s, :sl]
          tl := [t, :tl]
      empty? sl or empty? tl => false
      setTypeOf!(x, sn, removeDuplicates sl)
      setTypeOf!(x, tn, removeDuplicates tl)
      nodesTypeMatch!(x, sn, tn)
      true

    nodeSubTypeOf!(x : %, sn : TN, types : List(N)) : Boolean ==
      info(["Node" :: PF, bold(sn.index :: PF), "has subtype of" :: PF,
            bracket [t :: PF for t in types]])
      -- {%s[?]} <: [t1, t2, ...]
      hasUnknownType?(x, sn) => false
      -- {%s[s1, s2, ...] | S} <: [t1, t2, ...]
      sl : List(N) := []
      for s in typeOf(x, sn) repeat
        for t in types repeat
          isSubType(s, t) case "false" => "iterate"
          sl := [s, :sl]
      empty? sl => false
      sl := removeDuplicates sl
      -- {%s[s1, s2, ...] | S) <: %undef
      undefinedType? types =>
        -- let's choose a type that is super type of [s1, s2, ...]
        setTypeOf!(x, sn, [(#sl = 1 => first sl; nodeUnionType sl)])
        true
      setTypeOf!(x, sn, sl)
      true

    coerceTV (e : Record(key : TV, entry : List(N))) : PF ==
      t :=
        #(e.entry) = 1 => (first e.entry) :: PF
        bracket [t :: PF for t in e.entry]
      spaces [bold red right(8, e.key :: PF), ":" :: PF, bold t]

    coerce (x : %) : PF ==
      pfs : List(PF) := []
      for ns in entries x.m_nodes for i in 1.. repeat
        num := bold blue hconcat ["#" :: PF, i :: PF, ":" :: PF]
        vars := [coerceTV e for e in members(x.m_typevars)@TVS | e.key.major = i]
        s := (empty? vars => "" :: PF; " " :: PF)
        pfs := concat(pfs, [num, ns :: PF, s, :(reverse vars), s])
      pile ["Type tree representation:" :: PF, :pfs]