Bug in AbstractLevelMVar?

Stream: lean4

[Yicheng Qian]

I found that Lean didn't abstract universe metavariables correctly when I was working on a project. I looked into the source code

leanprover--lean4---nightly-2023-02-03/src/lean/Lean/Meta/AbstractMVars.lean

and found that abstractLevelMVars didn't try to instantiate a level metavariable before adding it to lmap, which seems wrong. This causes problem when a constant has levels which contain level mvars that has been assigned. Following abstractExprMVars, maybe we should change

        match s.lmap.find? mvarId with
        | some u => pure u
        | none   =>
          let paramId := Name.mkNum `_abstMVar s.nextParamIdx
          let u := mkLevelParam paramId
          modify fun s => { s with nextParamIdx := s.nextParamIdx + 1, lmap := s.lmap.insert mvarId u, paramNames := s.paramNames.push paramId }
          return u

(in abstractLevelMVars) into

        let uNew ← instantiateLevelMVars u
        if u != uNew then
          abstractLevelMVars uNew
        else
          match s.lmap.find? mvarId with
          | some u => pure u
          | none   =>
            let paramId := Name.mkNum `_abstMVar s.nextParamIdx
            let u := mkLevelParam paramId
            modify fun s => { s with nextParamIdx := s.nextParamIdx + 1, lmap := s.lmap.insert mvarId u, paramNames := s.paramNames.push paramId }
            return u