[Agda] heterogeneous equality

[Andrés Sicard-Ramírez]

2010/9/9 Nils Anders Danielsson <nad at cs.nott.ac.uk>:
> On 2010-09-09 05:07, Andrés Sicard-Ramírez wrote:
>>
>> I couldn't find the answer for this two years and a half old question.
>> Was it answered anywhere?
>
> Ulf and I discussed it in private.
>
> The question is irrelevant now, because type constructors are no longer
> (supposed to be) automatically injective.

Does it mean that using the option --injective-type-constructors your
example should type check?

-- 
Andrés