Never substitute unification variables for variables

[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)
}

When printing the checked AST, we observe:

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) }

Here, a:=a was substituted to a:=<a> where <a> is a hole corresponding to the inserted metavariable ?0 from the scrutinee type Eq(?0, x, y).

[BinderDavid]

The problem is that when we compute a unifying substitution for use in dependent pattern matching then unsolved metavariables shouldn't occur in the RHS of the substitution. Otherwise we might have accidental information flowing from inside a clause to the outside. (Cp. the problems described in the OutsideIn paper)