Pretty-printing checked output is not equal to pretty-printing unchecked output

[timsueberkrueb]

Consider the following example:

-- | The Martin-Löf equality type.
data Eq(implicit a: Type, x y: a) {
    -- | The reflexivity constructor.
    Refl(implicit a: Type, x: a): Eq(a:=a, x, x)
}

-- | Proof of symmetry of equality.
def Eq(x, y).sym(implicit a: Type, x y: a): Eq(a:=a, y, x) {
    Refl(a, x) => Refl(a:=a, x)
}

Our dependent pattern matching substitutes the unification not only on the rhs's expected type but also on the rhs expression. This means that the AST changes during typechecking. Therefore, it makes a difference whether we pretty-print the checked vs. the unchecked output:

cargo run -- fmt examples/foo.pol

-- | The Martin-Löf equality type.
data Eq(implicit a: Type, x y: a) {
    -- | The reflexivity constructor.
    Refl(implicit a: Type, x: a): Eq(a:=a, x, x)
}

-- | Proof of symmetry of equality.
def Eq(x, y).sym(implicit a: Type, x y: a): Eq(a:=a, y, x) { Refl(a, x) => Refl(a:=a, x) }

cargo run -- fmt --checked examples/foo.pol

-- | The Martin-Löf equality type.
data Eq(implicit a: Type, x y: a) {
    -- | The reflexivity constructor.
    Refl(implicit a: Type, x: a): Eq(a:=a, x, x)
}

-- | Proof of symmetry of equality.
def Eq(x, y).sym(implicit a: Type, x y: a): Eq(a:=a, y, x) { Refl(a, x) => Refl(a:=<a>, y) }

[BinderDavid]

Here is one idea I had about how to solve this: First, observe that substitution only changes variables. So we could change the AST node for variables to add an extra field:

struct Variable {
    ...,
    /// Elaborated due to dependent. pattern matching.
    elaborated: Option<Exp>
 }

And then we define an operation elaborate which is just like substitution, but fills in this elaboration instead of replacing the variable. We could also avoid code duplication by reusing the substitution code appropriately.