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.