#9223: Type equality makes type variable untouchable --------------------------------------------+------------------------------ Reporter: Feuerbach | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type checker) | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Test Case: | Difficulty: Unknown Blocking: | Blocked By: | Related Tickets: --------------------------------------------+------------------------------ Comment (by simonpj): GHC is being schizophrenic about an interesting design choice here. The issue is this. When typechecking `x2`'s RHS, we assume that the RHS has type `alpha`, for some fresh unification variable `alpha`, and generate constraints from the RHS, giving the constraint: {{{ forall m. (Monad m, TF m ~ ()) -- Comes from run2's type => (m alpha ~ m (), -- Matching result of (return ()) with expected type (m alpha) Monad m) -- Call of return }}} That leads to the constraint `(alpha ~ ())`, but underneath an implication constraint that has an equality (like a GADT) in it. So !OutsideIn refrains from unifying `alpha`. Then GHC tries to infer a type for `x2` anyway, getting (essentially) {{{ x2 :: forall a. (a ~ ()) => a }}} where we have decided to quantify over `alpha` to `a`. Finally we end up reporting the insoluble constraint `(a ~ alpha)`. So the question is: what error message would you like to see? This "untouchable" stuff is a bit disconcerting, so we could say this: {{{ Couldn't match expected type ‘a’ with actual type ‘()’ ‘a’ is a rigid type variable bound by the inferred type of x2 :: forall a. a at untouchable.hs:15:1 Relevant bindings include x2 :: a (bound at untouchable.hs:15:1) In the first argument of ‘return’, namely ‘()’ In the first argument of ‘run2’, namely ‘(return ())’ }}} Here you get to see the inferred type of `x2`. (Side note: actually GHC currently prints `the inferred type of x2 :: a`, suppressing the `forall`, but in this context I suspect we should print the `forall` regardless of `-fprint-explicit-foralls`. I'll make that change anyway unless anyone yells.) A merit of this error message is that if you, the programmer, give `x2` that type signature `x2 :: forall a. a`, then indeed that is very much the message that you'll get. But I suppose it leaves open the question of '''why''' GHC inferred that type for `x2`. Alternatively we could give you {{{ Couldn't match expected type ‘a’ with actual type ‘()’ ‘a’ is untouchable inside the constraints (Monad m, TF m ~ ()) bound by a type expected by the context: (Monad m, TF m ~ ()) => m a at untouchable.hs:15:6-21 Relevant bindings include x2 :: a (bound at untouchable.hs:15:1) In the first argument of ‘return’, namely ‘()’ In the first argument of ‘run2’, namely ‘(return ())’ }}} which perhaps exposes a bit more of the mechanism of !OutsideIn, and has the merit of displayin the constraint(s) that make it untouchable. Which would you prefer? Currently GHC displays both, which I agree is confusing. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9223#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 tvynr): I just ran into something that seems at least related. I'm trying to use Happy in tandem with statically typing the payload I get from different functions (so I don't have to do the thing the GHC parser does with explicit calls to unwrapping functions). Eventually, I got the essence of the problem down to this MWE: {{{ {-# LANGUAGE GADTs, ExistentialQuantification #-} module Main where data Token t = forall a. Token (SomeToken t a) data SomeToken t a = SomeToken (t a) a data TokenType a where TokLitInt :: TokenType Integer TokLitPlus :: TokenType () -- Without the type signature, GHC 7.8.3 can't infer the type of this function. --foo :: Token TokenType -> Integer foo (Token (SomeToken TokLitInt x)) = x + 1 foo _ = 0 main :: IO () main = undefined }}} The above code typechecks in GHC 7.6.3 with and without the type signature. In GHC 7.8.3, it fails to typecheck (unless the type signature is present) with the following error message: {{{ Couldn't match type ‘a’ with ‘Integer’ ‘a’ is untouchable inside the constraints (a1 ~ Integer) bound by a pattern with constructor TokLitInt :: TokenType Integer, in an equation for ‘foo’ at Test.hs:15:23-31 ‘a’ is a rigid type variable bound by the inferred type of foo :: Num a => Token TokenType -> a at Test.hs:15:1 Expected type: a Actual type: a1 Relevant bindings include foo :: Token TokenType -> a (bound at Test.hs:15:1) In the expression: x + 1 In an equation for ‘foo’: foo (Token (SomeToken TokLitInt x)) = x + 1 }}} This is unfortunate for me because Happy doesn't generate type signatures but does, in the approach I'm using, wind up generating code that behaves equivalently. Putting a type signature on the use of "x" doesn't help, either, though I'm guessing that this is unsurprising to those who understand the relevant paper better. :) If you'll forgive my naiveté, it seems pretty peculiar from the perspective of an amateur Haskell programmer that this type isn't inferred; I'd think that the type variable from the two arguments of SomeToken would be unified by the fact that they were introduced by the same pattern match. But the error message indicates two variables, "a" and "a1", and doesn't really seem to relate them. Am I missing something? That said, I need to read the paper mentioned in this thread rather thoroughly now and I understand if it sounds like I'm asking for a pony. :) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9223#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 tvynr): I'm glad the example is at least somewhat useful. :) I'm unfamiliar enough with the mechanics involved that I don't know if this is related. Should I open another ticket instead or just leave this stuff here? The thing that seems especially peculiar to me is that, in the example above, GHC 7.6.3 can infer the type just fine. This suggests that the GHC 7.8.3 inference algorithm has been made more conservative in some way. I'm guessing that this difference is related to fixing a bug of some kind but, as you say, this case only seems to have the one type which could be inferred. In the meanwhile, I suppose we'll just use the workaround of an explicit unwrapper function if we need to move to GHC 7.8. Thanks! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9223#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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

#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

#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): @porges: Yes, the two types should be equivalent. GHC HEAD (and 7.10) should be better in this regard. Can you try your example with that? @goldire: you may be right. But even if you are, there's a balance between trying to make type inference as clever as possible and making it so unpredictable that no one knows whether it'll work or not. But I'm open to suggetions. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9223#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler