[GHC] #8565: New GeneralisedNewtypeDeriving needs help with higher rank types

GHC ghc-devs at haskell.org
Tue Nov 26 11:01:39 UTC 2013


#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


More information about the ghc-tickets mailing list