add level to abbreviations in Texpand

[garrigue]

This is an alternative fix to #14769.
We change slightly the representation of Texpand nodes, to keep track explicitly of the level at which abbreviations have been checked.
This should also avoid checking the same abbreviation over and over again (across separate calls to update_level).

[gasche]

I looked at this out of curiosity and I have naive questions (showing that maybe I should have looked at the Texpand patch more):

1. What is the intended semantics of the level field of the Texpand description, and how does it differ from the level of the corresponding type_expr node? (Bonus question: could this maybe be documented somewhere?)

2. Why do we have check_level_type in the first place for Texpand nodes? I see

   and update_level_abbrev env level expand ty =
     iter_abbrev
       (fun p args ->
         if level < Path.scope p then forget_abbrev ty else
         if List.for_all (check_level_type level) args then () else
         if expand || needs_expand env level p args then forget_abbrev ty else
         List.iter (update_level env level expand) args)
       ty

   Why is it not enough to do

   if expand || level < Path.scope p || needs_expand env level p args
   then forget_abbrev ty
   else List.iter (update_level env level expand) args

   ? (Maybe this could be explained in a comment?)

[gasche]

Another naive question: unless I am missing something, update_level does not update the level of the result of the expansion? I find this a bit unintuitive. Are the level invariants expected from Texpand explained somewhere?

[garrigue]

I have added comments to check_level_type and update_abbrev_level.
The second one is lengthy, because this is a bit tricky.
As for your second question, in the two expansion cases (Tconstr), update_level is called on the result of the expansion: after link_type ty ty', ty and ty' share the same representative node (and level), the only difference being that ty may contain an abbreviation, which we want to check also.
There is no change in the invariants expected: levels should be decreasing when going from parent to child, the abbreviation also counting as child for the parent node. As before, levels on nodes Tlink or Texpand are ignored.