Opened 5 years ago

Last modified 5 years ago

#9730 new bug

Polymorphism and type classes

Reported by: mjaskel Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 7.8.3
Keywords: Typeclass, Polymorphism, ImpredicativeTypes Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

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

Change History (1)

comment:1 Changed 5 years ago by simonpj

I'm sorry but you really need impredicative polymorphism here, and GHC simply does not support it properly at the moment. (The ImpredicativeTypes stuff is badly broken.)

However in this case there's an easy workaround

a2c x = b2c (a2b x)

Now you don't need impredicativity

Simon

Note: See TracTickets for help on using tickets.