Non-exhaustive patterns in case in GHCi with quantified class contexts

This appears in the wip/T2893 branch.

To reproduce, create the following module

{-# LANGUAGE ConstraintKinds, GADTs, KindSignatures, QuantifiedConstraints #-}
module Bug where

import GHC.Exts

data Foo :: (* -> Constraint) -> * where
  MkFoo :: (forall a . c a => c (f a), c a) => (f a) -> Foo c

and load it into GHCi:

Bug> foo = MkFoo "foo" :: Foo Show
*** Exception: compiler/typecheck/TcType.hs:(1965,9)-(1985,76): Non-exhaustive patterns in case

Putting the same declaration into the module itself does not seem to trigger the bug.

Trac metadata

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