
#8565: New GeneralisedNewtypeDeriving needs help with higher rank types ------------------------------------+------------------------------------- Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.6.3 Keywords: | Operating System: Unknown/Multiple Architecture: Unknown/Multiple | Type of failure: None/Unknown Difficulty: Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | ------------------------------------+------------------------------------- Consider {{{ {-# LANGUAGE RankNTypes, GeneralizedNewtypeDeriving #-} module Foo where class C a where op :: (forall b. b -> a) -> a newtype T x = MkT x deriving( C ) }}} With the new "coerce" implementation of GND, this fails: {{{ Foo.hs:7:31: Cannot instantiate unification variable ‛b0’ with a type involving foralls: (forall b. b -> T x) -> T x Perhaps you want ImpredicativeTypes In the expression: GHC.Prim.coerce (op :: (forall (b :: *). b -> x) -> x) :: (forall (b :: *). b -> T x) -> T x In an equation for ‛op’: op = GHC.Prim.coerce (op :: (forall (b :: *). b -> x) -> x) :: (forall (b :: *). b -> T x) -> T x }}} We want to coerce betweeen {{{ (forall b. b -> x) -> x ~R (forall b. b -> T x) -> T x }}} There are two difficulties with the new `coerce` approach: * Regarded as source code, instance declaration {{{ instance C x => C (T x) where op = coerce (op :: (forall b. b -> x) -> x) }}} requires impredicative instantiation. * We probably don't have a decomposition rule for `Coercible (forall a. t1) (forall a. t2)` There is no difficulty in principle here, but it's not quite obvious what the best approach to a fix is. But it would be good to fix before release; we don't want to break `conduit` -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8565 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler