[GHC] #11152: GND accepts ill-roled coercion when manually defining it won't typecheck
#11152: GND accepts ill-roled coercion when manually defining it won't typecheck -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 (Type checker) | Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: GHC accepts Unknown/Multiple | invalid program Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- I wanted to see what error message might result from adding `join` to `Monad` and trying to derive it via `GeneralizedNewtypeDeriving`, so I used this code to simulate it: {{{#!hs {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# OPTIONS_GHC -ddump-deriv #-} module CoerceJoin where import qualified Control.Monad (join) import Data.Coerce (coerce) class MyMonad m where join :: m (m a) -> m a instance MyMonad Maybe where join = Control.Monad.join newtype MyMaybe a = MyMaybe (Maybe a) deriving MyMonad }}} To my surprise, this actually compiles: {{{ ==================== Derived instances ==================== Derived instances: instance CoerceJoin.MyMonad CoerceJoin.MyMaybe where CoerceJoin.join = GHC.Prim.coerce (CoerceJoin.join :: GHC.Base.Maybe (GHC.Base.Maybe a_axs) -> GHC.Base.Maybe a_axs) :: forall (a_axs :: *). CoerceJoin.MyMaybe (CoerceJoin.MyMaybe a_axs) -> CoerceJoin.MyMaybe a_axs Generic representation: Generated datatypes for meta-information: Representation types: }}} That seemed really odd, given my understanding of roles, so I tried to implement this instance manually: {{{#!hs newtype MyMaybe a = MyMaybe (Maybe a) instance MyMonad MyMaybe where join = coerce (join :: Maybe (Maybe a) -> Maybe a) :: MyMaybe (MyMaybe a) -> MyMaybe a }}} And now GHC will reject it: {{{ CoerceJoin.hs:18:10: Couldn't match representation of type `a0' with that of `a1' `a1' is a rigid type variable bound by an expression type signature: MyMaybe (MyMaybe a1) -> MyMaybe a1 at CoerceJoin.hs:18:10 arising from trying to show that the representations of `Maybe (Maybe a0) -> Maybe a0' and `MyMaybe (MyMaybe a1) -> MyMaybe a1' are the same Relevant role signatures: type role Maybe representational type role MyMaybe representational In the expression: coerce (join :: Maybe (Maybe a) -> Maybe a) :: MyMaybe (MyMaybe a) -> MyMaybe a In an equation for `join': join = coerce (join :: Maybe (Maybe a) -> Maybe a) :: MyMaybe (MyMaybe a) -> MyMaybe a In the instance declaration for `MyMonad MyMaybe' }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11152 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11152: GND accepts ill-roled coercion when manually defining it won't typecheck -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.2 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by rwbarton): Don't think there is a bug here. The GND is okay because `MyMaybe` is known to have a type parameter of representational role. The problem arises with types involving a variable monad, since we cannot or do not want to require all monads be representational. Your manual implementation is wrong because `a` does not refer to the type you want it to (compare `myid :: a -> a; myid x = x :: a`). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11152#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11152: GND accepts ill-roled coercion when manually defining it won't typecheck -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.2 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by rwbarton): Well, I suppose there is still a bug in that the derived instance is not valid Haskell source as displayed, but there are other issues with it already (like the use of the qualified name `CoerceJoin.join`). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11152#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11152: GND accepts ill-roled coercion when manually defining it won't typecheck -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.2 checker) | Resolution: invalid | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: #9123 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => closed * resolution: => invalid * related: => #9123 Comment: Oops, I overlooked the `forall (a_axs :: *)` part. It turns out that (and some language extensions) are needed to make the generated code compile when typed out manually: {{{#!hs {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE ScopedTypeVariables #-} module CoerceJoin where import qualified Control.Monad (join) import Data.Coerce (coerce) class MyMonad m where join :: m (m a) -> m a instance MyMonad Maybe where join = Control.Monad.join newtype MyMaybe a = MyMaybe (Maybe a) instance MyMonad MyMaybe where join = coerce (join :: Maybe (Maybe a) -> Maybe a) :: forall (a :: *). MyMaybe (MyMaybe a) -> MyMaybe a }}} Also, I think the issue I was trying to reproduce is #9123, so I'll add that to the related tickets as evidence that adding `join` to `Monad` ''would'' cause some trouble. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11152#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11152: GND accepts ill-roled coercion when manually defining it won't typecheck -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.2 checker) | Resolution: invalid | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: #9123 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Yes, #9123 is a serious, open issue! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11152#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11152: GND accepts ill-roled coercion when manually defining it won't typecheck -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.2 checker) | Resolution: invalid | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: #9123 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): So, is there a bug here? I'm tempted to close, but I wanted to double- check. (And, yes, #9123 is a serious, open issue. I think there's a viable approach written up in the ticket, but it would need a fair bit of work -- and quite possibly a research paper -- to sort out.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11152#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11152: GND accepts ill-roled coercion when manually defining it won't typecheck -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.2 checker) | Resolution: invalid | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: #9123 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): I don't believe there's a new bug, no (and I think I closed this issue earlier). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11152#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC