Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Merged
merged 8 commits into from
Oct 18, 2022

Conversation

zygoloid
Copy link
Contributor

@zygoloid zygoloid commented Oct 15, 2022

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.

Comment on lines 127 to 128
return ProgramError(source_loc) << "could not determine that "
<< *first << " == " << *current;
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looking at could not determine that 4 == 5 I'm wondering if more words may help explain what's going on. Like, can we instead say something like "Requires that constraints 4 and 5 are equal, which isn't provable."?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Wording improved. I'm avoiding saying "which isn't provable" because there are cases where such things are provable but we nonetheless can't discover the proof for ourselves. I've also added a test with an example of that.

explorer/interpreter/impl_scope.cpp Outdated Show resolved Hide resolved
common/check.h Show resolved Hide resolved
CARBON_FATAL() << "Can't convert value " << *value << " to type "
<< *destination_type;
default: {
CARBON_CHECK(isa<VariableType, AssociatedConstant>(destination_type))
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

You're doing this exact same multi-check in multiple places. Elsewhere, in the AST, we use parent classes to handle situations where multiple features behave identically. But I think it's actually particularly odd here: this is already switching on the Kind. If you need these to behave differently, not add a case?

Also, did this need to start handling VariableType as some consequence of your changes? I understand AssociatedConstant here because it's the focus of your changes, but VariableType seems a bit of an unusual side-effect and the reason why isn't obvious to me.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Factored out the duplicated check into a named function.

This isn't a consequence of my change; it's just that no-one had written a test that encountered this situation before.

CARBON_FATAL() << "Can't convert value " << *value << " to type "
<< *destination_type;
default: {
CARBON_CHECK(isa<VariableType, AssociatedConstant>(destination_type))
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

As above: when you're already switching on the Kind, shouldn't we prefer cases?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Let me know if you're unhappy with the new approach.

explorer/interpreter/type_checker.h Outdated Show resolved Hide resolved
This is not necessary any more as any desired equality relations should
already be in scope. Generally we want to look for `==` relations in the
same set of places where we look for `is` relations.
Remove a largely-unused accessor that doesn't belong in the TypeChecker
public API.
@@ -121,6 +121,13 @@ class Value {
const Kind kind_;
};

// Returns whether the fully-resolved kind that this value will eventually have
// is currently unknown, because it depends on a generic parameter.
inline bool IsValueKindDependent(Nonnull<const Value*> type) {
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

FWIW I think this name a bit hard to interpret, maybe "IsDependentType" similar to "IsConcreteType" or "IsType"?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Hm, this doesn't tell you whether the type is dependent, at least in the C++ sense. For example, Vector(T) would probably be considered a dependent type, but the value kind (NominalClassType) is not dependent -- this is specifically determining whether the Value::Kind is dependent. I'm having a hard time finding a better name that's still appropriate.

@zygoloid zygoloid merged commit 4b67951 into carbon-language:trunk Oct 18, 2022
zygoloid added a commit to zygoloid/carbon-lang that referenced this pull request Oct 18, 2022
@chandlerc chandlerc added the explorer Action items related to Carbon explorer code label Jan 13, 2023
@zygoloid zygoloid deleted the explorer-check-equality branch October 4, 2023 23:28
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
explorer Action items related to Carbon explorer code
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants