Proposal: GHC.Generics marked UNSAFE for SafeHaskell

[Edward Kmett]

Am I correct in understanding your issue arises from manually rolled
instances of Generic, not from Generic itself?

Wouldn't then perhaps the better fix be to resurrect the old rule for
derived Typeable instances and apply it to Generic and Generic1 instead?

The new rule would be that if you hand-implemented Generic or Generic1 in
your module it isn't Safe.

That would make it so that derived Generic, Generic1 would be considered
Safe, and you wouldn't break literally every user of the library who care
about Safe Haskell.

As it stands the things are damn-near impossible to get right instantiating
them by hand anyways, so I expect this would affect only 1 or 2 users
rather than all of them!

-Edward


On Sun, Oct 6, 2013 at 5:32 PM, Ryan Newton <rrnewton at gmail.com> wrote:

> Hi all,
>
> We had a discussion on haskell-cafe, which only confirmed the
> unreliability of "Eq" and "Ord".  Fine.  But if I instead want to define a
> SafeEq class and instances based on GHC.Generics, then I can't have users
> writing Generic instances that lie about the structure of their types.
>
> But as you can see this module is currently marked "Trustworthy":
>
>
> http://www.haskell.org/ghc/docs/7.4.1/html/libraries/ghc-prim-0.2.0.0/GHC-Generics.html
>
> I simply propose that this is changed to "Unsafe"! [1]
>
> *Context:*
> The bottom line is that I believe in the Safe-Haskell mission here, and I
> want to be able to deliver practical libraries that give a strong guarantee
> that types can't be broken.   Currently, the LVish<http://www.cs.indiana.edu/~rrnewton/papers/2013_07_LVish_quasiDet_working_draft.pdf>library has one big hole in it because of this Eq/Ord limitation; the
> problem is documented here<http://www.cs.indiana.edu/~rrnewton/haddock/lvish/Control-LVish.html#g:1>
> .
>    If we can provide incontrovertible Safe-Haskel guarantees, this is a
> huge, qualitative difference compared to what's possible in the C++, Java's
> and MLs of the world.  There are plenty of libraries that provide
> guarantees like "deterministic parallelism" IFF the user does everything
> right and breaks no rules (CnC, Pochoir, etc).  But we can do better!
>
> Best,
>   -Ryan
>
> [1]  Small detail... some of these bindings, like the class name "Generic"
> itself, will still need to be accessible from a Trustworthy library.  I
> propose GHC.Generics.Safe for that, following existing precedent.
>
> On Sun, Oct 6, 2013 at 5:18 PM, Ryan Newton <rrnewton at gmail.com> wrote:
>
>> Thanks for the responses all.
>>
>> I'm afraid the point about GHC.Generics got lost here.  I'll respond and
>> then rename this as a specific library proposal.
>>
>> I don't want to fix the world's Eq instances, but I am ok with requiring
>> that people "derive Generic" for any data they want to put in an LVar
>> container.  (From which I can give them a SafeEq instance.)
>>
>> It's not just LVish that is in this boat.... any library that tries to
>> provide deterministic parallelism outside of the IO monad has some very
>> fine lines to walk.  Take a look at Accelerate.  It is deterministic (as
>> long as you run only with the CUDA backend and only on one specific GPU...
>> otherwise fold topologies may look different and non-associative folds may
>> leak).  Besides, "runAcc" does a huge amount of implicit IO (writing to
>> disk, calling nvcc, etc)!  At the very least this could fail if the disk if
>> full.  But then again, regular "pure" computations fail when memory runs
>> out... so I'm ok grouping these in the same bucket for now.  "Determinism
>> modulo available resources."
>>
>> A possible problem with marking "instance Eq" as an unsafe feature is
>>> that many modules would be only Trustworthy instead of Safe.
>>>
>>
>> My proposal is actually more narrow than that.  My proposal is to mark
>> GHC.Generics as Unsafe.
>>
>> That way I can define my own SafeEq, and know that someone can't break it
>> by making a Generic instance that lies.  It is very hard for me to see why
>> people should be able to make their own Generic instances (that might lie
>> about the structure of the type), in Safe-Haskell.
>>
>>>
>>> That would go against my "every purely functional module is
>>> automatically safe because the compiler checks that it cannot launch the
>>> missiles" understanding of Safe Haskell.
>>>
>>
>>  Heh, that may already be violated by the fact that you can't use other
>> extensions like OverlappingInstances, or provide your own Typeable
>> instances.
>>
>>
>>>
>>> Actually, Eq instances are not unsafe per se, but only if I also use
>>> some other module that assumes certain properties about all Eq instances in
>>> scope. So in order to check safety, two independent modules (the provider
>>> and the consumer of the Eq instance) would have to cooperate.
>>
>>
>> I've found, that this is a very common problem that we have when trying
>> to make our libraries Safe-Haskell compliant -- often we want to permit and
>> deny combinations of modules.  I don't have a solution I'm afraid.
>>
>>
>>
>
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://www.haskell.org/mailman/listinfo/ghc-devs
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20131007/bd6ba344/attachment.html>