Opened 3 years ago

Closed 3 years ago

#12616 closed bug (fixed)

type synonyms confuse generalized newtype deriving role checking

Reported by: daviddarais Owned by: goldfire
Priority: low Milestone: 8.0.2
Component: Compiler Version: 8.0.1
Keywords: generalized newtype deriving roles rankntypes Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case: deriving/should_compile/T12616
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

Below is a small Haskell file showing the problem. It defines a simple MonadTrans typeclass, but using a type operator ~>. When using the type operator, GHC complains that generalized newtype deriving gets stuck on a nominal role, but when the type operator is not used then GND works just fine.

Perhaps this is just expected behavior with mixing RankNTypes and GND (and roles), but it's rather unfortunate.

{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}

module GND where

type m ~> n = forall a. m a -> n a

class MonadTrans t where
  -- > this line works:
  -- lift :: (Monad m) => m a -> t m a
  -- > this line doesn't:
  lift :: (Monad m) => m ~> t m

data StateT s m a = StateT { runStateT :: s -> m (a, s) }

instance MonadTrans (StateT s) where
  lift xM = StateT $ \ s -> do { x <- xM ; return (x,s) }

newtype OtherStateT s m a = OtherStateT { runOtherStateT :: StateT s m a }
  deriving (MonadTrans)

The error message is:

GND.hs:23:13: error:
    • Couldn't match representation of type ‘m1 ~> StateT s m1’
                               with that of ‘m1 a1 -> OtherStateT s m1 a1’
        arising from a use of ‘GHC.Prim.coerce’
    • In the expression:
          GHC.Prim.coerce (lift :: (~>) m (StateT s m)) ::
            forall (m :: TYPE GHC.Types.PtrRepLifted
                         -> TYPE GHC.Types.PtrRepLifted).
            Monad m => (~>) m (OtherStateT s m)
      In an equation for ‘lift’:
          lift
            = GHC.Prim.coerce (lift :: (~>) m (StateT s m)) ::
                forall (m :: TYPE GHC.Types.PtrRepLifted
                             -> TYPE GHC.Types.PtrRepLifted).
                Monad m => (~>) m (OtherStateT s m)
      When typechecking the code for ‘lift’
        in a derived instance for ‘MonadTrans (OtherStateT s)’:
        To see the code I am typechecking, use -ddump-deriv
      In the instance declaration for ‘MonadTrans (OtherStateT s)’
    • Relevant bindings include
        lift :: m ~> OtherStateT s m (bound at GND.hs:23:13)

Change History (5)

comment:1 Changed 3 years ago by goldfire

Owner: set to goldfire

I think this issue is just an infelicity in the code generator for GND. Should be easy to fix.

NB: There are no higher-rank types in the example. Just a fancy type synonym.

comment:2 Changed 3 years ago by Simon Peyton Jones <simonpj@…>

In b612da6/ghc:

Fix impredicativity (again)

This patch fixes Trac #12616.

Dignosis.  In TcUnify.tc_sub_type_ds we were going to some trouble to
support co- and contra-variance even for impredicative types.  With
-XImpredicativeTYpes, this allowed a unification variable to be
unified with a polytype (probably wrongly) and that caused later
trouble in the constraint solver, where -XImpredicativeTypes was /not/
on.  In effect, -XImpredicativeTypes can't be switched on locally.

Why did we want ImpredicativeTypes locally?  Because the program
generated by GND for a higher-rank method involved impredicative
instantation of 'coerce':
      op = coerce op   -- where op has a higher rank type
See Note [Newtype-deriving instances] in TcGenDeriv.

Cure.

1.  It is ghastly to rely on ImpredicativeTypes (a 100% flaky
    feature) to instantiate coerce polymorphically.  Happily we
    now have Visible Type Application, so I've used that instead
    which should be solid and reliable.

2.  I deleted the code in tc_sub_type_ds that allows the constraint
    solver to "look through" a unification variable to find a
    polytype.  That used to be essential in the days of ReturnTv,
    but it's utterly unreliable and should be consigned to the dustbin
    of history.  (We have ExpType now for the essential uses.)

Tests involving ImpredicativeTypes are affected, but I'm not worried
about them... it's advertised as a feature you can't rely on, and
I want to reform it outright.

comment:3 Changed 3 years ago by simonpj

Status: newmerge
Test Case: deriving/should_compile/T12616

Great bug report thank you.

Although the patch looks large it isn't really.

But it does change the behaviour of GHC with -XImpredicativeTypes. Since we don't advertise any particular behaviour, that might seem OK. Or someone might complain. Still, I'm inclined to merge the change to the 8.0 branch because it makes the compiler more stable and predictable.

comment:4 Changed 3 years ago by bgamari

Milestone: 8.0.2

comment:5 Changed 3 years ago by bgamari

Resolution: fixed
Status: mergeclosed

This was merged to ghc-8.0 as c93ad554c9f9788b3e2ec45fa4d0131101721536.

Note: See TracTickets for help on using tickets.