Opened 18 months ago

Closed 17 months ago

Last modified 16 months ago

#8745 closed bug (fixed)

GeneralizedNewtypeDeriving is still not Safe

Reported by: goldfire Owned by:
Priority: normal Milestone: 7.8.1
Component: Compiler Version: 7.8.1-rc1
Keywords: Safe Cc: nomeata
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: should_fail/TcCoercibleFailSafe
Blocked By: Blocking:
Related Tickets: Differential Revisions:

Description

In GHC 7.8, GeneralizedNewtypeDeriving (GND) is type-safe, due to the advent of roles. Although GND allows looking through unimported constructors, the notion of abstraction has changed -- for a type to be fully abstract in 7.8, it must not export its constructors, and the roles of all its parameters must be nominal. Thus, it would seem that GND should be Safe; that is, in the Safe Haskell subset. See also #5498.

Currently, GND is not considered Safe.

Along similar lines, the Coercible and coerce mechanism could be considered Safe, but there is no way to import these into a Safe module (they are in GHC.Exts).

Change History (27)

comment:1 Changed 18 months ago by thoughtpolice

  • Cc nomeata added

The GND change seems reasonable to me, and I believe we discussed it prior to this (but I can't find the mailing list post just yet) - we just need to remove -XGeneralizedNewtypeDeriving from unsafeFlags in DynFlags.

I'm not so sure about Coerce though, at least not yet - we're still considering it somewhat experimental I think, so perhaps exposing it to Safe Haskell isn't the best idea just yet.

Joachim, what are your thoughts on this? Do you think we should consider Coercible as safe? If so, I'm willing to defer to you here (and I'll even write the patch - but not sure where to export it from - perhaps a Trustworthy module called GHC.Coerce?)

comment:2 Changed 18 months ago by goldfire

The comments I've seen in relation to this are all in #5498.

GND is now actually built on top of coerce, so I think it's a little incongruent to have one be Safe but not the other.

To be fair, I'm not 100% sure that GND should be Safe, myself. While I am as confident as I can be about its type safety, it is very easy to imagine a library author omitting a key role annotation that would allow clients to (perhaps unwittingly) break class coherence or invariants. For example, if base's Set doesn't have a role annotation, it would be very easy to cause the Set operations to misbehave.

