#10281 closed bug (fixed)
Type error with Rank-n-types
Reported by: | rhjl | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | 8.0.1 |
Component: | Compiler (Type checker) | Version: | 7.10.1 |
Keywords: | Cc: | adamgundry | |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | GHC rejects valid program | Test Case: | Peirce_eq_LEM.hs |
Blocked By: | Blocking: | ||
Related Tickets: | Differential Rev(s): | ||
Wiki Page: |
Description
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
Attachments (2)
Change History (13)
Changed 3 years ago by
Attachment: | Peirce_eq_LEM.hs added |
---|
comment:1 Changed 3 years ago by
Version: | 7.8.4 → 7.10.1 |
---|
comment:2 Changed 3 years ago by
I just confirmed that the issue persists in version 7.10.1; additionally, the following code, also part of the attached file, now produces an error.
type DNE = ∀ 𝑎. Not (Not 𝑎) → 𝑎 peirce_implies_dne ∷ Peirce → DNE peirce_implies_dne peirce = \dn → peirce dn
The error is:
67:42: Couldn't match type ‘𝑏0’ with ‘𝑎1’ because type variable ‘𝑎1’ would escape its scope This (rigid, skolem) type variable is bound by a type expected by the context: 𝑎 -> 𝑎1 at Peirce_eq_LEM.hs:67:42-43 Expected type: (𝑎 -> 𝑏0) -> 𝑎 Actual type: Not 𝑎 -> 𝑎 In the first argument of ‘peirce’, namely ‘dn’ In the expression: peirce dn
This seems less confusing than the error in the original report; nevertheless I found it curious, because it is new in version 7.10.1, and because the expression naively unifies to the correct type.
comment:3 Changed 3 years ago by
When I copy/paste this into my emacs buffer the foralls show up ok but the a's and b's (and much else besides) do not. Could you do it in ASCII please?
Do you think the program needs impredicative polymorphism? If so, GHC just doesn't properly support that, notwithstanding the partially implemented -XImpredicativeTypes
.
I'm not sure what "it accepts it if the product type is replaced by tuples" means.
comment:4 Changed 3 years ago by
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 (→)
.
comment:5 Changed 3 years ago by
Cc: | adamgundry added |
---|
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.
comment:6 follow-up: 7 Changed 3 years ago by
Thank you for your explanations!
I think that I now understand the issue. I find your explanation of impredicative polymorphism better than the one given in the GHC manual:
This means that you can call a polymorphic function at a polymorphic type, and parameterise data structures over polymorphic types.
The hint about newtype
wrappers also helped me to adjust the module to work with RankNTypes
. I did not realise that newtype
wrappers hide the polymorphism of the type they wrap. I think that a remark of this sort in the section on rank-n-types of the GHC manual would also help.
By the way: this issue with impredicative instantiations precludes the use of ($)
and (.)
to get rid of excessive parenthesis in certain situations. Is there a workaround?
comment:7 follow-up: 8 Changed 3 years ago by
Replying to rhjl:
I find your explanation of impredicative polymorphism better than the one given in the GHC manual:
...
I think that a remark of this sort in the section on rank-n-types of the GHC manual would also help.
Could you propose some actual, concrete sentences to add or change in user manual? Then I'll just make the change. As a bona fide user you are in a far better position to draft the words than me.
By the way: this issue with impredicative instantiations precludes the use of
($)
and(.)
to get rid of excessive parenthesis in certain situations. Is there a workaround?
Becuase of this ($)
has its own special typing rule in GHC. But (.)
does not (yet).
comment:8 Changed 3 years ago by
Replying to simonpj:
Could you propose some actual, concrete sentences to add or change in user manual? Then I'll just make the change. As a bona fide user you are in a far better position to draft the words than me.
In 7.13.6 [Arbitrary-rank polymorphism], before two paragraphs “The -XRankNTypes
option is also […]” and “The obselete [sic] language options […]” add:
In particular, in
data
andnewtype
declarations the constructor arguments may be polymorphic types of any rank. Note that the declared types are nevertheless always monomorphic. This is important because by default GHC will not instantiate type variables to a polymorphic type (cf. 7.13.7 [Impredicative Polymorphism]). The examples below demonstrate some uses.
In 7.13.6.1 [Examples] replace the first two sentences with
These are examples of
data
andnewtype
declarations with polymorphic constructor arguments:
After the code that shows the types of the constructors add the following:
By default GHC will not instantiate type variables to a polymorphic type: given
f :: (forall a. a -> a) -> (forall a. a -> a)
the term
f id
has typeforall a. a -> a
, but the termid f
cannot be assigned a type because that would require an instantiation offorall a. a -> a
with the polymorphic type off
in place of the type variablea
. This does not present a problem when typing the termid id
; the typing in that case proceeds as follows:
- the top-level quantifiers in the types of the two occurrences of
id
are removed, and their bound variables are renamed to make them unique. This gives typesa -> a
andb -> b
;
- the type variable
a
is instantiated to the – now monomorphic – typeb -> b
;
- the free variable
b
in the result-typeb -> b
of the function application is universally quantified;
The same procedure for
id f
givesf
the type(forall a. a -> a) -> b -> b
for some unique type variableb
in step 1, by removing the effectively top level quantifier to the right of the arrow. The resulting type is nevertheless still polymorphic, and so step 2 fails. [I hope that I got this whole explanation remotely correct. Please feel free to improve it: I am sure that it can be expressed both briefer and more accurately. What I say here also does not explain why the definitionf = id
works, and in fact I am somewhat confused by that.] The next example illustrates how one can usenewtype
declarations to work around this issue.
type Poly = (forall a. a -> a) -> (forall a. a -> a) newtype Wrap = Wrap { unwrap :: Poly } f :: Poly f = id ok :: Poly ok = unwrap (id (Wrap f))
In 7.13.7 [Impredicative Polymorphism] replace the sentence “This means that you can call a polymorphic […]” with
Impredicative polymorphism allows type variables to be instantiated to polymorphic types (cf. 7.13.6 [Arbitrary-rank polymorphism]). For example the following is valid with
-XImpredicativeTypes
:
type Poly = (forall a. a -> a) -> (forall a. a -> a) f :: Poly f = id ok :: Poly ok = id f
In this example the type variable
a
in the typeforall a. a -> a
ofid
needs to be instantiated to a polymorphic type. Contrast this with the discussion in 7.13.6.1 [Examples] for more details.
In particular impredicative polymorphism also allows the application of type constructors to polymorphic types, and of various term constructors to terms of polymorphic types. For example, given the above definitions, the following makes sense:
ok2 :: [Poly] ok2 = [f]
Here is a more elaborate example: [continue with the current example]
By the way: this issue with impredicative instantiations precludes the use of
($)
and(.)
to get rid of excessive parenthesis in certain situations. Is there a workaround?Becuase of this
($)
has its own special typing rule in GHC. But(.)
does not (yet).
Is the special type of ($)
only available when using the Prelude?
comment:10 Changed 3 years ago by
Resolution: | → fixed |
---|---|
Status: | new → closed |
I've followed your suggestions more or less. Thank you!
Simon
comment:11 Changed 23 months ago by
Milestone: | → 8.0.1 |
---|
test case