Opened 4 years ago

Closed 4 years ago

#11458 closed bug (fixed)

Terrible failure of type inference in visible type application

Reported by: simonpj Owned by: goldfire
Priority: highest Milestone: 8.0.1
Component: Compiler (Type checker) Version: 7.10.3
Keywords: TypeApplications Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: typecheck/should_compile/T11458
Blocked By: Blocking:
Related Tickets: #11397 Differential Rev(s):
Wiki Page:



-- 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!!

Change History (6)

comment:1 Changed 4 years ago by simonpj

Keywords: TypeApplications added
Owner: set to goldfire

comment:2 Changed 4 years ago by goldfire

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

comment:3 Changed 4 years ago by 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.


comment:4 Changed 4 years ago by goldfire

Status: newmerge
Test Case: typecheck/should_compile/T11458

comment:5 Changed 4 years ago by Lemming

comment:6 Changed 4 years ago by bgamari

Resolution: fixed
Status: mergeclosed
Note: See TracTickets for help on using tickets.