[GHC] #8915: Instance context not respected in pattern match

[GHC]

#8915: Instance context not respected in pattern match
------------------------------------+-------------------------------------
       Reporter:  heisenbug         |             Owner:
           Type:  bug               |            Status:  new
       Priority:  normal            |         Milestone:
      Component:  Compiler          |           Version:  7.9
       Keywords:                    |  Operating System:  Unknown/Multiple
   Architecture:  Unknown/Multiple  |   Type of failure:  None/Unknown
     Difficulty:  Unknown           |         Test Case:
     Blocked By:                    |          Blocking:
Related Tickets:                    |
------------------------------------+-------------------------------------
 (I'll only excerpt here, see attached testcase for full program)

 I have an instance
 {{{
 class Foo (f :: Maybe Symbol)
 instance KnownSymbol a => Foo (Just a)
 }}}
 and a constructor constrained `Baz` with it:
 {{{
 data Bar (f :: Maybe Symbol) where
   Baz :: Foo (Just a) => Bar (Just a)
 }}}

 But the `KnownSymbol` constraint is not liberated when pattern matching on
 `Baz`:
 {{{
 test :: Bar (Just a) -> Bar (Just b) -> Bool
 test a at Baz b at Baz = case prox a `sameSymbol` prox b of
                    Just Refl -> True
                    _ -> False
    where prox :: Bar (Just a) -> Proxy a
          prox Baz = Proxy
 }}}

 I get this error:
 {{{
 instance-test.hs:14:32:
     Could not deduce (KnownSymbol a2)
       arising from a use of ‘sameSymbol’
     from the context ('Just a ~ 'Just a1, Foo ('Just a1))
       bound by a pattern with constructor
                  Baz :: forall (a :: Symbol). Foo ('Just a) => Bar ('Just
 a),
                in an equation for ‘test’
       at instance-test.hs:14:8-10
     or from ('Just b ~ 'Just a2, Foo ('Just a2))
       bound by a pattern with constructor
                  Baz :: forall (a :: Symbol). Foo ('Just a) => Bar ('Just
 a),
                in an equation for ‘test’
       at instance-test.hs:14:14-16
 }}}

 By my reasoning `Foo ('Just a2)` should imply `KnownSymbol a2`, why is GHC
 missing it?

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8915>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler