GitLab

Let us define some typeclasses

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

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

Trac metadata

Trac field	Value
Version	7.8.3
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture