Overlapping instances for poly-kinded data
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
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
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@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
| 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 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 type-checking 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 'regex-base', 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: ghc-devs [mailto:ghc-devs-bounces@haskell.org] On Behalf Of
| Richard Eisenberg
| Sent: 12 April 2015 18:11
| To: Gabor Greif
| Cc: ghc-devs
| Subject: Re: Overlapping instances for poly-kinded 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 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
participants (3)
-
Gabor Greif -
Richard Eisenberg -
Simon Peyton Jones