[GHC] #11364: Possible type-checker regression in GHC 8.0

[GHC]

#11364: Possible type-checker regression in GHC 8.0
-------------------------------------+-------------------------------------
        Reporter:  hvr               |                Owner:
            Type:  bug               |               Status:  closed
        Priority:  highest           |            Milestone:  8.0.1
       Component:  Compiler (Type    |              Version:  7.10.3
  checker)                           |
      Resolution:  invalid           |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Changes (by simonpj):

 * status:  new => closed
 * resolution:   => invalid


Comment:

 I think that 7.10 is wrong.  It generates this elaborated program
 {{{
   unthrow =
     \ (@ a_anq) (@ e_anr) (@ (proxy_ans :: * -> *)) _ [Occ=Dead] ->
       . @ (Wrap (Catch e_anr) a_anq)
         @ a_anq
 !!      @ (Throws e_anr => a_anq)
         (unWrap @ (Catch e_anr) @ a_anq (T11364.$fThrowsCatch @ e_anr))
         (. @ (Wrap e_anr a_anq)
            @ (Wrap (Catch e_anr) a_anq)
 !!         @ (Throws e_anr => a_anq)
            (coerceWrap @ e_anr @ a_anq)
            (\ (tpl_B1 :: Throws e_anr => a_anq) ->
               tpl_B1
               `cast` (Sym (T11364.NTCo:Wrap[0] <e_anr>_R <a_anq>_R)
                       :: (Throws e_anr => a_anq) ~R# Wrap e_anr a_anq)))
 }}}
 Look at the lines marked `!!`.  We are instantiating `(.)` with a
 qualified
 type, which is never supposed to happen.  (That's essentially
 impredicativity.)

 And if you eta-expand, you get the same error with 7.10 as you do with 8.0
 {{{
 unthrow :: forall aa ee proxy. proxy ee -> (Throws ee => aa) -> aa
 unthrow _ x = unWrap (coerceWrap (Wrap x))
 }}}
 we get
 {{{
     * Could not deduce (Throws ee) arising from a use of `x'
       from the context: Throws e0
 }}}
 So I count that as a win: 8.0 is behaving more self-consistently.

 Moreover, there's a good reason for it.  Look at the eta-expanded version.
 Nothing fixes the instantiation of `e` (namely `e0`) used for `Wrap` and
 `unWrap` to be
 the same `ee` that appears in the type signature for `unthrow`.

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