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 `forall`s 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
issue