#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