[GHC] #14859: Allow explicit impredicativity

[GHC]

#14859: Allow explicit impredicativity
-------------------------------------+-------------------------------------
           Reporter:  simonpj        |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.2.2
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 In [https://mail.haskell.org/pipermail/ghc-devs/2016-September/012940.html
 this email] I suggested allowing a simple form of impredicativity.  With a
 suitable extension flag (`-XExplicitImpredicativeTypes` perhaps), you
 woudl be allowed:

 * To write a polytype in a visible type argument; eg.  `f @(forall a.
 a->a)`

 * To write a polytype as an argument of a type in a signature  e.g.  `f ::
 [forall a. a->a] -> Int`

 ''But that’s all''.  A unification variable still cannot be unified with a
 polytype.  The only way you can call a polymorphic function at a polytype
 is to use Visible Type Application (VTA).

 So using impredicative types might be tiresome.  E.g.
 {{{
   type SID = forall a. a->a
   xs :: [forall a. a->a]
   xs = (:) @SID id ( (:) @SID id ([] @ SID))
 }}}
 In short, if you call a function at a polytype, you must use VTA.  Simple,
 easy, predictable; and doubtless annoying.  But at least it's possible.

 The main motivation is that we are naughtily doing this anyway in the
 implementation of `GeneralisedNewtypeDeriving` -- see Trac #14070
 comment:23 ff.  If we are doing it under the hood, we could just made it
 available to programmers.

 This is much less ambitious, and much easier to implement, than the
 proposed [https://www.microsoft.com/en-us/research/publication/guarded-
 impredicative-polymorphism/ Guarded impredicative polymorphism] (PLDI'18).

 This ticket just records the idea, to see what other use-cases people
 might want to add.  Then someone would have to write a GHC proposal.

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14859>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler