Opened 2 years ago

Closed 19 months ago

Last modified 16 months ago

#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 Iceland_jack

This would be an escape hatch like unsafeCoerce, until roles get improved

comment:2 Changed 2 years ago by RyanGlScott

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 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

comment:4 Changed 2 years ago by Iceland_jack

Also are there cases where this can cause segfaults and the such

comment:5 Changed 2 years ago by simonpj

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 Iceland_jack

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)
Last edited 2 years ago by Iceland_jack (previous) (diff)

comment:7 Changed 2 years ago 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:

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 simonpj

Keywords: QuantifiedContexts added
Last edited 2 years ago by simonpj (previous) (diff)

comment:9 in reply to:  7 Changed 2 years ago by Iceland_jack

I will respond in full in a bit but

Replying to 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?

comment:10 Changed 2 years ago by RyanGlScott

Keywords: deriving added

comment:11 Changed 2 years ago 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):

{-# 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 Lenses 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 in reply to:  7 ; Changed 2 years ago by Iceland_jack

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 involving Coercible.

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 in reply to:  12 ; Changed 2 years ago by RyanGlScott

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 in reply to:  13 ; Changed 2 years ago by Iceland_jack

Replying to RyanGlScott:

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).

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.

Last edited 2 years ago by Iceland_jack (previous) (diff)

comment:15 in reply to:  14 ; Changed 2 years ago by RyanGlScott

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 in reply to:  15 ; Changed 2 years ago by Iceland_jack

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 in reply to:  16 Changed 2 years ago by RyanGlScott

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 Iceland_jack

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)
Last edited 2 years ago by Iceland_jack (previous) (diff)

comment:19 Changed 2 years ago 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:

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 simonpj

Keywords: QuantifiedConstraints added; QuantifiedContexts removed

comment:21 Changed 19 months ago by RyanGlScott

Resolution: duplicate
Status: newclosed

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 simonpj

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 RyanGlScott

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 Changed 19 months ago by simonpj

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 in reply to:  24 Changed 19 months ago by RyanGlScott

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 simonpj

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.

comment:27 Changed 16 months ago by Ben Gamari <ben@…>

In 7df5896/ghc:

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
Note: See TracTickets for help on using tickets.