[Agda] pattern matching bug?

[Chris Casinghino]

Hi all,

The following code causes Agda to complain:

  Panic: blocked by dot pattern
  when checking the definition of exp-function

\begin{code}
data Typ : Set where
  Top : Typ
  All : Typ → Typ

id : Typ → Typ
id Top     = Top
id (All t) = All (id t)

data Exp : Typ → Set where
  Any1  : ∀ {t : Typ} → Exp t
  Any2  : ∀ {t : Typ} → Exp (id t)
  TLam  : ∀ {t : Typ} → Exp (All t)

exp-function : (t : Typ) → Exp t → Exp t
exp-function t       Any1 = ?
exp-function (All t) TLam = ?
exp-function .(id t) (Any2 {t}) = ?
\end{code}


This is as small as I could get the example.  It's not a huge problem
for me because Agda stops complaining if move the Any2 clause of
exp-function before the TLam clause or make the t argument implicit.
But, is this a bug?  I don't understand the error.

Deleting the Any1 constructor and its clause in exp-function triggers
a different error instead:

  Cannot split on the constructor Any2
  when checking the definition of exp-function

And deleting the TLam constructor and clause makes the error go away
entirely.

--Chris Casinghino