[GHC] #9223: Type equality makes type variable untouchable

[GHC]

#9223: Type equality makes type variable untouchable
-------------------------------------+-------------------------------------
              Reporter:  Feuerbach   |            Owner:
                  Type:  bug         |           Status:  new
              Priority:  normal      |        Milestone:
             Component:  Compiler    |          Version:  7.8.2
  (Type checker)                     |         Keywords:
            Resolution:              |     Architecture:  Unknown/Multiple
      Operating System:              |       Difficulty:  Unknown
  Unknown/Multiple                   |       Blocked By:
       Type of failure:              |  Related Tickets:
  None/Unknown                       |
             Test Case:              |
              Blocking:              |
Differential Revisions:              |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 Consider
 {{{
 data T a where
   T1 :: T Int
   T2 :: T Bool
   T3 :: T a

 f T2 = True

 g T1 = True
 }}}
 Can we infer a type for `f`?  Well we know it must be something like
 {{{
 f :: T a -> ??
 }}}
 just from the lambda and the pattern match.  What is the `??`?  Call it
 `beta`, a unification variable.  The pattern match gives us a "given"
 constraint `a~Bool`, and the RHS has type `Bool`, so the wanted"
 constraint is `beta~Bool`.  So we could unify `beta with `Bool` or with
 `a`; both would work. Since neither is more general than the other, we
 reject the program.

 What about `g`?  Here we have "given" `a~Int`, but the same wanted
 constraint is `beta~Bool` is generated.  Now there is only one solution,
 namely `beta:=Bool`, because the given `a~Int` can't help us with
 booleans.

 But you can see how delicate this is!  `f` has no principal type, while
 `g` does, but the difference is very slight.  It may be obvious to a naive
 programmer, but it certainly isn't obvious to GHC.

 GHC conservatively rejects both.  Your program is another variation with
 an existentially bound type instead of `Int` or `Bool`.  7.6.3 simply had
 a bug.

 I have no idea how to improve on this.  But that's not to say it could not
 be improved.

 Simon

 So yes, i

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