When defining a fancy version of an existing datatype (e.g. All as a fancy version of List), it would be nice to be able to mark it as the ornamented version of that datatype in agda2hs, so they can both be compiled to the same Haskell datatype. The condition here would be that compiling the ornamented version should result in the exact same Haskell code as the base type (modulo naming of the type).

Similarly, we could allow marking functions (e.g. map on the All type) as an ornamented version of an existing function, and compile calls to it to calls to that existing function. Again, this would require both versions of the function to compile down to the precise same Haskell code (modulo naming of the function).