Instance context not respected in pattern match
(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?
Trac metadata
Trac field | Value |
---|---|
Version | 7.9 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |