Redundant forcing of Given dictionaries
If you look at the test case for #13025 (closed) you'll see code like
f :: (a~~b) => a -> b -> Bool f d x y = case HEq_sc d of (cobox :: a ~# b) -> True
From the Given dictionary
(a~~b), the contraint solver generates a given binding, just in case
(cobox :: a~# b) = HEq_sc d
cobox is a coercion we evaluate this binding strictly, and so the desugarer produces the case expression above. Most redundant Given bindings are let-bound and hence discarded quickly by the occurrence analyser, but GHC doesn't discard cases (termination worries).
So the task here is to remove the redundant Given in some way. (Of course, if the equality is actually used, we need to keep it.)
Note [The equality types story] in
TysPrim for the meanagerie of equality types.