[Agda] heterogeneous equality

[Andrés Sicard-Ramírez]

Hi,

On Mon, Mar 3, 2008 at 9:16 AM, Nils Anders Danielsson
<nils.anders.danielsson at gmail.com> wrote:
> 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?

I couldn't find the answer for this two years and a half old question.
Was it answered anywhere?

Thanks,

-- 
Andrés