Require convertibility to the type of the associated constant when checking a rewrite constraint. (#2321)

Per recent discussion, in `... where .A = B`, require that `B` is implicitly convertible to the type of `A` immediately, rather than treating that as part of the criteria that a type must satisfy to satisfy the resulting constraint. Extend the implementation of implicit conversion so that conversion of a type to a constraint checks that the type satisfies the constraint.

As part of implementing this, stop duplicating rewrite constraints as equality constraints. Instead, when checking that a constraint is satisfied, check both its equality constraints and its rewrite constraints. This fixes an infinite recursion that would otherwise be caused by this change, and is also a necessary prerequisite for applying rewrite constraints to equality constraints, where we would otherwise collapse the implied equality constraints to a tautological `V == V` constraint.

In passing, make ErrorBuilder support building the error message more incrementally and use that to improve diagnostics for mismatched values with equality constraints.
This commit is contained in:
Richard Smith
2022-10-20 16:18:26 -07:00
committed by GitHub
parent 4601a9cce8
commit 374bf9f853
17 changed files with 572 additions and 233 deletions
+44 -9
View File
@@ -65,6 +65,31 @@ void ImplScope::AddParent(Nonnull<const ImplScope*> parent) {
parent_scopes_.push_back(parent);
}
// Checks that `a_evaluated == b_evaluated` for the purpose of an equality
// constraint. Produces an error if not.
static auto CheckEqualOrDiagnose(SourceLocation source_loc,
Nonnull<const Value*> a_written,
Nonnull<const Value*> a_evaluated,
Nonnull<const Value*> b_written,
Nonnull<const Value*> b_evaluated,
Nonnull<const EqualityContext*> equality_ctx)
-> ErrorOr<Success> {
if (ValueEqual(a_evaluated, b_evaluated, equality_ctx)) {
return Success();
}
auto error = ProgramError(source_loc);
error << "constraint requires that " << *a_written;
if (!ValueEqual(a_written, a_evaluated, std::nullopt)) {
error << " (with value " << *a_evaluated << ")";
}
error << " == " << *b_written;
if (!ValueEqual(b_written, b_evaluated, std::nullopt)) {
error << " (with value " << *b_evaluated << ")";
}
error << ", which is not known to be true";
return std::move(error);
}
auto ImplScope::Resolve(Nonnull<const Value*> constraint_type,
Nonnull<const Value*> impl_type,
SourceLocation source_loc,
@@ -103,10 +128,13 @@ auto ImplScope::Resolve(Nonnull<const Value*> constraint_type,
witnesses.push_back(result);
}
// Check that all equality constraints are satisfied in this scope.
if (llvm::ArrayRef<EqualityConstraint> equals =
constraint->equality_constraints();
!equals.empty()) {
// Check that all equality and rewrite constraints are satisfied in this
// scope.
llvm::ArrayRef<EqualityConstraint> equals =
constraint->equality_constraints();
llvm::ArrayRef<RewriteConstraint> rewrites =
constraint->rewrite_constraints();
if (!equals.empty() || !rewrites.empty()) {
std::optional<Nonnull<const Witness*>> witness;
if (constraint->self_binding()->impl_binding()) {
witness = type_checker.MakeConstraintWitness(witnesses);
@@ -121,13 +149,20 @@ auto ImplScope::Resolve(Nonnull<const Value*> constraint_type,
for (; it != equal.values.end(); ++it) {
Nonnull<const Value*> current =
type_checker.Substitute(local_bindings, *it);
if (!ValueEqual(first, current, &equality_ctx)) {
return ProgramError(source_loc)
<< "constraint requires that " << *first
<< " == " << *current << ", which is not known to be true";
}
CARBON_RETURN_IF_ERROR(
CheckEqualOrDiagnose(source_loc, equal.values.front(), first, *it,
current, &equality_ctx));
}
}
for (auto& rewrite : rewrites) {
Nonnull<const Value*> constant =
type_checker.Substitute(local_bindings, rewrite.constant);
Nonnull<const Value*> value = type_checker.Substitute(
local_bindings, rewrite.converted_replacement);
CARBON_RETURN_IF_ERROR(CheckEqualOrDiagnose(
source_loc, rewrite.constant, constant,
rewrite.converted_replacement, value, &equality_ctx));
}
}
return type_checker.MakeConstraintWitness(std::move(witnesses));
}