Check consistency of instances for unboxed records

[flupe]

When defining an unboxed record, one gets to define new instances for type classes on the Agda side. Those instances never get compiled, and code that uses instances over boxed values will compile to code that uses underlying instances over the underlying values.

Hence, when defining an instance for a unboxed record, we:

• need to make sure an instance for the underlying (boxed) type exists.
• the behavior of the instance for the unboxed record is "consistent" with the one for the underlying type.