Re: [isabelle] Conflict of type arities: What are the constraints on class instantiations?
On Tue Feb 16, 2021 at 1:52 PM CET, 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?
The restriction in question is that each ground type has at most one
instance of a type class.
> instance prod :: (not_singleton,type) not_singleton ..
> instance prod :: (type,not_singleton) not_singleton
In your example, a product of two non-singleton types would apply to
The motivation for this restriction is that if your typeclass defines a
constant, then the overlapping instances would constitute potentially
This archive was generated by a fusion of
Pipermail (Mailman edition) and