diff --git a/src/Lean/Meta/Instances.lean b/src/Lean/Meta/Instances.lean index f06174629d41..c2d989bfbfbf 100644 --- 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 index 0cdbb4f66dc8..6037f72027bd 100644 --- 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 index 707c333edea2..b1728d2d885a 100644 --- 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