[GHC] #11431: GHC instantiates levity-polymorphic type variables with foralls

[GHC]

#11431: GHC instantiates levity-polymorphic type variables with foralls
-------------------------------------+-------------------------------------
           Reporter:  gridaphobe     |             Owner:
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.1
           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:
-------------------------------------+-------------------------------------
 Consider the following use of `error`.

 {{{
 ghci> :t error
 error
   :: forall (v :: GHC.Types.Levity) (a :: TYPE v).
      (?callStack::GHC.Stack.Types.CallStack) =>
      [Char] -> a

 ghci> :t error "bad" :: (forall a. a -> a) -> a
 error "bad" :: (forall a. a -> a) -> a
   :: (?callStack::GHC.Stack.Types.CallStack) =>
      (forall a1. a1 -> a1) -> a
 }}}

 GHC is instantiating the type variable `a` in the output with `(forall a.
 a -> a) -> a`, which requires impredicative polymorphism. So this example
 should actually be rejected by the type checker.

 Note that GHC also does this with open-kinded type variables, so the
 behavior with `error` and `undefined` has been around for a while. There
 are tests that depend on it, and a Note that describes the decision to
 accept these programs. Still, Simon PJ says perhaps we should really just
 reject these programs.

 So here's a ticket to discuss the matter.

 For more information, see the discussion starting at
 https://phabricator.haskell.org/D1739#51408.

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