predicate_eq_structural: == in a predicate is structural, not your Eq

Inside a refinement predicate, a == b means “the same value”: every field equal. That is the meaning the checker proves things with, whatever Eq the type implements. The program’s own == runs the type’s eq, so for a type with a hand-written Eq the two can disagree: the program may call two values equal that the predicate calls different.

This is a warning. No verdict changes; it tells you why a predicate you wrote with your Eq in mind is checked against structural equality instead.

A program that triggers it

mod Main do
  type P = P(Int, Int)

  impl Eq(P) do
    fn eq(a : P, b : P) : Bool do
      match (a, b) do
        (P(x, _), P(y, _)) -> x == y
      end
    end
  end

  fn need(p : {P | _ == P(1, 2)}) : P do p end
end

How to fix it

• State the property your Eq checks directly, for example over the fields it compares: write a reflected function same_first(a : P, b : P) : Bool and use it in the predicate.
• Or derive Eq (derive Eq for P), so the two equalities agree.