feat: improve implementedBy errors, and relax type matching test

src/Lean/Compiler/ImplementedByAttr.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 import Lean.Attributes
+import Lean.Declaration
 import Lean.MonadEnv
 
 namespace Lean.Compiler
@@ -16,8 +17,12 @@ builtin_initialize implementedByAttr : ParametricAttribute Name ← registerPara
     let fnName ← Attribute.Builtin.getIdent stx
     let fnName ← resolveGlobalConstNoOverload fnName
     let fnDecl ← getConstInfo fnName
-    unless decl.type == fnDecl.type do
-      throwError "invalid function '{fnName}' type mismatch"
+    unless decl.levelParams.length == fnDecl.levelParams.length do
+      throwError "invalid 'implementedBy' argument '{fnName}', '{fnName}' has {fnDecl.levelParams.length} universe level parameter(s), but '{declName}' has {decl.levelParams.length}"
+    let declType := decl.type
+    let fnType := fnDecl.instantiateTypeLevelParams (decl.levelParams.map mkLevelParam)
+    unless declType == fnType do
+      throwError "invalid 'implementedBy' argument '{fnName}', '{fnName}' has type{indentExpr fnType}\nbut '{declName}' has type{indentExpr declType}"
     if decl.name == fnDecl.name then
       throwError "invalid 'implementedBy' argument '{fnName}', function cannot be implemented by itself"
     return fnName

tests/lean/implementedByIssue.lean

@@ -0,0 +1,19 @@
+namespace Hidden
+
+structure Array (α : Type u) (n : Nat) : Type u where
+  data : (i : Fin n) → α
+
+@[extern "some_extern"]
+def get {α} {n : Nat}
+        (A : Array α n) (i : Fin n) : α
+  := A.data i
+
+attribute [implementedBy get] Array.data -- ok
+
+def get_2 {α : Type} {n : Nat} (A : Array α n) (i : Fin n) : α := A.data i
+
+attribute [implementedBy get_2] Array.data -- error, number of universe parameters do not match
+
+def get_3 {α} {n : Nat} (i : Fin n) (A : Array α n) : α := A.data i
+
+attribute [implementedBy get_3] Array.data -- error, types do not match

tests/lean/implementedByIssue.lean.expected.out

@@ -0,0 +1,5 @@
+implementedByIssue.lean:15:32-15:42: error: invalid 'implementedBy' argument 'Hidden.get_2', 'Hidden.get_2' has 0 universe level parameter(s), but 'Hidden.Array.data' has 1
+implementedByIssue.lean:19:32-19:42: error: invalid 'implementedBy' argument 'Hidden.get_3', 'Hidden.get_3' has type
+  {α : Type u} → {n : Nat} → Fin n → Array α n → α
+but 'Hidden.Array.data' has type
+  {α : Type u} → {n : Nat} → Array α n → Fin n → α