[Agda] "Hiding of record parameters"

[Sergei Meshveliani]

Dear Agda developers,

You wrote yesterday (on the bug tracker) about fixing the bug of 

  Hiding of record parameters leads to hiding mismatch in 
  checkInternal (#1759).

Probably this implies a certain change/restriction in the record usage.
Because  Development Agda of March 3 2016  does not accept some of my
code related to the record usage.

Can you, please, formulate: 
what is the change in the record declaration and usage?

Regards, 

------
Sergei