[GHC] #10619: Order matters when type-checking

[GHC]

#10619: Order matters when type-checking
-------------------------------------+-------------------------------------
        Reporter:  goldfire          |                   Owner:
            Type:  bug               |                  Status:  new
        Priority:  normal            |               Milestone:
       Component:  Compiler          |                 Version:  7.10.1
      Resolution:                    |                Keywords:
Operating System:  Unknown/Multiple  |            Architecture:
 Type of failure:  None/Unknown      |  Unknown/Multiple
      Blocked By:                    |               Test Case:
 Related Tickets:                    |                Blocking:
                                     |  Differential Revisions:
-------------------------------------+-------------------------------------

Comment (by goldfire):

 It gets worse. The same problem happens between these two:

 This succeeds:

 {{{
 {-# LANGUAGE RankNTypes #-}

 module Bug where

 foo _ = if True
         then ((\x -> x) :: (forall a. a -> a) -> forall b. b -> b)
         else \y -> y
 }}}

 This fails:

 {{{
 foo _ = if True
         then \y -> y
         else ((\x -> x) :: (forall a. a -> a) -> forall b. b -> b)
 }}}

 But the cause is different. This second case is caused by the fact that
 `ReturnTv`s can unify with polytypes, and the `ReturnTv` for the whole
 expression is just pushed into the `if`'s branches. But even if the
 `ReturnTv` were replaced by a `TauTv` before pushing into the `if`'s
 branches, it would ''still'' be broken because a `TauTv` with an !OpenKind
 can also unify with polytypes.

 I think the solution for this case is to create a new flavor of `TauTv`
 that truly insists on being a tau-type.

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