Opened 3 years ago

Closed 3 years ago

Last modified 23 months ago

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

Peirce_eq_LEM.hs (1.8 KB) - added by rhjl 3 years ago.
test case
Peirce_eq_LEM_ASCII.hs (1.4 KB) - added by rhjl 3 years ago.
ASCII version of the test case

Download all attachments as: .zip

Change History (13)

Changed 3 years ago by rhjl

Attachment: Peirce_eq_LEM.hs added

test case

comment:1 Changed 3 years ago by rhjl

Version: 7.8.47.10.1

comment:2 Changed 3 years ago by rhjl

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 simonpj

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 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 (→).

Changed 3 years ago by rhjl

Attachment: Peirce_eq_LEM_ASCII.hs added

ASCII version of the test case

comment:5 Changed 3 years ago by adamgundry

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 Changed 3 years ago by rhjl

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 in reply to:  6 ; Changed 3 years ago by simonpj

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 in reply to:  7 Changed 3 years ago by rhjl

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 and newtype 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 and newtype 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 type forall a. a -> a, but the term id f cannot be assigned a type because that would require an instantiation of forall a. a -> a with the polymorphic type of f in place of the type variable a. This does not present a problem when typing the term id id; the typing in that case proceeds as follows:

  1. 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 types a -> a and b -> b;
  1. the type variable a is instantiated to the – now monomorphic ­– type b -> b;
  1. the free variable b in the result-type b -> b of the function application is universally quantified;

The same procedure for id f gives f the type (forall a. a -> a) -> b -> b for some unique type variable b 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 definition f = id works, and in fact I am somewhat confused by that.] The next example illustrates how one can use newtype 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 type forall a. a -> a of id 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:9 Changed 3 years ago by Simon Peyton Jones <simonpj@…>

In 746f086eae9e54ef9e02cf06b71c4f39e27617d5/ghc:

Better documetation of higher rank types

In response to suggestions on Trac #10281

comment:10 Changed 3 years ago by simonpj

Resolution: fixed
Status: newclosed

I've followed your suggestions more or less. Thank you!

Simon

comment:11 Changed 23 months ago by thomie

Milestone: 8.0.1
Note: See TracTickets for help on using tickets.