[GHC] #10281: Type error with Rank-n-types

[GHC]

#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