#14070 closed feature request (duplicate)
Allow ‘unsafe’ deriving strategy, deriving code with ‘unsafeCoerce’
Reported by: | Iceland_jack | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | |
Component: | Compiler | Version: | 8.0.1 |
Keywords: | QuantifiedConstraints, deriving | Cc: | george.karachalias@…, tom.schrijvers@… |
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: |
Description
This
newtype M m a = M (m a) deriving newtype Functor
produces something similar to
instance Functor m => Functor (M m) where fmap :: forall a a'. (a -> a') -> (M m a -> M m a') fmap = coerce (fmap @m @a @a')
but as wiki:Roles2 points out, this fails for methods such as join_
:
class MonadJoin m where join_ :: m (m a) -> m a newtype M m a = M (m a) deriving newtype MonadJoin -- Couldn't match representation of type ‘m (M m a)’ with that of ‘m (m a)’
I think the user should be given the option to respect the roles or not by supplying unsafe
wiki:Commentary/Compiler/DerivingStrategies
newtype M m a = M (m a) deriving unsafe newtype MonadJoin -- -( Produces `unsafeCoerce' instead of `coerce' )- -- instance MonadJoin m => MonadJoin (M m) where -- join_ :: forall a. M m (M m a) -> M m a -- join_ = unsafeCoerce (join_ @m @a)
This lets us (newtype
-) derive a host of instances that we currently can not: Traversable
, Distributive
(currently forbidden due to distribute), Trace, ProfunctorMonad / ProfunctorComonad, ...
It does not seem like lenses (FunctorWithIndex
, FoldableWithIndex
, TraversableWithIndex
) work with this though
Change History (27)
comment:1 Changed 2 years ago by
comment:2 Changed 2 years ago by
I will admit that the devil on my shoulder is trying to coax me into implementing this idea. But at the same time, the angel on my other shoulder is saying I should wait until we have QuantifiedContexts
, which would give us a principled solution to this problem.
I'm unable to pick a side at the moment, so I'll simply wait until I've heard more feedback.
comment:3 Changed 2 years ago by
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
comment:5 Changed 2 years ago by
Cc: | george.karachalias@… tom.schrijvers@… added |
---|
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.
comment:6 Changed 2 years ago by
That sounds excellent, I'm thrilled about this feature.
Incidentally is it possible to coerce Lens s a = forall f. Functor f => (a -> f a) -> (s -> f s)
types?
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. Lens (WrappedX t a) a x = unsafeCoerce x' where x' :: Lens (t a) a x' = x @t @a
fails with
• Could not deduce (Functor f0) arising from a use of ‘x'’ from the context: X t bound by the instance declaration at /tmp/uuu.hs:21:10-25 or from: Functor f bound by the type signature for: x :: Functor f => (a -> f a) -> WrappedX t a -> f (WrappedX t a)
comment:7 follow-ups: 9 12 Changed 2 years ago by
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:
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:
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:
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:
{-# 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.
comment:8 Changed 2 years ago by
Keywords: | QuantifiedContexts added |
---|
comment:9 Changed 2 years ago by
I will respond in full in a bit but
Replying to RyanGlScott:
This is important, since the
f
needs to scope over bothx
andx'
. In your example, thef
tucked underneath the two occurrences of theLens
type synonyms were distinct.
Ah yes, the million ISK question is whether GHC can coerce that automatically: or does that enter ImpredicativeTypes
territory?
comment:10 Changed 2 years ago by
Keywords: | deriving added |
---|
comment:11 Changed 2 years ago by
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
):
{-# 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.
comment:12 follow-up: 13 Changed 2 years ago by
Replying to RyanGlScott:
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 involvingCoercible
.
That's excellent and I hope that is indeed the case. A choice between forall a. Coercible (m (M m a)) (m (m a))
and forall a b. Coercible a b => Coercible (m a) (m b)
in the context is also interesting and makes me wonder if they differ in that example
Replying to RyanGlScott:
Happily, writing instances the way
GeneralizedNewtypeDeriving
.. doesn't suffer from this problem.
ah! So this means we can also derive optic methods once QuantifiedContexts
lands and (possibly / hopefully) that we can derive everything derivable? That would be huge for me and I would be fine with closing this ticket
It does require ImpredicativeTypes
written in the Haskell surface language, wasn't that removed in 8.2?
comment:13 follow-up: 14 Changed 2 years ago by
Replying to 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)
) 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.
comment:14 follow-up: 15 Changed 2 years ago by
Replying to RyanGlScott:
I'm pretty sure
QuantifiedContexts
should let us be able to useGeneralizedNewtypeDeriving
in any situation where we need tocoerce
underneath a higher-kinded type parameter (like thef
inLens (f a) a
).
Okay great
I mean, saying that you can derive everything that is derivable is a bit of a tautology.
It was a lazy question, 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.
comment:15 follow-up: 16 Changed 2 years ago by
Replying to 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.
comment:16 follow-up: 17 Changed 2 years ago by
Replying to RyanGlScott:
The real question is if something is GNDable and type-safe, but beyond GHC's reach.
That's what I was trying to get at, thanks for the explanation Ryan I feel very positive about this. Should the ticket be closed or kept open until we have QuantifiedContexts
?
comment:17 Changed 2 years ago by
Replying to 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.
comment:18 Changed 2 years ago by
I'll keep it, to push the boundaries of what can be derived:
-- instance Alternative Foo where -- empty = Foo (coerce (empty @IO @xx) :: forall xx. IO xx) -- Foo a <|> Foo b = Foo (coerce ((<|>) @IO @xx a b) :: forall xx. IO xx) newtype Foo a = Foo (forall xx. Show a => IO xx) deriving newtype Alternative instance Functor Foo instance Applicative Foo
Unlike Foo
my use case actually is an Alternative
:
type Pure xx a = Given (a -> IO xx) newtype Managed :: Type -> Type where -- Managed = Codensity IO Managed :: (forall xx. Pure xx a => IO xx) -> Managed a instance Alternative Managed where empty :: forall a. Managed a empty = Managed (coerce (empty @IO @xx) :: forall xx. IO xx) (<|>) :: forall a. Managed a -> Managed a -> Managed a Managed a <|> Managed b = Managed (a @xx <|> b @xx :: forall xx. Pure xx a => IO xx)
comment:19 Changed 2 years ago by
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:
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:
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:
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.
comment:20 Changed 20 months ago by
Keywords: | QuantifiedConstraints added; QuantifiedContexts removed |
---|
comment:21 Changed 19 months ago by
Related Tickets: | → #2893 |
---|---|
Resolution: | → duplicate |
Status: | new → closed |
We've decided not to hack an unsafe deriving strategy into GHC, and instead go with QuantifiedConstraints
. Therefore, closing in favor of #2893.
comment:22 Changed 19 months ago by
Are there some tests to add (to the QuantifiedConstraints
branch) to exemplify the solutions here and make sure they stay working?
comment:23 Changed 19 months ago by
Sure. Here's a test adapted from the original post:
{-# 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
).
comment:24 follow-up: 25 Changed 19 months ago by
Remind me:
join_ = coerce @(forall a. m ( m a) -> m a)
Do we allow this? (It's impredicative -- but in a benign way.)
comment:25 Changed 19 months ago by
Replying to 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
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.
comment:26 Changed 19 months ago by
I'm not sure I feel up to writing a proposal just now, but I made a ticket. (Better than an obscure email.) Trac #14859.
This would be an escape hatch like
unsafeCoerce
, until roles get improved