[isabelle] Conflict of type arities: What are the constraints on class instantiations?



Hi List,

I have naively tried to define a type-class for types that have more
than one element. However, when trying to make the obvious
instantiations, I get stuck with "Conflict of type arities" error
messages. I could not find any documentation on what the restrictions
are that I'm violating here, and how they are motivated. Any pointers?

  instance prod :: (not_singleton,type) not_singleton ..
  instance prod :: (type,not_singleton) not_singleton 

Conflict of type arities:
  prod :: (type, not_singleton) not_singleton and
  prod :: (not_singleton, type) not_singleton


Peter






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.