Pattern match interfering with calc

Stream: general

[Seul Baek]

I'm currently working with equality elimination, and I frequently use patterns like (eq::l) when equality constraints are encoded as lists. I found that this interferes with the calc enviroment in weird ways. Here's the minimal example I found so far:

lemma foo : ∀ x : list unit, unit
| []      := ()
| (eq::_) :=
  begin
    have h0 : 0 = 0 :=
    (calc 0
        = 0 : rfl
    ... = 0 : rfl)
  end

invalid occurrence of field notation
state:
foo : list unit → unit,
eq : unit,
_x : list unit
⊢ unit

The problem here seems to be that Lean isn't taking eq in the pattern as an arbitrary term of type unit, but as the actual eq : Π {α : Sort u_1}, α → α → Prop (the problem goes away when I rename it to something like x). But this is strange since if Lean considered eq to be the latter, it would usually give a typechecking error and inform you that this eq cannot occur in a list of units. That's precisely what it does when there is, say, a tt in its place.