Skip to content

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:
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information