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

[GHC]

#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