Subterms.hs

-- Note: this is an automatically generated file. Do not edit.

-- | The term-graph view of a typed graph: nodes are subterms, sharing is explicit, children are inline (a tree with symbolic cross-links). graphToTermGraph builds it; schemaToTypeGraph is the type-side twin. Term graphs are Ariola-Klop's nested systems of recursion equations.

module Hydra.Subterms where

import qualified Hydra.Ast as Ast
import qualified Hydra.Checking as Checking
import qualified Hydra.Coders as Coders
import qualified Hydra.Core as Core
import qualified Hydra.Docs as Docs
import qualified Hydra.Error.Checking as ErrorChecking
import qualified Hydra.Error.Core as ErrorCore
import qualified Hydra.Error.File as ErrorFile
import qualified Hydra.Error.Packaging as ErrorPackaging
import qualified Hydra.Error.System as ErrorSystem
import qualified Hydra.Errors as Errors
import qualified Hydra.Extract.Core as ExtractCore
import qualified Hydra.File as File
import qualified Hydra.Graph as Graph
import qualified Hydra.Json.Model as Model
import qualified Hydra.Lexical as Lexical
import qualified Hydra.Overlay.Haskell.Lib.Eithers as Eithers
import qualified Hydra.Overlay.Haskell.Lib.Equality as Equality
import qualified Hydra.Overlay.Haskell.Lib.Lists as Lists
import qualified Hydra.Overlay.Haskell.Lib.Logic as Logic
import qualified Hydra.Overlay.Haskell.Lib.Maps as Maps
import qualified Hydra.Overlay.Haskell.Lib.Optionals as Optionals
import qualified Hydra.Overlay.Haskell.Lib.Pairs as Pairs
import qualified Hydra.Overlay.Haskell.Lib.Sets as Sets
import qualified Hydra.Overlay.Haskell.Lib.Strings as Strings
import qualified Hydra.Packaging as Packaging
import qualified Hydra.Parsing as Parsing
import qualified Hydra.Paths as Paths
import qualified Hydra.Query as Query
import qualified Hydra.Reflect as Reflect
import qualified Hydra.Regex as Regex
import qualified Hydra.Relational as Relational
import qualified Hydra.Rewriting as Rewriting
import qualified Hydra.Substitution as Substitution
import qualified Hydra.System as System
import qualified Hydra.Tabular as Tabular
import qualified Hydra.Testing as Testing
import qualified Hydra.Time as Time
import qualified Hydra.Topology as Topology
import qualified Hydra.Typed as Typed
import qualified Hydra.Typing as Typing
import qualified Hydra.Util as Util
import qualified Hydra.Validation as Validation
import qualified Hydra.Variants as Variants
import Prelude hiding  (Enum, Ordering, decodeFloat, encodeFloat, fail, lines, map, pure, sum, unlines)
import qualified Data.Scientific as Sci
import Data.Void
import qualified Data.Map as M
import qualified Data.Set as S

