Enforce constraints on extensions to satisfy conformance requirements

[kyouko-taiga]

Consider the following program:

trait P {
  type X
  fun foo()
}

trait Q {}

extension P where X: Q {
  fun foo() {}
}

type B: P {
  typealias X = Bool
}

The current implementation will accept the conformance B: P after concluding that the definition of foo in P's extensions satisfies P's requirement. However, that's wrong because Bool does not conform to Q. To fix this problem, we have to collect the constraints associated with the implementations we're considering while processing the requirements of a trait and make sure they are satisfied by the model.

The general problem consists of ensuring that the accumulated constraints on an implementation are implied by the constraints on a requirement. That is not an easy thing to prove but there are probably a couple of simplifications we can make. The first is to say that a generic implementation can never satisfy a requirement unless they have the same signature, modulo substitution of their generic parameters. With this simplification, I think we can say that we only need to care about constraints defined on extensions declaring the implementations we're considering.

The proof that constraints are satisfied has to be made in appendIfDefinition(_:matchting:to:). One change we have to make before that is to ensure constraint solving doesn't prematurely insert diagnostics in the checker, so that we can tentatively solve the constraints of candidate implementations.