TooManyFields.agda

module TooManyFields where

postulate X : Set

record D : Set where
  field x : X

d : X -> D
d x = record {x = x; y = x}