GHC doesn't use the fact that Coercible is symmetric

{-# Language ScopedTypeVariables, GADTs, DeriveGeneric #-}

import GHC.Generics
import Data.Type.Coercion

data AB = A | B deriving (Generic)
data XY = X | Y deriving (Generic)

data This ab xy where
  At :: This AB XY

foo :: This ab xy -> Coercion (Rep ab a) (Rep xy a)
foo At = Coercion

bar :: forall ab xy a. This ab xy -> Coercion (Rep ab a) (Rep xy a)
bar at
  | Coercion <- foo at :: Coercion (Rep ab a) (Rep xy a)
  = Coercion

This compiles on 8.2.1 and 8.3.20170920 but flipping the arguments to Coercion fails

-- ...

-- • Could not deduce: Coercible (Rep xy a) (Rep ab a)
--     arising from a use of ‘Coercion’
--   from the context: Coercible (Rep ab a) (Rep xy a)
--     bound by a pattern with constructor:

bar :: forall ab xy a. This ab xy -> Coercion (Rep xy a) (Rep ab a)
bar at
  | Coercion <- foo at :: Coercion (Rep ab a) (Rep xy a)
  = Coercion

Conceptually there should be an (Undecidable) superclass constraint for Coercible

class Coercible b a => Coercible a b

Trac metadata

Trac field	Value
Version	8.2.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture