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.

[flupe]

Related PR: #332

[jespercockx]

The recently merged compile-to pragma (#430) has basically the same problem as unboxed records: one could have instances for the fancy version of the type that are inconsistent with the instances for the type it is compiled to. The solution might be that we should require these instances to be marked with a compile-to pragma too. Then when checking this pragma we could make sure that the instance is compatible with the one of the "base" type.