`Typed.Bool.symbol`, etc. don't check types at all

[sim642]

Typed.Bool contains

smtml/src/smtml/typed.ml

Line 461 in f50d5bf

let[@inline] symbol x = Expr.symbol x

Not only does it not check the symbol type at compile time, it also doesn't check at runtime!
So Smtml is completely happy with

Typed.Bool.symbol (Symbol.make Ty_int "x")

This defeats the point of the Typed interface because all the safety it provides can be just bypassed.
These inner symbol functions should at least check the types at runtime.

And if this check is unnecessarily expensive for some use case, I guess there could be Typed.Unsafe.Bool.symbol with the current unchecked definition.

[filipeom]

Thanks for detecting this!

And if this check is unnecessarily expensive for some use case,

It shouldn't be expensive to do at runtime. But I would prefer that the typed interface enforced it at runtime.

I guess there could be Typed.Unsafe.Bool.symbol with the current unchecked definition.

What about having those function take a string instead of a Symbol? Something like:

(* Would stay the same *)
val symbol : 'a ty -> string -> 'a expr

...

module Bool : sig
  type t = bool expr
  
  (* Still only 1 argument, but it is now a string *)
  val symbol : string -> t
end

What do you think @redianthus? Is there a reason we explicitly need this API? I'll try to do this in Owi and see where it falls short.

[redianthus]

I think it'll make the code better in Owi too actually 😅

[sim642]

What about having those function take a string instead of a Symbol?

I think Bool.symbol might be more convenient than symbol Types.bool but it makes things even harder when access to the underlying Symbol.t is needed (e.g. #550).

[filipeom]

What about having those function take a string instead of a Symbol?

I think Bool.symbol might be more convenient than symbol Types.bool but it makes things even harder when access to the underlying Symbol.t is needed (e.g. #550).

Ah didn't see #550 at the time. Then maybe adding a 'a Typed.symbol as you suggested might be make more sense? It would help in both cases I think