-- | The expected type to thread into an immediate child, given this node's (synthesized) type, its term, and the step reaching the child. This is the term->type position map underlying the TermGraph:TypeGraph erasure: element positions get the container element type, mapEntry gets pair<K,V>, lambdaBody the codomain, and so on. `none` where the child's type is not fixed top-down (e.g. a function-position subterm), which is fine for non-empty children.
expectedForStep :: M.Map Core.Name Core.Type -> Core.Type -> Core.Term -> Paths.SubtermStep -> Maybe Core.Type
expectedForStep schema typ term step =

      let elementOfList =
              \t -> case t of
                Core.TypeList v0 -> Just v0
                _ -> Nothing
          elementOfSet =
                  \t -> case t of
                    Core.TypeSet v0 -> Just v0
                    _ -> Nothing
          elementOfOptional =
                  \t -> case t of
                    Core.TypeOptional v0 -> Just v0
                    _ -> Nothing
          codomainOf =
                  \t -> case t of
                    Core.TypeFunction v0 -> Just (Core.functionTypeCodomain v0)
                    _ -> Nothing
          mapPairType =
                  \t -> case t of
                    Core.TypeMap v0 -> Just (Core.TypePair (Core.PairType {
                      Core.pairTypeFirst = (Core.mapTypeKeys v0),
                      Core.pairTypeSecond = (Core.mapTypeValues v0)}))
                    _ -> Nothing
      in case step of
        Paths.SubtermStepListElement _ -> elementOfList typ
        Paths.SubtermStepSetElement _ -> elementOfSet typ
        Paths.SubtermStepOptionalGiven -> elementOfOptional typ
        Paths.SubtermStepLambdaBody -> codomainOf typ
        Paths.SubtermStepMapEntry _ -> mapPairType typ
        Paths.SubtermStepPairFirst -> case typ of
          Core.TypePair v1 -> Just (Core.pairTypeFirst v1)
          _ -> Nothing
        Paths.SubtermStepPairSecond -> case typ of
          Core.TypePair v1 -> Just (Core.pairTypeSecond v1)
          _ -> Nothing
        Paths.SubtermStepRecordField v0 -> fieldTypeFromSchema schema term v0
        Paths.SubtermStepInjectField v0 -> fieldTypeFromSchema schema term v0
        _ -> Nothing

-- | The expected type of a record field / injected union field, from the named type in the schema
fieldTypeFromSchema :: M.Map Core.Name Core.Type -> Core.Term -> Core.Name -> Maybe Core.Type
fieldTypeFromSchema schema term fname =
    case term of
      Core.TermRecord v0 -> Optionals.bind (Maps.lookup (Core.recordTypeName v0) schema) (\sty -> Eithers.either (\_ -> Nothing) (\fields -> findFieldTypeIn fname fields) (ExtractCore.recordType (Core.recordTypeName v0) sty))
      Core.TermInject v0 -> Optionals.bind (Maps.lookup (Core.injectionTypeName v0) schema) (\sty -> Eithers.either (\_ -> Nothing) (\fields -> findFieldTypeIn fname fields) (ExtractCore.unionType (Core.injectionTypeName v0) sty))
      _ -> Nothing

-- | The type of the named field within a list of field types, if present
findFieldTypeIn :: Core.Name -> [Core.FieldType] -> Maybe Core.Type
findFieldTypeIn fname fields =
    Optionals.map Core.fieldTypeType (Lists.head (Lists.filter (\f -> Equality.equal (Core.fieldTypeName f) fname) fields))

-- | The term-graph view of a typed graph: one root node per binding. Sharing is explicit; children are inline (a tree); variable occurrences become symbolic references carrying their binding node's id. Input must be a POST-INFERENCE (elaborated) graph: binding schemes present, lambda domains present, typeLambda/typeApplication explicit. Node types are synthesized in one O(n) bidirectional pass; a missing annotation (or an untyped empty leaf) is a precondition failure.
graphToTermGraph :: Graph.Graph -> Either Errors.Error Paths.TermGraph
graphToTermGraph graph =

      let boundTerms = Graph.graphBoundTerms graph
          schema = Maps.map (\ts -> Core.typeSchemeBody ts) (Graph.graphBoundTypes graph)
      in (Eithers.map (\roots -> Paths.TermGraph {
        Paths.termGraphRoots = (Maps.fromList roots)}) (Eithers.mapList (\nt ->
        let name = Pairs.first nt
            term = Pairs.second nt
            expected = rootExpectedType schema name
        in (Eithers.map (\node -> (name, node)) (termGraphNode graph schema name Maps.empty Sets.empty expected (Paths.SubtermPath []) term))) (Maps.toList boundTerms)))

-- | The expected type for a root binding node: its declared type in the schema, if present
rootExpectedType :: Ord t0 => (M.Map t0 t1 -> t0 -> Maybe t1)
rootExpectedType schema name = Maps.lookup name schema

