Automatic ext lemmas fails when using parameters

Stream: general

[Praneeth Kolichala]

The following:

import tactic.ext

section
parameter (α : Type)

@[ext]
structure TestStruct :=
(x : α)

end

fails with the following error message:

injection tactic failed, argument must be an equality proof where lhs and rhs are of the form (c ...), where c is a constructor
α : Type,
x y : α,
ᾰ : {x := x} = {x := y}
⊢ {x := x}.x = {x := y}.x

The example works if parameter is changed to variable. Why does this happen, and are there any workarounds?

[Eric Wieser]

The usual workaround is to not ever use parameter; we pretty much avoid it everywhere in mathlib