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

Defer resolving rewrites until we apply a constraint to a binding #2333

Merged
merged 10 commits into from
Oct 24, 2022

Conversation

zygoloid
Copy link
Contributor

Instead of checking and resolving rewrites eagerly, defer doing so until a constraint is applied to a binding. Actual resolution of rewrites is not yet implemented, so this is mostly just refactoring, but the eventual goal is to support things like (Constraint where .T = .U) & (Constraint where .U = V) (however they are reached) by applying one rewrite to the other, as agreed with @josh11b in discussion of #2173.

One nice consequence is that substitution into a constraint type no longer has a failure path, so substitution is once again not able to fail.

@zygoloid zygoloid requested a review from jonmeow October 21, 2022 23:32
@zygoloid zygoloid added the explorer Action items related to Carbon explorer code label Oct 21, 2022
Comment on lines +24 to +28
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; }
Copy link
Contributor

Choose a reason for hiding this comment

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

Is any of this necessary to trigger the error? Can it be removed? If you want to keep it, can you add a comment explaining why?

The compile error is on line 20, so I wouldn't have expected later code to matter. If it's required, then I'm genuinely confused, because it seems like the location of these implementation is intended the source of the error. Maybe you want it to check top-down evaluation -- but that should be explicit.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Oops -- the intent here is for this testcase to be accepted, but we're a couple of changes away from it actually working. Added a TODO for now to capture that this entire file is supposed to be valid.

<< " " << *rewrite.unconverted_replacement;
}
}
void AddRewriteConstraint(RewriteConstraint rewrite) {
Copy link
Contributor

Choose a reason for hiding this comment

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

With this simplification, maybe just removed the function?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

It's still part of the public API of the class.

@zygoloid zygoloid merged commit adc78fb into carbon-language:trunk Oct 24, 2022
@zygoloid zygoloid deleted the explorer-resolve-constraints 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.

2 participants