A tricky bug to do with the way the implication constraints are solved in TcSimplify. See Note [Reducing implication constraints].