Currently, the expression

```
merge { T = λ(t : Type) → λ(x : t) → x } < T = Natural >
```

does not typecheck, either in the standard or in the Haskell implementation. dhall-haskell gives a confusing error

```
Error: Unbound variable: t
```

The standard does not allow this to typecheck because the relevant judgment:

```
Γ ⊢ t :⇥ { y : ∀(x : A₀) → T₀, ts… }
Γ ⊢ u :⇥ < y : A₁ | us… >
Γ ⊢ (merge { ts… } < us… > : T₁) : T₂
A₀ ≡ A₁
↑(-1, x, 0, T₀) = T₁
──────────────────────────────────── ; `x` not free in `T₀`
Γ ⊢ merge t u : T₀
```

has the condition "`x`

not free in `T₀`

". This condition disallows the function

```
λ(t : Type) → λ(x : t) → x
```

as a handler because it has type:

```
∀(t : Type) → ∀(x : t) → t
```

In this type, `t`

is free in `∀(x : t) → t`

so the condition fails.

My question is: why? What is this condition for? It seems perfectly reasonable to me that

```
merge { T = λ(t : Type) → λ(x : t) → x } < T = Natural >
```

should normalize to:

```
λ(x : Natural) → x
```

Is there some weird edge case of the type system requires this condition?