#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