Are rewrites done as part of type checking or monomorphization?

[josh11b]

Summary of issue:

Right now, which rewrite is applied to uses of the subscript operator depends on which interfaces are implemented for the types, see #2274 . There is a final blanket implementation to ensure that the two rewrites produce consistent answers with the same type. However, the category of the result, whether it is a value or a reference, depends on which rewrite is applied. In a generic context, it can be known that subscripting is implemented, and the type that will result, without knowing if it produces a reference expression.

Similarly, #3720 will apply a different rewrite for binding depending on the category of the input. The type of the answer is constrained to match, but different implementations would be used in the two cases.

This leaves two possibilities, neither of which are good:

• If the rewrite is done at type checking time based on how much we know about the type, then the same code can do different things in a generic context and a concrete context.
• If the rewrite is done as part of monomorphization, then we would always do the same thing but sometimes use an impl that wasn't part of the constraints on the generic.

Details:

Details with an example may be found here.

Any other information that you want to share?

This came up in these contexts:

• Open discussion on 2024-05-23
• #typesystem in Discord

[zygoloid]

See also #3985 in which I thought I had a solution to this that allowed early rewrites. That doesn't work, but I think that approach with late rewrites does work, and still allows us to guarantee that monomorphization will succeed if generic type checking succeeds. However, because it's doing late rewrites, that means non-template-dependent code in a generic can vary more during monomorphization than would be possible with an early rewrite model -- and for example that will have an impact on what operations we would consider to be object-safe.