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

the way I have understood this - correct me if I am wrong - is that to prove that ('a, 'b) tycon is in some type class, the system needs to know unambiguously what type classes 'a amd 'b have to be in - there is no backtracking / trying multiple possibilities - presumably for efficiency reasons


On 17/2/21 12:04 am, Tobias Nipkow wrote:
The type system requires that your type constructor signatures satisfy a property called coregularity. If you have two type constructor signatures
kappa :: (S1,...) C
kappa :: (T1,...) D
and D is a subclass of C then Ti must be a subsort of Si. Otherwise terms do not have the principal types. With your two declarations you would lose the pricipal types property.


On 16/02/2021 13:52, Peter Lammich wrote:
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


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