[isabelle-dev] A better policy for the typerep class

[Brian Huffman]

I thought it would be good to clarify my position in a shorter email:

The automatically-generated typerep instances work fine on typedef or  
datatype commands, where the instance resides in the same theory as  
the type definition.

It is also OK if instances are generated *within Typerep.thy* for all  
types defined in earlier theories.

However, if the merging of two theories causes a typerep instance to  
be generated, this is *very bad*.

As far as I can tell, Florian would not necessarily disagree with  
this. His advice to Amine, recommending to contort his theory  
dependencies, has the effect of avoiding theory merges which would  
cause typerep instances to be generated.

My advice is to simply disable theory-merge instance generation. This  
would be much better than the current workaround, which relies on  
carefully preventing this feature from ever being exercised.

If, during a theory merge, the typerep package noticed a missing  
instance, printing an error message would actually be more helpful  
than the current behavior.

- Brian