Overlapping instances for polykinded data
Simon Peyton Jones
simonpj at microsoft.com
Mon Apr 13 07:48:52 UTC 2015
 Personally, I'm ambivalent on this skipoverlapcheckininstances
 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 agree that it's a "bit disturbing". Here's the comment that justifies it. If someone can think of a better way, I'm all ears.
Simon
Note [Subtle interaction of recursion and overlap]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider this
class C a where { op1,op2 :: a > a }
instance C a => C [a] where
op1 x = op2 x ++ op2 x
op2 x = ...
instance C [Int] where
...
When typechecking the C [a] instance, we need a C [a] dictionary (for
the call of op2). If we look up in the instance environment, we find
an overlap. And in *general* the right thing is to complain (see Note
[Overlapping instances] in InstEnv). But in *this* case it's wrong to
complain, because we just want to delegate to the op2 of this same
instance.
Why is this justified? Because we generate a (C [a]) constraint in
a context in which 'a' cannot be instantiated to anything that matches
other overlapping instances, or else we would not be executing this
version of op1 in the first place.
It might even be a bit disguised:
nullFail :: C [a] => [a] > [a]
nullFail x = op2 x ++ op2 x
instance C a => C [a] where
op1 x = nullFail x
Precisely this is used in package 'regexbase', module Context.hs.
See the overlapping instances for RegexContext, and the fact that they
call 'nullFail' just like the example above. The DoCon package also
does the same thing; it shows up in module Fraction.hs.
Conclusion: when typechecking the methods in a C [a] instance, we want to
treat the 'a' as an *existential* type variable, in the sense described
by Note [Binding when looking up instances]. That is why isOverlappableTyVar
responds True to an InstSkol, which is the kind of skolem we use in
tcInstDecl2.
 Original Message
 From: ghcdevs [mailto:ghcdevsbounces at haskell.org] On Behalf Of
 Richard Eisenberg
 Sent: 12 April 2015 18:11
 To: Gabor Greif
 Cc: ghcdevs
 Subject: Re: Overlapping instances for polykinded data

 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 skipoverlapcheckininstances
 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?spe
 > c=svn2465&r=2465)
 >
 > Cheers,
 >
 > Gabor
 > _______________________________________________
 > ghcdevs mailing list
 > ghcdevs at haskell.org
 > http://mail.haskell.org/cgibin/mailman/listinfo/ghcdevs

 _______________________________________________
 ghcdevs mailing list
 ghcdevs at haskell.org
 http://mail.haskell.org/cgibin/mailman/listinfo/ghcdevs
More information about the ghcdevs
mailing list