Overlapping instances for poly-kinded data

[Richard Eisenberg]

I believe this is expected behavior, for sufficiently nuanced expectations.

Let's consider a simpler story:

```
{-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-}

class ShowType a where
  showType :: a -> String

instance ShowType Int where
  showType _ = "Int"
instance ShowType Bool where
  showType _ = "Bool"

instance ShowType [a] where
  showType _ = "list"
instance {-# OVERLAPPING #-} ShowType String where
  showType _ = "String"

class ShowType a => IsListy a where
  isListy :: a -> String

instance IsListy Int where
  isListy x = showType x ++ " is not listy."
instance IsListy Bool where
  isListy x = showType x ++ " is not listy."

instance IsListy [a] where
  isListy x = showType x ++ " is indeed listy."
```

The Int and Bool instances are just for exposition -- they don't really matter.

The question here is: should the `IsListy [a]` instance compile? (Spoiler: It does.) It seems at first that the instance should not compile. For the definition of `isListy` to compile, GHC needs an instance for `ShowType [a]`. But, we don't know what `a` is... so there are two potential instances. Indeed, if we add the following definition

```
topIsListy :: [a] -> String
topIsListy x = showType x ++ " is indeed listy."
```

we get a "several potential instances" error. Yet, the instance compiles.

The reason is that GHC is a little cheeky when picking instances while in the middle of an instance declaration: it skips the check for extra instances that might match. To understand why this happens, imagine adding the following declaration to our module:

```
instance {-# OVERLAPPING #-} IsListy String where
  isListy _ = "Strings sure are listy!"
```

Such an instance makes sense in this context. Yet, if GHC did a full overlap check when compiling the  `IsListy [a]` instance, that instance would fail, and we'd never get to write the nice, coherent set of instances we see here (including the new overlapping string instance). So, GHC skips the overlap check.

The exact same scenario is happening with your Show instance. The new orphans are overlapping, but GHC skips the overlap check in your Show instance. PolyKinds is not at issue.

Personally, I'm ambivalent on this skip-overlap-check-in-instances behavior. I understand why it's there, but I find it somewhat disturbing. If others do, too, I wouldn't be against opening a debate about this design decision.

I hope this is helpful!
Richard

On Apr 12, 2015, at 3:33 PM, Gabor Greif <ggreif at gmail.com> wrote:

> Hi all,
> 
> I observe a strange "deriving Show" behaviour for my data type Foo
> that has proxies:
> 
> data Foo :: k -> * where
>  Foo :: Proxy t -> Foo t
> 
> deriving instance Show (Foo t)
> 
> This works as expected. But now I add
> 
> instance {-# OVERLAPPING #-} KnownSymbol s => Show (Proxy (s :: Symbol)) where
>  show = ('#' :) . symbolVal
> instance {-# OVERLAPPING #-} KnownNat n => Show (Proxy (n :: Nat)) where
>  show = ('#' :) . show . natVal
> 
> these orphan instances, and "deriving Show" won't pick them up. When I
> go and specialise
> deriving instance {-# OVERLAPPING #-} KnownNat t => Show (Foo (t :: Nat))
> deriving instance {-# OVERLAPPING #-} KnownSymbol s => Show (Foo (s :: Symbol))
> 
> then it seems to work allright. Is polykinded derivation so different
> from the monokinded one? Or is this simply a bug?
> 
> (a more elaborate WIP example can be found here:
> https://code.google.com/p/omega/source/browse/mosaic/CloudAtlas.hs?spec=svn2465&r=2465)
> 
> Cheers,
> 
>    Gabor
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs