[GHC] #10281: Type error with Rank-n-types

[GHC]

#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