Now, it bases the type the quantifier ranges over on the goal, instead
of the witness. This works better when dealing with witnesses involving
type class constraints.