Repeating type variables in MultiParamTypeClasses instance heads

Hello Haskell-Cafe, I have a question regarding the rules on type class instances with the MultiParamTypeClasses extension. For single-parameter type classes, there is the restriction that an instance head must have the form `C (T a1 ... an)`, where `C` is a type class, `T` is a data type constructor and `a1 ... an` are distinct type variables ( https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/instances.html ). To my knowledge, this restriction ensures the impossibility of potential overlap between instances (except for the case where two instance heads are equivalent, but this case is caught by an error message). This restriction can be lifted with the FlexibleInstances extension, so that instances like `instance C (a, a, b)` and `instance C (a, b, b)` are allowed. As can be seen in this example, FlexibleInstances introduces the potential of overlap with single-parameter type classes. When using MultiParamTypeClasses without FlexibleInstances, the current restrictions on instance heads are similiar to those for single-parameter classes. For each parameter, the instance type must have the form `(T a1 ... an)` with `a1 ... an` being distinct from one another, but type variables can be shared between instance types. Therefore, instances like `instance D [a] [a] [b]` and `instance D [a] [b] [b]` are allowed and do cause potential overlap. If there was the restriction of all type variables in the instance head being different from one another however, I think there would be no potential for overlap, just like with single-parameter type classes. To me, these instances allowed by MultiParamTypeClasses seem similar to the single-parameter class instances that are only possible with FlexibleInstances. And just like FlexibleInstances for single-parameter class instances, they introduce potential overlap, so that the MultiParamTypeClasses extension by itself becomes less "safe" than it otherwise would be. Therefore, it seems reasonable to me to only allow these repeated type variables in instance heads with the FlexibleInstances extension. So, is there a good reason for the design choice of allowing these kinds of overlap without FlexibleInstances? Am I missing something here? Or are the current rules the way they are because of historic reasons? Best regards, Leif-Erik Krüger

On Thu, 6 May 2021, Leif-Erik Krüger wrote:
So, is there a good reason for the design choice of allowing these kinds of overlap without FlexibleInstances? Am I missing something here?
I am surprised. I just tried it with different GHC versions, all of them accept those overlapping instances without enabling FlexibleInstances. {-# LANGUAGE MultiParamTypeClasses #-} module FlexibleInstance where class C a b c where instance C [a] [a] [b] where instance C [a] [b] [b] where

On Thu, May 06, 2021 at 10:51:32PM +0200, Henning Thielemann wrote:
{-# LANGUAGE MultiParamTypeClasses #-} module FlexibleInstance where
class C a b c where
This class has an empty interface, it just builds triples of types that imply a constraint. No matter how many such triples one creates, there can't be any conflict between them.
instance C [a] [a] [b] where instance C [a] [b] [b] where
These don't conflict. -- Viktor.

Even without a method you can trigger the overlapping error. Consider the following program. class C a b c instance C [a] [a] [b] instance C [a] [b] [b] f :: C a b c => a -> b -> c -> Bool f _ _ _ = True g = f [True] [True] [True] The use of 'f' in 'g' produces the following message. Overlapping instances for D [Bool] [Bool] [Bool] arising from a use of ‘f’ Matching instances: instance D [a] [a] [b] instance D [a] [b] [b] • In the expression: f [True] [True] [True] Cheers, Finn On 06/05/2021 23:05, Viktor Dukhovni wrote:
On Thu, May 06, 2021 at 10:51:32PM +0200, Henning Thielemann wrote:
{-# LANGUAGE MultiParamTypeClasses #-} module FlexibleInstance where
class C a b c where
This class has an empty interface, it just builds triples of types that imply a constraint. No matter how many such triples one creates, there can't be any conflict between them.
instance C [a] [a] [b] where instance C [a] [b] [b] where
These don't conflict.
participants (4)
-
Finn Teegen
-
Henning Thielemann
-
Leif-Erik Krüger
-
Viktor Dukhovni