[asl] maintain a type annotation for every typechecked expression by Roman-Manevich · Pull Request #1870 · herd/herdtools7

Roman-Manevich · 2026-06-18T11:48:39Z

This PR enables maintaining the type inferred for each expression during typechecking as an annotation attached to the expression. The intention is to make this available for tools built on top of aslref.

hrutvik · 2026-06-18T11:51:15Z


-let integer_exact' e = well_constrained' [ Constraint_Exact e ]
+let integer_exact' e =
+  well_constrained' [ Constraint_Exact (e |> with_integer_ty) ]


Is this right? I'm a bit surprised that this is editing the type of e

This replaces e with a copy that has the integer type as its type annotation

Would we not expect e to be type-annotated already? If not, does the integer type annotation add anything?

hrutvik · 2026-06-18T11:52:03Z


 let qualifier_equal (q1 : func_qualifier option) q2 = Option.equal ( = ) q1 q2
-let var_ x = E_Var x |> add_dummy_annotation
+let int_expr_of_var x = E_Var x |> add_dummy_annotation |> with_integer_ty


In general, the usage of with_integer_ty seems suspect to me - how do we know whether it should be (un)constrained, parameterised? I think we should be relying on type-checking to fill this in wherever possible, and avoiding overwriting types as we do several times in this file

The is needed for the cases where we are constructing typed AST expressions without later annotating them. In such cases, we need to establish the types ourselves.

I understand that we may not have annotated these, but how can we know that integer is the right type?

Note that it is possible that we could type-check those expressions, even if it's a bit useless.

hrutvik · 2026-06-18T11:53:59Z

  List.map plug_one
+
+(** Checks that all expressions have [opt_type = Some t] *)
+module CheckTypeAnnotations = struct


Why are we performing this check? This is just additional information, it's not mandated?

I used it for testing and then turned it off. We can probably remove it, but we may want to preserve it until we have more validation by some actual use cases.

I think we should remove for the merge of this PR.

we may want to preserve it until we have more validation by some actual use cases.

I think the opposite actually - this is speculating a need for exhaustivity that we don't yet have supported by usage. I suggest we start with a basic level of annotation and expand as necessary

HadrienRenaud

I think this needs to be more carefully documented. For example one of the important thing that is not said is that none of those type informations are used for type-checking.

Another important choice made here is not to use dependent types for some constructed expressions. This needs to be justified. I can see other options:

Do not put any type annotations for those.
Put only integer, as is done here
Use recursive values to provide full precision types for literal values (this seems dangerous to me).

Maybe this should be hidden behind a command line flag not to impact the reference interpreter.
In the long term, we should probably write a typed AST which would incorporate those informations, and document what precision is given by those.

HadrienRenaud · 2026-06-18T11:52:13Z

+type 'a annotated = {
+  desc : 'a;
+  pos_start : position;
+  pos_end : position;
+  version : version;
+  opt_type : ty option;
+}


I would keep it separated with the following:

Suggested change

type 'a annotated = {

desc : 'a;

pos_start : position;

pos_end : position;

version : version;

opt_type : ty option;

}

type ('term, 'ty) annotated = {

desc : 'term;

pos_start : position;

pos_end : position;

version : version;

opt_type : 'ty option;

}

And then declare expr as (expr_desc, ty) annotated, while for example stmt could be (stmt_desc, unit) annotated

HadrienRenaud · 2026-06-18T11:54:32Z


-let integer_exact' e = well_constrained' [ Constraint_Exact e ]
+let integer_exact' e =
+  well_constrained' [ Constraint_Exact (e |> with_integer_ty) ]


Why this? At the very least, the choice of typing those as integer needs to be documented and justified. Also what needs to be justified is that this does not break anything, as now a naive implementation of type_of would find those of type integer and not integer {e}, and maybe this breaks the invariant that all expressions in types are bounded.

IMHO if it is possible, we would leave those without a type.

Naive implementation of type_of for reference.

let type_of e = match e.type_opt with | Some t -> t | None -> Typing.annotate_expr e |> snd

Note that here type_of one_expr != Typing.annotate_expr one_expr |> snd

IMHO if it is possible, we would leave those without a type.

Agreed with this - I think any type annotations we introduce in the first instance should be coming out of the existing type-checking

HadrienRenaud · 2026-06-18T12:18:48Z


    let primitives =
-      let e_var x = E_Var x |> add_dummy_annotation in
+      let e_int_var x = E_Var x |> add_dummy_annotation |> with_integer_ty in


This also needs to be justified.

I'm not sure in what sense this needs to be justified as this is a construction function. Each of the usages indeed requires an integer-typed variable (for bitwidth, for an integer exponentiation operation, and for the integer variable N.

