is it possible to get some more verbose information on how Haskell works with instances? Some of these combinations seem impossible. Even just a link to a document explaining the mechanism would be appreciated
How Haskell works with instances is very simple. You're dealing with multiple experimental language extensions provided by GHC, so the primary source of information is the GHC User's Guide.
Is there a more specific definition to how OverlappingInstances work? I feel like I'm missing something (like maybe the "specificity" argument works only with jthe type variables, not with the number of constraints...)
Your guess is correct. From the User's Guide section explaining OverlappingInstances
:
When GHC tries to resolve, say, the constraint
C Int Bool
, it tries to match every instance declaration against the constraint, by instantiating the head of the instance declaration. For example, consider these declarations:instance context1 => C Int a where ... -- (A) instance context2 => C a Bool where ... -- (B) instance context3 => C Int [a] where ... -- (C) instance context4 => C Int [Int] where ... -- (D)
The instances (A) and (B) match the constraint
C Int Bool
, but (C) and (D) do not. When matching, GHC takes no account of the context of the instance declaration (context1
etc).
Think of it as something like patterns vs. guards:
instanceOfC Int a | context1 Int a = ...
instanceOfC a Bool | context2 a Bool = ...
Because type classes are "open" there's no well-defined order of matches as there is with a function, which is why there are instead restrictions on "patterns" that match the same arguments. I elaborated further on the analogy to patterns and guards in a previous answer.
If we translate your instances to a pseudo-function via the above analogy, the result is something like this:
hNoNils (e:l) | e == EmptyNil = hNoNils l
hNoNils (e:l) = e : hNoNils l
hNoNils [] = []
Knowing that "guards" are ignored when choosing a "pattern" it's clear that the first two patterns can't be distinguished.
But I expect you'd like to know how to make things work, not merely why they currently don't. (N.B. -- I don't have a GHC at hand right now so this is all from memory and has not been tested. I may have gotten a few details wrong.)
There are several ways of dealing with this sort of thing. Probably the most general is a two-step process of first using type functions in the context of a generic instance, then deferring to a specific instance of a auxiliary class that takes extra parameters:
class FooConstraint a b r | a b -> r -- some sort of type predicate
-- the "actual" type function we want
class (FooConstraint a b result, FooAux a b result c) => Foo a b c | a b -> c
-- a single maximally generic instance
instance (FooConstraint a b result, FooAux a b result c) => Foo a b c
-- this class receives the original a and b as arguments, but also the
-- output of the predicate FooConstraint
class FooAux a b result c | a b result -> c
-- which lets us indirectly choose instances based on a constraint
instance ( ... ) => FooAux a b True c
-- more instances, &c.
It's a huge hassle, as you can see, but sometimes it's all you have.
Fortunately, your case is much easier. Recall the translation to a pseudo-function above--would you actually write that function that way? Of course not, because it would be clearer like this:
hNoNils (EmptyNil:l) = hNoNils l
hNoNils (e:l) = e : hNoNils l
hNoNils [] = []
Since EmptyNil
is a constructor you can pattern match on it, simplifying the code and avoiding a superfluous Eq
constraint.
The same applies to the type-level equivalent: replace the type equality predicate with simply using EmptyNil
in the instance head:
instance (HNoNils l l') => HNoNils (HCons EmptyNil l) l'
instance (HNoNils l l') => HNoNils (HCons e l) (HCons e l')
instance HNoNils HNil HNil
This version will still fail in one situation, which there's really no good way around. If the type list contains type variables that could potentially unify with EmptyNil
--keeping in mind that constraints are ignored at this point, and that GHC has to account for arbitrary instances being later added for EmptyNil
--the first two instances are unavoidably ambiguous.
Ambiguity issues of this last sort can be partly avoided by ensuring that all relevant cases can be distinguished. For example, rather than removing a type like EmptyNil
, you could instead have type constructors like:
data Some a
data None
And then write a type-level version of catMaybes
:
class CatOptions l l'
instance (CatOptions l l') => CatOptions (HCons None l) l'
instance (CatOptions l l') => CatOptions (HCons (Some e) l) (HCons e l')
instance CatOptions HNil HNil
This limits ambiguity problems to only the situations that are truly ambiguous, rather than cases where a list contains e.g. a polymorphic type representing an arbitrary Num
instance.