Soundness: an int passed to a float refined parameter is not checked #303

Description

An unconstrained int argument passed to a float parameter with a refinement is accepted. The same code with a float argument is correctly rejected (true is not a subtype of value >= 0.0 && value <= 1.0), and an unconstrained int passed to an int refinement is also correctly rejected. The int-to-float widening seems to drop the check, so the verifier misses real errors.

Minimal reproducer

import liquidjava.specification.Refinement;

public class Repro {
    static void setQuality(@Refinement("_ >= 0.0 && _ <= 1.0") float quality) {}

    static void fromInt(int percent) {
        setQuality(percent);        // expected error: percent is unconstrained (e.g. 85)
    }
}

Expected

A refinement error at setQuality(percent) (e.g. counterexample percent == 85).

Actual

Correct! Passed Verification.

Reproduced on main at 8816186 (liquidjava-verifier 0.0.35), and on 0.0.33.

Context

Found while turning real open-source Java code into study examples for the error-message study: real code hits this constantly, so the examples have to be rewritten around it or cannot be verified. Real case: a diagram exporter clamps an int quality to 0..100 and passes it to ImageWriteParam.setCompressionQuality(float) (which needs 0..1). The JVM throws IllegalArgumentException: Quality out of bounds!, but LiquidJava accepts it.