#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@Baz b@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