Gabriella Gonzalez: Mechanized type inference for record concatenation

The context behind this post is that I'm working on a type checker and language server for Nix and there are three features of the language which make it tricky to typecheck (which I'll dub the "three horsemen of Nix type inference"):

• computed imports (imports that depend on values in scope)1
• computed record2 fields and field accesses
• // (the biased record concatenation operator) which is the subject of this post!

Here "biased record concatenation" means combining two records, preferring fields from one record if they overlap. For example, in Nix the // operator prefers fields from the right record in case of overlap:

nix-repl> { x = 1; y = 2; } // { y = true; z = "hi"; }
{ x = 1; y = true; z = "hi"; }

The good news is that type inference for biased record concatenation is not a research problem because the algorithm was published in 1991 as Type inference for record concatenation and multiple inheritance by Mitchell Wand (henceforth "the Wand paper"). The bad news is that as far as I can tell no language in existence implements the type inference algorithm described in that paper, so even though it's not a research problem it's still not a solved problem.

A big reason why is that the paper isn't "easy to mechanize" meaning that it doesn't translate well to code. In this post I hope to fix that by by spelling out a formal algorithm equivalent to the original paper. In particular, I'll formalize the algorithm in three ways:

• a declarative natural deduction semantics
• an algorithmic semantics using constraint generation and resolution
• a reference Haskell implementation (≈400 lines of code)

… and I also published a companion project on GitHub that you can use to test the reference Haskell implementation.

This post builds upon my previous post: Record type inference for dummies. Reading that post will not necessarily prepare you for this post if you're a type theory newcomer, but it will at least help you understand the basic terminology/syntax and also appreciate why this is a challenging problem to solve.

Motivation

Why do we even want to support type inference for this specific operator? After all, there are variations on this operator that are easier to type check, like a record concatenation operator that rejects conflicting fields. Maybe we should just use something like that instead?

Well, I know that Nix needs this specific operator and not other variations, because this operator (plus recursion) powers Nixpkgs support for "late binding" of dependencies, where you can override a package and all reverse dependencies pick up the overridden package. This is a critical feature in the age of rampant supply chain attacks because you need to be able to patch or upgrade a dependency and ensure that all downstream packages pick up the fixed dependency.

The fundamental reason why the // operator is tricky to type-check is because late binding is tricky to type-check. We could replace Nix's // operator with some other operator or language feature, but so long as Nixpkgs needs late binding then type inference will remain tricky.

I'm hoping that this post will not only progress the state-of-the-art for type checking Nix but also pave the way for more typed languages to support the Wand inference algorithm. That way we can get nicer inferred types with smaller constraints requiring fewer annotations.

Prior art

Currently only one language I'm aware of (PureScript) supports biased record concatenation and also can infer a useful type for this example function (taken from the paper):

… or using Nix syntax:

r: s: (r // s).x + 1

Note that there are a few typed languages that support biased record concatenation:

• Dhall (using the same operator as Nix: r // s)
• Typescript/Flow (using spread syntax: { ...r, ...s })
• PureScript (using the Record.merge function)

… but Dhall, TypeScript, and Flow can only work forwards when performing type inference on this operator, meaning they require concrete types for the two input records (e.g. r and s).

For example, in TypeScript if you try to define :

function example(r, s): number {
    return { ...r, ...s }.x + 1;
};

… the type checker will complain that r and s have an inferred type of any because the type checker cannot work backwards to infer useful types for the inputs.

PureScript is the only language in that list that can infer a useful and general type for that function without any annotation:

-- This type annotation is optional.  PureScript already infers this
-- type
example
  :: forall a b c d
  .  Union b a c
  => Nub c (x :: Int | d)
  => Record a
  -> Record b
  -> Int
example r s = (merge s r).x + 1

However, PureScript is not using the approach described in the paper and I prefer the approach from the paper because it leads to simpler inferred types and constraints. As I mentioned earlier, no language implements the original paper because it's so loosely formalized, but I hope to fix that by translating the paper into an algorithm that any person (or any coding agent) can methodically translate to code.

Domains

The Wand paper observes that you can think of a row-polymorphic record type such as this one:

… as a potentially infinite record consisting of explicit fields ( and ) and an implicit set of potential fields denoted by a "row variable" (). This row variable stands in for all other fields that might be present, and we'll call those other fields the row variable's "domain".

However, not all row variables are created equal. For example, consider this other record type:

Both and range over two potentially infinite sets of fields (two domains), but they do not range over the same two domains. Specifically, ranges over "all fields that are neither nor " and ranges over "all fields that are not " so ranges over one more potential field () than . That means we can't compare and as-is because that wouldn't be an apples-to-apples comparison.

The Wand paper builds on that idea to note that record unification gets much easier when both records share the same set of explicit fields, because then you only need to handle three cases3:

• Case 0: unifying two closed record types (e.g. )

  Since both records share the same set of explicit fields you can unify the two record types by unifying their respective field types (e.g. ).

• Case 1: unifying two open record types (e.g. )

  Similar to Case 0, except we also unify their row variables (e.g. ) because they share the same domain.

• Case 2, where one record type is open (e.g. )

  We solve this case by solving to be the empty set of fields.

Field instantiation - Part 1

This means we need some way to fix any two record types to share the same set of explicit fields and we'll call this process field instantiation.

For example, if we were to unify these two record types:

… they start off with a mismatch where only the left record type mentions and only the right record type mentions . However, we can fix the mismatch by taking (all fields that are not ) and "splitting out" an explicit field for and leaving behind a new row variable representing all fields that are neither nor :

Here we've introduced a new bit of syntax, , to denote that is a potential field, meaning that we're still not sure whether is present or not. However, whether or not is present no longer ranges over .

We can similarly replace with an explicit mention of and a new row variable representing all fields that are neither nor :

Now we can unify and because they share same domain (fields that are neither nor ) but how do we unify with ?

Field annotations

This is where we need to introduce some formal notation for potential fields (henceforth, just "fields"), which can be either (with an associated field type ), , or unknown (represented by a field variable, like ):

So, for example:

• means the record has a field named storing a
• means the record has no field named
• means that we don't know whether the field is present or not

We also define to be syntactic sugar for to support traditional record types, so if we were to unify these two types:

… we would "desugar" to :

… then desugar to :

… and then pairwise field unification produces:

… while row unification produces:

… and if we substitute those equations back into our types, we get the following unified type for both records (arbitrarily preferring ):

… which we can "resugar" to:

What would happen, though, if we were to unify two closed record types like these:

Well, we'd still make them agree on their explicit fields, but since the right record type is closed we have no potential fields to draw upon, so we can only introduce an field:

Then if we were to desugar the left record type:

… we would get an irreconcilable mismatch because we can't unify with , so unification fails.

Constraints

Now let's revisit the same example from before:

What type should we infer for that example?

Before we dive into formal notation, let's think out loud in English. The part we know for sure is:

• and must be records (since we concatenate them using )
• must be a record field storing a (since we add to it)

… but we don't know which record comes from because could be a field of or a field of or a field of both records (in which case we'd source the field from since prefers the right record in case of overlap).

The Wand inference algorithm handles this uncertainty by producing a type alongside a constraint (similar to PureScript). The base type the paper would infer (adapted to the notation I'm using in this post) would be:

… which says that our function's inputs are both records, each of which may or may not have an field and they may also have some other fields, too. Also, the function's output is a .

Additionally, the Wand algorithm would generate a constraint saying:

…which you can read as saying that our field either comes from the left record (if is missing from the right record) or from the right record (regardless of whether is present in the left record).

We could even present that constraint to the end user as part of the inferred type, like this:

However, I'm not really a fan of that notation and in this post I will propose a simpler notation for constraints, not just to shorten the type signature but also to support an algorithm that's easier to mechanize.

Field concatenation

The notation I'll propose is to define a new type-level operator that "merges" two fields:

Specifically, this operator returns the right-most field that is , and returns if neither field is :

You can think of this operator as analogous to the operator, but merging field types instead of field values.

This operator simplifies constraints quite a bit. For example, we can use this operator to simplify the inferred type of to:

… which is equivalent to the type the Wand algorithm infers.

Proof: is true if and only if is true, which you can demonstrate by computing a truth table for both constraints ranging over all nine permutations of where .

Now, there are multiple ways we could model this operator in our formal semantics. One approach is to define this operator as another type of field:

I'm not a fan of that approach because this is not a canonical representation for a field, meaning that our abstract syntax lets us represent the same field in multiple ways. For example, under this approach and are two different syntactic representations for the same field, and that's undesirable.

A canonical representation is one in which every field has a unique syntactic representation and in my experience canonical representations promote simpler algorithms (and proofs). A better (canonical) way to represent fields while still supporting field concatenation is:

Here I've introduced a new bit of notation: the bar above means "zero or more repetitions", so means "zero or more field variables".

In this representation, means that we know for sure that the field is present and might have type unless a field variable in overrides that type. Vice versa, means that the field might be absent, unless a field variable in is .

We'll also add a little bit of syntactic sugar and write as as shorthand for or more generally write as a shorthand for .

Using Haskell code this would look like:

newtype Variable = ID Int

data Field
    = Present Type [Variable]
           -- ^ We haven't defined Type yet, but we're about to
    | Absent [Variable]

present :: Type -> Field
present fieldType = Present fieldType []

absent :: Field
absent = Absent []

Now let's define in terms of this new representation:

This definition obeys the following algebraic properties (monoid laws):

… and the proof of the monoid laws is included in the Appendix.

Conceptually, this canonical representation keeps track of the right-most field (if any). If such a field exists then we discard everything to the left, and preserve all field variables to the right. If no such field exists then we preserve all field variables.

This representation also gives us a simple algorithm for field equality: two fields are equal if their canonical representations are equal.

For example, and are both equal because they share the same canonical representation: .

In Haskell we'll use the Semigroup append operator, (<>), as the Haskell analog of :

instance Semigroup Field where
    _ <> Present a gs = Present a gs

    Present a fs <> Absent gs = Present a (fs ++ gs)

    Absent fs <> Absent gs = Absent (fs ++ gs)

instance Monoid Field where
    mempty = Absent []

We can also define a convenience function to merge zero or more fields into a single field:

… which in Haskell is just mconcat (the function that flattens a list into a single value using mempty and (<>)):

mergeFields :: [Field] -> Field
mergeFields = mconcat

Treating as a function rather than syntax means that we can simplify any occurrence of , like in the constraint I proposed earlier:

… because there we can desugar to:

… which evaluates to:

… and we can resugar that to the shorthand version: , which essentially deletes the from the constraint:

… which we can read as saying "either or is and the right-most one stores a "

Row concatenation

We'll restructure row variables in a similar way, but we first need to introduce an abstract syntax for types:

… which in Haskell would be:

import Data.Map (Map)

newtype Identifier = Identifier Text

newtype Variable = ID Int

newtype Row = Row [Variable]

data Type
    = BooleanType
    | StringType
    | NumberType
    | RecordType (Map Identifier Field) Row
    | FunctionType Type Type
    | VariableType Variable

If you read my previous post on record type inference you can see that this is similar to before with a few differences:

• the syntax for each field type changed from to

  This means that we can now mark fields explicitly absent (using ) or specify that we're not sure if a field is present (using ). However, we can still use as a shorthand for , though, so this syntax is a superset of our old syntax.

• record types now include 0 or more row variables

  Traditional type inference algorithms for row polymorphism let a record have at most one row variable, but this representation lets us have more than one row variable. These extra row variables reduce the number of constraints our type inference algorithm needs to track.

Now we can define an operator on rows that merges them:

… and the implementation of this operator is very simple:

instance Semigroup Row where
    Row ps0 <> Row ps1 = Row (ps0 ++ ps1)

instance Monoid Row where
    mempty = Row []

… or we could have just done:

newtype Row = Row [Variable]
    deriving newtype (Semigroup, Monoid)

In other words, this operator literally just concatenates the two lists of row variables. It's hardly even worth defining the operator, but I included it for symmetry.

Syntax

Now I can formalize the full algorithm, which is based on the following abstract syntax for lambda calculus supplemented with record operations, addition, and scalar values:

newtype Identifier = Identifier Text

data Expression
    = Variable Identifier
    | Lambda Identifier Expression
    | Apply Expression Expression
    | Let Identifier Expression Expression
    | Record (Map Identifier Expression)
    | FieldAccess Expression Identifier
    | FieldExtension Expression Identifier Expression
    | FieldRemoval Expression Identifier
    | RecordConcatenation Expression Expression
    | Addition Expression Expression
    | Boolean Bool
    | String Text
    | Number Double

We'll also define a context () as an ordered list of variables annotated with their types:

type Context = [(Identifier, Type)]

Natural deduction semantics

The declarative typing rules in natural deduction form are:

Those rules are simple, but they also leave out a lot of details (like how to unify records, which is the hard part of the algorithm). That's why the rest of the post walks through the algorithmic semantics.

I'll present the algorithmic semantics alongside Haskell code fragments and you can also find the complete Haskell code in the Appendix (and on GitHub) so you don't have to assemble the Haskell code fragments yourself.

Constraint generation

The algorithmic semantics differ from the natural deduction semantics by generating constraints as part of unification:

data Constraint
    = UnifyTypes  Type  Type
    | UnifyFields Field Field
    | UnifyRows   Row   Row

… and our typing judgments now infer a list of constraints in addition to inferring a type:

import Control.Monad.RWS
    (RWST(..), MonadReader(..), MonadState(..), MonadWriter(..))

infer
    :: ( MonadReader Context m       -- Our type checking context
       , MonadWriter [Constraint] m  -- Accumulated constraints
       , MonadState Variable m       -- Supply of fresh variables
       , MonadError TypeError m      -- Type errors if inference fails
       )
    => Expression -> m Type

We then resolve these constraints in a subsequent constraint resolution step.

The algorithmic semantics for constraint generation are very similar to the natural deduction semantics except that wherever we need to guess a type (or field, or row) we generate a fresh type variable (or field variable, or row variable) and any necessary constraints:

The corresponding Haskell implementation is a very direct translation of the typing rules, except I'll use complete words instead of letters to name things:

freshVariable :: MonadState Variable m => m Variable
freshVariable = state (\n -> (n, n + 1))

freshType :: MonadState Variable m => m Type
freshType = do
    variable <- freshVariable

    return (VariableType variable)

freshField :: MonadState Variable m => m Field
freshField = do
    variable <- freshVariable

    return (Absent [variable])

freshRow :: MonadState Variable m => m Row
freshRow = do
    variable <- freshVariable

    return (Row [variable])

unify :: MonadWriter [Constraint] m => Type -> Type -> m ()
unify left right = tell [UnifyTypes left right]

infer
    :: ( MonadReader Context m
       , MonadWriter [Constraint] m
       , MonadState Variable m
       , MonadError TypeError m
       )
    => Expression -> m Type
infer (Variable identifier) = do
    context <- ask

    case lookup identifier context of
        Just assignmentType ->
            return assignmentType

        Nothing ->
            throwError UnboundVariable

infer (Lambda identifier body) = do
    inputType <- freshType

    outputType <- local ((identifier, inputType) :) (infer body)

    return (FunctionType inputType outputType)

infer (Apply function argument) = do
    functionType <- infer function
    inputType    <- infer argument

    outputType <- freshType

    unify functionType (FunctionType inputType outputType)

    return outputType

infer (Let identifier assignment expression) = do
    assignmentType <- infer assignment

    local ((identifier, assignmentType) :) (infer expression)

infer (Record fields) = do
    fieldTypes <- traverse infer fields

    return (RecordType (fmap present fieldTypes) mempty)

infer (FieldAccess record identifier) = do
    recordType <- infer record

    fieldType <- freshType

    row <- freshRow

    unify recordType (RecordType [(identifier, present fieldType)] row)

    return fieldType

infer (FieldExtension record identifier expression) = do
    recordType     <- infer record
    expressionType <- infer expression

    field <- freshField

    row <- freshRow

    unify recordType (RecordType [(identifier, field)] row)

    return (RecordType [(identifier, present expressionType)] row)

infer (FieldRemoval record identifier) = do
    recordType <- infer record

    field <- freshField

    row <- freshRow

    unify recordType (RecordType [(identifier, field)] row)

    return (RecordType [(identifier, absent)] row)

infer (RecordConcatenation leftRecord rightRecord) = do
    leftRecordType  <- infer leftRecord
    rightRecordType <- infer rightRecord

    leftRow  <- freshRow
    rightRow <- freshRow

    unify leftRecordType  (RecordType [] leftRow )
    unify rightRecordType (RecordType [] rightRow)

    return (RecordType [] (leftRow <> rightRow))

infer (Addition leftNumber rightNumber) = do
    leftNumberType  <- infer leftNumber
    rightNumberType <- infer rightNumber

    unify leftNumberType  NumberType
    unify rightNumberType NumberType

    return NumberType

infer (Boolean _) = return BooleanType
infer (String  _) = return StringType
infer (Number  _) = return NumberType

Constraint resolution

To solve these generated constraints, we'll define a solver function, denoted by :

… where represents some input constrained type and represents the final constrained type where as many constraints have been solved as possible and no reducible constraints remain.

In Haskell our solver function's type is:

data Constrained = Constrained [Constraint] Type

solve
    ::  ( MonadError TypeError m  -- Constraint resolution can fail
        , MonadState Variable m   -- We'll still need fresh variables
        )
    =>  [Constraint]   -- "stuck" constraints that cannot be reduced
    ->  Constrained    -- a constrained type to reduce
    ->  m Constrained  -- the final constrained type

This function will process the constraints one-by-one until reaching the end of the list (the base case), where the solver returns all "stuck" constraints:

solve stuck (Constrained [] _T) = do
    return (Constrained stuck _T)

Trivial constraints

Constraints like these are easy to solve:

Our solver just drops those trivial constraints, proceeding to solve the remainder of the constraints:

solve stuck (Constrained (constraint : constraints) _T) = do
    let next = Constrained constraints _T

    …

    case constraint of
        UnifyTypes BooleanType BooleanType -> solve stuck next
        UnifyTypes StringType  StringType  -> solve stuck next
        UnifyTypes NumberType  NumberType  -> solve stuck next

        …

Simple unification

We can also unify two function types by unifying their inputs and outputs:

… and unify two present fields (with no field variables) by unifying their types:

solve stuck (Constrained (constraint : constraints) _T) = do
    …

    case constraint of
        …

        UnifyTypes (FunctionType _A0 _B0) (FunctionType _A1 _B1) -> do
            let newConstraints =
                      UnifyTypes _A0 _A1
                    : UnifyTypes _B0 _B1
                    : constraints

            solve stuck (Constrained newConstraints _T)

        UnifyFields (Present _A0 []) (Present _A1 []) -> do
            let newConstraints = UnifyTypes _A0 _A1 : constraints

            solve stuck (Constrained newConstraints _T)

Substitution

The next few cases for our solver will cover substitution for types, rows, and fields. For example, if we unify a type variable with a type (e.g. ) then we can satisfy the constraint using substitution.

This means we need to define a function to substitute a type by replacing all occurrences of some type variable with a replacement type .

… such that:

Note that the above definition also requires also defining type substitution on fields (e.g. ), so we can "overload" the same substitution function to work on fields:

In fact, we can keep overloading this function to also work on constraints:

… and constrained types, too:

However, for future similar functions I'll skip these sorts of tedious overloaded definitions and only define the most interesting cases (typically the base case).

The Haskell version of type substitution is:

import Data.Data.Lens (biplate)

import qualified Control.Lens as Lens

substituteType :: Variable -> Type -> Type -> Type
substituteType a _A (VariableType a')
    | a == a' = _A
    | otherwise = VariableType a' 

substituteType a _A (FunctionType _B0 _C0) = FunctionType _B1 _C1
  where
    _B1 = substituteType a _A _B0
    _C1 = substituteType a _A _C0

substituteType a _A (RecordType fields _P) =
    RecordType (Lens.over biplate (substituteType a _A) fields) _P

substituteType _ _ BooleanType = BooleanType
substituteType _ _ StringType  = StringType
substituteType _ _ NumberType  = NumberType

If you're wondering what this is about:

substituteType a _A (RecordType fields _P) =
    RecordType (Lens.over biplate (substituteType a _A) fields) _P

Here we're making use of a clever trick so that we don't need to write multiple overloaded definitions of the same function. If we use the biplate optic from Haskell's lens package then we can automatically overload substituteType to work on any type that may have Types stored somewhere inside of it. In the above Haskell snippet we don't need to define a separate version of this function that works on fields; instead, the code uses Lens.over biplate to lift our substituteType function to transform every Type inside of fields.

We also need our solver to substitute rows, so we'll define a row substitution function:

… that substitutes a row by replacing all occurrences of the row variable with a row :

substituteRow :: Variable -> Row -> Row -> Row
substituteRow p (Row ps) (Row ps') = Row (concatMap replace ps')
  where
    replace p' = if p == p' then ps else [p']

Similar to before, we'll overload this row substitution function to also work on types, fields, constraints, and constrained types, but this time I won't spell out those cases.

The substitution function for fields is the trickiest one:

… but we can make use of the earlier operator to simplify the definition:

In other words, we split a field into chunks delimited by , replace each with and then combine the result back together again using .

substituteField :: Variable -> Field -> Field -> Field
substituteField f _F field =
    mconcat (List.intersperse _F (chunks field))
  where
    chunks (Present _A fs) =
        case List.break (== f) fs of
            (_, []) ->
                [Present _A fs]
            (prefix, _ : suffix) ->
                Present _A prefix : chunks (Absent suffix)

    chunks (Absent fs) =
        case List.break (== f) fs of
            (_, []) ->
                [Absent fs]
            (prefix, _ : suffix) ->
                Absent prefix : chunks (Absent suffix)

Now we can use these three substitution functions to solve constraints where one or the other side is a variable:

There are also symmetric rules for the constraints , , and , but in this post I'll omit symmetric typing rules for the sake of space:

occursCheck :: MonadError TypeError m => Variable -> Variable -> m ()
occursCheck a b
    | a == b = throwError OccursCheckFailed
    | otherwise = return ()

…

solve stuck (Constrained (constraint : constraints) _T) = do
    let other = Constrained (stuck ++ constraints) _T

    …

    case constraint of
        …

        UnifyTypes (VariableType a) _A -> do
            Lens.traverseOf_ biplate (occursCheck a) _A

            solve [] (Lens.over biplate (substituteType a _A) other)

        UnifyRows (Row [p]) _P -> do
            Lens.traverseOf_ biplate (occursCheck p) _P

            solve [] (Lens.over biplate (substituteRow p _P) other)

        UnifyFields (Absent [f]) _F -> do
            Lens.traverseOf_ biplate (occursCheck f) _F

            solve [] (Lens.over biplate (substituteField f _F) other)

        …

Carefully note that our solver needs to perform substitution on all other constraints in the list, including the stuck ones, since they might no longer be stuck after substitution.

The above Haskell snippet demonstrates another useful application of biplate: we can write an occursCheck that just works on Variables and automatically lift it to work on types, rows, and fields.

Deletion

If a constraint unifies any row () with an empty row () then we can just delete all row variables mentioned within , because and setting a row variable to is the same thing as deleting that row variable. So that means we'll define a function to delete row variables:

deleteRow :: Row -> Row -> Row
deleteRow (Row _P) (Row _Q) = Row (_Q \\ _P)

… and overload that function to work on constrained types so that we can solve a constraint with an empty row:

solve stuck (Constrained (constraint : constraints) _T) = do
    let other = Constrained (stuck ++ constraints) _T

    …

    case constraint of
        …

        UnifyRows (Row []) _P -> do
            solve [] (Lens.over biplate (deleteRow _P) other)

Similarly, if a constraint unifies zero or more field variables with an empty field (i.e. ) then we can also delete all of those field variables. So we'll define a function to delete field variables:

deleteFields :: [Variable] -> Field -> Field
deleteFields fs (Present _A gs) = Present _A (gs \\ fs)
deleteFields fs (Absent     gs) = Absent     (gs \\ fs)

… and then overload that function to solve constraints with an empty field:

solve stuck (Constrained (constraint : constraints) _T) = do
    let other = Constrained (stuck ++ constraints) _T

    …

    case constraint of
        …

        UnifyFields (Absent []) (Absent fs) -> do
            solve [] (Lens.over biplate (deleteFields fs) other)

Field instantiation - Part 2

Robert Virding, who developed Erlang with me, was famed for his comment. … Singular. The entire stuff he wrote had one comment in the middle of the pattern matching compiler. There was a single line that said "and now for the tricky bit". - Joe Armstrong, The Mess We're In

Field instantiation is the "tricky bit" of this algorithm, so I'll go a bit slower here.

I can explain the interesting part by revisiting the original pathological example:

If we run that through constraint generation we will generate the following constrained type:

Our solver would then drop the trivial constraint and solve three more constraints by substitution:

• substitute with
• substitute with
• substitute with

… which would leave us with this simpler constrained type:

But how do we solve that last remaining constraint?

Earlier we said we need to fix field mismatches when unifying record types, but we can't use the same trick as before because the record type on the right has not one but two row variables. If the right record had just one field variable:

… then we could replace with a fresh unknown field, , and a new row variable :

… and then we could easily unify the two fields and the two rows. However, our record type has two row variables so we can't use the same trick … or can we?

Well, let's go back to the constrained type with two "sibling" row variables:

… and think through what would happen if we were to:

• substitute with
• substitute with

We can't perform either of those two substitutions individually, but we can perform them both simultaneously, and if we do so we get the following new constrained type:

… and now the fields and rows line up so we can decompose that type constraint into a field constraint and a row constraint:

… and then substitution solves the second constraint, leaving us with the same type as before (just with different variable names):

Sibling row variables

There are some limitations on the above trick, though. Specifically, we can only instantiate row variables within a record type subject to the following conditions:

• we must instantiate all row variables within a record type simultaneously

  This is because before instantiation every "sibling" row variable within a record type ranges over the same domain (the same potentially infinite set of fields) and if you instantiate some but not all of the row variables then you end up with siblings with mismatched domains.

• we must instantiate the same set of fields for each row variable within a record type

  If we instantiate different fields for sibling row variables then we end up with same domain mismatch problem.

I'll call the above two conditions the "domain conditions".

Actually, it's a bit more complicated than that because