Check equality constraints when checking whether a constraint is satisfied

common/check.h

@@ -21,18 +21,18 @@ namespace Carbon {
 //
 // For example:
 // CARBON_CHECK(is_valid) << "Data is not valid!";
-#define CARBON_CHECK(condition) \
- (condition) ? (void)0 \
- : CARBON_RAW_EXITING_STREAM() \
- << "CHECK failure at " << __FILE__ << ":" << __LINE__ \
- << ": " #condition  \
- << Carbon::Internal::ExitingStream::AddSeparator()
+#define CARBON_CHECK(...)  \
+ (__VA_ARGS__) ? (void)0 \
+  : CARBON_RAW_EXITING_STREAM() \
+  << "CHECK failure at " << __FILE__ << ":" << __LINE__ \
+  << ": " #__VA_ARGS__ \
+  << Carbon::Internal::ExitingStream::AddSeparator()
 
 // DCHECK calls CHECK in debug mode, and does nothing otherwise.
 #ifndef NDEBUG
-#define CARBON_DCHECK(condition) CARBON_CHECK(condition)
+#define CARBON_DCHECK(...) CARBON_CHECK(__VA_ARGS__)
 #else
-#define CARBON_DCHECK(condition) CARBON_CHECK(true || (condition))
+#define CARBON_DCHECK(...) CARBON_CHECK(true || (__VA_ARGS__))
 #endif
 
 // This is similar to CHECK, but is unconditional. Writing CARBON_FATAL() is

explorer/data/prelude.carbon

@@ -18,9 +18,21 @@ interface ImplicitAs(T:! Type) {
  extends As(T);
 }
 
-// Every type implicitly converts to itself.
-impl forall [T:! Type] T as ImplicitAs(T) {
- fn Convert[me: Self]() -> T { return me; }
+// TODO: Should we just use an intrinsic for this?
+interface __EqualConverter {
+ let T:! Type;
+ fn Convert(t: T) -> Self;
+}
+fn __EqualConvert[T:! Type](t: T, U:! __EqualConverter where .T = T) -> U {
+ return U.Convert(t);
+}
+impl forall [U:! Type] U as __EqualConverter where .T = U {
+ fn Convert(u: U) -> U { return u; }
+}
+
+// Every type implicitly converts to single-step-equal types.
+impl forall [T:! Type, U:! Type where .Self == T] T as ImplicitAs(U) {
+ fn Convert[me: Self]() -> U { return __EqualConvert(me, U); }
 }
 
 // TODO: Simplify this once we have variadics.

explorer/interpreter/impl_scope.cpp

@@ -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

explorer/interpreter/impl_scope.h

@@ -153,6 +153,26 @@ class ImplScope {
  std::vector<Nonnull<const ImplScope*>> parent_scopes_;
 };
 
+// An equality context that considers two values to be equal if they are a
+// single step apart according to an equality constraint in the given impl
+// scope.
+struct SingleStepEqualityContext : public EqualityContext {
+ public:
+ SingleStepEqualityContext(Nonnull<const ImplScope*> impl_scope)
+ : impl_scope_(impl_scope) {}
+
+ // Visits the values that are equal to the given value and a single step away
+ // according to an equality constraint that is in the given impl scope. Stops
+ // and returns `false` if the visitor returns `false`, otherwise returns
+ // `true`.
+ auto VisitEqualValues(Nonnull<const Value*> value,
+ llvm::function_ref<bool(Nonnull<const Value*>)> visitor)
+ const -> bool override;
+
+ private:
+ Nonnull<const ImplScope*> impl_scope_;
+};
+
 } // namespace Carbon
 
 #endif // CARBON_EXPLORER_INTERPRETER_IMPL_SCOPE_H_

explorer/interpreter/interpreter.cpp

@@ -538,35 +538,47 @@ auto Interpreter::EvalRecursively(std::unique_ptr<Action> action)
 auto Interpreter::EvalAssociatedConstant(
  Nonnull<const AssociatedConstant*> assoc, SourceLocation source_loc)
  -> ErrorOr<Nonnull<const Value*>> {
- // Find the witness.
+ // Instantiate the associated constant.
+ CARBON_ASSIGN_OR_RETURN(Nonnull<const Value*> base,
+ InstantiateType(&assoc->base(), source_loc));
+ CARBON_ASSIGN_OR_RETURN(Nonnull<const Value*> interface,
+ InstantiateType(&assoc->interface(), source_loc));
  CARBON_ASSIGN_OR_RETURN(Nonnull<const Witness*> witness,
  InstantiateWitness(&assoc->witness()));
- if (!isa<ImplWitness>(witness)) {
+ Nonnull<const AssociatedConstant*> instantiated_assoc =
+ arena_->New<AssociatedConstant>(base, cast<InterfaceType>(interface),
+ &assoc->constant(), witness);
+
+ auto* impl_witness = dyn_cast<ImplWitness>(witness);
+ if (!impl_witness) {
  CARBON_CHECK(phase() == Phase::CompileTime)
  << "symbolic witnesses should only be formed at compile time";
- return ProgramError(source_loc)
- << "value of associated constant " << *assoc << " is not known";
+ return instantiated_assoc;
  }
 
- auto& impl_witness = cast<ImplWitness>(*witness);
+ // We have an impl. Extract the value from it.
  Nonnull<const ConstraintType*> constraint =
- impl_witness.declaration().constraint_type();
+ impl_witness->declaration().constraint_type();
  std::optional<Nonnull<const Value*>> result;
- constraint->VisitEqualValues(assoc, [&](Nonnull<const Value*> equal_value) {
- // TODO: The value might depend on the parameters of the impl. We need to
- // substitute impl_witness.type_args() into the value or constraint.
- if (isa<AssociatedConstant>(equal_value)) {
- return true;
- }
- // TODO: This makes an arbitrary choice if there's more than one equal
- // value. It's not clear how to handle that case.
- result = equal_value;
- return false;
- });
+ // TODO: We should pick the value from the rewrite constraint, not some other
+ // equality constraint that happens to be in the impl's constraint type.
+ constraint->VisitEqualValues(instantiated_assoc,
+ [&](Nonnull<const Value*> equal_value) {
+ // TODO: The value might depend on the
+ // parameters of the impl. We need to
+ // substitute impl_witness->type_args() into
+ // the value or constraint.
+ if (isa<AssociatedConstant>(equal_value)) {
+ return true;
+ }
+ result = equal_value;
+ return false;
+ });
  if (!result) {
- CARBON_FATAL() << impl_witness.declaration() << " with constraint "
+ CARBON_FATAL() << impl_witness->declaration() << " with constraint "
  << *constraint
- << " is missing value for associated constant " << *assoc;
+ << " is missing value for associated constant "
+ << *instantiated_assoc;
  }
  return *result;
 }
@@ -585,6 +597,14 @@ auto Interpreter::InstantiateType(Nonnull<const Value*> type,
  }
  return value;
  }
+ case Value::Kind::InterfaceType: {
+ const auto& interface_type = cast<InterfaceType>(*type);
+ CARBON_ASSIGN_OR_RETURN(
+ Nonnull<const Bindings*> bindings,
+ InstantiateBindings(&interface_type.bindings(), source_loc));
+ return arena_->New<InterfaceType>(&interface_type.declaration(),
+ bindings);
+ }
  case Value::Kind::NominalClassType: {
  const auto& class_type = cast<NominalClassType>(*type);
  CARBON_ASSIGN_OR_RETURN(
@@ -603,7 +623,7 @@ auto Interpreter::InstantiateType(Nonnull<const Value*> type,
  CARBON_ASSIGN_OR_RETURN(
  Nonnull<const Value*> type_value,
  EvalAssociatedConstant(cast<AssociatedConstant>(type), source_loc));
- return InstantiateType(type_value, source_loc);
+ return type_value;
  }
  default:
  return type;
@@ -715,9 +735,12 @@ auto Interpreter::Convert(Nonnull<const Value*> value,
  InstantiateType(destination_type, source_loc));
  return arena_->New<NominalClassValue>(inst_dest, value);
  }
- default:
- CARBON_FATAL() << "Can't convert value " << *value << " to type "
- << *destination_type;
+ default: {
+ CARBON_CHECK(IsValueKindDependent(destination_type))
+ << "Can't convert value " << *value << " to type "
+ << *destination_type;
+ return value;
+ }
  }
  }
  case Value::Kind::StructType: {
@@ -747,9 +770,12 @@ auto Interpreter::Convert(Nonnull<const Value*> value,
  &array_type.element_type());
  break;
  }
- default:
- CARBON_FATAL() << "Can't convert value " << *value << " to type "
- << *destination_type;
+ default: {
+ CARBON_CHECK(IsValueKindDependent(destination_type))
+ << "Can't convert value " << *value << " to type "
+ << *destination_type;
+ return value;
+ }
  }
  CARBON_CHECK(tuple->elements().size() ==
  destination_element_types.size());
@@ -767,6 +793,10 @@ auto Interpreter::Convert(Nonnull<const Value*> value,
  CARBON_ASSIGN_OR_RETURN(
  Nonnull<const Value*> value,
  EvalAssociatedConstant(cast<AssociatedConstant>(value), source_loc));
+ if (isa<AssociatedConstant>(value)) {
+ return ProgramError(source_loc)
+ << "value of associated constant " << *value << " is not known";
+ }
  return Convert(value, destination_type, source_loc);
  }
  }