Opened 13 months ago

Last modified 7 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 13 months ago by goldfire

I'm a little confused about what's going on about the core complaint, but, tangentially, it seems to me that calling a a "rigid type variable" is wrong here. Isn't a a 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 a with m () where a is 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.

comment:2 Changed 13 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 12 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 7 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 7 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 7 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 7 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: Changed 7 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

Last edited 7 months ago by simonpj (previous) (diff)

comment:9 Changed 7 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 7 months ago by goldfire

Replying to 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.

comment:11 Changed 7 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?

Last edited 7 months ago by porges (previous) (diff)

comment:12 Changed 7 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

Last edited 7 months ago by simonpj (previous) (diff)
Note: See TracTickets for help on using tickets.