[GHC] #9242: Implement {-# OVERLAPPABLE #-} and {-# INCOHERENT #-} pragmas

[GHC]

#9242: Implement {-# OVERLAPPABLE #-} and {-# INCOHERENT #-} pragmas
-------------------------------------+-------------------------------------
              Reporter:  simonpj     |            Owner:  diatchki
                  Type:  feature     |           Status:  new
  request                            |        Milestone:
              Priority:  normal      |          Version:  7.8.2
             Component:  Compiler    |         Keywords:
            Resolution:              |     Architecture:  Unknown/Multiple
      Operating System:              |       Difficulty:  Unknown
  Unknown/Multiple                   |       Blocked By:
       Type of failure:              |  Related Tickets:
  None/Unknown                       |
             Test Case:              |
              Blocking:              |
Differential Revisions:              |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 Sigh. One last observation.  Read the Description of this ticket.  I
 thought we'd end up with
 {{{
 instance {-# INCOHERENT #-} Typeable (n::Nat) where ...
 instance (Typeable f, Typeable a) => Typeable (f a) where ...
 }}}
 The weird one is the `Typeable (n:Nat)` instance.  Our reasoning is that
 we don't want to worry about instantiations of `n`.  And this is what we
 wrote in the Description.

 But actually the rules above mean that we have to write this
 {{{
 instance Typeable (n::Nat) where ...
 instance {-# INCOHERENT #-} (Typeable f, Typeable a) => Typeable (f a)
 where ...
 }}}
 (and that is indeed what is in `Data.Typeable.Internals` today.  The
 incoherent flag is on the innocent `Typeable (f a)` declaration.

 Obviously incoherence is an area where we don't expect "right" answers.
 But the above does suggest that it could make sense to change the
 behaviour of incoherence, to this: ignoring a non-candidate unifying
 instance when (and only when) there is an incoherent matching instance.

 Here is another example to illustrate
 {{{
 class C a where
   op :: a -> Bool

 instance {-# INCOHERENT? #-} C [a] where
   op x = True

 instance {-# INCOHERENT? #-} C [Int] where
   op x = False

 f :: [a] -> Bool
 f x = op x
 }}}
 Without incoherence, `f` is rejected even with overlapping instances,
 because the choice depends on the instantiation of `a`.  So, which
 instance needs `{-# INCOHERENT #-}` to make it acceptable?  Today the
 answer is the second one; with the change proposed here, it'd be the first
 one.

 I don't feel very strongly about this, but the `Typeable` example (which
 drove the entire thread!) is quite compelling to me.

 Simon

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9242#comment:22>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler