[Agda] Should adding eta-equality help here?

[Andreas Abel]

Hi Martin,

thanks for reporting.  This is a bug in the conversion checker.

eta-equality is turned on for your records by default.  You do not need 
to declare it explicitly.

Cheers,
Andreas
On 15.05.2017 05:24, Martin Stone Davis wrote:
> I wonder if adding eta-equality should help or should even be necessary
> here. In any case, Agda complains with the following error and I'm
> unsure whether this is a bug.
>
> The error:
>
> Sub.super1 /= Sub.super2
> when checking that the expression refl has type
> Sub.super1 fails ≡ Sub.super2 fails
>
> The code:
>
> open import Agda.Builtin.Equality
>
> record Super : Set₁ where
>   eta-equality
>   field
>     set : Set
>
> record Sub : Set₁ where
>   eta-equality
>   field
>     super1 : Super
>     super2 : Super
>     super1=2 : super1 ≡ super2
>
> postulate
>   X : Set
>
> works : Sub
> works .Sub.super1 = record { set = X }
> works .Sub.super2 .Super.set = X
> works .Sub.super1=2 = refl
>
> fails : Sub
> fails .Sub.super1 .Super.set = X
> fails .Sub.super2 .Super.set = X
> fails .Sub.super1=2 = refl
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www.cse.chalmers.se/~abela/