
#9242: Implement {-# OVERLAPPABLE #-} and {-# INCOHERENT #-} pragmas -------------------------------------+------------------------------------ Reporter: simonpj | Owner: diatchki Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Description changed by simonpj: Old description:
The language extensions `-XIncoherentInstances` and `-XOverlappingInstances` (described in [http://www.haskell.org/ghc/docs/latest/html/users_guide/type-class- extensions.html#instance-overlap the user manual]) apply to every instance declaration in the module. Internally, however, GHC records this information on a per-instance-declaration basis.
It would be much better for the programmer to be able to control these matters on a per-instance-declaration basis. Thus: {{{ instance Show a => Show [a] where {-# OVERLAPPABLE #-} ...
instance Show [Char] where ... }}} We came across the need for this when discussing the `Typeable` instances. We have a generic instance like this: {{{ instance (Typeable f, Typeable a) => Typeable (f a) where .... }}} but also want {{{ instance KnownNat n => Typeable (n :: Nat) where ... }}} If we seek `(Typeable (x::Nat))`, we should pick the second instance even though in principle you might imagine that `x` might be instantiated to `(f a)`, for some `f` and `a`. But we know that there are no type constructors `f` of kind `blah -> Nat`, so this can never happen and it's safe to pick the second instance. So a local `{-# INCOHERENT #-}` pragma for this particular instance declaration would be very useful to express this fact. {{{ instance KnownNat n => Typeable (n :: Nat) where {-# INCOHERENT #-} ... }}} Quite apart from this special case, it's plain better to have per- instance control * Rather than a remote per-module flag, the pragma draws attention that ''this particular instance'' is incoherent, overlappable or whatever. * The current situation almost certainly means that more instances are marked overlapping than are really necessary.
I have some design questions. * Where should the pragma appear, syntactically? {{{ instance {-# OVERLAPPABLE #-} Show a => Show [a] where ... or instance Show a => Show [a] {-# OVERLAPPABLE #-} where ... or instance Show a => Show [a] where {-# OVERLAPPABLE #-} }}} Remember that `SPECIALISE INSTANCE` pragmas appear in the third of the above positions, so I mildly favour that.
* The user manual (link above) allows overlap if ''either'' instance is compiled with `-XOverlappingInstances` (see the rules towards the end of [http://www.haskell.org/ghc/docs/latest/html/users_guide/type-class- extensions.html#instance-overlap 7.6.3.5]. It would be more explicit to have two pragmas, one to say "I can be overlapped" and one to say "I can overlap something else". The rule would then be that "either IX is marked `{-# OVERLAPPABLE #-}` or IY is marked `{-# OVERLAPPING #-}`.
New description: The language extensions `-XIncoherentInstances` and `-XOverlappingInstances` (described in [http://www.haskell.org/ghc/docs/latest/html/users_guide/type-class- extensions.html#instance-overlap the user manual]) apply to every instance declaration in the module. Internally, however, GHC records this information on a per-instance-declaration basis. It would be much better for the programmer to be able to control these matters on a per-instance-declaration basis. Thus: {{{ instance Show a => Show [a] where {-# OVERLAPPABLE #-} ... instance Show [Char] where ... }}} We came across the need for this when discussing the `Typeable` instances. We have a generic instance like this: {{{ instance (Typeable f, Typeable a) => Typeable (f a) where .... }}} but also want {{{ instance KnownNat n => Typeable (n :: Nat) where ... }}} If we seek `(Typeable (x::Nat))`, we should pick the second instance even though in principle you might imagine that `x` might be instantiated to `(f a)`, for some `f` and `a`. But we know that there are no type constructors `f` of kind `blah -> Nat`, so this can never happen and it's safe to pick the second instance. So a local `{-# INCOHERENT #-}` pragma for this particular instance declaration would be very useful to express this fact. {{{ instance KnownNat n => Typeable (n :: Nat) where {-# INCOHERENT #-} ... }}} Quite apart from this special case, it's plain better to have per-instance control * Rather than a remote per-module flag, the pragma draws attention that ''this particular instance'' is incoherent, overlappable or whatever. * The current situation almost certainly means that more instances are marked overlapping than are really necessary. I have some design questions. * Where should the pragma appear, syntactically? {{{ instance {-# OVERLAPPABLE #-} Show a => Show [a] where ... or instance Show a => Show [a] {-# OVERLAPPABLE #-} where ... or instance Show a => Show [a] where {-# OVERLAPPABLE #-} }}} Remember that `SPECIALISE INSTANCE` pragmas appear in the third of the above positions, so I mildly favour that. * The user manual (link above) allows overlap if ''either'' instance is compiled with `-XOverlappingInstances` (see the rules towards the end of [http://www.haskell.org/ghc/docs/latest/html/users_guide/type-class- extensions.html#instance-overlap 7.6.3.5]). It would be more explicit to have two pragmas, one to say "I can be overlapped" and one to say "I can overlap something else". The rule would then be that "either IX is marked `{-# OVERLAPPABLE #-}` or IY is marked `{-# OVERLAPPING #-}`. -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9242#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler