Type error with Rank-n-types

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:

{-# 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

Trac metadata

Trac field	Value
Version	7.8.4
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture