[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):

 So what remains now is to decide about the behaviour of "incoherent".
 Here is a possible re-draft:
 {{{
 Suppose that, in some client module, we are searching for an instance
 of the target constraint (C ty1 .. tyn). The search works like this.

  * Find all instances I that match the target constraint; that is, the
    target constraint is a substitution instance of I. These instance
    declarations are the candidates.

  * Eliminate any candidate IX for which both of the following hold:
    * There is another candidate IY that is strictly more specific;
      that is, IY is a substitution instance of IX but not vice versa.

    * Either IX is overlappable or IY is overlapping.

  * If only one candidate remains, pick it. Otherwise if all remaining
    candidates are incoherent, pick an arbitrary candidate. Otherwise fail.

  * If the selected candidate (from the previous step) is not
    incoherent, then find all non-candidate instances that unify
    with the target constraint. Such non-candidates instances
    might match when the target constraint is further
    instantiated. If all of them are incoherent, proceed; if not,
    the search fails.

  * Return the selected candidate.
 }}}
 The difference is that we are slightly more permissive in the case of
 incoherent instances: if the selected candidate is incoherent, then we
 ignore all unifying ones.

 That would allow us to write
 {{{
 instance {-# INCOHERENT #-} Typeable (n::Nat) where ...
 instance (Typeable f, Typeable a) => Typeable (f a) where ...
 }}}
 as was proposed in the original Description of this ticket, rather than
 making the `(f a)` instance incoherent.

 I think this would affect practically no one, and would accept a few more
 programs.  So I don't think it's very controversial.

 Simon

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