Simon PJ has advocated (see #5498) that GND should be Safe, on the other hand.

My goal in creating this ticket is to make a reasoned decision on the matter, as opposed to letting inertia make the decision for us.

comment:3 Changed 18 months ago by nomeata

We have some special handling in Safe mode in place where we do the Coerible thing, but it is neither well tested nor well discussed. (getCoercibleInst in TcInteract)

Currently, in Safe Mode, the following additional restrictions exist when checking whether something is Coercible:

To coerce under a type constructor, all data constructors of all type constructors involved in the definition of that type constructors need to be in scope.

No additional constraint is put on unfolding a newtype, but there we already require the constructor to be in scope.

I believe that this condition is sufficient for “the use can implement coerce himself (ignoring the run-time cost)”. If anything, it might turn out too strong.

If that works as intended, Coercible and GND should be safe. There might possibly be ways to break it, maybe with different modules, some safe and some not... but that would simply be bugs then, and I’m not claiming bug freeness.

A trustworthy GHC.Coerce might be nice. Or maybe even Data.Coerce? After all the interface could be provided by other compilers as well... Not only for Safe, but to avoid people having to import the mingle-mangle of GHC.Exts.

comment:4 Changed 18 months ago by goldfire

I had forgotten about this detail. With this in place (is it tested by anything in the testsuite?), I'm much more in favor of labeling GND and coerce as Safe. It's possible that the (rather draconian, admittedly) check that Joachim (nomeata) describes could be relaxed in the future once library authors are more familiar with role annotations.

I no longer see a downside to making GND and coerce Safe.

comment:5 Changed 18 months ago by goldfire

I've found a weird corner case that is very relevant.

Consider

class Foo a where ...
type role Foo representational
data PackFoo a where
  MkPF :: Foo a => PackFoo a
instance Foo Int where ...
newtype Age = MkAge Int
instance Foo Age where ...
incoherent :: PackFoo Age
incoherent = coerce (MkPF :: PackFoo Int)
useIncoherent = case incoherent of MkPF -> {- here, we two incompatible instances of Foo Age available! -}

The problem, as I see it, boils down to the role annotation on Foo, which allows users to create incoherence. Should we perhaps disallow role annotations on classes in Safe Haskell? It would be analogous to the restrictions on overlapping instances, I think.

comment:6 Changed 18 months ago by nomeata

  • Test Case set to should_fail/TcCoercibleFailSafe

With this in place (is it tested by anything in the testsuite?)

One simple test case is in place (typecheck/should_fail/TcCoercibleFailSafe).

class Foo a where ... type role Foo representational

Why is that even accepted? I thought role annotation can only stricten roles (i.e. P→N, P→R, R→N), and we have decided that classes have role nominal by default, so I would expect type role Foo representational to be rejected even in non-Safe Haskell.

comment:7 Changed 18 months ago by goldfire

The role annotation story is this: the annotations, if provided, simply override defaults (phantom for datatypes, nominal for classes). Then role inference happens (annotations or no). If, after inference, the annotations disagree with the inferred roles, the annotation is rejected. Because it's perfectly type-safe to have a class with a representational parameter, the role annotation is accepted and works. This can be useful if, say, someone wanted to have something like Coercible implemented in user-land somehow -- note that Coercible's parameters are representational.

One way forward here is to allow role annotations on classes only when we have IncoherentInstances. In fact, I rather like that solution -- a role annotation on a class quickly leads to the possibility of incoherence, and this solution also neatly prohibits such annotations in Safe Haskell. Thoughts?

comment:8 Changed 18 months ago by nomeata

One way forward here is to allow role annotations on classes only when we have IncoherentInstances. In fact, I rather like that solution -- a role annotation on a class quickly leads to the possibility of incoherence, and this solution also neatly prohibits such annotations in Safe Haskell. Thoughts?

That’s what I was about to propose as well.

comment:9 Changed 18 months ago by goldfire

Great. I've made #8773 to track that offshoot of this bug. I expect to do it and push tomorrow.

comment:10 Changed 18 months ago by thoughtpolice

  • Milestone set to 7.8.1

comment:11 Changed 18 months ago by thoughtpolice

  • Blocked By 8773 added

comment:12 Changed 18 months ago by goldfire

  • Blocked By 8773 removed

#8773 fixed.

comment:13 Changed 18 months ago by Austin Seipp <austin@…>

In a8a01e742434df11b830ab99af12d9045dfcbc4b/ghc:

Fix #8745 - GND is now -XSafe compatible.

As discussed in the ticket, after the landing of #8773, GND is now
-XSafe compatible.

This fixes the test fallout as well. In particular SafeLang07 was
removed following in the steps of SafeLang06, since it no longer failed
from GND, but failed due to roles and was thus invalid.

The other tests were tweaked to use TemplateHaskell instead of GND in
order to trigger safety warnings.

Signed-off-by: Austin Seipp <[email protected]>

comment:14 Changed 18 months ago by thoughtpolice

  • Status changed from new to merge

comment:15 Changed 18 months ago by thoughtpolice

  • Resolution set to fixed
  • Status changed from merge to closed

Merged in 7.8.

comment:16 Changed 17 months ago by goldfire

Did this fix also export coerce from a Trustworthy module?

comment:17 Changed 17 months ago by thoughtpolice

Ah, no, it did not. I forgot that. We can still do this under the caveat that coerce is still experimental, but I'm literally making the RC2 srcdist as we speak... So it'll have to wait for the final release at best.

comment:18 Changed 17 months ago by goldfire

  • Resolution fixed deleted
  • Status changed from closed to new

Reopening the ticket, as without a Safe way of importing coerce, this issue isn't fully solved.

comment:19 Changed 17 months ago by thoughtpolice

For the record, unless there are any other suggestions, I'll likely take Joachim's suggestion of putting this in Data.Coerce. Any other suggestions?

comment:20 Changed 17 months ago by nomeata

I’m still on holidays with bad connection, otherwise I’d do it. Data.Coerce sounds good, which should be the haddock home module. GHC.Exts should then only re-export that module.

comment:21 Changed 17 months ago by Austin Seipp <austin@…>

In f932b79948f0f8e2ac354cdcaea21c5b7c59a27a/base:

Create Data.Coerce (#8745)

Data.Coerce is a Trustworthy module which safely exports both
`Coercible` and `coerce` for use by users, as it can now be considered
safe under role checking.

See the ticket for details.

Signed-off-by: Austin Seipp <[email protected]>

comment:22 Changed 17 months ago by thoughtpolice

  • Status changed from new to merge

comment:23 Changed 17 months ago by thoughtpolice

  • Resolution set to fixed
  • Status changed from merge to closed

Merged in 7.8 for RC2.

comment:24 Changed 17 months ago by Herbert Valerio Riedel <hvr@…>

In 44dec750a618a89202f80dcd695e5eb9fb74a74f/base:

Tweak documentation and update changelog.md

This adds release note entries to changelog and tweaks Haddock comments
with respect to the recent commits 1a9abe7a1a3c7 (re #8797) and
f932b79948f0 (re #8745)

Signed-off-by: Herbert Valerio Riedel <[email protected]>

comment:25 Changed 17 months ago by goldfire

See also 59722295bb8da8f01d37356fbed6aef7321a8195/ghc which was meant to reference this ticket.

comment:26 Changed 16 months ago by Austin Seipp <austin@…>

In 8f7303774237a8b0787d98c5ab6f605e3e897f19/ghc:

Revert "Fix #8745 - GND is now -XSafe compatible."

See #8827 - for now, we're making GND unsafe again.

This also fixes the tests since they were originally not using the new
unicode quote style we're using.

This reverts commit a8a01e742434df11b830ab99af12d9045dfcbc4b.

comment:27 Changed 16 months ago by simonpj

Don't miss the long discussion in #8827

Note: See TracTickets for help on using tickets.