Changes between Version 5 and Version 6 of SafeHaskell/NewOverlappingInstances


Ignore:
Timestamp:
May 14, 2015 9:52:14 PM (4 years ago)
Author:
dterei
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • SafeHaskell/NewOverlappingInstances

    v5 v6  
    3131interface despite the unsafe internals.
    3232
    33 == Instance Selection ==
     33== GHC 7.10 & Earlier ==
     34
     35This is how overlapping instances were handled in GHC 7.10 and earlier.
     36
     37=== Instance Selection ===
    3438
    3539In the security use-case, if we have code involving overlapping
     
    5256else.
    5357
    54 == Instances and Safe-Inference ==
     58=== Instances and Safe-Inference ===
    5559
    5660How do we infer safety given the above policy? We take a conservative
     
    7074need to be conservative.
    7175
    72 === Bug in Safe vs Safe-Inferred ===
     76==== Bug in Safe vs Safe-Inferred ====
    7377
    7478Interestingly, this isn't exactly true. Consider the following module:
     
    123127`-XOverlappingInstances` specified needs to be tested.
    124128
    125 == New Overlapping Instances -- a.k.a Instance Specific Pragmas ==
    126 
    127 GHC 7.10 is adding in instance specific pragmas to control overlapping
     129== GHC 7.12 & Later ==
     130
     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.
     134
     135=== Overlapping Instance Pragmas ===
     136
     137GHC 7.10 added in instance specific pragmas to control overlapping
    128138of instances. They consist of:
    129139
     
    135145  equivalent to the old `-XOverlappingInstances` behavior.
    136146
    137 Addressing them individually for code compiled with `-XSafe`:
    138 
    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.
    152 
    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).
    159 
    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.
    161 
    162 === Safe Inference ===
    163 
    164 Safe inference becomes a trickier question with the new pragmas.
    165 Firstly, an easy decision:
    166 
    167 * `-XOverlappingInstances` -- causes a module to be inferred unsafe.
    168 
    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:
    174 
    175 * `OVERLAPPABLE` -- leaves M in current state (i.e., safe).
    176 * `OVERLAPPING` -- switches M to be unsafe.
    177 * `OVERLAPS` -- switches M to be unsafe.
    178 
    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.
    183 
    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 ===
     148
     149==== Can't detect declaration of overlapping instances ====
     150
     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.
     156
     157For example, it is perfectly reasonable to write two modules
     158as follows:
     159
     160{{{
     161module A where
     162
     163  instance C [a] where { op = ... }
     164
     165module B where
     166
     167   instance C [Int] where { op = ... }
     168}}}
     169
     170Neither module in isolation declares overlapping instances. It's
     171only when we import both modules and call `op` that we can detect
     172the overlap.
     173
     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.
     177
     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.
     185
     186However, MPTC make this tricky. So we decided to detect unsafe
     187overlaps at call-sites, not at declaration.
     188
     189==== Safe Inference ====
     190
     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.
     195
     196=== GHC 7.12 Approach ===
     197
     198We detect unsafe overlaps at call-sites and ensure symmetry
     199between `-XSafe` and safe-inference.
     200
     201The rule to determine if a particular call-site of a type-class
     202method is '''unsafe''' is:
     203
     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`.
     210
     211=== Where this check applies ===
     212
     213This check is enforced in `-XSafe` and `-XTrustworthy` modules.
     214We also use it to infer safety. `-XUnsafe` modules don't have the
     215check enforced.
     216
     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.
     224
     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.