[Agda] Should adding eta-equality help here?

[Martin Stone Davis]

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