[Agda] heterogeneous equality

[Nils Anders Danielsson]

On Mon, Mar 3, 2008 at 10:44 AM, Ulf Norell <ulfn at cs.chalmers.se> wrote:
>
> The unification performed when pattern matching only handled data
> constructors (not type constructors), so Tm G nat and Tm G' nat didn't unify
> (with G' := G). Fixed now.

I have a related issue. The following does not type check:

data _≡_ {a : Set1} (x : a) : a -> Set where
  refl : x ≡ x

proj₁ : forall {a₁ b₁ a₂ b₂ : Set} ->
        (a₁ -> b₁) ≡ (a₂ -> b₂) -> a₁ ≡ a₂
proj₁ refl = refl

Agda complains about the pattern refl (a₁ != a₂). In light of your
recent patch, is there any reason not to allow also this function?

-- 
/NAD