Overlapping instances for poly-kinded data
Richard Eisenberg
eir at cis.upenn.edu
Sun Apr 12 17:10:57 UTC 2015
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
More information about the ghc-devs
mailing list