[GHC] #9730: Polymorphism and type classes

#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

#9730: Polymorphism and type classes -------------------------------------+------------------------------------- Reporter: mjaskel | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.3 (Type checker) | Keywords: Typeclass, Resolution: | Polymorphism, ImpredicativeTypes Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: GHC | Blocked By: rejects valid program | Related Tickets: Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (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 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9730#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC