#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