From d770c553262c4aed8b6bea936918c5d77cf192d1 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 25 Feb 2021 13:21:53 -0800
Subject: [PATCH] feat: universe level parameters in instances are `outParam`
 by default

This commit makes sure Lean 4 treats universe level parameters in
instances as `outParam`s. This the behavior in Lean 3.

fixes #319
---
 src/Lean/Meta/SynthInstance.lean | 27 ++++++++++++++++++---------
 tests/lean/run/319.lean          | 14 ++++++++++++++
 2 files changed, 32 insertions(+), 9 deletions(-)
 create mode 100644 tests/lean/run/319.lean

diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean
index 2bda5089a6..769ea0a840 100644
--- a/src/Lean/Meta/SynthInstance.lean
+++ b/src/Lean/Meta/SynthInstance.lean
@@ -510,15 +510,17 @@ private def preprocess (type : Expr) : MetaM Expr :=
     let type ← whnf type
     mkForallFVars xs type
 
-private def preprocessLevels (us : List Level) : MetaM (List Level) := do
-  let mut r := []
+private def preprocessLevels (us : List Level) : MetaM (List Level × Bool) := do
+  let mut r := #[]
+  let mut modified := false
   for u in us do
     let u ← instantiateLevelMVars u
     if u.hasMVar then
-      r := (← mkFreshLevelMVar)::r
+      r := r.push (← mkFreshLevelMVar)
+      modified := true
     else
-      r := u::r
-  pure r.reverse
+      r := r.push u
+  return (r.toList, modified)
 
 private partial def preprocessArgs (type : Expr) (i : Nat) (args : Array Expr) : MetaM (Array Expr) := do
   if h : i < args.size then
@@ -532,7 +534,7 @@ private partial def preprocessArgs (type : Expr) (i : Nat) (args : Array Expr) :
     | _ =>
       throwError "type class resolution failed, insufficient number of arguments" -- TODO improve error message
   else
-    pure args
+    return args
 
 private def preprocessOutParam (type : Expr) : MetaM Expr :=
   forallTelescope type fun xs typeBody => do
@@ -540,15 +542,22 @@ private def preprocessOutParam (type : Expr) : MetaM Expr :=
     | c@(Expr.const constName us _) =>
       let env ← getEnv
       if !hasOutParams env constName then
-        pure type
+        /- We treat all universe level parameters as "outParam" -/
+        let (us, modified) ← preprocessLevels us
+        if modified then
+          let c := mkConst constName us
+          mkForallFVars xs (mkAppN c typeBody.getAppArgs)
+        else
+          return type
       else do
         let args := typeBody.getAppArgs
-        let us    ← preprocessLevels us
+        let (us, _) ← preprocessLevels us
         let c := mkConst constName us
         let cType ← inferType c
         let args ← preprocessArgs cType 0 args
         mkForallFVars xs (mkAppN c args)
-    | _ => pure type
+    | _ =>
+      return type
 
 /-
   Remark: when `maxResultSize? == none`, the configuration option `synthInstance.maxResultSize` is used.
diff --git a/tests/lean/run/319.lean b/tests/lean/run/319.lean
new file mode 100644
index 0000000000..01e22ceeab
--- /dev/null
+++ b/tests/lean/run/319.lean
@@ -0,0 +1,14 @@
+class Class.{u} where
+  dummy : PUnit.{u}
+
+def notWork [Class.{u}] : PUnit := Class.dummy
+def alsoNotWork [Class.{1}] : PUnit := Class.dummy
+def work [Class.{u}] : PUnit.{u} := Class.dummy
+def alsoWork [Class.{u}] := Class.dummy.{u}
+
+
+class Category.{v, u} (Ob : Type u) where
+  Hom : Ob → Ob → Type v
+
+variable (C : Type u) [Category.{v} C] (X : C)
+#check (Category.Hom X X)