The behaviour provided by this HeytingAlgebra instance is of course useful but it's not a law-abiding instance, unfortunately. For instance, conj and disj are required to be commutative but they're not here, and also, if both a and b are failures, then a || (a && b) will produce a much more verbose error than a; however the HeytingAlgebra laws require that a || (a && b) = a.