[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    |           Version:  7.8.4
  (Type checker)                     |  Operating System:  Unknown/Multiple
              Keywords:              |   Type of failure:  GHC rejects
          Architecture:              |  valid program
  Unknown/Multiple                   |        Blocked By:
             Test Case:              |   Related Tickets:
  Peirce_eq_LEM.hs                   |
              Blocking:              |
Differential Revisions:              |
-------------------------------------+-------------------------------------
 GHC rejects the following program (which is also attached); it accepts it
 if the product type is replaced by tuples and the ImpredicativeTypes
 option is added.  I am not sure if this is a bug or an expected
 consequence of the typing rules, which I do not know very well.  In the
 latter case a better error message would be helpful.

 The error message is:

 {{{
 54:17:
     Couldn't match type ‘(Not 𝑎0 -> 𝑐0) -> (𝑎0 -> 𝑐0) -> 𝑐0’ with ‘LEM’
     Expected type: (((Peirce -> LEM) -> 𝑐) ⨿ ((LEM -> Peirce) -> 𝑐))
                    -> 𝑐
       Actual type: (((Peirce -> (Not 𝑎0 -> 𝑐0) -> (𝑎0 -> 𝑐0) -> 𝑐0)
                      -> 𝑐)
                     ⨿ ((LEM -> ((𝑎1 -> 𝑏0) -> 𝑎1) -> 𝑎1) -> 𝑐))
                    -> 𝑐
     In the expression: peirce_implies_lem `and` lem_implies_peirce
     In an equation for ‘peirce_eq_lem’:
         peirce_eq_lem = peirce_implies_lem `and` lem_implies_peirce
 }}}

 This is the code:

 {{{#!hs
 {-# LANGUAGE NoImplicitPrelude #-}
 {-# LANGUAGE RankNTypes        #-}
 {-# LANGUAGE TypeOperators     #-}
 {-# LANGUAGE UnicodeSyntax     #-}

 -- truth

 type True  = ∀ 𝑎. 𝑎 → 𝑎
 type False = ∀ 𝑎. 𝑎

 id ∷ True
 id 𝑥 = 𝑥

 (∘) ∷ ∀ 𝑎 𝑏 𝑐. (𝑏 → 𝑐) → (𝑎 → 𝑏) → 𝑎 → 𝑐
 𝑓 ∘ 𝑔 = \𝑥 → 𝑓 (𝑔 𝑥)

 -- negation

 type Not 𝑎 = 𝑎 → False

 -- disjunction / coproduct

 type 𝑎 ⨿ 𝑏 = ∀ 𝑐. (𝑎 → 𝑐) → (𝑏 → 𝑐) → 𝑐

 𝜄₀ ∷ ∀ 𝑎 𝑏. 𝑎 → 𝑎 ⨿ 𝑏
 𝜄₀ 𝑥 = \𝑙 _ → 𝑙 𝑥

 𝜄₁ ∷ ∀ 𝑎 𝑏. 𝑏 → 𝑎 ⨿ 𝑏
 𝜄₁ 𝑥 = \_ 𝑟 → 𝑟 𝑥

 -- conjunction / product

 type 𝑎 × 𝑏 = ∀ 𝑐. (𝑎 → 𝑐) ⨿ (𝑏 → 𝑐) → 𝑐

 𝜋₀ ∷ ∀ 𝑎 𝑏. 𝑎 × 𝑏 → 𝑎
 𝜋₀ 𝑝 = 𝑝 (𝜄₀ id)

 𝜋₁ ∷ ∀ 𝑎 𝑏. 𝑎 × 𝑏 → 𝑏
 𝜋₁ 𝑝 = 𝑝 (𝜄₁ id)

 and ∷ ∀ 𝑎 𝑏. 𝑎 → 𝑏 → 𝑎 × 𝑏
 𝑥 `and` 𝑦 = \𝑐 → 𝑐 (\𝑙 → 𝑙 𝑥) (\𝑟 → 𝑟 𝑦)

 -- equivalence

 type 𝑎 ↔ 𝑏 = (𝑎 → 𝑏) × (𝑏 → 𝑎)

 -- peirce ↔ lem

 type Peirce = ∀ 𝑎 𝑏. ((𝑎 → 𝑏) → 𝑎) → 𝑎
 type LEM    = ∀ 𝑎. (Not 𝑎) ⨿ 𝑎

 peirce_eq_lem ∷ Peirce ↔ LEM
 peirce_eq_lem = peirce_implies_lem `and` lem_implies_peirce

 peirce_implies_lem ∷ Peirce → LEM
 peirce_implies_lem peirce = peirce (\𝑘 → 𝜄₀ (𝑘 ∘ 𝜄₁))

 lem_implies_peirce ∷ LEM → Peirce
 lem_implies_peirce lem = \𝑓 → lem (\𝑥 → 𝑓 𝑥) id
 }}}

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/10281>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler