# the_implicit_types := [];;
val it : unit = ()
# `mul 1 x`;;
Warning: inventing type variables
val it : term = `mul 1 x`
# map dest_var (frees it);;
val it : (string * hol_type) list =
[("mul", `:num->?83058->?83057`); ("x", `:?83058`)]
However, if we use the implicit types to require that the variable # the_implicit_types := ["mul",`:A->A->A`; "iv",`:A->A`];;
val it : unit = ()
# `mul 1 x`;;
val it : term = `mul 1 x`
# map dest_var (frees it);;
val it : (string * hol_type) list =
[("mul", `:num->num->num`); ("x", `:num`)]