Changes between Version 5 and Version 6 of SafeHaskell/NewOverlappingInstances

May 14, 2015 9:52:14 PM (5 years ago)



  • SafeHaskell/NewOverlappingInstances

    v5 v6  
    3131interface despite the unsafe internals.
    33 == Instance Selection ==
     33== GHC 7.10 & Earlier ==
     35This is how overlapping instances were handled in GHC 7.10 and earlier.
     37=== Instance Selection ===
    3539In the security use-case, if we have code involving overlapping
    54 == Instances and Safe-Inference ==
     58=== Instances and Safe-Inference ===
    5660How do we infer safety given the above policy? We take a conservative
    7074need to be conservative.
    72 === Bug in Safe vs Safe-Inferred ===
     76==== Bug in Safe vs Safe-Inferred ====
    7478Interestingly, this isn't exactly true. Consider the following module:
    123127`-XOverlappingInstances` specified needs to be tested.
    125 == New Overlapping Instances -- a.k.a Instance Specific Pragmas ==
    127 GHC 7.10 is adding in instance specific pragmas to control overlapping
     129== GHC 7.12 & Later ==
     131We have significantly changed how overlapping instances work in
     132GHC 7.12 and later. This is both to improve the design, and also to
     133make use of the new overlapping instance pragmas added in GHC 7.10.
     135=== Overlapping Instance Pragmas ===
     137GHC 7.10 added in instance specific pragmas to control overlapping
    128138of instances. They consist of:
    135145  equivalent to the old `-XOverlappingInstances` behavior.
    137 Addressing them individually for code compiled with `-XSafe`:
    139 * `OVERLAPPABLE` -- We will adopt the convention that all-bets
    140   are off with such instances. Code compiled with `-XSafe` will be
    141   allowed to overlap such instances, even if they are in a different
    142   module.
    143 * `OVERLAPPING` -- This will keep the current instance behavior. Code
    144   in `-XSafe` code can only overlap instances declared `OVERLAPPING`
    145   if those instances are from the same module.
    146 * `OVERLAPS` -- Ideally we'd like to remove this pragma as we think
    147   it's security implications (since it implies OVERLAPPABLE and
    148   OVERLAPPING which both have very different security properties) are
    149   subtle and could easily lead to developers expressing the wrong
    150   policy. Instead, we'd prefer developer specify both instance overlap
    151   policies manually.
    153 This enables more flexibility than before with Safe Haskell. Now you
    154 can allow your instances to be overlapped through `OVERLAPPABLE`
    155 (i.e., somewhat analogous to being an open type class), or
    156 simply overlap your own instances through `OVERLAPPING` but not export
    157 that property to the world (i.e., somewhat analogous to being a closed
    158 type class).
    160 The nice thing is the new design also encourages library authors to be specific about the overlap property of their instances. So hopefully fixing the current bug with safe-inference and overlapping instances has even less of an effect.
    162 === Safe Inference ===
    164 Safe inference becomes a trickier question with the new pragmas.
    165 Firstly, an easy decision:
    167 * `-XOverlappingInstances` -- causes a module to be inferred unsafe.
    169 What should the use of `OVERLAPPABLE`, `OVERLAPPING` and `OVERLAPS` do
    170 though? Let's assume a module M is considered safe by default, and
    171 when we consider each instance declared in a module M, we can either
    172 leave M considered safe, or switch M to be unsafe (a one-way
    173 transition). Our initial thoughts are the following:
    175 * `OVERLAPPABLE` -- leaves M in current state (i.e., safe).
    176 * `OVERLAPPING` -- switches M to be unsafe.
    177 * `OVERLAPS` -- switches M to be unsafe.
    179 Why this? Well because if we infer a module M containing only
    180 `OVERLAPPABLE` instances as Safe, then compiling M instead with
    181 `-XSafe` will give you a module M' with the same semantics as M when
    182 consumed.
    184 However, if M contains `OVERLAPPING` or `OVERLAPS` instances, then
    185 consumers of M get slightly different behavior when M is considered
    186 safe compared to when it is considered unsafe. Safe inference
    187 shouldn't change the behavior of a module, so we must infer M as
    188 unsafe.
     147=== Problems with GHC 7.10 Approach ===
     149==== Can't detect declaration of overlapping instances ====
     151We previously try to detect when a module declared overlapping
     152instances and mark it unsafe when it did (at least for inference).
     153This doesn't work. Overlapping instances are a global property.
     154We only know when an overlap occurs at a particular call site for
     155a type-class method.
     157For example, it is perfectly reasonable to write two modules
     158as follows:
     161module A where
     163  instance C [a] where { op = ... }
     165module B where
     167   instance C [Int] where { op = ... }
     170Neither module in isolation declares overlapping instances. It's
     171only when we import both modules and call `op` that we can detect
     172the overlap.
     174Due to the new instance specific pragmas in GHC 7.10, we could
     175simply declare all modules that declare `OVERLAPPABLE` instances
     176to be unsafe. But this would be heavily over-approximate.
     178A closer approximation would be to declare all orphan instances
     179that are marked `OVERLAPPABLE` as unsafe. Since, if at a
     180type-class method call site, if the instance selected is not
     181an orphan instance, then I must either depend on the type
     182declared in the same module as the instance, or I must depend
     183on the type-class declared in the same module. In both situations
     184the dependency is explicit, so safe.
     186However, MPTC make this tricky. So we decided to detect unsafe
     187overlaps at call-sites, not at declaration.
     189==== Safe Inference ====
     191GHC 7.10 had a different rule for `-XSafe` modules and
     192safe-inferred modules with respect to overlapping instances.
     193This lack of symmetry is a huge problem. See the bugs it
     194causes for example, list earlier.
     196=== GHC 7.12 Approach ===
     198We detect unsafe overlaps at call-sites and ensure symmetry
     199between `-XSafe` and safe-inference.
     201The rule to determine if a particular call-site of a type-class
     202method is '''unsafe''' is:
     204* Most specific instance, '''Ix'''', defined in an `-XSafe`
     205  compiled module.
     206* '''Ix''' is an orphan instance or a multi-parameter-type-class.
     207* At least one overlapped instance, '''Iy''', is both:
     208    * From a different module than '''Ix'''
     209    * '''Iy''' is not marked `OVERLAPPABLE`.
     211=== Where this check applies ===
     213This check is enforced in `-XSafe` and `-XTrustworthy` modules.
     214We also use it to infer safety. `-XUnsafe` modules don't have the
     215check enforced.
     217A nice extension may be to tie this check into whether a module was
     218imported as a safe import or not. This wouldn't change `-XSafe`
     219modules, but would allow selective application of the rule to
     220`-XTrustworthy` and `-XUnsafe` modules. So far we haven't done this
     221as it isn't clear where an instance is imported from, since they
     222can be brought into scope recursively by multiple imports. It also
     223complicates safe imports and isn't clear if the gain is worth it.
     225One way forward would be to implement this extension, and when an
     226import is imported through multiple paths, to take the conservative
     227join of the two.