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

**Note:**See TracTickets for help on using tickets.

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

Now you don't need impredicativity

Simon