[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 goldfire):

 Replying to [comment:8 simonpj]:
 > 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.

 I would argue that `g` does ''not'' have a principal type. It can be given
 the type `T a -> Bool`, but it can also be given the type `T a -> F a`,
 where `F Int = Bool`. If no such `F` is in scope at the time of the
 definition of `g`, I suppose it ''does'' have the principal type you
 suggest, but predicating the principality of types based on what's in
 scope is terribly fragile, and so my personal definition of "principal
 type" includes the possibility of type functions defined later.

 @tvynr's example is different, I think, in that it seems there is a
 principal type no matter what other type-level definitions are available.
 Without thinking about the details, I conjecture that it's possible to
 detect variables whose scopes are appropriate w.r.t. the available
 equalities such that we can declare these variables to be touchable, where
 universally-quantified variables would be untouchable.

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