Files
carbon-lang/toolchain/check/require_impls.h
T
Dana Jansens 32aa7cb1fa Make identifying a facet type an operation on a (self+facet type) pair (#6592)
Identifying a facet type takes both a self and facet type as a pair, and
then encode the self into the IdentifiedFacetType. This makes a
constraint that requires some _other_ type implements an interface
visible in the IdentifiedFacetType. And it will help to enable facet
types with `where T impls Z` for `T` that is not `.Self` in the future.

IdentifiedFacetTypes are now stored in a CanonicalValueStore instead of
a RelationalValueStore as they key is the combination of self and
(declared) facet type together now.

When the self-type is a facet value (has type FacetType) this is most
straightforward. But when it's a type we need to construct a FacetValue
to construct a specific for a require decl, to replace the generic
binding of the symbolic `Self`, which has type FacetType. To do so, we
make a FacetValue with an empty FacetType (equivalent to TypeType). This
prevents any looking for witnesses through the FacetType, which matches
what you can get from a type directly, requiring witnesses to come from
finding an `impl` decl.

Add additional InstNamer logic for such empty facet types so they print
as `<typename>.type.facet` if possible instead of as just `facet_value`.
2026-01-14 17:34:56 +00:00

53 lines
2.3 KiB
C++

// 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
#ifndef CARBON_TOOLCHAIN_CHECK_REQUIRE_IMPLS_H_
#define CARBON_TOOLCHAIN_CHECK_REQUIRE_IMPLS_H_
#include "toolchain/check/context.h"
#include "toolchain/sem_ir/ids.h"
#include "toolchain/sem_ir/require_impls.h"
namespace Carbon::Check {
// A type-safe wrapper around the specific id of a RequireImpls entity.
// Constructed from a specific for its enclosing interface or constraint entity.
struct RequireImplsSpecific {
SemIR::SpecificId specific_id;
};
// Get the specific of a RequireImpls from the specific of its enclosing
// interface or named constraint. Since a `require` declaration can not
// introduce new generic bindings, the specific for the RequireImpls can be
// constructed from the enclosing one.
auto GetRequireImplsSpecificFromEnclosingSpecific(
Context& context, const SemIR::RequireImpls& require,
SemIR::SpecificId enclosing_specific_id) -> RequireImplsSpecific;
// Like GetRequireImplsSpecificFromEnclosingSpecific but the `Self` value in the
// specific is replaced by a given facet value.
auto GetRequireImplsSpecificFromEnclosingSpecificWithSelfFacetValue(
Context& context, const SemIR::RequireImpls& require,
SemIR::SpecificId enclosing_specific_id,
SemIR::ConstantId self_facet_value_id) -> RequireImplsSpecific;
// Returns the constant value of `inst_id` from inside a RequireImpls
// declaration, mapped into `enclosing_specific_id`. If an error results, it
// returns ErrorInst.
//
// An error can occur during monomorphization when the self-type was valid as a
// symbolic but becomes invalid with a more concrete specific.
//
// RequireImpls is always generic, so the instructions inside it must have a
// specific applied. That specific is constructed from a specific for the
// enclosing generic entity, with GetRequireImplsSpecificFromEnclosingSpecific.
auto GetConstantValueInRequireImplsSpecific(Context& context,
RequireImplsSpecific specific,
SemIR::InstId inst_id)
-> SemIR::ConstantId;
} // namespace Carbon::Check
#endif // CARBON_TOOLCHAIN_CHECK_REQUIRE_IMPLS_H_