The assertion corresponds to specific domain knowledge about the resolution process. I would expect maybe a comment to explain it (to make the code easier to follow locally). Another option would be to use the more robust

| Symbol s1, Symbol s2 when s1 == s2 -> resolved
| Const c1, Const c2 when c1 == c2 -> resolved
| <rest of the cases>

In that case it is locally obvious that the physical equality is an optimization that does not change the program semantics.

(My first idea was to rewrite the called functions to not re-allocate the same constructor (turn | Const s -> Const s into Const _ as c -> c) and then check named == resolved, but that does not work as the types differ -- the two Const constructors involved are at different types.)

The point about physical equality was actually whether this is a valid use. I think it's undefined behaviour strictly speaking even if it does the right thing at the moment... (Since the things being compared are immutable.)

I'm not sure I get the point. Is there something particularly bad about this specific use of physical equality? While it is correct that its behavior is currently not defined, it is not "specified as an undefined behavior" either. In particular, any specification should imply that for types where structural equality is defined, two values are only physically equal when they are also structurally equal. With my when .. == .. variant, it should then be clear that the code is correct as the branch-is-taken-more-often when .. = .. code is functionally correct. (For the assertion presentation, of course this specification does not guarantee you that the assertion will pass.)

any specification should imply that for types where structural equality is defined, two values are only physically equal when they are also structurally equal

Only if you define structurally equal with Pervasives.compare .. .. = 0 (because (nan == nan, nan = nan)).

What about dropping the physical equality check altogether? It is only used as a proxy for checking the real invariant which matters, semantically (structural equality of the strings).

What might actually be more problematic is the use of physical equality as an optimization in the generic mapping functions, but this is not affected by this patch and I think this is fine.

You could keep the code is before, and change the generic mapping function to use a custom equality testing instead of using physical equality (something faster than structural equality, but "larger" than physical equality). This would also serve other occurrences, it seems.

@alainfrisch I do not see the problem of physical equality in the mapping function. This only shortcuts some useless computation when the mapping is the identity. This does not affect the semantics, only compilation speed. Also, using any kind of real equality (that needs to traverse completely the values), would result in something quadratic.

@mshinwell Physical equality is not well defined, but I would consider this to be almost equivalent to the property asserted in Set.add. I don't know the right definition, but if it breaks here, I'd prefer to be aware. So I would suggest keeping it.

I did not say there is a problem with using the physical equality in the mapping function: it's just that given the definition of the physical equality and since the flambda IR is immutable, the compiler would be allowed to copy values, which would break the optimization. As said, I really don't think that this is problematic, but if one wonders about the implication of the lack of full specification for the physical equality, this is a more interesting question than the one raised by this patch (where the check could be dropped altogether).

using any kind of real equality (that needs to traverse completely the values), would result in something quadratic.

What I had in mind was something which would check the equality of constructors and physical equality of their arguments. This would cover the case added by this patch, but also, apprently more of the same kind (cf other instances of Symbol s -> Symbol s or Const c -> Const c in lift_constants.ml). And it seems better that all "optimizations" based on physical equality are located in a single place.