Unclear why instances are overlapping

Question

When I try compiling the following code with GHC 7.10.3, it throws an "Overlapping Instances" error at me:

{-# LANGUAGE DataKinds         #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs             #-}
{-# LANGUAGE KindSignatures    #-}
{-# LANGUAGE TypeOperators     #-}

module Main where

class Bar a where
  bar :: Foo a

-- Instance #1
instance Bar '[a] where
  bar = C1

-- Instance #2
instance (Bar as) => Bar (a ': as) where
  bar = C2 bar

data Foo :: [*] -> * where
  C1 :: Foo '[a]
  C2 :: Foo as -> Foo (a ': as)

main :: IO ()
main = undefined

foobar :: Foo '[Int]
foobar = bar

28 col 10 error: Overlapping instances for Bar '[Int] arising from a use of ‘bar’

Matching instances:

instance Bar '[a] -- Defined at test.hs:13:10

instance Bar as => Bar (a : as) -- Defined at test.hs:17:10

In the expression: bar

In an equation for ‘foobar’: foobar = bar

Clearly '[Int] is an instance of Bar through #1. Now I am surprised, because (from my understanding of the situtation) '[Int] = (Int ': '[]) cannot be an instance of Bar through #2 since '[] itself is not an instance of Bar (which is required). I have vague memories of constraints on instanciation not being what I thought it was, and I suspect that the problem here lies in ... (Bar as) => ... though I cannot be sure. Any help appreciated.

@user2297560 No, the analysis in the question is correct on this point: only when as ~ [] are a ': as and '[a] the same. — Daniel Wagner
@DanielWagner Ah, I see. Thanks. This kind of type level stuff is still a bit magical to me. — user2297560

ErikR ErikR · Accepted Answer · 2016-05-29T21:55:21

Chris Done has written up a blog post about this:

http://chrisdone.com/posts/haskell-constraint-trick

His makes this observation:

The constraints of an instance don’t have anything to do with deciding whether an instance is picked from the list of instances available. Constraints only apply after GHC has already decided it’s going with this instance.

So so constraint present in:

instance Bar as => Bar (a ': as)

doesn't preclude GHC from matching it against '[Int].

Unclear why instances are overlapping

1 Answers