#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