[GHC] #12616: type synonyms confuse generalized newtype deriving role checking
#12616: type synonyms confuse generalized newtype deriving role checking -------------------------------------+------------------------------------- Reporter: daviddarais | Owner: Type: bug | Status: new Priority: low | Milestone: Component: Compiler | Version: 8.0.1 Keywords: generalized | Operating System: Unknown/Multiple newtype deriving roles rankntypes | Architecture: | Type of failure: GHC rejects Unknown/Multiple | valid program Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- 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. {{{#!hs {-# 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) }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12616> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#12616: type synonyms confuse generalized newtype deriving role checking -------------------------------------+------------------------------------- Reporter: daviddarais | Owner: goldfire Type: bug | Status: new Priority: low | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: generalized | newtype deriving roles rankntypes Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * owner: => goldfire Comment: 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. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12616#comment:1> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#12616: type synonyms confuse generalized newtype deriving role checking -------------------------------------+------------------------------------- Reporter: daviddarais | Owner: goldfire Type: bug | Status: new Priority: low | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: generalized | newtype deriving roles rankntypes Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Simon Peyton Jones <simonpj@…>): In [changeset:"b612da667fe8fa5277fc78e972a86d4b35f98364/ghc" b612da6/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="b612da667fe8fa5277fc78e972a86d4b35f98364" 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. }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12616#comment:2> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#12616: type synonyms confuse generalized newtype deriving role checking -------------------------------------+------------------------------------- Reporter: daviddarais | Owner: goldfire Type: bug | Status: merge Priority: low | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: generalized | newtype deriving roles rankntypes Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | deriving/should_compile/T12616 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * status: new => merge * testcase: => deriving/should_compile/T12616 Comment: 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. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12616#comment:3> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#12616: type synonyms confuse generalized newtype deriving role checking -------------------------------------+------------------------------------- Reporter: daviddarais | Owner: goldfire Type: bug | Status: merge Priority: low | Milestone: 8.0.2 Component: Compiler | Version: 8.0.1 Resolution: | Keywords: generalized | newtype deriving roles rankntypes Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | deriving/should_compile/T12616 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * milestone: => 8.0.2 -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12616#comment:4> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#12616: type synonyms confuse generalized newtype deriving role checking -------------------------------------+------------------------------------- Reporter: daviddarais | Owner: goldfire Type: bug | Status: closed Priority: low | Milestone: 8.0.2 Component: Compiler | Version: 8.0.1 Resolution: fixed | Keywords: generalized | newtype deriving roles rankntypes Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | deriving/should_compile/T12616 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * status: merge => closed * resolution: => fixed Comment: This was merged to `ghc-8.0` as c93ad554c9f9788b3e2ec45fa4d0131101721536. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12616#comment:5> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
participants (1)
-
GHC