This looks good to me! Surprised it didn't pop up before. Thanks!

Hi, yes, I was surprised too!
I changed the embedding to be sure I'm not breaking anyone's code, but seems like there is no much code that relies on the definition of ident given in ulib's FStar.Reflection.Types module.
@R1kM suggested me to change directly the definition of ident in FStar.Reflection.Types, so that we respect a bit more the ident type from FStar.Ident (which is a record), so I reverted my previous commit and just pushed that modification instead.

As discussed during today's F* meeting, it's unlikely that this was used anywhere since this would lead to the errors you observed. Thanks for the fix and for documenting this in CHANGES.md!