GitLab

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

But because 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.)

NB: See Note [The equality types story] in TysPrim for the meanagerie of equality types.

Trac metadata

Trac field	Value
Version	8.0.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture