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
both instances.

The motivation for this restriction is that if your typeclass defines a
constant, then the overlapping instances would constitute potentially
contradictory definitions.

Jakub Kądziołka

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