Swapping arguments of type comparison operator ~ induces a type error

Summary

Edit2: see later comments for an even smaller repro.

Edit: a minimal repro is at https://play.haskell.org/saved/EtiAllWh (uncomment the bit swapping ~ arguments to make it fail)

The following commit, swapping arguments of an application of the type comparison operator ~ induces, a type error. No plugins are used in this file.

https://github.com/Mikolaj/horde-ad/commit/3905cf0515ce5ce2723b4b0140184e4c8dcc9599

Steps to reproduce

Compile with and without this commit, using cabal build -j1 (for GHC 9.6 add --allow-newer). It should compile fine without the commit and with it it should fail emitting

simplified/HordeAd/Core/AstInterpret.hs:200:16: error: [GHC-05617]
    • Could not deduce ‘BooleanOf (Ranked (Primal a) n)
                        ~ BooleanOf (IntOf a)’
      from the context: InterpretAst a
        bound by the type signature for:
                   interpretAstBool :: forall a.
                                       InterpretAst a =>
                                       AstEnv a
                                       -> AstMemo a
                                       -> AstBool (ScalarOf a)
                                       -> (AstMemo a, BooleanOf (Primal a))
        at simplified/HordeAd/Core/AstInterpret.hs:(190,1)-(192,77)
      Expected: BooleanOf (Primal a)
        Actual: BooleanOf (Ranked (Primal a) n)
        NB: ‘BooleanOf’ is a non-injective type family
    • In the expression: interpretAstRelOp opCodeRel args2
      In the expression: (memo2, interpretAstRelOp opCodeRel args2)
      In the expression:
        let (memo2, args2) = mapAccumR (interpretAstPrimal env) memo args
        in (memo2, interpretAstRelOp opCodeRel args2)
    • Relevant bindings include
        memo2 :: AstMemo a
          (bound at simplified/HordeAd/Core/AstInterpret.hs:199:10)
        args2 :: [Ranked (Primal a) n]
          (bound at simplified/HordeAd/Core/AstInterpret.hs:199:17)
        args :: [AstPrimalPart n (ScalarOf a)]
          (bound at simplified/HordeAd/Core/AstInterpret.hs:198:20)
        memo :: AstMemo a
          (bound at simplified/HordeAd/Core/AstInterpret.hs:193:22)
        env :: AstEnv a
          (bound at simplified/HordeAd/Core/AstInterpret.hs:193:18)
        interpretAstBool :: AstEnv a
                            -> AstMemo a
                            -> AstBool (ScalarOf a)
                            -> (AstMemo a, BooleanOf (Primal a))
          (bound at simplified/HordeAd/Core/AstInterpret.hs:193:1)
    |
200 |     in (memo2, interpretAstRelOp opCodeRel args2)

Expected behavior

Compiles both with and without the commit.

Environment

• GHC version used: 9.4.5 and 9.6.1

BTW, a different version of this code, one that does not require QuantifiedConstraints and has foralls in a very different place, is similarly fragile (flip argumenta in both BooleanOf (IntOf a) ~ BooleanOf (Ranked (Primal a) n) to make it fail): https://github.com/Mikolaj/horde-ad/blob/f40c4706657b80e8326468bb299456d319cce325/simplified/HordeAd/Core/AstInterpret.hs#L102-L122