Opened 8 months ago

Last modified 3 months ago

## #9223 new bug

# Type equality makes type variable untouchable

Reported by: | Feuerbach | Owned by: | |
---|---|---|---|

Priority: | normal | Milestone: | |

Component: | Compiler (Type checker) | Version: | 7.8.2 |

Keywords: | Cc: | ||

Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |

Type of failure: | None/Unknown | Test Case: | |

Blocked By: | Blocking: | ||

Related Tickets: | Differential Revisions: |

### Description

This doesn't look right:

{-# LANGUAGE RankNTypes, TypeFamilies #-} type family TF (m :: * -> *) run1 :: (forall m . Monad m => m a) -> a run1 = undefined run2 :: (forall m . (Monad m, TF m ~ ()) => m a) -> a run2 = undefined -- this works x1 = run1 (return ()) -- this fails x2 = run2 (return ()) {- 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 ‘a’ is a rigid type variable bound by the inferred type of x2 :: 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 ())’ -}

I would expect x2 to type check just like x1 does.

### Change History (12)

### comment:1 Changed 8 months ago by goldfire

### comment:2 Changed 8 months ago 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

### comment:3 Changed 8 months ago by goldfire

I may have said this elsewhere, but if we keep the "untouchable" stuff in the error message, it would be great to include a link to more information. Untouchable variables are really subtle, and an understanding of them is necessary for a programmer to make progress here. Section 5.2 of the OutsideIn paper is a great starting place for what should be at the other end of the link.

Personally, I favor the second message above -- it has more information a programmer might use to fix the problem.

### comment:4 Changed 3 months ago 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. :)

### comment:5 Changed 3 months ago by goldfire

Interesting example! I'm not convinced this is related to the original ticket, but it is curious. I do see why OutsideIn refuses to type-check this, in the presence of the GADT pattern-match on `TokIntLit`. But what's interesting to me is that I can't come up with a type other than `Token TokenType -> Integer` for `foo`. As I note above, usually when we get untouchable variable errors, there is an alternate type that could be assigned... but here, that doesn't seem to be the case, because the GADT pattern-match is happening over an existentially-bound variable.

I don't know what the fix is here, but it's an interesting case.

### comment:6 Changed 3 months ago 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!

### comment:7 Changed 3 months ago by goldfire

My guess is that this *is* separate from the first post, but, in both cases, there is an untouchable type variable where there is a principal type. I'd wait for Simon's opinion before splitting this off.

### comment:8 follow-up: ↓ 10 Changed 3 months ago 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

### comment:9 Changed 3 months ago by tvynr

Ah ha! This makes perfect sense; thank you for the excellent example and explanation. In particular, this points out that whether a principled type exists is dependent upon some pretty incidental factors, like whether the output type and the input type happen to have anything in common. I can see why GHC conservatively rejects both of these, since getting it to work would result in a somewhat fragile system.

I had previously supposed that the problem was somehow related to the fact that I had two data -- the `TokenType` and the payload -- and that the `a` in the first parameter of `SomeToken` (`t a`) was not being unified with the `a` in the second parameter (`a`) for the purposes of inference. I think I had gotten than impression by the names `a` and `a1` without realizing that one of them arose merely due to the use of `+` in the body.

Thanks again!

### comment:10 in reply to: ↑ 8 Changed 3 months ago by goldfire

Replying to simonpj:

What about

g? Here we have "given"a~Int, but the same wanted constraint isbeta~Boolis generated. Now there is only one solution, namelybeta:=Bool, because the givena~Intcan'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.

### comment:11 Changed 3 months ago by porges

I ran into something similar to this with a type like:

forall t. (forall m. (C m, m ~ t) => m) -> t

This marked 't' untouchable. The solution was to write instead:

forall t. ((C t) => t) -> t

Are there any cases in which these aren't equivalent? If not, why is GHC not able to reduce the first to the second?

### comment:12 Changed 3 months ago by simonpj

@porges: Yes, the two types should be equivalent. GHC HEAD (and 7.10) should be better in this regard (see #9211). 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

**Note:**See TracTickets for help on using tickets.

I'm a little confused about what's going on about the core complaint, but, tangentially, it seems to me that calling

aa "rigid type variable" is wrong here. Isn'taa metavariable, especially if it's untouchable?I should say that blindly following the rules from OutsideIn about untouchable variables does lead me to a place of unifying

m awithm ()whereais untouchable. But, something is still fishy about it that I can't quite pin down. In other cases, when something is untouchable, I can construct a way in which the type in question is not a principal type... and I can't quite do this here, hence my confusion.