[Agda] ANNOUNCE: Agda 2.2.10

[Jean-Philippe Bernardy]

On Sun, Feb 20, 2011 at 7:23 PM, Nils Anders Danielsson <nad at chalmers.se> wrote:

> * Irrelevant declarations.

I tried to define:

data Eq (A : Set) (a : A) : .A -> Set where
  refl : Eq A a a

(which works fine)

but:

subst : ∀ A a b -> (P : A -> Set) -> Eq A a b -> P a -> P b
subst A a .a p refl = ?

gives the rather unhelpful message:

_ != _ of type A
when checking that the pattern refl has type Eq A a _

Can somebody offer insight to what is going on?

Thanks!
-- JP