Check equality constraints when checking whether a constraint is satisfied (#2294)

Add checking that a type only satisfies a constraint if it satisfies all of that constraint's equality and rewrite constraints.

Enforce the rule that `=` must be used in impls when specifying associated constant values rather than `==`.

Turn off the pre-#2173 single-step equality behavior. This is getting somewhat ahead of the approved design, but it's a one-line change to restore the old behavior.

Fix `CARBON_CHECK` to handle top-level `,`s in its argument, such as may happen in template argument lists, as this change introduces such a check.
This commit is contained in:
Richard Smith
2022-10-17 22:07:19 -07:00
committed by GitHub
parent 8ee0ecec94
commit 4b679510e7
43 changed files with 443 additions and 200 deletions
+34 -1
View File
@@ -103,7 +103,34 @@ auto ImplScope::Resolve(Nonnull<const Value*> constraint_type,
source_loc, type_checker));
witnesses.push_back(result);
}
// TODO: Check satisfaction of same-type constraints.
// Check that all equality constraints are satisfied in this scope.
if (llvm::ArrayRef<EqualityConstraint> equals =
constraint->equality_constraints();
!equals.empty()) {
std::optional<Nonnull<const Witness*>> witness;
if (constraint->self_binding()->impl_binding()) {
witness = type_checker.MakeConstraintWitness(*constraint, witnesses,
source_loc);
}
Bindings local_bindings = bindings;
local_bindings.Add(constraint->self_binding(), impl_type, witness);
SingleStepEqualityContext equality_ctx(this);
for (auto& equal : equals) {
auto it = equal.values.begin();
Nonnull<const Value*> first =
type_checker.Substitute(local_bindings, *it++);
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";
}
}
}
}
return type_checker.MakeConstraintWitness(*constraint, std::move(witnesses),
source_loc);
}
@@ -233,4 +260,10 @@ void ImplScope::Print(llvm::raw_ostream& out) const {
}
}
auto SingleStepEqualityContext::VisitEqualValues(
Nonnull<const Value*> value,
llvm::function_ref<bool(Nonnull<const Value*>)> visitor) const -> bool {
return impl_scope_->VisitEqualValues(value, visitor);
}
} // namespace Carbon