From 374bf9f853a5b4c74a5669655c603c8ffee3dd16 Mon Sep 17 00:00:00 2001 From: Richard Smith Date: Thu, 20 Oct 2022 16:18:26 -0700 Subject: [PATCH] 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. --- common/error.h | 12 +- explorer/interpreter/impl_scope.cpp | 53 +- explorer/interpreter/interpreter.cpp | 35 +- explorer/interpreter/type_checker.cpp | 493 +++++++++++------- explorer/interpreter/type_checker.h | 28 +- explorer/interpreter/value.cpp | 10 +- explorer/interpreter/value.h | 25 +- .../assoc_const/fail_different_type.carbon | 2 +- .../assoc_const/fail_different_value.carbon | 2 +- .../assoc_const/fail_equal_indirectly.carbon | 4 +- .../fail_equal_to_dependent_type.carbon | 6 +- .../fail_implied_constraints.carbon | 33 ++ .../assoc_const/fail_missing_equal.carbon | 27 + .../assoc_const/fail_missing_rewrite.carbon | 27 + .../fail_overspecified_impl.carbon | 2 +- ...il_rewrite_depends_on_later_rewrite.carbon | 23 + .../rewrite_depends_on_prior_rewrite.carbon | 23 + 17 files changed, 572 insertions(+), 233 deletions(-) create mode 100644 explorer/testdata/assoc_const/fail_implied_constraints.carbon create mode 100644 explorer/testdata/assoc_const/fail_missing_equal.carbon create mode 100644 explorer/testdata/assoc_const/fail_missing_rewrite.carbon create mode 100644 explorer/testdata/assoc_const/fail_rewrite_depends_on_later_rewrite.carbon create mode 100644 explorer/testdata/assoc_const/rewrite_depends_on_prior_rewrite.carbon diff --git a/common/error.h b/common/error.h index bc0d27f21c1a..3975cde03e70 100644 --- a/common/error.h +++ b/common/error.h @@ -131,9 +131,17 @@ class ErrorBuilder { : location_(std::move(location)), out_(std::make_unique(message_)) {} - // Accumulates string message. + // Accumulates string message to a temporary `ErrorBuilder`. After streaming, + // the builder must be converted to an `Error` or `ErrorOr`. template - [[nodiscard]] auto operator<<(const T& message) -> ErrorBuilder& { + [[nodiscard]] auto operator<<(const T& message) && -> ErrorBuilder&& { + *out_ << message; + return std::move(*this); + } + + // Accumulates string message for an lvalue error builder. + template + auto operator<<(const T& message) & -> ErrorBuilder& { *out_ << message; return *this; } diff --git a/explorer/interpreter/impl_scope.cpp b/explorer/interpreter/impl_scope.cpp index 0d6668ef9173..a7a97c300310 100644 --- a/explorer/interpreter/impl_scope.cpp +++ b/explorer/interpreter/impl_scope.cpp @@ -65,6 +65,31 @@ void ImplScope::AddParent(Nonnull 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 a_written, + Nonnull a_evaluated, + Nonnull b_written, + Nonnull b_evaluated, + Nonnull equality_ctx) + -> ErrorOr { + 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 constraint_type, Nonnull impl_type, SourceLocation source_loc, @@ -103,10 +128,13 @@ auto ImplScope::Resolve(Nonnull constraint_type, witnesses.push_back(result); } - // Check that all equality constraints are satisfied in this scope. - if (llvm::ArrayRef equals = - constraint->equality_constraints(); - !equals.empty()) { + // Check that all equality and rewrite constraints are satisfied in this + // scope. + llvm::ArrayRef equals = + constraint->equality_constraints(); + llvm::ArrayRef rewrites = + constraint->rewrite_constraints(); + if (!equals.empty() || !rewrites.empty()) { std::optional> witness; if (constraint->self_binding()->impl_binding()) { witness = type_checker.MakeConstraintWitness(witnesses); @@ -121,13 +149,20 @@ auto ImplScope::Resolve(Nonnull constraint_type, for (; it != equal.values.end(); ++it) { Nonnull 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 constant = + type_checker.Substitute(local_bindings, rewrite.constant); + Nonnull 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)); } diff --git a/explorer/interpreter/interpreter.cpp b/explorer/interpreter/interpreter.cpp index a040ba0c034d..ffe5ee82685b 100644 --- a/explorer/interpreter/interpreter.cpp +++ b/explorer/interpreter/interpreter.cpp @@ -537,46 +537,39 @@ auto Interpreter::EvalAssociatedConstant( Nonnull assoc, SourceLocation source_loc) -> ErrorOr> { // Instantiate the associated constant. - CARBON_ASSIGN_OR_RETURN(Nonnull base, - InstantiateType(&assoc->base(), source_loc)); CARBON_ASSIGN_OR_RETURN(Nonnull interface, InstantiateType(&assoc->interface(), source_loc)); CARBON_ASSIGN_OR_RETURN(Nonnull witness, InstantiateWitness(&assoc->witness())); - Nonnull instantiated_assoc = - arena_->New(base, cast(interface), - &assoc->constant(), witness); const auto* impl_witness = dyn_cast(witness); if (!impl_witness) { CARBON_CHECK(phase() == Phase::CompileTime) << "symbolic witnesses should only be formed at compile time"; - return instantiated_assoc; + CARBON_ASSIGN_OR_RETURN(Nonnull base, + InstantiateType(&assoc->base(), source_loc)); + return arena_->New(base, cast(interface), + &assoc->constant(), witness); } // We have an impl. Extract the value from it. Nonnull constraint = impl_witness->declaration().constraint_type(); std::optional> result; - // 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 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(equal_value)) { - return true; - } - result = equal_value; - return false; - }); + for (auto& rewrite : constraint->rewrite_constraints()) { + if (&rewrite.constant->constant() == &assoc->constant() && + TypeEqual(&rewrite.constant->interface(), interface, std::nullopt)) { + // TODO: The value might depend on the parameters of the impl. We need to + // substitute impl_witness->type_args() into the value. + result = rewrite.converted_replacement; + break; + } + } if (!result) { CARBON_FATAL() << impl_witness->declaration() << " with constraint " << *constraint << " is missing value for associated constant " - << *instantiated_assoc; + << *interface << "." << assoc->constant().binding().name(); } return *result; } diff --git a/explorer/interpreter/type_checker.cpp b/explorer/interpreter/type_checker.cpp index bc076516828b..7da79e414b57 100644 --- a/explorer/interpreter/type_checker.cpp +++ b/explorer/interpreter/type_checker.cpp @@ -20,10 +20,12 @@ #include "explorer/interpreter/pattern_analysis.h" #include "explorer/interpreter/value.h" #include "llvm/ADT/DenseSet.h" +#include "llvm/ADT/ScopeExit.h" #include "llvm/ADT/StringExtras.h" #include "llvm/ADT/TinyPtrVector.h" #include "llvm/Support/Casting.h" #include "llvm/Support/Error.h" +#include "llvm/Support/SaveAndRestore.h" using llvm::cast; using llvm::dyn_cast; @@ -482,19 +484,12 @@ auto TypeChecker::IsImplicitlyConvertible( break; } case Value::Kind::TypeType: - // TODO: This seems suspicious. Shouldn't this require that the type - // implements the interface? - if (isa(destination)) { - return true; - } - break; case Value::Kind::InterfaceType: case Value::Kind::ConstraintType: - // TODO: These types should presumably also convert to constraint types. - if (isa(destination)) { - return true; - } - break; + // TODO: We can't tell whether the conversion to this type-of-type would + // work, because that depends on the source value, and we only have its + // type. + return IsTypeOfType(destination); default: break; } @@ -520,6 +515,24 @@ auto TypeChecker::ImplicitlyConvert(std::string_view context, -> ErrorOr> { Nonnull source_type = &source->static_type(); + // A type implicitly converts to a constraint if there is an impl of that + // constraint for that type in scope. + if (isa(destination)) { + CARBON_ASSIGN_OR_RETURN( + Nonnull destination_constraint, + ConvertToConstraintType(source->source_loc(), "implicit conversion", + destination)); + CARBON_ASSIGN_OR_RETURN(Nonnull source_value, + InterpExp(source, arena_, trace_stream_)); + // Note, we discard the witness. We don't actually need it in order to + // perform the conversion, but we do want to know it exists. + CARBON_RETURN_IF_ERROR(impl_scope.Resolve( + destination_constraint, source_value, source->source_loc(), *this)); + // This conversion is a no-op at runtime. + // TODO: Should we record the change in type in the AST? + return source; + } + // TODO: If a builtin conversion works, for now we don't create any // expression to do the conversion and rely on the interpreter to know how to // do it. @@ -1073,12 +1086,25 @@ class TypeChecker::ConstraintTypeBuilder { : ConstraintTypeBuilder(arena, MakeSelfBinding(arena, source_loc)) {} ConstraintTypeBuilder(Nonnull arena, Nonnull self_binding) - : self_binding_(PrepareSelfBinding(arena, self_binding)), + : arena_(arena), + self_binding_(PrepareSelfBinding(arena, self_binding)), impl_binding_(AddImplBinding(arena, self_binding_)) {} - ConstraintTypeBuilder(Nonnull /*arena*/, + ConstraintTypeBuilder(Nonnull arena, Nonnull self_binding, Nonnull impl_binding) - : self_binding_(self_binding), impl_binding_(impl_binding) {} + : arena_(arena), + self_binding_(self_binding), + impl_binding_(impl_binding) {} + + // Returns the self binding for this builder. + auto self_binding() const -> Nonnull { + return self_binding_; + } + + // Returns the current set of rewrite constraints for this builder. + auto rewrite_constraints() const -> llvm::ArrayRef { + return rewrite_constraints_; + } // Produces a type that refers to the `.Self` type of the constraint. auto GetSelfType() const -> Nonnull { @@ -1125,21 +1151,18 @@ class TypeChecker::ConstraintTypeBuilder { ConstraintType::RewriteConstraint rewrite) -> ErrorOr { for (ConstraintType::RewriteConstraint existing : rewrite_constraints_) { - if (ValueEqual(existing.interface, rewrite.interface, std::nullopt) && - // TODO: Want a "declares same entity" check. - GetName(*existing.constant) == GetName(*rewrite.constant)) { - if (ValueEqual(&existing.replacement->value(), - &rewrite.replacement->value(), std::nullopt) && - TypeEqual(&existing.replacement->static_type(), - &rewrite.replacement->static_type(), std::nullopt)) { + if (ValueEqual(existing.constant, rewrite.constant, std::nullopt)) { + if (ValueEqual(existing.unconverted_replacement, + rewrite.unconverted_replacement, std::nullopt) && + TypeEqual(existing.unconverted_replacement_type, + rewrite.unconverted_replacement_type, std::nullopt)) { return Success(); } return ProgramError(source_loc) - << "multiple different rewrites for `.(" - << *rewrite.interface << "." << *GetName(*rewrite.constant) - << ")`:\n" - << " " << existing.replacement->value() << "\n" - << " " << rewrite.replacement->value(); + << "multiple different rewrites for `" << *rewrite.constant + << "`:\n" + << " " << *existing.unconverted_replacement << "\n" + << " " << *rewrite.unconverted_replacement; } } rewrite_constraints_.push_back(rewrite); @@ -1162,6 +1185,7 @@ class TypeChecker::ConstraintTypeBuilder { // resulting constraint, and can be `GetSelfWitness()`. The `bindings` // parameter specifies any additional substitutions to perform. auto AddAndSubstitute(const TypeChecker& type_checker, + SourceLocation source_loc, Nonnull constraint, Nonnull self, Nonnull self_witness, @@ -1190,22 +1214,42 @@ class TypeChecker::ConstraintTypeBuilder { constraint->self_binding(), self, type_checker.MakeConstraintWitness(std::move(witnesses))); + // If lookups into the resulting constraint should look into this added + // constraint, then rewrites for this added constraint become rewrites for + // the resulting constraint. Otherwise, discard the rewrites and keep only + // their corresponding equality constraints. // TODO: What happens if these rewrites appear in the impl constraints? // TODO: What happens if these rewrites appear in each other? for (const auto& rewrite_constraint : constraint->rewrite_constraints()) { const auto* interface = cast(type_checker.Substitute( - local_bindings, rewrite_constraint.interface)); - Nonnull value = type_checker.Substitute( - local_bindings, &rewrite_constraint.replacement->value()); - Nonnull type = type_checker.Substitute( - local_bindings, &rewrite_constraint.replacement->static_type()); - auto* replacement = type_checker.arena_->New( - rewrite_constraint.replacement->source_loc(), value, type, - ValueCategory::Let); - CARBON_RETURN_IF_ERROR(AddRewriteConstraint( - replacement->source_loc(), {.interface = interface, - .constant = rewrite_constraint.constant, - .replacement = replacement})); + local_bindings, &rewrite_constraint.constant->interface())); + Nonnull converted_value = type_checker.Substitute( + local_bindings, rewrite_constraint.converted_replacement); + + // Form a symbolic value naming the non-rewritten associated constant. + // The impl constraint will always already exist. + int index = AddImplConstraint({.type = self, .interface = interface}); + const auto* witness = + type_checker.MakeConstraintWitnessAccess(self_witness, index); + const auto* constant_value = arena_->New( + self, interface, &rewrite_constraint.constant->constant(), witness); + + if (add_lookup_contexts) { + // Add the constraint `.(I.C) = V`, tracking the value and type prior + // to conversion for use in rewrites. + Nonnull value = type_checker.Substitute( + local_bindings, rewrite_constraint.unconverted_replacement); + Nonnull type = type_checker.Substitute( + local_bindings, rewrite_constraint.unconverted_replacement_type); + CARBON_RETURN_IF_ERROR(AddRewriteConstraint( + source_loc, {.constant = constant_value, + .unconverted_replacement = value, + .unconverted_replacement_type = type, + .converted_replacement = converted_value})); + } else { + // Add the constraint `Self.(I.C) == V`. + AddEqualityConstraint({.values = {constant_value, converted_value}}); + } } for (const auto& equality_constraint : constraint->equality_constraints()) { @@ -1231,33 +1275,45 @@ class TypeChecker::ConstraintTypeBuilder { return Success(); } - class ImplsInScopeTracker { + class ConstraintsInScopeTracker { friend class ConstraintTypeBuilder; private: - int num_added = 0; + int num_impls_added = 0; + int num_equals_added = 0; }; - // Brings all the `impl`s accumulated so far into the given impl scope. - // If this will be called more than once, an ImplsInScopeTracker can be - // provided to avoid adding the same impls more than once. - void BringImplsIntoScope( - const TypeChecker& type_checker, Nonnull impl_scope, - std::optional> tracker = std::nullopt) { - llvm::ArrayRef impl_constraints = - impl_constraints_; - if (tracker) { - impl_constraints = impl_constraints.drop_front((*tracker)->num_added); - (*tracker)->num_added = impl_constraints_.size(); + // Brings all the constraints accumulated so far into the given impl scope, + // as if we built the constraint type and then added it into the scope. If + // this will be called more than once, an ImplsInScopeTracker can be provided + // to avoid adding the same impls more than once. + void BringConstraintsIntoScope(const TypeChecker& type_checker, + Nonnull impl_scope, + Nonnull tracker) { + // Figure out which constraints we're going to add. + int first_impl_to_add = + std::exchange(tracker->num_impls_added, impl_constraints_.size()); + int first_equal_to_add = + std::exchange(tracker->num_equals_added, equality_constraints_.size()); + auto new_impl_constraints = + llvm::ArrayRef(impl_constraints_) + .drop_front(first_impl_to_add); + auto new_equality_constraints = + llvm::ArrayRef( + equality_constraints_) + .drop_front(first_equal_to_add); + + // Add all of the new constraints. + impl_scope->Add(new_impl_constraints, llvm::None, llvm::None, + GetSelfWitness(), type_checker); + for (auto& equal : new_equality_constraints) { + impl_scope->AddEqualityConstraint(arena_->New(equal)); } - impl_scope->Add(impl_constraints, llvm::None, llvm::None, GetSelfWitness(), - type_checker); - // TODO: Bring equality constraints into scope too. } // Converts the builder into a ConstraintType. Note that this consumes the // builder. - auto Build(Nonnull arena) && -> Nonnull { + auto Build() && -> Nonnull { // Rewrite `Self.X is Y` to `Replacement is Y` if we have a rewrite for // `Self.X`. // TODO: Properly apply rewrites throughout all the constraints. Check for @@ -1267,13 +1323,10 @@ class TypeChecker::ConstraintTypeBuilder { do { performed_rewrite = false; if (const auto* assoc = - dyn_cast(impl_constraint.type); - assoc && ValueEqual(&assoc->base(), GetSelfType(), std::nullopt)) { + dyn_cast(impl_constraint.type)) { for (const auto& rewrite : rewrite_constraints_) { - if (&assoc->constant() == rewrite.constant && - ValueEqual(&assoc->interface(), rewrite.interface, - std::nullopt)) { - impl_constraint.type = &rewrite.replacement->value(); + if (ValueEqual(assoc, rewrite.constant, std::nullopt)) { + impl_constraint.type = rewrite.converted_replacement; performed_rewrite = true; } } @@ -1282,7 +1335,7 @@ class TypeChecker::ConstraintTypeBuilder { } // Create the new type. - auto* result = arena->New( + auto* result = arena_->New( self_binding_, std::move(impl_constraints_), std::move(equality_constraints_), std::move(rewrite_constraints_), std::move(lookup_contexts_)); @@ -1326,6 +1379,7 @@ class TypeChecker::ConstraintTypeBuilder { return impl_binding; } + Nonnull arena_; Nonnull self_binding_; Nonnull impl_binding_; std::vector impl_constraints_; @@ -1439,15 +1493,16 @@ auto TypeChecker::Substitute(const Bindings& bindings, cast(Substitute(bindings, &assoc.interface())); // If we're substituting into an associated constant, we may now be able // to rewrite it to a concrete value. - if (std::optional rewritten_value = + if (auto rewritten_value = LookupRewriteInTypeOf(base, interface, &assoc.constant())) { - return &rewritten_value.value()->value(); + return (*rewritten_value)->converted_replacement; } const auto* witness = cast(Substitute(bindings, &assoc.witness())); - if (std::optional rewritten_value = + witness = RefineWitness(witness, base, interface); + if (auto rewritten_value = LookupRewriteInWitness(witness, interface, &assoc.constant())) { - return &rewritten_value.value()->value(); + return (*rewritten_value)->converted_replacement; } return arena_->New(base, interface, &assoc.constant(), witness); @@ -1543,16 +1598,18 @@ auto TypeChecker::Substitute(const Bindings& bindings, } ConstraintTypeBuilder builder(arena_, constraint.self_binding()->source_loc()); - ErrorOr result = - builder.AddAndSubstitute(*this, &constraint, builder.GetSelfType(), - builder.GetSelfWitness(), bindings, - /*add_lookup_contexts=*/true); + // Diagnostics are discarded (except in CHECK failure message). + SourceLocation source_loc("", 0); + ErrorOr result = builder.AddAndSubstitute( + *this, source_loc, &constraint, builder.GetSelfType(), + builder.GetSelfWitness(), bindings, + /*add_lookup_contexts=*/true); // TODO: This appears to theoretically be possible, and should be handled // better. CARBON_CHECK(result.ok()) << "substitution into " << constraint << " failed: " << result.error(); Nonnull new_constraint = - std::move(builder).Build(arena_); + std::move(builder).Build(); if (trace_stream_) { **trace_stream_ << "substitution: " << constraint << " => " << *new_constraint << "\n"; @@ -1635,6 +1692,42 @@ auto TypeChecker::Substitute(const Bindings& bindings, } } +auto TypeChecker::RefineWitness(Nonnull witness, + Nonnull type, + Nonnull constraint) const + -> Nonnull { + if (!top_level_impl_scope_) { + return witness; + } + + // See if this is already resolved as some number of layers of + // ConstraintImplWitness applied to an ImplWitness. + Nonnull inner_witness = witness; + while (auto* inner_constraint_impl_witness = + dyn_cast(inner_witness)) { + inner_witness = inner_constraint_impl_witness->constraint_witness(); + } + if (isa(inner_witness)) { + return witness; + } + + // No source location; diagnostics will be discarded. + SourceLocation source_loc("", 0); + + // Attempt to look for an impl witness in the top-level impl scope. + if (auto refined_witness = (*top_level_impl_scope_) + ->Resolve(constraint, type, source_loc, *this); + refined_witness.ok()) { + return *refined_witness; + } else { + if (trace_stream_) { + **trace_stream_ << "could not refine " << *witness << ": " + << refined_witness.error().message() << "\n"; + } + return witness; + } +} + auto TypeChecker::MatchImpl(const InterfaceType& iface, Nonnull impl_type, const ImplScope::Impl& impl, @@ -1706,7 +1799,7 @@ auto TypeChecker::MakeConstraintWitnessAccess(Nonnull witness, } auto TypeChecker::MakeConstraintForInterface( - SourceLocation source_loc, Nonnull iface_type) + SourceLocation source_loc, Nonnull iface_type) const -> ErrorOr> { CARBON_RETURN_IF_ERROR( ExpectCompleteType(source_loc, "constraint", iface_type)); @@ -1720,16 +1813,16 @@ auto TypeChecker::MakeConstraintForInterface( } ConstraintTypeBuilder builder(arena_, source_loc); - CARBON_RETURN_IF_ERROR( - builder.AddAndSubstitute(*this, *constraint_type, builder.GetSelfType(), - builder.GetSelfWitness(), iface_type->bindings(), - /*add_lookup_contexts=*/true)); - return std::move(builder).Build(arena_); + CARBON_RETURN_IF_ERROR(builder.AddAndSubstitute( + *this, source_loc, *constraint_type, builder.GetSelfType(), + builder.GetSelfWitness(), iface_type->bindings(), + /*add_lookup_contexts=*/true)); + return std::move(builder).Build(); } -auto TypeChecker::ConvertToConstraintType(SourceLocation source_loc, - std::string_view context, - Nonnull constraint) +auto TypeChecker::ConvertToConstraintType( + SourceLocation source_loc, std::string_view context, + Nonnull constraint) const -> ErrorOr> { if (const auto* constraint_type = dyn_cast(constraint)) { return constraint_type; @@ -1740,10 +1833,8 @@ auto TypeChecker::ConvertToConstraintType(SourceLocation source_loc, if (isa(constraint)) { // TODO: Should we build this once and cache it? ConstraintTypeBuilder builder(arena_, source_loc); - return std::move(builder).Build(arena_); + return std::move(builder).Build(); } - // TODO: Should we convert `TypeOfXType` into the constraint - // `Type where .Self == X`? return ProgramError(source_loc) << "expected a constraint in " << context << ", found " << *constraint; @@ -1755,12 +1846,12 @@ auto TypeChecker::CombineConstraints( -> ErrorOr> { ConstraintTypeBuilder builder(arena_, source_loc); for (Nonnull constraint : constraints) { - CARBON_RETURN_IF_ERROR( - builder.AddAndSubstitute(*this, constraint, builder.GetSelfType(), - builder.GetSelfWitness(), Bindings(), - /*add_lookup_contexts=*/true)); + CARBON_RETURN_IF_ERROR(builder.AddAndSubstitute( + *this, source_loc, constraint, builder.GetSelfType(), + builder.GetSelfWitness(), Bindings(), + /*add_lookup_contexts=*/true)); } - return std::move(builder).Build(arena_); + return std::move(builder).Build(); } auto TypeChecker::DeduceCallBindings( @@ -1866,15 +1957,34 @@ auto TypeChecker::LookupInConstraint(SourceLocation source_loc, } // Look for a rewrite to use when naming the given interface member in a type -// declared with the given type-of-type. -static auto LookupRewrite(Nonnull type_of_type, +// that has the given list of rewrites. +static auto LookupRewrite(llvm::ArrayRef rewrites, Nonnull interface, Nonnull member) - -> std::optional { + -> std::optional { if (!isa(member)) { return std::nullopt; } + for (auto& rewrite : rewrites) { + if (ValueEqual(interface, &rewrite.constant->interface(), std::nullopt) && + // TODO: Using name comparison here seems brittle. + GetName(*member) == GetName(rewrite.constant->constant())) { + // A ConstraintType can only have one rewrite per (interface, member) + // pair, so we don't need to check the rest. + return &rewrite; + } + } + + return std::nullopt; +} + +// Look for a rewrite to use when naming the given interface member in a type +// declared with the given type-of-type. +static auto LookupRewrite(Nonnull type_of_type, + Nonnull interface, + Nonnull member) + -> std::optional { // Find the set of rewrites. Only ConstraintTypes have rewrites. // TODO: If we can ever see an InterfaceType here, we should convert it to a // constraint type. @@ -1883,17 +1993,7 @@ static auto LookupRewrite(Nonnull type_of_type, rewrites = constraint_type->rewrite_constraints(); } - for (ConstraintType::RewriteConstraint rewrite : rewrites) { - if (ValueEqual(interface, rewrite.interface, std::nullopt) && - // TODO: Using name comparison here seems brittle. - GetName(*member) == GetName(*rewrite.constant)) { - // A ConstraintType can only have one rewrite per (interface, member) - // pair, so we don't need to check the rest. - return rewrite.replacement; - } - } - - return std::nullopt; + return LookupRewrite(rewrites, interface, member); } auto TypeChecker::GetTypeForAssociatedConstant( @@ -1908,7 +2008,7 @@ auto TypeChecker::GetTypeForAssociatedConstant( auto TypeChecker::LookupRewriteInTypeOf( Nonnull type, Nonnull interface, Nonnull member) const - -> std::optional { + -> std::optional { // Given `(T:! C).Y`, look in `C` for rewrites. if (const auto* var_type = dyn_cast(type)) { if (!var_type->binding().has_static_type()) { @@ -1917,6 +2017,15 @@ auto TypeChecker::LookupRewriteInTypeOf( // say there are no rewrites yet. return std::nullopt; } + // If the type is the self type of an incomplete `where` expression, find + // its set of rewrites. These rewrites may not be complete -- earlier + // rewrites will have been applied to later ones, but not vice versa -- but + // those are the intended semantics in this case. + for (auto* where : partial_where_expressions_) { + if (&var_type->binding() == where->self_binding()) { + return LookupRewrite(where->rewrite_constraints(), interface, member); + } + } return LookupRewrite(&var_type->binding().static_type(), interface, member); } @@ -1934,7 +2043,7 @@ auto TypeChecker::LookupRewriteInTypeOf( auto TypeChecker::LookupRewriteInWitness( Nonnull witness, Nonnull interface, Nonnull member) const - -> std::optional { + -> std::optional { if (const auto* impl_witness = dyn_cast(witness)) { Nonnull constraint = Substitute(impl_witness->bindings(), @@ -1945,11 +2054,12 @@ auto TypeChecker::LookupRewriteInWitness( } // Rewrites a member access expression to produce the given constant value. -static void RewriteMemberAccess(Nonnull access, - Nonnull value) { - access->set_static_type(&value->static_type()); - access->set_value_category(value->value_category()); - access->set_constant_value(&value->value()); +static void RewriteMemberAccess( + Nonnull access, + Nonnull value) { + access->set_value_category(ValueCategory::Let); + access->set_static_type(value->unconverted_replacement_type); + access->set_constant_value(value->unconverted_replacement); } // Determine whether the given member declaration declares an instance member. @@ -2432,9 +2542,8 @@ auto TypeChecker::TypeCheckExp(Nonnull e, CARBON_ASSIGN_OR_RETURN( Nonnull impl, impl_scope.Resolve(*iface, *base_type, e->source_loc(), *this)); - if (std::optional> replacement = - LookupRewriteInWitness(impl, *iface, - *member_name.member().declaration())) { + if (auto replacement = LookupRewriteInWitness( + impl, *iface, *member_name.member().declaration())) { RewriteMemberAccess(&access, *replacement); return Success(); } @@ -3029,6 +3138,13 @@ auto TypeChecker::TypeCheckExp(Nonnull e, auto& self = where.self_binding(); ConstraintTypeBuilder builder(arena_, &self); + ConstraintTypeBuilder::ConstraintsInScopeTracker constraint_tracker; + + // Keep track of the builder so that we can look up its rewrites while + // processing later constraints. + partial_where_expressions_.push_back(&builder); + auto pop_partial_where = + llvm::make_scope_exit([&] { partial_where_expressions_.pop_back(); }); // Note, we don't want to call `TypeCheckPattern` here. Most of the setup // for the self binding is instead done by the `ConstraintTypeBuilder`. @@ -3043,17 +3159,19 @@ auto TypeChecker::TypeCheckExp(Nonnull e, base_type)); // Start with the given constraint. - CARBON_RETURN_IF_ERROR( - builder.AddAndSubstitute(*this, base, builder.GetSelfType(), - builder.GetSelfWitness(), Bindings(), - /*add_lookup_contexts=*/true)); - // Constraints from the LHS of `where` are in scope in the RHS. But - // constraints from earlier `where` clauses are not in scope in later - // clauses. - builder.BringImplsIntoScope(*this, &inner_impl_scope); + CARBON_RETURN_IF_ERROR(builder.AddAndSubstitute( + *this, where.source_loc(), base, builder.GetSelfType(), + builder.GetSelfWitness(), Bindings(), + /*add_lookup_contexts=*/true)); // Type-check and apply the `where` clauses. for (Nonnull clause : where.clauses()) { + // Constraints from the LHS of `where` are in scope in the RHS, and + // constraints from earlier `where` clauses are in scope in later + // clauses. + builder.BringConstraintsIntoScope(*this, &inner_impl_scope, + &constraint_tracker); + CARBON_RETURN_IF_ERROR(TypeCheckWhereClause(clause, inner_impl_scope)); switch (clause->kind()) { @@ -3071,10 +3189,10 @@ auto TypeChecker::TypeCheckExp(Nonnull e, "expression after `is`", constraint)); // Transform `where .B is (C where .D is E)` into `where .B is C // and .B.D is E` then add all the resulting constraints. - CARBON_RETURN_IF_ERROR( - builder.AddAndSubstitute(*this, constraint_type, type, - builder.GetSelfWitness(), Bindings(), - /*add_lookup_contexts=*/false)); + CARBON_RETURN_IF_ERROR(builder.AddAndSubstitute( + *this, is_clause.source_loc(), constraint_type, type, + builder.GetSelfWitness(), Bindings(), + /*add_lookup_contexts=*/false)); break; } case WhereClauseKind::EqualsWhereClause: { @@ -3105,45 +3223,55 @@ auto TypeChecker::TypeCheckExp(Nonnull e, << rewrite_clause.member_name() << "` does not name an associated constant"; } - // TODO: Decide what type constraints we want to impose on the - // replacement. Given - // - // interface A { - // let N:! i32; - // } - // fn F[T:! A where .N = (i32, i32)]() {} - // - // ... no call can ever succeed. Should we reject? We want to - // preserve the type of the replacement in the case where it is a - // constraint type containing further rewrites. - CARBON_ASSIGN_OR_RETURN(Nonnull replacement_value, - InterpExp(&rewrite_clause.replacement(), - arena_, trace_stream_)); - auto* replacement = arena_->New( - rewrite_clause.source_loc(), replacement_value, - &rewrite_clause.replacement().static_type(), - ValueCategory::Let); - CARBON_RETURN_IF_ERROR(builder.AddRewriteConstraint( - rewrite_clause.source_loc(), {.interface = result.interface, - .constant = constant, - .replacement = replacement})); - // Also find (or add) `.Self is I`, and add `.Self.T == V`. + + // Find (or add) `.Self is I`, and form a symbolic value naming the + // associated constant. + // TODO: Reject if the impl constraint didn't already exist. int index = builder.AddImplConstraint( {.type = builder.GetSelfType(), .interface = result.interface}); const auto* witness = MakeConstraintWitnessAccess(builder.GetSelfWitness(), index); - builder.AddEqualityConstraint( - {.values = {arena_->New( - builder.GetSelfType(), result.interface, - constant, witness), - replacement_value}}); + auto* constant_value = arena_->New( + builder.GetSelfType(), result.interface, constant, witness); + + // Find the replacement value prior to conversion to the constant's + // type. This is the value we'll rewrite to when type-checking a + // member access. + CARBON_ASSIGN_OR_RETURN(Nonnull replacement_value, + InterpExp(&rewrite_clause.replacement(), + arena_, trace_stream_)); + auto* replacement_literal = arena_->New( + rewrite_clause.source_loc(), replacement_value, + &rewrite_clause.replacement().static_type(), + ValueCategory::Let); + + // Convert the replacement value to the type of the associated + // constant and find the converted value. This is the value that + // we'll produce during evaluation and substitution. + CARBON_ASSIGN_OR_RETURN( + Nonnull converted_expression, + ImplicitlyConvert( + "rewrite constraint", impl_scope, replacement_literal, + GetTypeForAssociatedConstant(constant_value))); + CARBON_ASSIGN_OR_RETURN( + Nonnull converted_value, + InterpExp(converted_expression, arena_, trace_stream_)); + + // Add the rewrite constraint. + CARBON_RETURN_IF_ERROR(builder.AddRewriteConstraint( + rewrite_clause.source_loc(), + {.constant = constant_value, + .unconverted_replacement = replacement_value, + .unconverted_replacement_type = + &replacement_literal->static_type(), + .converted_replacement = converted_value})); break; } } } where.set_rewritten_form(arena_->New( - where.source_loc(), std::move(builder).Build(arena_), + where.source_loc(), std::move(builder).Build(), arena_->New(), ValueCategory::Let)); return Success(); } @@ -3376,9 +3504,9 @@ auto TypeChecker::TypeCheckPattern( // to `T:! `. ConstraintTypeBuilder builder(arena_, &binding, impl_binding); CARBON_RETURN_IF_ERROR(builder.AddAndSubstitute( - *this, constraint, val, witness, Bindings(), + *this, binding.source_loc(), constraint, val, witness, Bindings(), /*add_lookup_contexts=*/true)); - type = std::move(builder).Build(arena_); + type = std::move(builder).Build(); BringImplIntoScope(impl_binding, impl_scope); } @@ -4197,7 +4325,7 @@ auto TypeChecker::DeclareInterfaceDeclaration( // Build a constraint corresponding to this interface. ConstraintTypeBuilder builder(arena_, iface_decl->self()); - ConstraintTypeBuilder::ImplsInScopeTracker impl_tracker; + ConstraintTypeBuilder::ConstraintsInScopeTracker constraint_tracker; iface_decl->self()->set_static_type(iface_type); // The impl constraint says only that the direct members of the interface are @@ -4228,7 +4356,7 @@ auto TypeChecker::DeclareInterfaceDeclaration( ConvertToConstraintType(m->source_loc(), "extends declaration", base)); CARBON_RETURN_IF_ERROR(builder.AddAndSubstitute( - *this, constraint_type, builder.GetSelfType(), + *this, m->source_loc(), constraint_type, builder.GetSelfType(), builder.GetSelfWitness(), Bindings(), /*add_lookup_contexts=*/true)); break; @@ -4247,10 +4375,10 @@ auto TypeChecker::DeclareInterfaceDeclaration( Nonnull constraint_type, ConvertToConstraintType(m->source_loc(), "impl as declaration", constraint)); - CARBON_RETURN_IF_ERROR( - builder.AddAndSubstitute(*this, constraint_type, impl_type, - builder.GetSelfWitness(), Bindings(), - /*add_lookup_contexts=*/false)); + CARBON_RETURN_IF_ERROR(builder.AddAndSubstitute( + *this, m->source_loc(), constraint_type, impl_type, + builder.GetSelfWitness(), Bindings(), + /*add_lookup_contexts=*/false)); break; } @@ -4271,10 +4399,10 @@ auto TypeChecker::DeclareInterfaceDeclaration( ConvertToConstraintType(assoc->source_loc(), "type of associated constant", constraint)); - CARBON_RETURN_IF_ERROR( - builder.AddAndSubstitute(*this, constraint_type, assoc_value, - builder.GetSelfWitness(), Bindings(), - /*add_lookup_contexts=*/false)); + CARBON_RETURN_IF_ERROR(builder.AddAndSubstitute( + *this, assoc->source_loc(), constraint_type, assoc_value, + builder.GetSelfWitness(), Bindings(), + /*add_lookup_contexts=*/false)); } break; } @@ -4285,10 +4413,10 @@ auto TypeChecker::DeclareInterfaceDeclaration( } // Add any new impl constraints to the scope. - builder.BringImplsIntoScope(*this, &iface_scope, &impl_tracker); + builder.BringConstraintsIntoScope(*this, &iface_scope, &constraint_tracker); } - iface_decl->set_constraint_type(std::move(builder).Build(arena_)); + iface_decl->set_constraint_type(std::move(builder).Build()); if (trace_stream_) { **trace_stream_ << "** finished declaring interface " << iface_decl->name() @@ -4494,11 +4622,11 @@ auto TypeChecker::DeclareImplDeclaration(Nonnull impl_decl, Nonnull constraint_type; { ConstraintTypeBuilder builder(arena_, impl_decl->source_loc()); - CARBON_RETURN_IF_ERROR( - builder.AddAndSubstitute(*this, implemented_constraint, impl_type_value, - builder.GetSelfWitness(), Bindings(), - /*add_lookup_contexts=*/true)); - constraint_type = std::move(builder).Build(arena_); + CARBON_RETURN_IF_ERROR(builder.AddAndSubstitute( + *this, impl_decl->source_loc(), implemented_constraint, impl_type_value, + builder.GetSelfWitness(), Bindings(), + /*add_lookup_contexts=*/true)); + constraint_type = std::move(builder).Build(); impl_decl->set_constraint_type(constraint_type); } @@ -4510,8 +4638,10 @@ auto TypeChecker::DeclareImplDeclaration(Nonnull impl_decl, // Compute a witness that the impl implements its constraint. Nonnull impl_witness; { + std::vector rewrite_constraints_as_equality_constraints; ImplScope self_impl_scope; self_impl_scope.AddParent(&impl_scope); + // For each interface we're going to implement, this impl is the witness // that that interface is implemented. for (auto lookup : constraint_type->lookup_contexts()) { @@ -4519,11 +4649,17 @@ auto TypeChecker::DeclareImplDeclaration(Nonnull impl_decl, self_impl_scope.Add(iface_type, impl_type_value, self_witness, *this); } } - // This impl also provides all of its equalities. - // TODO: Only the ones from rewrite constraints. - for (const auto& eq : constraint_type->equality_constraints()) { + + // This impl also provides all of the equalities from its rewrite + // constraints. + for (const auto& rewrite : constraint_type->rewrite_constraints()) { + rewrite_constraints_as_equality_constraints.push_back( + {.values = {rewrite.constant, rewrite.converted_replacement}}); + } + for (const auto& eq : rewrite_constraints_as_equality_constraints) { self_impl_scope.AddEqualityConstraint(&eq); } + // Ensure that's enough for our interface to be satisfied. CARBON_ASSIGN_OR_RETURN( impl_witness, self_impl_scope.Resolve(constraint_type, impl_type_value, @@ -4573,6 +4709,8 @@ void TypeChecker::BringAssociatedConstantsIntoScope( } } } + + // TODO: Find a way to bring rewrite constraints into scope. } auto TypeChecker::TypeCheckImplDeclaration(Nonnull impl_decl, @@ -4735,6 +4873,11 @@ auto TypeChecker::DeclareAliasDeclaration(Nonnull alias, auto TypeChecker::TypeCheck(AST& ast) -> ErrorOr { ImplScope impl_scope; ScopeInfo top_level_scope_info = ScopeInfo::ForNonClassScope(&impl_scope); + + // Track that `impl_scope` is the top-level `ImplScope`. + llvm::SaveAndRestore + set_top_level_impl_scope(top_level_impl_scope_, &impl_scope); + for (Nonnull declaration : ast.declarations) { CARBON_RETURN_IF_ERROR( DeclareDeclaration(declaration, top_level_scope_info)); diff --git a/explorer/interpreter/type_checker.h b/explorer/interpreter/type_checker.h index f259379804f5..a2be2d238cdc 100644 --- a/explorer/interpreter/type_checker.h +++ b/explorer/interpreter/type_checker.h @@ -16,6 +16,7 @@ #include "explorer/interpreter/dictionary.h" #include "explorer/interpreter/impl_scope.h" #include "explorer/interpreter/interpreter.h" +#include "explorer/interpreter/value.h" namespace Carbon { @@ -43,6 +44,14 @@ class TypeChecker { auto Substitute(const Bindings& bindings, Nonnull type) const -> Nonnull; + // Attempts to refine a witness that might be symbolic into an impl witness, + // using `impl` declarations that have been declared and type-checked so far. + // If a more precise witness cannot be found, returns `witness`. + auto RefineWitness(Nonnull witness, + Nonnull type, + Nonnull constraint) const + -> Nonnull; + // If `impl` can be an implementation of interface `iface` for the given // `type`, then return the witness for this `impl`. Otherwise return // std::nullopt. @@ -398,15 +407,15 @@ class TypeChecker { // Given an interface type, form a corresponding constraint type. The // interface must be a complete type. - auto MakeConstraintForInterface(SourceLocation source_loc, - Nonnull iface_type) + auto MakeConstraintForInterface( + SourceLocation source_loc, Nonnull iface_type) const -> ErrorOr>; // Convert a value that is expected to represent a constraint into a // `ConstraintType`. auto ConvertToConstraintType(SourceLocation source_loc, std::string_view context, - Nonnull constraint) + Nonnull constraint) const -> ErrorOr>; // Given a list of constraint types, form the combined constraint. @@ -432,14 +441,14 @@ class TypeChecker { auto LookupRewriteInTypeOf(Nonnull type, Nonnull interface, Nonnull member) const - -> std::optional; + -> std::optional; // Given a witness value, look for a rewrite for the given associated // constant. auto LookupRewriteInWitness(Nonnull witness, Nonnull interface, Nonnull member) const - -> std::optional; + -> std::optional; // Adds a member of a declaration to collected_members_ auto CollectMember(Nonnull enclosing_decl, @@ -458,6 +467,15 @@ class TypeChecker { GlobalMembersMap collected_members_; std::optional> trace_stream_; + + // The top-level ImplScope, containing `impl` declarations that should be + // usable from any context. This is used when we want to try to refine a + // symbolic witness into an impl witness during substitution. + std::optional top_level_impl_scope_; + + // `where` expressions that are currently being built. These may have + // rewrites that are not yet visible in any type. + std::vector partial_where_expressions_; }; } // namespace Carbon diff --git a/explorer/interpreter/value.cpp b/explorer/interpreter/value.cpp index 0298b590a69a..15004599e4bd 100644 --- a/explorer/interpreter/value.cpp +++ b/explorer/interpreter/value.cpp @@ -434,9 +434,11 @@ void Value::Print(llvm::raw_ostream& out) const { llvm::ListSeparator sep(" and "); for (const ConstraintType::RewriteConstraint& rewrite : constraint.rewrite_constraints()) { - out << sep << ".(" << *rewrite.interface << "." - << *GetName(*rewrite.constant) - << ") = " << rewrite.replacement->value(); + out << sep << ".("; + PrintNameWithBindings(out, &rewrite.constant->interface().declaration(), + rewrite.constant->interface().args()); + out << "." << *GetName(rewrite.constant->constant()) + << ") = " << *rewrite.unconverted_replacement; } for (const ConstraintType::ImplConstraint& impl : constraint.impl_constraints()) { @@ -515,7 +517,7 @@ void Value::Print(llvm::raw_ostream& out) const { out << "(" << assoc.base() << ").("; PrintNameWithBindings(out, &assoc.interface().declaration(), assoc.interface().args()); - out << "." << assoc.constant().binding().name() << ")"; + out << "." << *GetName(assoc.constant()) << ")"; break; } case Value::Kind::ContinuationValue: { diff --git a/explorer/interpreter/value.h b/explorer/interpreter/value.h index 0ece1c44b437..05ab6771f53a 100644 --- a/explorer/interpreter/value.h +++ b/explorer/interpreter/value.h @@ -24,7 +24,7 @@ namespace Carbon { class Action; -class ImplScope; +class AssociatedConstant; // Abstract base class of all AST nodes representing values. // @@ -749,6 +749,19 @@ struct EqualityConstraint { std::vector> values; }; +// A constraint indicating that access to an associated constant should be +// replaced by another value. +struct RewriteConstraint { + // The associated constant value that is rewritten. + Nonnull constant; + // The replacement in its original type. + Nonnull unconverted_replacement; + // The type of the replacement. + Nonnull unconverted_replacement_type; + // The replacement after conversion to the type of the associated constant. + Nonnull converted_replacement; +}; + // A type-of-type for an unknown constrained type. // // These types are formed by the `&` operator that combines constraints and by @@ -773,15 +786,9 @@ class ConstraintType : public Value { Nonnull interface; }; - using EqualityConstraint = Carbon::EqualityConstraint; + using RewriteConstraint = Carbon::RewriteConstraint; - // A constraint indicating that access to an associated constant should be - // replaced by another value. - struct RewriteConstraint { - Nonnull interface; - Nonnull constant; - Nonnull replacement; - }; + using EqualityConstraint = Carbon::EqualityConstraint; // A context in which we might look up a name. struct LookupContext { diff --git a/explorer/testdata/assoc_const/fail_different_type.carbon b/explorer/testdata/assoc_const/fail_different_type.carbon index ac50fb87f0d1..c01c11606556 100644 --- a/explorer/testdata/assoc_const/fail_different_type.carbon +++ b/explorer/testdata/assoc_const/fail_different_type.carbon @@ -21,7 +21,7 @@ external impl Bad as Iface where .T = Bad {} fn Main() -> i32 { F(Good); - // CHECK:STDERR: COMPILATION ERROR: {{.*}}/explorer/testdata/assoc_const/fail_different_type.carbon:[[@LINE+1]]: constraint requires that class Bad == i32, which is not known to be true + // CHECK:STDERR: COMPILATION ERROR: {{.*}}/explorer/testdata/assoc_const/fail_different_type.carbon:[[@LINE+1]]: constraint requires that (T).(Iface.T) (with value class Bad) == i32, which is not known to be true F(Bad); return 0; } diff --git a/explorer/testdata/assoc_const/fail_different_value.carbon b/explorer/testdata/assoc_const/fail_different_value.carbon index 3818e99c4a13..f754ce5b4280 100644 --- a/explorer/testdata/assoc_const/fail_different_value.carbon +++ b/explorer/testdata/assoc_const/fail_different_value.carbon @@ -21,7 +21,7 @@ external impl Bad as Iface where .N = 4 {} fn Main() -> i32 { F(Good); - // CHECK:STDERR: COMPILATION ERROR: {{.*}}/explorer/testdata/assoc_const/fail_different_value.carbon:[[@LINE+1]]: constraint requires that 4 == 5, which is not known to be true + // CHECK:STDERR: COMPILATION ERROR: {{.*}}/explorer/testdata/assoc_const/fail_different_value.carbon:[[@LINE+1]]: constraint requires that (T).(Iface.N) (with value 4) == 5, which is not known to be true F(Bad); return 0; } diff --git a/explorer/testdata/assoc_const/fail_equal_indirectly.carbon b/explorer/testdata/assoc_const/fail_equal_indirectly.carbon index 9e375b857044..aa9d7ddae4f5 100644 --- a/explorer/testdata/assoc_const/fail_equal_indirectly.carbon +++ b/explorer/testdata/assoc_const/fail_equal_indirectly.carbon @@ -25,8 +25,8 @@ fn G[U:! Type where .Self == i32, T:! Iface where .T = U](x: T, y: U) { } // Not OK: would require looking through two levels of `==`. -fn H[U:! Type where .Self == i32, T:! Iface where .T == U](x: T, y: U) { - // CHECK:STDERR: COMPILATION ERROR: {{.*}}/explorer/testdata/assoc_const/fail_equal_indirectly.carbon:[[@LINE+1]]: constraint requires that (T).(Iface.T) == i32, which is not known to be true +fn H[V:! Type where .Self == i32, W:! Iface where .T == V](x: W, y: V) { + // CHECK:STDERR: COMPILATION ERROR: {{.*}}/explorer/testdata/assoc_const/fail_equal_indirectly.carbon:[[@LINE+1]]: constraint requires that (T).(Iface.T) (with value (W).(Iface.T)) == i32, which is not known to be true F(x); } diff --git a/explorer/testdata/assoc_const/fail_equal_to_dependent_type.carbon b/explorer/testdata/assoc_const/fail_equal_to_dependent_type.carbon index 645755abc1d4..9c02b4e5554d 100644 --- a/explorer/testdata/assoc_const/fail_equal_to_dependent_type.carbon +++ b/explorer/testdata/assoc_const/fail_equal_to_dependent_type.carbon @@ -14,12 +14,12 @@ interface Iface { fn F[T:! Iface where .T == i32](x: T) {} -fn G[T:! Iface where .T == i32](x: T) { +fn G[U:! Iface where .T == i32](x: U) { F(x); } -fn H[T:! Iface](x: T) { - // CHECK:STDERR: COMPILATION ERROR: {{.*}}/explorer/testdata/assoc_const/fail_equal_to_dependent_type.carbon:[[@LINE+1]]: constraint requires that (T).(Iface.T) == i32, which is not known to be true +fn H[V:! Iface](x: V) { + // CHECK:STDERR: COMPILATION ERROR: {{.*}}/explorer/testdata/assoc_const/fail_equal_to_dependent_type.carbon:[[@LINE+1]]: constraint requires that (T).(Iface.T) (with value (V).(Iface.T)) == i32, which is not known to be true F(x); } diff --git a/explorer/testdata/assoc_const/fail_implied_constraints.carbon b/explorer/testdata/assoc_const/fail_implied_constraints.carbon new file mode 100644 index 000000000000..4907db55b77d --- /dev/null +++ b/explorer/testdata/assoc_const/fail_implied_constraints.carbon @@ -0,0 +1,33 @@ +// Part of the Carbon Language project, under the Apache License v2.0 with LLVM +// Exceptions. See /LICENSE for license information. +// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception +// +// AUTOUPDATE +// RUN: %{not} %{explorer-run} +// RUN: %{not} %{explorer-run-trace} + +package ExplorerTest api; + +interface X(T:! Type) {} + +interface Y(T:! Type) { + let M:! X(T); +} + +interface Z { + // We reject this even though it is the responsibility of the `impl as Z` to + // provide a type `N` such that `i32 is X(N)`. We might want to treat this as + // an implied constraint and allow this in the future. + // CHECK:STDERR: COMPILATION ERROR: {{.*}}/explorer/testdata/assoc_const/fail_implied_constraints.carbon:[[@LINE+1]]: could not find implementation of interface X(T = N) for i32 + let N:! Y(.Self) where .M = i32; +} + +impl i32 as X(i32) {} +impl i32 as Y(i32) where .M = i32 {} +impl i32 as Z where .N = i32 {} + +fn F[A:! Z](a: A) -> A { return a; } + +fn Main() -> i32 { + return F(0); +} diff --git a/explorer/testdata/assoc_const/fail_missing_equal.carbon b/explorer/testdata/assoc_const/fail_missing_equal.carbon new file mode 100644 index 000000000000..9578fb9d6ccd --- /dev/null +++ b/explorer/testdata/assoc_const/fail_missing_equal.carbon @@ -0,0 +1,27 @@ +// Part of the Carbon Language project, under the Apache License v2.0 with LLVM +// Exceptions. See /LICENSE for license information. +// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception +// +// AUTOUPDATE +// RUN: %{not} %{explorer-run} +// RUN: %{not} %{explorer-run-trace} + +package ExplorerTest api; + +interface Container { + let Element:! Type; + fn Front[me: Self]() -> Element; +} + +fn A[T:! Container where .Element == i32](x: T) -> T.Element { + return x.Front(); +} + +fn B[T:! Container](x: T) -> T.Element { + // CHECK:STDERR: COMPILATION ERROR: {{.*}}/explorer/testdata/assoc_const/fail_missing_equal.carbon:[[@LINE+1]]: constraint requires that (T).(Container.Element) (with value (T).(Container.Element)) == i32, which is not known to be true + return A(x); +} + +fn Main() -> i32 { + return 0; +} diff --git a/explorer/testdata/assoc_const/fail_missing_rewrite.carbon b/explorer/testdata/assoc_const/fail_missing_rewrite.carbon new file mode 100644 index 000000000000..6a74e85b98c8 --- /dev/null +++ b/explorer/testdata/assoc_const/fail_missing_rewrite.carbon @@ -0,0 +1,27 @@ +// Part of the Carbon Language project, under the Apache License v2.0 with LLVM +// Exceptions. See /LICENSE for license information. +// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception +// +// AUTOUPDATE +// RUN: %{not} %{explorer-run} +// RUN: %{not} %{explorer-run-trace} + +package ExplorerTest api; + +interface Container { + let Element:! Type; + fn Front[me: Self]() -> Element; +} + +fn A[T:! Container where .Element = i32](x: T) -> T.Element { + return x.Front(); +} + +fn B[T:! Container](x: T) -> i32 { + // CHECK:STDERR: COMPILATION ERROR: {{.*}}/explorer/testdata/assoc_const/fail_missing_rewrite.carbon:[[@LINE+1]]: constraint requires that (T).(Container.Element) (with value (T).(Container.Element)) == i32, which is not known to be true + return A(x); +} + +fn Main() -> i32 { + return 0; +} diff --git a/explorer/testdata/assoc_const/fail_overspecified_impl.carbon b/explorer/testdata/assoc_const/fail_overspecified_impl.carbon index 243ed4c80c57..9fc6b9321563 100644 --- a/explorer/testdata/assoc_const/fail_overspecified_impl.carbon +++ b/explorer/testdata/assoc_const/fail_overspecified_impl.carbon @@ -12,7 +12,7 @@ interface HasType { let T:! Type; } -// CHECK:STDERR: COMPILATION ERROR: {{.*}}/explorer/testdata/assoc_const/fail_overspecified_impl.carbon:[[@LINE+3]]: multiple different rewrites for `.(interface HasType.T)`: +// CHECK:STDERR: COMPILATION ERROR: {{.*}}/explorer/testdata/assoc_const/fail_overspecified_impl.carbon:[[@LINE+3]]: multiple different rewrites for `(.Self).(HasType.T)`: // CHECK:STDERR: i32 // CHECK:STDERR: {.a: i32} external impl i32 as HasType where .T = i32 and .T = {.a: i32} {} diff --git a/explorer/testdata/assoc_const/fail_rewrite_depends_on_later_rewrite.carbon b/explorer/testdata/assoc_const/fail_rewrite_depends_on_later_rewrite.carbon new file mode 100644 index 000000000000..71ad34fde34a --- /dev/null +++ b/explorer/testdata/assoc_const/fail_rewrite_depends_on_later_rewrite.carbon @@ -0,0 +1,23 @@ +// Part of the Carbon Language project, under the Apache License v2.0 with LLVM +// Exceptions. See /LICENSE for license information. +// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception +// +// AUTOUPDATE +// RUN: %{not} %{explorer-run} +// RUN: %{not} %{explorer-run-trace} + +package ExplorerTest api; + +interface HasTypeAndValue { + let T:! Type; + let V:! T; +} + +// CHECK:STDERR: COMPILATION ERROR: {{.*}}/explorer/testdata/assoc_const/fail_rewrite_depends_on_later_rewrite.carbon:[[@LINE+1]]: type error in rewrite constraint: 'i32' is not implicitly convertible to '(.Self).(HasTypeAndValue.T)' +fn F(X:! HasTypeAndValue where .V = 5 and .T = i32) -> i32 { return X.V; } + +impl i32 as HasTypeAndValue where .T = i32 and .V = 5 {} + +fn Main() -> i32 { + return F(i32); +} diff --git a/explorer/testdata/assoc_const/rewrite_depends_on_prior_rewrite.carbon b/explorer/testdata/assoc_const/rewrite_depends_on_prior_rewrite.carbon new file mode 100644 index 000000000000..4aec35784b38 --- /dev/null +++ b/explorer/testdata/assoc_const/rewrite_depends_on_prior_rewrite.carbon @@ -0,0 +1,23 @@ +// Part of the Carbon Language project, under the Apache License v2.0 with LLVM +// Exceptions. See /LICENSE for license information. +// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception +// +// AUTOUPDATE +// RUN: %{explorer-run} +// RUN: %{explorer-run-trace} +// CHECK:STDOUT: result: 5 + +package ExplorerTest api; + +interface HasTypeAndValue { + let T:! Type; + let V:! T; +} + +fn F(X:! HasTypeAndValue where .T = i32 and .V = 5) -> i32 { return X.V; } + +impl i32 as HasTypeAndValue where .T = i32 and .V = 5 {} + +fn Main() -> i32 { + return F(i32); +}