Coercion symmetry breaks with data families
Summary
I'm seeing some major fragility combining Coercible
with data families.
Steps to reproduce
data family Fool a
-- This works
joe :: Coercible (Fool a) (Fool b) => Fool a -> Fool b
joe = coerce
-- This does not
bob :: Coercible (Fool a) (Fool b) => Fool b -> Fool a
bob = coerce
bob
gives me an error
.../Internal.hs:1036:7: error:
• Could not deduce (b ~ a) arising from a use of ‘coerce’
from the context: Coercible (Fool a) (Fool b)
bound by the type signature for:
bob :: forall a b. Coercible (Fool a) (Fool b) => Fool b -> Fool a
at ...
‘b’ is a rigid type variable bound by
the type signature for:
bob :: forall a b. Coercible (Fool a) (Fool b) => Fool b -> Fool a
at ...
‘a’ is a rigid type variable bound by
the type signature for:
bob :: forall a b. Coercible (Fool a) (Fool b) => Fool b -> Fool a
at ...
• In the expression: coerce
In an equation for ‘bob’: bob = coerce
• Relevant bindings include
bob :: Fool b -> Fool a
Expected behavior
I expect joe
and bob
both to compile. As a worse alternative, I expect neither to compile.
Environment
- GHC version used: 9.4
Optional:
- Operating System:
- System Architecture: