`instantiate` can produce terms that are not parsable

[htzh]

For example:

utop # t1;;
- : term = `\x. s x`
utop # x1, type_of x1;;
- : term * hol_type = (`x`, `:A->bool`)
utop # let s1 = frees t1 |> hd;;
val s1 : term = `s`
utop # instantiate (term_match [] s1 x1) t1;;
- : term = `\x. x x`

The last term is semantically (and type-wise) okay but will not be accepted by the parser (even with explicit type annotations). The reason is that the two xs have different types so the bound variable is not renamed. On the other hand the following sequence produces the correct renaming:

utop # t2;;
- : term = `\x. s + x`
utop # x2, type_of x2;;
- : term * hol_type = (`x`, `:num`)
utop # let s2 = frees t2 |> hd;;
val s2 : term = `s`
utop # instantiate (term_match [] s2 x2) t2;;
- : term = `\x'. x + x'`

[PetrosPapapa]

Hate to say it, but that's a known problem. See this paper for a more detailed discussion and examples with worse consequences. Typing, in particular, is a common source of unexpected results. See the bottom of this post for relevant comments and the same copied code here to help you inspect the types of variables in your terms (at the cost of significant verbosity). Hope this helps!