#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