type checker fails to infer an implicit parameter constraint in the presence of existential types.

In this code,

{-# LANGUAGE ImplicitParams, GADTs #-}

class Foo a

data M where M :: Foo a => a -> M

x :: (?x :: ()) => ()
x = undefined

-- foo :: (?x :: ()) => M -> ()
foo y = case y of
    M _ -> x

I'd expect ghc to infer the commented out type for foo. However, it fails to do that:

foo.hs:12:12:
    Unbound implicit parameter (?x::())
      arising from a use of `x' at foo.hs:12:12
    In the expression: x
    In a case alternative: M _ -> x
    In the expression: case y of { M _ -> x }

Is this a bug or an expected shortcoming of the type checker? The program compiles fine with the explicit type signature. (In the original program the type signature was big and completely unenlightening, so I'd rather not have to write it.)

Trac metadata

Trac field	Value
Version	6.13
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture