Impact: an alias whose arguments reuse its own parameter names in a different order is expanded wrongly, because the arguments are substituted one at a time. At the declaration this gives a false "This refinement can never be true" warning. Call sites look right in this repro, because their arguments are renamed to fresh variables before the alias is expanded. Any other path that expands an alias over unrenamed names would check the wrong formula.

Minimal reproducer

import liquidjava.specification.Refinement;
import liquidjava.specification.RefinementAlias;

@RefinementAlias("Below(int a, int b) { a < b }")
public class Probe {
    static void need(int a, int b, @Refinement("Below(b, a)") int unused) {}

    static void run() {
        need(5, 3, 0); // Below(3, 5) = 3 < 5: holds
    }

    static void run2() {
        need(3, 5, 0); // Below(5, 3) = 5 < 3: must be rejected
    }
}

Actual (main @ cd49fea):

Warning: This refinement can never be true
6 |     static void need(int a, int b, @Refinement("Below(b, a)") int unused) {}
  |                                                 ^^^^^^^^^^^
Refinement Error: b == 5 && a == 3 is not a subtype of Below(b, a)      (line 13, correct)

run() passes and run2() is rejected, both correct. The warning is wrong: b < a is satisfiable.

Cause. Expression.changeAlias builds the expansion with sub = sub.substitute(varExp, aliasExp) for each parameter in turn. For Below(b, a) with parameters (a, b): a < b becomes b < b after a := b, then a < a after b := a. The unsatisfiability check in TypeChecker expands the declared refinement with the parameters' own names, so it checks a < a.

Expected: substitute all arguments at once, i.e. a simultaneous substitution, or rename the alias parameters to fresh names first. Then the declaration gets no warning.

Found while working on #295 (PR #489 builds its expansions with a simultaneous substitution for the where lines, but does not change changeAlias).