#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: -------------------------------------+------------------------------------- Changes (by adamgundry): * cc: adamgundry (added) Comment: Thanks for the report! I think that both errors are genuine, because both definitions require impredicative instantiations to typecheck, not just `RankNTypes`. An impredicative instantiation is where a type variable needs to be filled in with a polymorphic type. For example, in `peirce_eq_lem`, the use of `and` needs `a = Peirce -> LEM, b = LEM -> Peirce` and both `LEM` and `Peirce` expand to polytypes. If you inline `and` then the definition is accepted by 7.10.1 with just `RankNTypes`. In general, you will probably find such definitions easier to work with if you use `newtype` wrappers instead of polymorphic `type` synonyms. That will give you more control over exactly where polymorphism is introduced and eliminated. I agree that the error messages could be better, but it's hard to see how to improve them in general. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10281#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler