How does haskell resolve overlapping instances?

Question

Please excuse me if I use the wrong terminology, I am much a beginner in haskell type manipulation... I am trying to use overlapping instances with functional dependencies to do some type-level programming with HLists.

Here my objective is to try and write a typeclass HNoNils l l', where HNoNils l l' means that, with l being a list type (ex: Int : String : EmptyNil : Int : HNil), l' is the corresponding list type without the specific empty type EmptyNil( result of example: Int:String:Int:HNil):

{-# LANGUAGE ExistentialQuantification,
  FunctionalDependencies,
  FlexibleInstances,
  UndecidableInstances,
  OverlappingInstances,
  TypeFamilies #-}

import Data.HList 
import Data.TypeLevel.Bool

--Type Equality operators
--usedto check if a type is equal to another
class TtEq a b eq | a b -> eq
instance     TtEq a a True
instance eq~False => TtEq a b eq 


data EmptyNil = EmptyNil deriving (Show) --class representing empty channel
--class intended to generate a list type with no type of EmptyNil
-- Example: HCons Int $ HCons EmptyNil HNil should give HCons Int HNil
class (HList list, HList out) => HNoNils list out | list -> out 
    where  hNoNils :: list -> out 

-- l gives l' means (HCons EmptyNil l) gives l'
instance (HNoNils l l',TtEq e EmptyNil True ) => HNoNils (HCons e l) l'
    where hNoNils (HCons e l) = hNoNils l

-- l gives l' means (HCons e l) gives (HCons e l') for all e 
instance (HNoNils l l') => HNoNils (HCons e l) (HCons e l')
    where hNoNils (HCons e l) = hCons e $ hNoNils l

--base case
instance  HNoNils HNil HNil
    where hNoNils _ = hNil

testList  = HCons EmptyNil $ HCons EmptyNil HNil
testList1 = HCons "Hello"  $ HCons EmptyNil HNil 
testList2 = HCons EmptyNil $ HCons "World"  HNil
testList3 = HCons "Hello"  $ HCons "World"  HNil

main:: IO ()
main = do
    print $ hNoNils testList  -- should get HNil
    print $ hNoNils testList1 -- should get HCons "Hello" HNil
    print $ hNoNils testList2 -- should get HCons "World" HNil
    print $ hNoNils testList3 -- should get HCons "Hello" (HCons "World" HNil)

When I run this code as-is, however, all my hNoNils calls seem to resolve through the least specific, second, instance declaration, meaning (at least it seems), that for all l, I have HNoNils l l.

Based off of what I have read, with the OverlappingInstances extension, The system is supposed to always resolve to the most specific instance.

Here

• the first instance has the constraints (HNoNils l l',TtEq e EmptyNil True )

• the second instance has the constraints HNoNils l l'

Forgive me if I'm wrong, but it seems like the first instance is more specific than the second, so it should go for that one, right?

I have tried adding constraints to try and get rid of the overlap, namely by adding the seperate, oposite equality constraint to the second instance:

-- l gives l' means (HCons EmptyNil l) gives l'
instance (HNoNils l l',TtEq e EmptyNil True ) => HNoNils (HCons e l) l'
    where hNoNils (HCons e l) = hNoNils l

-- l gives l' means (HCons e l) gives (HCons e l') for all e 
-- added constraint of TtEq e EmptyNil False
instance (HNoNils l l',TtEq e EmptyNil False) => HNoNils (HCons e l) (HCons e l')
    where hNoNils (HCons e l) = hCons e $ hNoNils l

I tried removing the overlapping instance extension here, and I'm getting overlap errors.

Overlapping instances for HNoNils
                                (HCons EmptyNil (HCons [Char] HNil)) (HCons EmptyNil l')
Matching instances:
      instance (HNoNils l l', TtEq e EmptyNil True) =>
               HNoNils (HCons e l) l'
        -- Defined at /home/raphael/Dropbox/IST/AFRP/arrow.hs:32:10
      instance (HNoNils l l', TtEq e EmptyNil False) =>
               HNoNils (HCons e l) (HCons e l')
        -- Defined at /home/raphael/Dropbox/IST/AFRP/arrow.hs:36:10

I don't understand the second match. After all, in this resolution, we have e equal to EmptyNil, so TtEq e EmptyNil True ... right? And for that matter, how does the type system even get to a situation where it's asking this question, after all with the constraints you should never have a situation of the sort HNoNils (Hcons EmptyNil l) (HCons EmptyNil l')), at least I don't think so.

When adding back OverlappingInstances, I get even weirder errors that I don't understand:

 Couldn't match type `True' with `False'
    When using functional dependencies to combine
      TtEq a a True,
        arising from the dependency `a b -> eq'
        in the instance declaration at /home/raphael/Dropbox/IST/AFRP/arrow.hs:23:14
      TtEq EmptyNil EmptyNil False,
        arising from a use of `hNoNils'
        at /home/raphael/Dropbox/IST/AFRP/arrow.hs:53:13-19
    In the second argument of `($)', namely `hNoNils testList2'
    In a stmt of a 'do' block: print $ hNoNils testList2

the second statement, TtEq EmptyNil EmptyNil False, seems to say that an instance has been generated by a function call...? I am a bit confused as to where it came from.

So in trying to figure this out, I was wondering:

• 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

• 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...)

edit: So I tried one of the suggestions of C.A. McCann (removing some of the constraints) to the following:

instance (HNoNils l l') => HNoNils (HCons EmptyNil l) l'

instance (HNoNils l l') => HNoNils (HCons e l) (HCons e l')

instance  HNoNils HNil HNil

Doing this gives me some nasty overlapping instances errors:

Overlapping instances for HNoNils
                                (HCons EmptyNil (HCons [Char] HNil)) (HCons EmptyNil l')
      arising from a use of `hNoNils'
    Matching instances:
      instance [overlap ok] HNoNils l l' => HNoNils (HCons EmptyNil l) l'
        -- Defined at /Users/raphael/Dropbox/IST/AFRP/arrow.hs:33:10
      instance [overlap ok] HNoNils l l' =>
                            HNoNils (HCons e l) (HCons e l')
        -- Defined at /Users/raphael/Dropbox/IST/AFRP/arrow.hs:37:10

I feel as if the resolution method is top down instead of bottom up (where the system would never try to find an instance such as this).

edit 2: By adding a small constraint to the second condition, I got the expected behavior (see McCann's comment on his answer):

-- l gives l' means (HCons EmptyNil l) gives l'
instance (HNoNils l l') => HNoNils (HCons EmptyNil l) l'
    where hNoNils (HCons EmptyNil l) = hNoNils l

-- l gives l' means (HCons e l) gives (HCons e l') for all e 
instance (HNoNils l l',r~ HCons e l' ) => HNoNils (HCons e l) r
    where hNoNils (HCons e l) = hCons e $ hNoNils l

here the added thing is the r~HCons e l' constraint on the second instance.

Answer 1

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.