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

GHC ghc-devs at haskell.org
Sat Aug 2 00:32:08 UTC 2014


#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 dterei):

 I'd like to propose we remove the `OVERLAPS` pragma. Why?

 == Long Version ==
 https://ghc.haskell.org/trac/ghc/wiki/SafeHaskell/NewOverlappingInstances#NewOverlappingInstances
 --a.k.aInstanceSpecificPragmas

 == Short Version (kind-of) ==
 The security implications of OVERLAPPABLE vs. OVERLAPPING are fairly
 different. Remember, in Safe Haskell we apply a policy of only
 allowing instances from a module M compiled with `-XSafe` to overlap
 other instances from module M. If it overlaps (and is the most
 specific overlap) instances from modules other than M then we don't
 allow this to succeed. This is done to ensure that untrusted code
 compiled with `-XSafe` can't alter the behavior of existing code, some
 of which may be part of the TCB and security critical.

 Brining the new finer grained pragmas into the story we get the following:
 * OVERLAPPABLE is the programmer communicating that they can be
 overlapped, an open instance if you will. We want to relax the above
 restriction and allow instances from `-XSafe` modules to overlap
 instances from their own module AND instances declared OVERLAPPABLE
 that reside in any module.
 * OVERLAPPING is the programming simply declaring they may overlap
 less specific instances. We want to keep the above restriction for
 these instances. That is, a instance I1 from a `-XSafe` module M won't
 be able to overlap as the most specific instance, a instance I2 from
 another module if I2 is marked as OVERLAPPING.

 This distinction enables new encodings in Safe Haskell by allowing
 security library authors to distinguish how untrusted code can overlap
 their instances. In some way giving them open vs closed instances.

 This distinction is subtle and important. Having a pragma OVERLAPS
 that implies both glosses over this and will encourage developers to
 use this without much thought.

 ## Safe Inference
 We can also safely infer a module that only has OVERLAPPABLE instances
 as safe, while ones that contain OVERLAPPING or OVERLAPS instances
 must be regarded as unsafe since there is a difference in semantics of
 these pragmas under Safe vs Unsafe.

 So we also have an advantage if developers are more specific about
 what they want, than just defaulting to OVERLAPS.

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


More information about the ghc-tickets mailing list