#10281: Type error with Rank-n-types -------------------------------------+------------------------------------- Reporter: rhjl | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.1 checker) | Keywords: Resolution: | Architecture: Operating System: Unknown/Multiple | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | Peirce_eq_LEM.hs Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by rhjl): I will attach an ASCII version of the test case. What I mean by replacing the product type with tuples is to change the definition of `𝑎 × 𝑏` to `(𝑎,𝑏)` and to make the appropriate adjustments in the functions associated to that type. With those changes and `ImpredicativeTypes` GHC accepts the module. My undoubtedly wrong idea of impredicative polymorphism is that it (recursively) allows polymorphic types as any arguments to any type constructor, whereas arbitrary rank polymorphism (recursively) allows polymorphic types in the arguments to `(→)` only. Using these definitions I do not think that the module should need impredicative polymorphism, because – after resolving all aliases – it uses no type constructors other than `(→)`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10281#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler