fix test, change

leanprover · Jul 13, 2024 · cf600e0 · cf600e0
1 parent 99dcb90
commit cf600e0
Show file tree

Hide file tree

Showing 3 changed files with 7 additions and 5 deletions.
diff --git a/src/Lean/Meta/Instances.lean b/src/Lean/Meta/Instances.lean
@@ -192,6 +192,9 @@ private partial def computeSynthOrder (inst : Expr) : MetaM (Array Nat) :=
   return synthed
 
 def addInstance (declName : Name) (attrKind : AttributeKind) (prio : Nat) : MetaM Unit := do
+  let type := (← getConstInfo declName).type
+  unless (← isClass? type).isSome do
+    throwError "type class instance expected{indentExpr type}"
   let c ← mkConstWithLevelParams declName
   let keys ← mkInstanceKey c
   addGlobalInstance declName attrKind
@@ -203,9 +206,6 @@ builtin_initialize
     name  := `instance
     descr := "type class instance"
     add   := fun declName stx attrKind => do
-      let type := (← getConstInfo declName).type
-      unless (← isClass? type |>.run' {} {}).isSome do
-        throwError "type class instance expected{indentExpr type}"
       let prio ← getAttrParamOptPrio stx[1]
       discard <| addInstance declName attrKind prio |>.run {} {}
     erase := fun declName => do

diff --git a/tests/lean/run/simp_proj_transparency_issue.lean b/tests/lean/run/simp_proj_transparency_issue.lean
@@ -2,6 +2,8 @@ structure Foo where
   x : Nat
   y : Nat := 10
 
+attribute [class] Foo
+
 @[instance]
 def f (x : Nat) : Foo :=
   { x := x + x }

diff --git a/tests/lean/synthorder.lean.expected.out b/tests/lean/synthorder.lean.expected.out
@@ -1,6 +1,6 @@
-synthorder.lean:4:0-4:40: error: instance does not provide concrete values for (semi-)out-params
+synthorder.lean:4:0-4:8: error: instance does not provide concrete values for (semi-)out-params
   Foo A (B × ?C)
-synthorder.lean:7:0-7:38: error: cannot find synthesization order for instance @instFooNat with type
+synthorder.lean:7:0-7:8: error: cannot find synthesization order for instance @instFooNat with type
   {A : Type} → [inst : Foo A Nat] → Foo Nat A
 all remaining arguments have metavariables:
   Foo ?A Nat