Opened 4 years ago

Closed 4 years ago

#8915 closed bug (invalid)

Instance context not respected in pattern match

Reported by: heisenbug Owned by:
Priority: normal Milestone:
Component: Compiler Version: 7.9
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:


(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:

    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?

Attachments (1)

instance-test.hs (533 bytes) - added by heisenbug 4 years ago.
repro testcase

Download all attachments as: .zip

Change History (2)

Changed 4 years ago by heisenbug

Attachment: instance-test.hs added

repro testcase

comment:1 Changed 4 years ago by goldfire

Resolution: invalid
Status: newclosed

This is not how instances work, I'm afraid. You've stated that KnownSymbol a implies Foo (Just a), but not the other way around. So, pattern matching will bring Foo (Just a) into the context, but that says nothing about KnownSymbol a.

I don't have a good reference of where to point you to explaining this in detail -- sorry.

Note: See TracTickets for help on using tickets.