#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