[GHC] #9730: Polymorphism and type classes

[GHC]

#9730: Polymorphism and type classes
-------------------------------------+-------------------------------------
       Reporter:  mjaskel            |                   Owner:
           Type:  bug                |                  Status:  new
       Priority:  normal             |               Milestone:
      Component:  Compiler (Type     |                 Version:  7.8.3
  checker)                           |        Operating System:
       Keywords:  Typeclass,         |  Unknown/Multiple
  Polymorphism, ImpredicativeTypes   |         Type of failure:  GHC
   Architecture:  Unknown/Multiple   |  rejects valid program
     Difficulty:  Unknown            |               Test Case:
     Blocked By:                     |                Blocking:
Related Tickets:                     |  Differential Revisions:
-------------------------------------+-------------------------------------
 Let us define some typeclasses

 {{{#!hs
 class A a where

 class B b where

 class C c where
 }}}

 I often use `RankNTypes` and write a type `forall a. A a => a` to mean
 that only the members of type class `A` have been used to construct its
 elements.

 If I have a function that converts programs written only with members of
 `A` into a programs written only with members of `B`, and an analogous one
 to convert from `B` to `C`, I would expect to be able to compose them

 {{{#!hs
 a2b :: (forall a. A a => a) -> (forall b. B b => b)
 a2b = undefined

 b2c :: (forall b. B b => b) -> (forall c. C c => c)
 b2c = undefined

 a2c :: (forall a. A a => a) -> (forall c. C c => c)
 a2c = b2c . a2b
 }}}


 However, I get many types error of the form:

 {{{
 Cannot instantiate unification variable ‘b0’
     with a type involving foralls: forall b. B b => b
       Perhaps you want ImpredicativeTypes
 }}}

 Every `forall` is under a function type, but I enable `ImpredicativeTypes`
 anyway, and I get the following error:

 {{{
  Could not deduce (B (forall b. B b => b))
       arising from a use of ‘a2b’
  from the context (C c)
       bound by the type signature for
                  a2c :: C c => (forall a. A a => a) -> c
 }}}

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9730>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler