#14070: Allow ‘unsafe’ deriving strategy, deriving code with ‘unsafeCoerce’ -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): This would be an escape hatch like `unsafeCoerce`, until roles get improved -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14070#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14070: Allow ‘unsafe’ deriving strategy, deriving code with ‘unsafeCoerce’ -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): Is there an ETA on quantified contexts? Do they cover legitimate uses of '`UnsafeDeriving`' or are there cases where it would still be useful? If we must wait a few releases for quantified constraints to hit this can function as a stopgap solution, could be marked as experimental -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14070#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14070: Allow ‘unsafe’ deriving strategy, deriving code with ‘unsafeCoerce’ -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * cc: george.karachalias@…, tom.schrijvers@… (added) Comment: Let's just do `QuantifiedContexts`. Tom and George (cc'd) have a Haskell Symposium 2017 paper, and I think are motivated to push it into GHC. Richard and I are strongly supportive. No ETA though. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14070#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14070: Allow ‘unsafe’ deriving strategy, deriving code with ‘unsafeCoerce’ -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott):

Do they cover legitimate uses of '`UnsafeDeriving`' or are there cases where it would still be useful?

My hunch is that just about every use case for this proposed `unsafe newtype` deriving strategy would be subsumed by the ability to have quantified contexts involving `Coercible`. To use your earlier example: {{{#!hs class MonadJoin m where join_ :: m (m a) -> m a newtype M m a = M (m a) deriving newtype MonadJoin }}} In a brave new quantified world, this would generate code to the effect of: {{{#!hs instance (forall a. Coercible (m (M m a)) (m (m a)), MonadJoin m) => MonadJoin (M m) where join_ = coerce @(forall a. m (m a) -> m a) @(forall a. M m (M m a) -> M m a) join_ }}} Where the `forall a. Coercible (m (M m a)) (m (m a))` bit is needed to convince the typechecker that one can `coerce` underneath `m` in the right spot. Another possible design for this would be to use an implication constraint instead: {{{#!hs instance (forall a b. Coercible a b => Coercible (m a) (m b), MonadJoin m) => MonadJoin (M m) where join_ = coerce @(forall a. m (m a) -> m a) @(forall a. M m (M m a) -> M m a) join_ }}} Would this always be the right thing to do? My gut feeling is "yes", since if you can coerce between `m (M m a)` and `m (m a)` (for any `a`), it feels like you should be able to coerce between `m a` and `m b` for _any_ pair of inter-`Coercible` types `a` and `b`. But I haven't worked out the full details yet, so this is purely speculation on my end for the time being.

Incidentally is it possible to coerce `Lens s a = forall f. Functor f => (a -> f a) -> (s -> f s)` types?

Sure! The example you gave only doesn't typecheck because you didn't expand the `Lens` type synonym: {{{#!hs {-# LANGUAGE InstanceSigs #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} import Unsafe.Coerce type Lens s a = forall f. Functor f => (a -> f a) -> (s -> f s) class X f where x :: Lens (f a) a newtype WrappedX f a = WrapX (f a) instance X t => X (WrappedX t) where x :: forall a f. Functor f => (a -> f a) -> WrappedX t a -> f (WrappedX t a) x = unsafeCoerce x' where x' :: (a -> f a) -> t a -> f (t a) x' = x @t @a }}} This is important, since the `f` needs to scope over both `x` and `x'`. In your example, the `f` tucked underneath the two occurrences of the `Lens` type synonyms were distinct. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14070#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14070: Allow ‘unsafe’ deriving strategy, deriving code with ‘unsafeCoerce’ -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | QuantifiedContexts Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): I will respond in full in a bit but Replying to [comment:7 RyanGlScott]:

This is important, since the `f` needs to scope over both `x` and `x'`. In your example, the `f` tucked underneath the two occurrences of the `Lens` type synonyms were distinct.

Ah yes, the million ISK question is whether GHC can coerce that automatically: or does that enter `ImpredicativeTypes` territory? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14070#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14070: Allow ‘unsafe’ deriving strategy, deriving code with ‘unsafeCoerce’ -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | QuantifiedContexts, deriving Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): GHC can "coerce" that just fine (roles notwithstanding) if you do it the way `GeneralizedNewtypeDeriving` generates code (pretend I'm using `coerce` instead of `unsafeCoerce`): {{{#!hs {-# LANGUAGE ImpredicativeTypes #-} {-# LANGUAGE InstanceSigs #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} import Unsafe.Coerce type Lens s a = forall f. Functor f => (a -> f a) -> (s -> f s) class X f where x :: Lens (f a) a newtype WrappedX f a = WrapX (f a) instance X t => X (WrappedX t) where x = unsafeCoerce @(forall a. Lens (t a) a) @(forall a. Lens (WrappedX t a) a) x }}} I put "coerce" in quotes because we're not actually coercing the `f`. Rather, the two occurrences of `f` tucked underneath the `Lens`es get unified. But you were writing this instance in a somewhat unorthodox way where you manually applied `@t` and `@a` to `x`, but neglected `f` (`f` isn't in scope the way you wrote it, but it's hiding underneath the `Lens`). Because of this, GHC was unable to conclude that the `f` in `x'` and the `f` in the instance signature were the same. Happily, writing instances the way `GeneralizedNewtypeDeriving` does (by visibly applying the full type signatures to `coerce`) doesn't suffer from this problem. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14070#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14070: Allow ‘unsafe’ deriving strategy, deriving code with ‘unsafeCoerce’ -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | QuantifiedContexts, deriving Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Replying to [comment:12 Iceland_jack]:

ah! So this means we can also derive optic methods once `QuantifiedContexts` lands

I'm not sure what's special about "optic methods", but yes, I'm pretty sure `QuantifiedContexts` should let us be able to use `GeneralizedNewtypeDeriving` in any situation where we need to `coerce` underneath a higher-kinded type parameter (like the `f` in `Lens (f a) a`).

and (possibly / hopefully) that we can derive everything derivable?

I mean, saying that you can derive everything that is derivable is a bit of a tautology. But I think the answer to that question is yes :)

It does require `ImpredicativeTypes` written in the Haskell surface language, wasn't that removed in 8.2?

Alas, `ImpredicativeTypes` hasn't been removed yet. Simon laid out a proposal for doing so, while still preserving the ability to use `TypeApplications` to instantiate polytypes (as in `coerce @(forall a. Lens (t a) a)`) [https://mail.haskell.org/pipermail/ghc- devs/2016-September/012824.html here], but no one has drafted that up into a concrete GHC proposal yet. I'd do this myself, except I'm far too unfamiliar with the typechecker details to come up with a comprehensive document explaining how this change would work. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14070#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14070: Allow ‘unsafe’ deriving strategy, deriving code with ‘unsafeCoerce’ -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | QuantifiedContexts, deriving Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Replying to [comment:14 Iceland_jack]:

I was wondering if there is anything GNDerivable in theory that would be outside of GHC's reach even given quantified constraints (and your hunch).. Just as `join` is 'derivable' but is not derivable currently.

In theory, //everything// is GNDable - after all, `GeneralizedNewtypeDeriving` is just a glorified `unsafeCoerce` hack. The real question is if something is GNDable //and// type-safe, but beyond GHC's reach. The only cases that I'm aware of where this happens involves roles, so if you find other scenarios where `GeneralizedNewtypeDeriving` emits code that doesn't typecheck, file another ticket. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14070#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14070: Allow ‘unsafe’ deriving strategy, deriving code with ‘unsafeCoerce’ -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | QuantifiedContexts, deriving Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Replying to [comment:16 Iceland_jack]:

Should the ticket be closed or kept open until we have `QuantifiedContexts`?

That's up to you. At some point (be it now or after `QuantifiedContexts` is a thing) I'd like to have a ticket for modifying `GeneralizedNewtypeDeriving` to infer quantified `Coercible` constraints. I'd be fine with either making this the ticket for that feature, or for closing this in favor of a different one. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14070#comment:17 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14070: Allow ‘unsafe’ deriving strategy, deriving code with ‘unsafeCoerce’ -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | QuantifiedContexts, deriving Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Quantified contexts wouldn't make that example work. There's a bigger problem with that example in that there's no way for GHC to reason about how it should be derived. To pick a slightly simpler example: {{{ λ> newtype Foo a = Foo (forall xx. Show a => IO xx) deriving newtype Functor <interactive>:7:67: error: • Can't make a derived instance of ‘Functor Foo’ with the newtype strategy: cannot eta-reduce the representation type enough • In the newtype declaration for ‘Foo’ }}} This error message hints at the fundamental limitation here that `GeneralizedNewtypeDeriving` faces. Let's describe algorithmically what GND is doing on a simple example: {{{#!hs class C (a :: * -> *) newtype N a = N (UnderlyingType a) deriving newtype C }}} First, in order for this to work about, one must be able to drop a type variable from `N`, since the last parameter to `C` is of kind `* -> *`. We //can// do this, so everything is good so far. But there's another issue: GHC wants to emit an instance like this: {{{#!hs instance <context> => C N }}} What should `<context>` be? To determine this, GHC must be able to take `UnderlyingType a`, eta reduce one type variable from it, attach `C` in front, and simplify. For instance, if `UnderlyingType a` is `Identity a`, then GHC would first emit: {{{#!hs instance C Identity => C N }}} And then simplify `C Identity` as much as possible. (For instance, if there is a `C Identity` instance in scope, the derived instance would simplify down to just `instance C N`.) But if `UnderlyingType a = forall xx. Show a => IO xx`, this won't work out, since `a` can't be eta reduced! (The ability to eta reduce a type is really a property that only certain types exhibit, such as data type constructors.) Not even an `unsafe newtype` strategy would help you here, since the issue doesn't concern typechecking code, but rather coming up with the code that needs to be typechecked in the first place. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14070#comment:19 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14070: Allow ‘unsafe’ deriving strategy, deriving code with ‘unsafeCoerce’ -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: duplicate | Keywords: | QuantifiedConstraints, deriving Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #2893 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => closed * resolution: => duplicate * related: => #2893 Comment: We've decided not to hack an unsafe deriving strategy into GHC, and instead go with `QuantifiedConstraints`. Therefore, closing in favor of #2893. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14070#comment:21 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14070: Allow ‘unsafe’ deriving strategy, deriving code with ‘unsafeCoerce’ -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: duplicate | Keywords: | QuantifiedConstraints, deriving Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #2893 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Sure. Here's a test adapted from the original post: {{{#!hs {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE ImpredicativeTypes #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE QuantifiedConstraints #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} import Data.Coerce import Data.Kind class Monad m => MonadJoin m where join_ :: m (m a) -> m a newtype T m a = T (m a) deriving (Functor, Applicative, Monad) type Representational1 f = (forall a b. Coercible a b => Coercible (f a) (f b) :: Constraint) instance (MonadJoin m, Representational1 m) => MonadJoin (T m) where join_ = coerce @(forall a. m ( m a) -> m a) @(forall a. T m (T m a) -> T m a) join_ }}} As this is essentially the code that this proposed deriving strategy would have generated (except with `unsafeCoerce` replaced with `coerce`). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14070#comment:23 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14070: Allow ‘unsafe’ deriving strategy, deriving code with ‘unsafeCoerce’ -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: duplicate | Keywords: | QuantifiedConstraints, deriving Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #2893 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Replying to [comment:24 simonpj]:

Do we allow this?

Sadly, not without `ImpredicativeTypes` (which `GeneralizedNewtypeDeriving` enables under the hood).

(It's impredicative -- but in a benign way.)

Indeed. You had proposed a way to allow this without `ImpredicativeTypes` [https://mail.haskell.org/pipermail/ghc-devs/2016-September/012940.html here]—do you think you could create a GHC proposal about this? The details of this are far beyond my understanding, so it'd take someone with your level of expertise to get the details right in such a hypothetical proposal. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14070#comment:25 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14070: Allow ‘unsafe’ deriving strategy, deriving code with ‘unsafeCoerce’ -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: duplicate | Keywords: | QuantifiedConstraints, deriving Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #2893 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Ben Gamari ): In [changeset:"7df589608abb178efd6499ee705ba4eebd0cf0d1/ghc" 7df5896/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="7df589608abb178efd6499ee705ba4eebd0cf0d1" Implement QuantifiedConstraints We have wanted quantified constraints for ages and, as I hoped, they proved remarkably simple to implement. All the machinery was already in place. The main ticket is Trac #2893, but also relevant are #5927 #8516 #9123 (especially! higher kinded roles) #14070 #14317 The wiki page is https://ghc.haskell.org/trac/ghc/wiki/QuantifiedConstraints which in turn contains a link to the GHC Proposal where the change is specified. Here is the relevant Note: Note [Quantified constraints] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ The -XQuantifiedConstraints extension allows type-class contexts like this: data Rose f x = Rose x (f (Rose f x)) instance (Eq a, forall b. Eq b => Eq (f b)) => Eq (Rose f a) where (Rose x1 rs1) == (Rose x2 rs2) = x1==x2 && rs1 >= rs2 Note the (forall b. Eq b => Eq (f b)) in the instance contexts. This quantified constraint is needed to solve the [W] (Eq (f (Rose f x))) constraint which arises form the (==) definition. Here are the moving parts * Language extension {-# LANGUAGE QuantifiedConstraints #-} and add it to ghc-boot-th:GHC.LanguageExtensions.Type.Extension * A new form of evidence, EvDFun, that is used to discharge such wanted constraints * checkValidType gets some changes to accept forall-constraints only in the right places. * Type.PredTree gets a new constructor ForAllPred, and and classifyPredType analyses a PredType to decompose the new forall-constraints * Define a type TcRnTypes.QCInst, which holds a given quantified constraint in the inert set * TcSMonad.InertCans gets an extra field, inert_insts :: [QCInst], which holds all the Given forall-constraints. In effect, such Given constraints are like local instance decls. * When trying to solve a class constraint, via TcInteract.matchInstEnv, use the InstEnv from inert_insts so that we include the local Given forall-constraints in the lookup. (See TcSMonad.getInstEnvs.) * topReactionsStage calls doTopReactOther for CIrredCan and CTyEqCan, so they can try to react with any given quantified constraints (TcInteract.matchLocalInst) * TcCanonical.canForAll deals with solving a forall-constraint. See Note [Solving a Wanted forall-constraint] Note [Solving a Wanted forall-constraint] * We augment the kick-out code to kick out an inert forall constraint if it can be rewritten by a new type equality; see TcSMonad.kick_out_rewritable Some other related refactoring ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ * Move SCC on evidence bindings to post-desugaring, which fixed #14735, and is generally nicer anyway because we can use existing CoreSyn free-var functions. (Quantified constraints made the free-vars of an ev-term a bit more complicated.) * In LookupInstResult, replace GenInst with OneInst and NotSure, using the latter for multiple matches and/or one or more unifiers }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14070#comment:27 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler