Confusing error message "Could not deduce ‘(Bool :: Type) ~ (Bool :: Type)’"

[Edit: this commit fails on HEAD+head.hackage later than the original one and closer to the right place: https://github.com/Mikolaj/horde-ad/commit/999e4575c4e84638505abd26fba98965c4a50ffc]

[Edit2: a tentative summary after the first couple dozen comments up to #23589 (comment 511022): in GHC 9.4.5 the Could not deduce Bool ~ Bool message is a symptom that the workaround from #14860 (comment 495352) doesn't work where it should work[see below]; in GHC 9.6.2 the silly message only appears when the programmer abuses the workaround (uses it for type families of rank 2 instead of rank 1), so this is only an error message quality issue; in HEAD, compilation fails earlier when faced with the abuse and has a plausible error message, which however gives no hint that the abuse of a workaround is the underlying problem.]

[Edit3: Edsko confirms I've used the workaround wrongly even in the simpler examples where GHC 9.4.5 emits Bool~Bool --- I was quantifying over a variable that is involved in the resolution of the type family (appears in a type expression within the arity of the type family instead of later on). So the only problem is GHC reacting badly (with Bool~Bool) to an abuse of a workaround, which may or may not indicate deeper problems in GHC and certainly the error message could be improved.]

To reproduce, with GHC 9.6.2 do cabal test simplifiedOnlyTest --disable-optimization -ftest_seq --allow-newer on this commit

https://github.com/Mikolaj/horde-ad/commit/ac95ff02c660b95eb40a56ea8f38fbe25e3bb15b

The second error from the bottom will be presented with the following absurd error message. The extra kinds come from -fprint-explicit-kinds. I'm pretty sure I don't define any other Bool type in this repo.

test/tool/CrossTesting.hs:83:12: error: [GHC-39999]
    • Could not deduce ‘(Bool :: Type) ~ (Bool :: Type)’
        arising from the head of a quantified constraint
        arising from a use of ‘interpretAst’
      from the context: (KnownNat n, KnownNat m, ADReady AstRanked r,
                         InterpretAstR (Flip @{GHC.TypeNats.Nat} @{Type} OR.Array) r,
                         InterpretAstR
                           (ADVal
                              @GHC.TypeNats.Nat (Flip @{GHC.TypeNats.Nat} @{Type} OR.Array))
                           r,
                         (v :: Type)
                         ~ (Flip @{GHC.TypeNats.Nat} @{Type} OR.Array r m :: Type),
                         (g :: Type)
                         ~ (Flip @{GHC.TypeNats.Nat} @{Type} OR.Array r n :: Type))
        bound by the type signature for:
                   rev' :: forall r (m :: GHC.TypeNats.Nat) (n :: GHC.TypeNats.Nat) v
                                  g.
                           (KnownNat n, KnownNat m, ADReady AstRanked r,
                            InterpretAstR (Flip @{GHC.TypeNats.Nat} @{Type} OR.Array) r,
                            InterpretAstR
                              (ADVal
                                 @GHC.TypeNats.Nat (Flip @{GHC.TypeNats.Nat} @{Type} OR.Array))
                              r,
                            (v :: Type)
                            ~ (Flip @{GHC.TypeNats.Nat} @{Type} OR.Array r m :: Type),
                            (g :: Type)
                            ~ (Flip @{GHC.TypeNats.Nat} @{Type} OR.Array r n :: Type)) =>
                           (forall (f :: Type -> GHC.TypeNats.Nat -> Type) x.
                            ADReady f x =>
                            f x n -> f x m)
                           -> g
                           -> (v, v, v, v, v, v, v, v, g, g, g, g, g, g, g, AstRanked r m,
                               AstRanked r m, v, v, v, v, v, v, v, v, v, v, v, v, v, v, g, g, g,
                               g, g, g, g, g, g, g, g, g, g, g)
        at test/tool/CrossTesting.hs:(40,1)-(50,52)
      or from: ADReady f1 r
        bound by the type signature for:
                   h :: forall (f1 :: Type -> GHC.TypeNats.Nat -> Type).
                        ADReady f1 r =>
                        (f1 r m -> AstRanked r m)
                        -> (AstRanked r n -> f1 r n)
                        -> (AstRanked r m -> AstRanked r m)
                        -> Domains @{Type} (ADValClown OD.Array) r
                        -> ADVal
                             @GHC.TypeNats.Nat (Flip @{GHC.TypeNats.Nat} @{Type} OR.Array) r m
        at test/tool/CrossTesting.hs:(76,7)-(79,36)
      or from: GoodScalar rb41
        bound by a quantified context at test/tool/CrossTesting.hs:83:12-23
    • In the expression: interpretAst env (gx ast)
      In the expression:
        let
          (var, ast) = funToAstR (tshape vals) (fx1 . f . fx2)
          env = extendEnvR var (parseDomains vals inputs) EM.empty
        in interpretAst env (gx ast)
      In an equation for ‘h’:
          h fx1 fx2 gx inputs
            = let
                (var, ast) = funToAstR (tshape vals) (fx1 . f . fx2)
                env = extendEnvR var (parseDomains vals inputs) EM.empty
              in interpretAst env (gx ast)
   |
83 |         in interpretAst env (gx ast)
   |            ^^^^^^^^^^^^

The message may stem from a quantified constraint where type family applications eventually reduce the "head" of the constraint to Bool ~ Bool, but a "context" of the constraint is a constraint that can't be satisfied due to ambiguous type variables. That's just a guess.

The program fails with GHCs <= 9.4.* much earlier due to another GHC bug (to be reported). The program actually has, sort of, a type error and it's, sort of, signalled by the other error messages. It's that the GoodScalar constraint in class (forall rb41. GoodScalar rb41 => c ranked rb41) is not needed, but can't be satisfied in some cases due to non-injective type families applied to all occurrences of r, which makes r ambiguous. After removing the constraint, the program compiles fine in GHC 9.6.2.