feat: convert universe metavariables into parameters after elaborating theorem header

closes #318

Like Lean 3, we are doing it only for theorems.
@Kha, we talked about doing it for definitions too, it sounded like a
good idea, and it would make the system's behavior more uniform, but
unfortunately it creates too many problems. There are so many trivial
cases where it breaks. Here are some examples.

1- Definitions that take multiple bundled structures
```
def foo (s1 : Group) (s2 : CommRing) ...
```
They are universe polymorphic, and the different structures must be in
the same universe, but we don't know it when we elaborate the header,
that is, we need to elaborate the body.

An extreme case is `PUnit` occurring in the header. It is universe
polymorphic, but we only lear the constraints on this universe after
we elaborate the body.

2- All files containing unification hints broke.
Again, there are universe constraints on the header that we only learn
after we elaborate the body.

3- Many `CoeSort` and `CoeFun` examples broke.
Example:
```
structure Group :=
  (carrier : Type u) (mul : carrier → carrier → carrier) (one : carrier)

instance GroupToType : CoeSort Group (Type u) :=
  CoeSort.mk (fun g => g.carrier)
```
We would have to write
```
instance GroupToType : CoeSort Group.{u} (Type u) :=
  CoeSort.mk (fun g => g.carrier)
```
We would have to provide universe level parameters manually in this
kind of instance. I think it would be too annoying.

src/Lean/Elab/MutualDef.lean

@@ -600,9 +600,23 @@ private def getAllUserLevelNames (headers : Array DefViewElabHeader) : List Name
   else
     []
 
+/-- Eagerly convert universe metavariables occurring in theorem headers to universe parameters. -/
+private def levelMVarToParamHeaders (views : Array DefView) (headers : Array DefViewElabHeader) : TermElabM (Array DefViewElabHeader) := do
+  let rec process : StateRefT Nat TermElabM (Array DefViewElabHeader) := do
+    let mut newHeaders := #[]
+    for view in views, header in headers do
+      if view.kind.isTheorem then
+        newHeaders := newHeaders.push { header with type := (← levelMVarToParam' header.type) }
+      else
+        newHeaders := newHeaders.push header
+    return newHeaders
+  let newHeaders ← process.run' 1
+  newHeaders.mapM fun header => return { header with type := (← instantiateMVars header.type) }
+
 def elabMutualDef (vars : Array Expr) (views : Array DefView) : TermElabM Unit := do
   let scopeLevelNames ← getLevelNames
   let headers ← elabHeaders views
+  let headers ← levelMVarToParamHeaders views headers
   let allUserLevelNames := getAllUserLevelNames headers
   withFunLocalDecls headers fun funFVars => do
     let values ← elabFunValues headers

tests/lean/297.lean.expected.out

@@ -1,10 +1,6 @@
 297.lean:1:10-1:11: error: typeclass instance problem is stuck, it is often due to metavariables
   OfNat (Sort ?u) 0
-297.lean:2:0-2:1: error: failed to synthesize instance
-  OfNat (Id PUnit) 0
-297.lean:2:4-2:5: error: failed to synthesize instance
-  OfNat Prop 0
+297.lean:1:13-3:1: error: invalid universe level, u_1 is not greater than 0
 297.lean:1:10-1:11: error: failed to synthesize instance
-  OfNat (Type ?u) 0
-297.lean:2:10-2:11: error: failed to synthesize instance
-  OfNat (Id PUnit) 0
+  OfNat (Sort u_1) 0
+297.lean:1:8-1:9: error: (kernel) declaration has metavariables 'r'

tests/lean/rewrite.lean.expected.out

@@ -1,9 +1,9 @@
-α : Type ?u
+α : Type u_1
 as bs : List α
 ⊢ as ++ bs ++ bs = as ++ (bs ++ bs)
 rewrite.lean:12:20-12:29: error: tactic 'rewrite' failed, did not find instance of the pattern in the target expression
   List.reverse (List.reverse ?m)
-α : Type ?u
+α : Type u_1
 as bs : List α
 ⊢ as ++ [] ++ [] ++ bs ++ bs = as ++ (bs ++ bs)
 x y z : Nat

tests/lean/run/depHd.lean

@@ -1,12 +1,12 @@
 def Hd : List α → Type
-  | []     => Unit
+  | []     => PUnit
   | a :: _ => α
 
 def hd : (as : List α) → Hd as
   | []     => ()
   | a :: l => a
 
-theorem inj_hd : (a a': α) → (l l' : List α) → a :: l = a' :: l' → a = a' := by
+theorem inj_hd (α : Type) : (a a': α) → (l l' : List α) → a :: l = a' :: l' → a = a' := by
   intro a a' l l' h
   show hd (a :: l) = hd (a' :: l')
   cases h