Make the expression type a GADT

[filipeom]

Mainly resistant due to operators types. Maybe we could type operators like this?

(* ty.ml *)
type _ t =
  | Ty_int : [ `Ty_int ] t
  | Ty_real : [ `Ty_real ] t
  | Ty_bool : [ `Ty_bool ] t
  | Ty_str : [ `Ty_str ] t
  | Ty_bitv : int -> [ `Ty_bitv ] t
  | Ty_fp : int -> [ `Ty_fp ] t

type _ unop =
  | Abs : [< `Ty_real | `Ty_fp ] unop
  | Ceil : [< `Ty_real | `Ty_fp ] unop
  | Clz : [ `Ty_bitv ] unop
  | Ctz : [ `Ty_bitv ] unop
  | Floor : [< `Ty_real | `Ty_fp ] unop
  | Is_nan : [ `Ty_fp ] unop
  | Len : [ `Ty_str ] unop
  | Neg : [< `Ty_int | `Ty_real | `Ty_bitv | `Ty_fp ] unop
  | Nearest : [< `Ty_real | `Ty_fp ] unop
  | Not : [< `Ty_bitv | `Ty_bool ] unop
  | Sqrt : [< `Ty_real | `Ty_fp ] unop
  | Trim : [ `Ty_str ] unop
  | Trunc : [< `Ty_real | `Ty_fp ] unop

...

[sim642]

Quickly looking at the TACAS '26 paper preprint, specifically Section 2.1 makes the following claim about the issue in Listing 1:

In contrast, Smt.ml expressions are well-typed by construction, avoiding this class of bugs and promoting code correctness and reliability in the development process.

But all I see in the API is Smtml.Expr.t which doesn't really seem any more stronger typed than Z3.Expr.expr. I kind of expected Smtml.Expr.t to already be a GADT.

Am I missing something here? Or what is the paper's "well-typed by construction" claim about?

[filipeom]

These features have not been upstreamed yet. There are still a few API-level issues that need to be aligned and reviewed by major smtml clients first. Namely, #351.

Similarly, the DSL used for specifying simplifications has not yet been upstreamed for the same reasons. That said, this part is much closer to completion and can already be found here: https://github.com/formalsec/smtml/tree/tacas2026.

In short, the concerns raised stem from the current state of the public API rather than from the design described in the paper. We fully expect these remaining details to be resolved and all relevant features to be merged before the final camera-ready version is released.