From: Peter Lammich <lammich@in.tum.de>

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

From: Tobias Nipkow <nipkow@in.tum.de>

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.

Tobias

smime.p7s

From: Jakub Kądziołka <kuba@kadziolka.net>

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.

Regards,

Jakub Kądziołka

From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>

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

Jeremy

Last updated: Jan 25 2022 at 01:11 UTC