However it doesn't justify why this shouldn't be a constrained or parameterised integer. For example I see it used in a T_Bits, which usually needs a constrained or parameterised integer right?

HadrienRenaud · 2026-06-18T12:39:54Z

  and annotate_expr env (e : expr) : ty * expr * SES.t =
+    let t, e', ses = annotate_expr_impl env e in
+    let e_with_type = { e' with opt_type = Some t } in
+    (t, e_with_type, ses)
+
+  (** [annotate_expr_impl] annotates the expression [e] in [env] without setting
+      a type annotation. *)
+  and annotate_expr_impl env (e : expr) : ty * expr * SES.t =
    let () = if false then Format.eprintf "@[Annotating %a@]@." PP.pp_expr e in
    let here x = add_pos_from ~loc:e x and loc = to_pos e in
    match e.desc with


You can avoid putting a new function in this very recursive definition with the following:

Suggested change

and annotate_expr env (e : expr) : ty * expr * SES.t =

let t, e', ses = annotate_expr_impl env e in

let e_with_type = { e' with opt_type = Some t } in

(t, e_with_type, ses)

(** [annotate_expr_impl] annotates the expression [e] in [env] without setting

a type annotation. *)

and annotate_expr_impl env (e : expr) : ty * expr * SES.t =

let () = if false then Format.eprintf "@[Annotating %a@]@." PP.pp_expr e in

let here x = add_pos_from ~loc:e x and loc = to_pos e in

match e.desc with

(** [annotate_expr] annotates the expression [e] in [env]. *)

and annotate_expr env (e : expr) : ty * expr * SES.t =

let () = if false then Format.eprintf "@[Annotating %a@]@." PP.pp_expr e in

let here x = add_pos_from ~loc:e x and loc = to_pos e in

set_type3

@@

match e.desc with

Maybe in ASTUtils.ml

let set_type3: 'ty * ('val, 'ty) annotated * 'data -> 'ty * ('val, 'ty) annotated * 'data = fun (t, e, d) -> (t, with_ty_annot t e, d)

Thanks. I went with set_expr_type_annotation instead of set_type3.

HadrienRenaud · 2026-06-18T12:43:28Z

    If both arguments are physically equal, then the result is also physically
    equal. *)

+val with_ty_annot : AST.ty -> 'a annotated -> 'a annotated


With my proposal for the definition of annotated, it can have a more flexible definition, without losing the type constraints:

Suggested change

val with_ty_annot : AST.ty -> 'a annotated -> 'a annotated

val with_ty_annot : 'ty -> ('a, 'ty) annotated -> ('a, 'ty) annotated

(with a slight change in how with_ty_annot is written, we could also transform it to 'ty -> ('a, 'b) annotated -> ('a, 'ty) annotated)

HadrienRenaud · 2026-06-18T12:58:50Z

+      match C.check with
+      | TypeCheck ->
+          false (* set to true if debugging missing annotations is needed *)
+      | _ -> false


Can you not add a command line flag for this? I'm wondering if adding the type information should also be a command line flag.

hrutvik

I think we need to reduce the scope of this PR. I think it should contain only:

Mechanism for storing type annotations - whether the existing version or Hadrien's proposal.
Storing type annotations as calculated during type-checking already (i.e. wrap annotate_{expr,lexpr}, base_value)

I.e. the additional type annotations not provided by the type system, the exhaustivity checks should be removed. In future we can discuss whether we consider "missing" type annotations as truly missing (and if so whether they should be inserted post-hoc or the type system should be changed to calculate them appropriately), and how this could all be encoded into a truly typed AST.

Please let me know if you disagree.

Roman-Manevich requested review from HadrienRenaud and hrutvik June 18, 2026 11:48

hrutvik reviewed Jun 18, 2026

View reviewed changes

Roman-Manevich force-pushed the asl-910-maintain-types branch from a8097cc to 124b7b9 Compare June 18, 2026 12:56

Roman-Manevich requested a review from hrutvik June 18, 2026 12:57

HadrienRenaud reviewed Jun 18, 2026

View reviewed changes

[asl] maintain a type annotation for every typechecked expression

df82466

Roman-Manevich force-pushed the asl-910-maintain-types branch from 124b7b9 to df82466 Compare June 18, 2026 13:01

hrutvik requested changes Jun 24, 2026

View reviewed changes

	val with_ty_annot : AST.ty -> 'a annotated -> 'a annotated
	val with_ty_annot : 'ty -> ('a, 'ty) annotated -> ('a, 'ty) annotated

Uh oh!

Conversation

Roman-Manevich commented Jun 18, 2026

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

HadrienRenaud left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

hrutvik left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

hrutvik left a comment •

edited

Loading