Terrible failure of type inference in visible type application

[simonpj]

Consider

-- optIntArg :: (Maybe Int -> t2) -> (t2,t2)
optIntArg f = (f Nothing, f (Just True))

This is rejected (by HEAD)

T11379a.hs:5:30: error:
    * Couldn't match type `a' with `Bool'
      `a' is a rigid type variable bound by
        a type expected by the context:
          forall a. Maybe a
        at T11379a.hs:5:30
      Expected type: forall a. Maybe a
        Actual type: Maybe Bool
    * In the first argument of `f', namely `(Just True)'
      In the expression: f (Just True)
      In the expression: (f Nothing, f (Just True))

but if you put the tuple components the other way round, it works fine

optIntArg f = (f (Just True), f Nothing)

Adding the commented-out signature also makes it work fine.

I'm almost certain that this is caused by visible type application; perhaps Nothing gets delayed instantiation, and then f's type becomes forall a. Maybe a. Utterly bogus.

I suspect it'll be fixed by Richards ReturnTv work, but let's make sure it is. We can't release this!!

[goldfire]

Yes. This is a ReturnTv problem. Fix is nearly done -- I'm just going through the testsuite today.

[Richard Eisenberg <eir@…>]

In 00cbbab3/ghc:

Refactor the typechecker to use ExpTypes.

The idea here is described in [wiki:Typechecker]. Briefly,
this refactor keeps solid track of "synthesis" mode vs
"checking" in GHC's bidirectional type-checking algorithm.
When in synthesis mode, the expected type is just an IORef
to write to.

In addition, this patch does a significant reworking of
RebindableSyntax, allowing much more freedom in the types
of the rebindable operators. For example, we can now have
`negate :: Int -> Bool` and
`(>>=) :: m a -> (forall x. a x -> m b) -> m b`. The magic
is in tcSyntaxOp.

This addresses tickets #11397, #11452, and #11458.

Tests:
  typecheck/should_compile/{RebindHR,RebindNegate,T11397,T11458}
  th/T11452

[bgamari]

This was merged in 278e1fa2fd7b33254e323d394706e72f4664ad02.