-- | The type-graph view of a schema: one root node per named type. A Type.variable referencing a schema-bound name is a nominal reference; a forall-bound variable in scope is a variable reference to its binding node; leaf types and non-type constituents are carried as links.
schemaToTypeGraph :: M.Map Core.Name Core.Type -> Either Errors.Error Paths.TypeGraph
schemaToTypeGraph schema =

      let schemaNames = Maps.keys schema
      in (Eithers.map (\roots -> Paths.TypeGraph {
        Paths.typeGraphRoots = (Maps.fromList roots)}) (Eithers.mapList (\nt ->
        let name = Pairs.first nt
            typ = Pairs.second nt
        in (Eithers.map (\node -> (name, node)) (typeGraphNode (Sets.fromList schemaNames) name Maps.empty (Paths.SubtypePath []) typ))) (Maps.toList schema)))

-- | Synthesize the type of an elaborated subterm, syntax-directed and without unification, threading `expected` top-down. Reads annotations (lambda domain, typeApplication type) and combines child types bottom-up; synthesis-incomplete leaves (empty list/set/map, optional none, either's absent branch) CONSUME `expected`. `expected = none` at such a leaf is a precondition failure with path.
synthesizeType :: t0 -> M.Map Core.Name Core.Type -> M.Map Core.Name Core.Type -> Core.Name -> Maybe Core.Type -> t1 -> Core.Term -> Either Errors.Error Core.Type
synthesizeType graph schema env root expected path term =

      let recurseInto = \mexp -> \child -> synthesizeType graph schema env root mexp path child
          fail =
                  \msg -> Left (Errors.ErrorOther (Errors.OtherError (Strings.concat2 (Strings.concat2 "synthesizeType precondition: " msg) (Strings.concat2 " at " (Core.unName root)))))
          consumeExpected = \what -> Optionals.match expected (fail (Strings.concat2 "untyped " what)) (\t -> Right t)
          elementOfExpected =
                  Optionals.bind expected (\t -> case t of
                    Core.TypeList v0 -> Just v0
                    Core.TypeSet v0 -> Just v0
                    Core.TypeOptional v0 -> Just v0
                    _ -> Nothing)
          codomainOfExpected =
                  Optionals.bind expected (\t -> case t of
                    Core.TypeFunction v0 -> Just (Core.functionTypeCodomain v0)
                    _ -> Nothing)
      in case term of
        Core.TermApplication v0 -> Eithers.bind (recurseInto Nothing (Core.applicationFunction v0)) (\ftype -> case ftype of
          Core.TypeFunction v1 -> Right (Core.functionTypeCodomain v1)
          _ -> fail "application of a non-function")
        Core.TermLambda v0 -> Optionals.match (Core.lambdaDomain v0) (fail "lambda without a domain annotation") (\dom -> Eithers.map (\bt -> Core.TypeFunction (Core.FunctionType {
          Core.functionTypeDomain = dom,
          Core.functionTypeCodomain = bt})) (recurseInto codomainOfExpected (Core.lambdaBody v0)))
        Core.TermTypeLambda v0 -> Eithers.map (\bt -> Core.TypeForall (Core.ForallType {
          Core.forallTypeParameter = (Core.typeLambdaParameter v0),
          Core.forallTypeBody = bt})) (recurseInto Nothing (Core.typeLambdaBody v0))
        Core.TermTypeApplication v0 -> Eithers.bind (recurseInto Nothing (Core.typeApplicationTermBody v0)) (\bt -> case bt of
          Core.TypeForall v1 -> Right (Substitution.substInType (Substitution.singletonTypeSubst (Core.forallTypeParameter v1) (Core.typeApplicationTermType v0)) (Core.forallTypeBody v1))
          _ -> fail "type application of a non-forall")
        Core.TermVariable v0 -> Optionals.match (Maps.lookup v0 env) (Optionals.match (Maps.lookup v0 schema) (fail (Strings.concat2 "unbound variable " (Core.unName v0))) (\t -> Right t)) (\t -> Right t)
        Core.TermUnit -> Right Core.TypeUnit
        Core.TermLiteral v0 -> Right (Core.TypeLiteral (Reflect.literalType v0))
        Core.TermOptional v0 -> Optionals.match v0 (consumeExpected "optional none") (\t -> Eithers.map (\x -> Core.TypeOptional x) (recurseInto elementOfExpected t))
        Core.TermList v0 -> Optionals.match (Lists.head v0) (consumeExpected "empty list") (\t0 -> Eithers.map (\x -> Core.TypeList x) (recurseInto elementOfExpected t0))
        Core.TermSet v0 -> Optionals.match (Lists.head (Sets.toList v0)) (consumeExpected "empty set") (\t0 -> Eithers.map (\x -> Core.TypeSet x) (recurseInto elementOfExpected t0))
        Core.TermMap v0 -> Optionals.match (Lists.head (Maps.toList v0)) (consumeExpected "empty map") (\kv -> Eithers.bind (recurseInto Nothing (Pairs.first kv)) (\kt -> Eithers.map (\vt -> Core.TypeMap (Core.MapType {
          Core.mapTypeKeys = kt,
          Core.mapTypeValues = vt})) (recurseInto Nothing (Pairs.second kv))))
        Core.TermPair v0 -> Eithers.bind (recurseInto Nothing (Pairs.first v0)) (\ft -> Eithers.map (\st -> Core.TypePair (Core.PairType {
          Core.pairTypeFirst = ft,
          Core.pairTypeSecond = st})) (recurseInto Nothing (Pairs.second v0)))
        Core.TermEither _ -> consumeExpected "either value"
        Core.TermRecord v0 -> Optionals.match (Maps.lookup (Core.recordTypeName v0) schema) (fail (Strings.concat2 "record type not in schema: " (Core.unName (Core.recordTypeName v0)))) (\t -> Right t)
        Core.TermInject v0 -> Optionals.match (Maps.lookup (Core.injectionTypeName v0) schema) (fail (Strings.concat2 "union type not in schema: " (Core.unName (Core.injectionTypeName v0)))) (\t -> Right t)
        Core.TermWrap v0 -> Optionals.match (Maps.lookup (Core.wrappedTermTypeName v0) schema) (fail (Strings.concat2 "wrapper type not in schema: " (Core.unName (Core.wrappedTermTypeName v0)))) (\t -> Right t)
        Core.TermAnnotated v0 -> recurseInto expected (Core.annotatedTermBody v0)
        Core.TermLet v0 -> recurseInto expected (Core.letBody v0)
        Core.TermProject v0 ->
          let tname = Core.projectionTypeName v0
              fname = Core.projectionFieldName v0
          in (Optionals.match (Maps.lookup tname schema) (fail (Strings.concat2 "projection type not in schema: " (Core.unName tname))) (\sty -> Eithers.bind (ExtractCore.recordType tname sty) (\fields -> Optionals.match (findFieldTypeIn fname fields) (fail (Strings.concat2 "projected field not in record type: " (Core.unName fname))) (\ftyp -> Right (Core.TypeFunction (Core.FunctionType {
            Core.functionTypeDomain = (Core.TypeVariable tname),
            Core.functionTypeCodomain = ftyp}))))))
        Core.TermUnwrap v0 -> Optionals.match (Maps.lookup v0 schema) (fail (Strings.concat2 "unwrap type not in schema: " (Core.unName v0))) (\sty -> Eithers.map (\inner -> Core.TypeFunction (Core.FunctionType {
          Core.functionTypeDomain = (Core.TypeVariable v0),
          Core.functionTypeCodomain = inner})) (ExtractCore.wrappedType v0 sty))
        Core.TermCases v0 ->
          let tname = Core.caseStatementTypeName v0
              rep =
                      Optionals.match (Core.caseStatementDefault v0) (Optionals.map Core.caseAlternativeHandler (Lists.head (Core.caseStatementCases v0))) (\d -> Just d)
          in (Optionals.match rep (fail "case statement with no branches") (\handler -> Eithers.bind (recurseInto Nothing handler) (\htype -> Eithers.map (\ft -> Core.TypeFunction (Core.FunctionType {
            Core.functionTypeDomain = (Core.TypeVariable tname),
            Core.functionTypeCodomain = (Core.functionTypeCodomain ft)})) (ExtractCore.functionType htype))))
        _ -> fail "unsupported term constructor"

-- | The content attribute links contributed by a term constructor (a non-term constituent, with its value)
termAttributesOf :: Core.Term -> [Paths.TermAttributeLink]
termAttributesOf term =
    case term of
      Core.TermCases v0 -> [
        Paths.TermAttributeLinkCasesTypeName (Core.caseStatementTypeName v0)]
      Core.TermInject v0 -> [
        Paths.TermAttributeLinkInjectTypeName (Core.injectionTypeName v0)]
      Core.TermLambda v0 -> Lists.concat2 [
        Paths.TermAttributeLinkLambdaParameter (Core.lambdaParameter v0)] (Optionals.match (Core.lambdaDomain v0) [] (\d -> [
        Paths.TermAttributeLinkLambdaDomainGiven d]))
      Core.TermLiteral v0 -> [
        Paths.TermAttributeLinkLiteral v0]
      Core.TermProject v0 -> [
        Paths.TermAttributeLinkProjectTypeName (Core.projectionTypeName v0),
        (Paths.TermAttributeLinkProjectFieldName (Core.projectionFieldName v0))]
      Core.TermRecord v0 -> [
        Paths.TermAttributeLinkRecordTypeName (Core.recordTypeName v0)]
      Core.TermTypeApplication v0 -> [
        Paths.TermAttributeLinkTypeApplicationType (Core.typeApplicationTermType v0)]
      Core.TermTypeLambda v0 -> [
        Paths.TermAttributeLinkTypeLambdaParameter (Core.typeLambdaParameter v0)]
      Core.TermUnwrap v0 -> [
        Paths.TermAttributeLinkUnwrapTypeName v0]
      Core.TermWrap v0 -> [
        Paths.TermAttributeLinkWrapTypeName (Core.wrappedTermTypeName v0)]
      _ -> []

-- | Build a term-graph node (inline) for the subterm at the given path within a root binding. `env` maps each in-scope local variable to its (binder node id, type); `lambdaScope` marks the lambda-bound subset. `expected` is the type flowing top-down, consumed by synthesis-incomplete leaves. A variable child is not a node: the parent emits a reference link for it.
termGraphNode :: Graph.Graph -> M.Map Core.Name Core.Type -> Core.Name -> M.Map Core.Name (Paths.TermNodeId, Core.Type) -> S.Set Core.Name -> Maybe Core.Type -> Paths.SubtermPath -> Core.Term -> Either Errors.Error Paths.TermNode
termGraphNode graph schema root env lambdaScope expected path term =

      let steps = Paths.unSubtermPath path
          thisId =
                  Paths.TermNodeId {
                    Paths.termNodeIdRoot = root,
                    Paths.termNodeIdPath = path}
          envTypes = Maps.map (\p -> Pairs.second p) env
          childEnv =
                  case term of
                    Core.TermLambda v0 -> Maps.insert (Core.lambdaParameter v0) (thisId, (Optionals.withDefault (Core.TypeVariable (Core.Name "?")) (Core.lambdaDomain v0))) env
                    Core.TermLet v0 -> Lists.foldl (\acc -> \b ->
                      let bname = Core.bindingName b
                          bid =
                                  Paths.TermNodeId {
                                    Paths.termNodeIdRoot = root,
                                    Paths.termNodeIdPath = (Paths.SubtermPath (Lists.concat2 steps [
                                      Paths.SubtermStepLetBinding bname]))}
                          btype = Optionals.withDefault (Core.TypeVariable (Core.Name "?")) (Optionals.map Core.typeSchemeBody (Core.bindingTypeScheme b))
                      in (Maps.insert bname (bid, btype) acc)) env (Core.letBindings v0)
                    _ -> env
          childLambdaScope =
                  case term of
                    Core.TermLambda v0 -> Sets.insert (Core.lambdaParameter v0) lambdaScope
                    _ -> lambdaScope
      in (Eithers.bind (synthesizeType graph schema envTypes root expected path term) (\typ ->
        let attrLinks = Lists.map (\x -> Paths.TermLinkAttribute x) (termAttributesOf term)
        in (Eithers.bind (Eithers.mapList (\st ->
          let step = Pairs.first st
              child = Pairs.second st
              childPath = Paths.SubtermPath (Lists.concat2 steps [
                    step])
              childExpected = expectedForStep schema typ term step
          in case child of
            Core.TermVariable v0 -> Eithers.map (\ref -> Paths.TermLinkReference (Paths.TermReferenceLink {
              Paths.termReferenceLinkStep = step,
              Paths.termReferenceLinkTarget = ref})) (termReferenceFor graph childEnv childLambdaScope v0)
            _ -> Eithers.map (\cnode -> Paths.TermLinkSubterm (Paths.SubtermLink {
              Paths.subtermLinkStep = step,
              Paths.subtermLinkChild = cnode})) (termGraphNode graph schema root childEnv childLambdaScope childExpected childPath child)) (Rewriting.subtermsWithSteps term)) (\childLinks -> Right (Paths.TermNode {
          Paths.termNodeTerm = term,
          Paths.termNodeType = typ,
          Paths.termNodeLinks = (Lists.concat2 attrLinks childLinks)})))))

-- | Classify a variable occurrence, carrying its binder's node id: lambda-bound (node = the binding lambda), let-bound — locally or as a graph binding — (node = the bound term), or a primitive; a free variable is a precondition failure. `lambdaScope` marks which local names are lambda-bound.
termReferenceFor :: Graph.Graph -> M.Map Core.Name (Paths.TermNodeId, Core.Type) -> S.Set Core.Name -> Core.Name -> Either Errors.Error Paths.TermReference
termReferenceFor graph env lambdaScope name =
    Optionals.match (Maps.lookup name env) (Logic.ifElse (Maps.member name (Graph.graphBoundTerms graph)) (Right (Paths.TermReferenceLet (Paths.LetVariableReference {
      Paths.letVariableReferenceVariable = name,
      Paths.letVariableReferenceBindingNode = Paths.TermNodeId {
        Paths.termNodeIdRoot = name,
        Paths.termNodeIdPath = (Paths.SubtermPath [])},
      Paths.letVariableReferenceType = (Optionals.withDefault (Core.TypeVariable (Core.Name "?")) (Optionals.map Core.typeSchemeBody (Maps.lookup name (Graph.graphBoundTypes graph))))}))) (Logic.ifElse (Maps.member name (Graph.graphPrimitives graph)) (Right (Paths.TermReferencePrimitive (Paths.PrimitiveReference {
      Paths.primitiveReferenceName = name,
      Paths.primitiveReferenceType = (Core.TypeVariable (Core.Name "?"))}))) (Left (Errors.ErrorOther (Errors.OtherError (Strings.concat2 "free variable in term graph: " (Core.unName name))))))) (\idType ->
      let binderId = Pairs.first idType
          occType = Pairs.second idType
      in (Logic.ifElse (Sets.member name lambdaScope) (Right (Paths.TermReferenceLambda (Paths.LambdaVariableReference {
        Paths.lambdaVariableReferenceVariable = name,
        Paths.lambdaVariableReferenceBoundByNode = binderId,
        Paths.lambdaVariableReferenceType = occType}))) (Right (Paths.TermReferenceLet (Paths.LetVariableReference {
        Paths.letVariableReferenceVariable = name,
        Paths.letVariableReferenceBindingNode = binderId,
        Paths.letVariableReferenceType = occType})))))

-- | The content attribute links contributed by a type constructor: annotation, forall parameter, or literal type
typeAttributesOf :: Core.Type -> [Paths.TypeAttributeLink]
typeAttributesOf typ =
    case typ of
      Core.TypeAnnotated v0 -> [
        Paths.TypeAttributeLinkAnnotatedAnnotation (Core.annotatedTypeAnnotation v0)]
      Core.TypeForall v0 -> [
        Paths.TypeAttributeLinkForallParameter (Core.forallTypeParameter v0)]
      Core.TypeLiteral v0 -> [
        Paths.TypeAttributeLinkLiteral v0]
      _ -> []

-- | Build a type-graph node (inline) for the subtype at the given path within a named root type
typeGraphNode :: S.Set Core.Name -> Core.Name -> M.Map Core.Name Paths.TypeNodeId -> Paths.SubtypePath -> Core.Type -> Either Errors.Error Paths.TypeNode
typeGraphNode schemaNames root forallScope path typ =
    Eithers.map (\links -> Paths.TypeNode {
      Paths.typeNodeType = typ,
      Paths.typeNodeLinks = links}) (typeLinks schemaNames root forallScope path typ)

-- | The outgoing links of a type node: its content attributes, and one link per immediate subtype — a variable occurrence becomes a reference link on the parent (occurrences are not nodes), any other subtype an inline subtype link. `forallScope` maps each in-scope forall variable to its binding node id.
typeLinks :: S.Set Core.Name -> Core.Name -> M.Map Core.Name Paths.TypeNodeId -> Paths.SubtypePath -> Core.Type -> Either Errors.Error [Paths.TypeLink]
typeLinks schemaNames root forallScope path typ =

      let steps = Paths.unSubtypePath path
          thisId =
                  Paths.TypeNodeId {
                    Paths.typeNodeIdRoot = root,
                    Paths.typeNodeIdPath = path}
          attrLinks = Lists.map (\x -> Paths.TypeLinkAttribute x) (typeAttributesOf typ)
          childScope =
                  case typ of
                    Core.TypeForall v0 -> Maps.insert (Core.forallTypeParameter v0) thisId forallScope
                    _ -> forallScope
      in (Eithers.bind (Eithers.mapList (\st ->
        let step = Pairs.first st
            child = Pairs.second st
            childPath = Paths.SubtypePath (Lists.concat2 steps [
                  step])
        in case child of
          Core.TypeVariable v0 -> Eithers.map (\ref -> Paths.TypeLinkReference (Paths.TypeReferenceLink {
            Paths.typeReferenceLinkStep = step,
            Paths.typeReferenceLinkTarget = ref})) (typeReferenceFor schemaNames childScope v0)
          _ -> Eithers.map (\cnode -> Paths.TypeLinkSubtype (Paths.SubtypeLink {
            Paths.subtypeLinkStep = step,
            Paths.subtypeLinkChild = cnode})) (typeGraphNode schemaNames root childScope childPath child)) (Rewriting.subtypesWithSteps typ)) (\childLinks -> Right (Lists.concat2 attrLinks childLinks)))

-- | Classify a type variable occurrence: a schema-bound name is a nominal reference; a forall-bound variable in scope is a variable reference carrying its binding forall's node id; anything else is a free-variable precondition failure.
typeReferenceFor :: S.Set Core.Name -> M.Map Core.Name Paths.TypeNodeId -> Core.Name -> Either Errors.Error Paths.TypeReference
typeReferenceFor schemaNames forallScope name =
    Logic.ifElse (Sets.member name schemaNames) (Right (Paths.TypeReferenceNominal (Paths.NominalTypeReference {
      Paths.nominalTypeReferenceName = name}))) (Optionals.match (Maps.lookup name forallScope) (Left (Errors.ErrorOther (Errors.OtherError (Strings.concat2 "free type variable in type graph: " (Core.unName name))))) (\binderId -> Right (Paths.TypeReferenceVariable (Paths.TypeVariableReference {
      Paths.typeVariableReferenceVariable = name,
      Paths.typeVariableReferenceBoundByNode = binderId}))))