[GHC] #10281: Type error with Rank-n-types
#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
#10281: Type error with Rank-n-types -------------------------------------+------------------------------------- Reporter: rhjl | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.1 checker) | Keywords: Resolution: | Architecture: Operating System: Unknown/Multiple | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | Peirce_eq_LEM.hs Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Changes (by rhjl): * version: 7.8.4 => 7.10.1 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10281#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10281: Type error with Rank-n-types -------------------------------------+------------------------------------- Reporter: rhjl | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.1 checker) | Keywords: Resolution: | Architecture: Operating System: Unknown/Multiple | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | Peirce_eq_LEM.hs Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Comment (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. {{{#!hs 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10281#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10281: Type error with Rank-n-types -------------------------------------+------------------------------------- Reporter: rhjl | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.1 checker) | Keywords: Resolution: | Architecture: Operating System: Unknown/Multiple | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | Peirce_eq_LEM.hs Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10281#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10281: Type error with Rank-n-types -------------------------------------+------------------------------------- Reporter: rhjl | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.1 checker) | Keywords: Resolution: | Architecture: Operating System: Unknown/Multiple | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | Peirce_eq_LEM.hs Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Comment (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 `(β)`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10281#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10281: Type error with Rank-n-types -------------------------------------+------------------------------------- Reporter: rhjl | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.1 checker) | Keywords: Resolution: | Architecture: Operating System: Unknown/Multiple | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | Peirce_eq_LEM.hs Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Changes (by adamgundry): * cc: adamgundry (added) Comment: 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10281#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10281: Type error with Rank-n-types -------------------------------------+------------------------------------- Reporter: rhjl | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.1 checker) | Keywords: Resolution: | Architecture: Operating System: Unknown/Multiple | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | Peirce_eq_LEM.hs Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Comment (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? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10281#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10281: Type error with Rank-n-types -------------------------------------+------------------------------------- Reporter: rhjl | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.1 checker) | Keywords: Resolution: | Architecture: Operating System: Unknown/Multiple | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | Peirce_eq_LEM.hs Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by simonpj): Replying to [comment:6 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). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10281#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10281: Type error with Rank-n-types -------------------------------------+------------------------------------- Reporter: rhjl | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.1 checker) | Keywords: Resolution: | Architecture: Operating System: Unknown/Multiple | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | Peirce_eq_LEM.hs Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by rhjl): Replying to [comment:7 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 {{{#!hs 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`; 2. the type variable `a` is instantiated to the β now monomorphic Ββ type `b -> b`; 3. 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. {{{#!hs 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`: {{{#!hs 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: {{{#!hs 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? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10281#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10281: Type error with Rank-n-types
-------------------------------------+-------------------------------------
Reporter: rhjl | Owner:
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler (Type | Version: 7.10.1
checker) | Keywords:
Resolution: | Architecture:
Operating System: Unknown/Multiple | Unknown/Multiple
Type of failure: GHC rejects | Test Case:
valid program | Peirce_eq_LEM.hs
Blocked By: | Blocking:
Related Tickets: | Differential Revisions:
-------------------------------------+-------------------------------------
Comment (by Simon Peyton Jones
#10281: Type error with Rank-n-types -------------------------------------+------------------------------------- Reporter: rhjl | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.1 checker) | Keywords: Resolution: fixed | Architecture: Operating System: Unknown/Multiple | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | Peirce_eq_LEM.hs Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Changes (by simonpj): * status: new => closed * resolution: => fixed Comment: I've followed your suggestions more or less. Thank you! Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10281#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC