Overlapping instances for poly-kinded data

[Simon Peyton Jones]

|  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 at 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 <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
|  > _______________________________________________
|  > ghc-devs mailing list
|  > ghc-devs at haskell.org
|  > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
|  
|  _______________________________________________
|  ghc-devs mailing list
|  ghc-devs at haskell.org
|  http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs