By the way, SMT solvers are (sometimes) able to do this in a non-brute-force way. That is, they will actually make logical deductions to avoid exploring impossible parts of the space. I think logic programming languages will also commonly implement efficient searches for satisfying assignments so that you're not exploring the literal Cartesian product of the variable's domains in every case.

I've heard repeatedly about the interesting discovery that Boolean satisfiability is "hard in theory, but not in practice" because most constraint solving that we want to do inspired by real-world problems apparently has structure that software can identify.

But I also think this is an interesting challenge in its own right for thinking about polymorphism, even without getting into how to find opportunities to make the search non-exhaustive.