feat: make #check <ident> always show the signature without elaboration

src/Lean/Elab/BuiltinCommand.lean

@@ -235,22 +235,23 @@ open Meta
 
 def elabCheckCore (ignoreStuckTC : Bool) : CommandElab
   | `(#check%$tk $term) => withoutModifyingEnv <| runTermElabM fun _ => Term.withDeclName `_check do
+    -- show signature for `#check id`/`#check @id`
+    if let `($_:ident) := term then
+      try
+        for c in (← resolveGlobalConstWithInfos term) do
+          addCompletionInfo <| .id term c (danglingDot := false) {} none
+          logInfoAt tk <| .ofPPFormat { pp := fun
+            | some ctx => ctx.runMetaM <| PrettyPrinter.ppSignature c
+            | none     => return f!"{c}"  -- should never happen
+          }
+          return
+      catch _ => pure ()  -- identifier might not be a constant but constant + projection
     let e ← Term.elabTerm term none
     Term.synthesizeSyntheticMVarsNoPostponing (ignoreStuckTC := ignoreStuckTC)
     let e ← Term.levelMVarToParam (← instantiateMVars e)
     let type ← inferType e
     if e.isSyntheticSorry then
       return
-    -- show signature for `#check id`/`#check @id`
-    match term with
-    | `($_:ident) | `(@$_:ident) =>
-      if let .const c _ := e then
-        logInfoAt tk <| .ofPPFormat { pp := fun
-          | some ctx => ctx.runMetaM <| PrettyPrinter.ppSignature c
-          | none     => return f!"{c}"  -- should never happen
-        }
-        return
-    | _ => pure ()
     logInfoAt tk m!"{e} : {type}"
   | _ => throwUnsupportedSyntax
 

tests/lean/1026.lean

@@ -10,4 +10,4 @@ theorem ex : foo 0 = 0 := by
   unfold foo
   sorry
 
-#check @foo._unfold
+#check foo._unfold

tests/lean/1098.lean

@@ -9,7 +9,7 @@ inductive R : FoldImpl α β → FoldImpl α β → Prop where
 
 #print R
 
-#check @R.intro
+#check R.intro
 -- @R.intro : ∀ {α β γ γ' : Type u_1} {x₀ : γ} {y₀ : γ'} {f : γ → α → γ} {g : γ' → α → γ'} {out : γ → β} {out' : γ' → β},
 --   R { γ := γ, x₀ := x₀, f := f, out := out } { γ := γ', x₀ := y₀, f := g, out := out' }
 

tests/lean/604.lean.expected.out

@@ -1,4 +1,4 @@
 foo ⦃u : Unit⦄ : Unit
 foo : ⦃u : Unit⦄ → Unit
-bla : Unit
+bla {u : Unit} : Unit
 fun {u} => bla : {u : Unit} → Unit

tests/lean/714.lean.expected.out

@@ -1 +1 @@
-test : Type
+test {α : Type} [inst✝ : LT α] : Type

tests/lean/974.lean

@@ -10,9 +10,9 @@ def Formula.count_quantifiers : {n:Nat} → Formula n → Nat
 
 attribute [simp] Formula.count_quantifiers
 
-#check @Formula.count_quantifiers._eq_1
-#check @Formula.count_quantifiers._eq_2
-#check @Formula.count_quantifiers._eq_3
+#check Formula.count_quantifiers._eq_1
+#check Formula.count_quantifiers._eq_2
+#check Formula.count_quantifiers._eq_3
 
 @[simp] def Formula.count_quantifiers2 : Formula n → Nat
 | imp f₁ f₂ => f₁.count_quantifiers2 + f₂.count_quantifiers2

tests/lean/986.lean

@@ -1,4 +1,4 @@
 attribute [simp] Array.insertionSort.swapLoop
 
-#check @Array.insertionSort.swapLoop._eq_1
-#check @Array.insertionSort.swapLoop._eq_2
+#check Array.insertionSort.swapLoop._eq_1
+#check Array.insertionSort.swapLoop._eq_2

tests/lean/LE.lean

@@ -1,5 +1,5 @@
 inductive LE' : Nat → Nat → Prop where
   | refl (n : Nat) : LE' n n
 
-#check @LE'.refl
+#check LE'.refl
 #print LE'

tests/lean/autoBoundImplicits1.lean

@@ -30,7 +30,7 @@ variable (xs : Vec α n) -- works
 
 def f := xs
 
-#check @f
+#check f
 
 #check f mkVec
 

tests/lean/autoBoundImplicits2.lean.expected.out

@@ -1,4 +1,4 @@
-g1 : ?m → ?m
+g1.{u} {α : Type u} (a : α) : α
 autoBoundImplicits2.lean:30:17-30:18: error: unknown universe level 'u'
 autoBoundImplicits2.lean:33:17-33:18: error: unknown universe level 'β'
 def h1.{u} : {m : Type u → Type u} → {α : Type u} → m α → m α :=

tests/lean/autoImplicitChainNameIssue.lean

@@ -9,4 +9,4 @@ theorem palindrome_reverse (h : Palindrome as) : Palindrome as.reverse := by
   | single a => exact Palindrome.single a
   | sandwish a h ih => simp; exact Palindrome.sandwish _ ih
 
-#check @palindrome_reverse
+#check palindrome_reverse

tests/lean/autoIssue.lean

@@ -3,7 +3,7 @@ structure A :=
   x : Nat
   a' : x = 1 := by trivial
 
-#check @A.a'
+#check A.a'
 
 example (z : A) : z.x = 1 := by
   have := z.a'
@@ -15,7 +15,7 @@ example (z : A) : z.x = 1 := by
   trace_state
   exact this
 
-#check @A.rec
+#check A.rec
 
 example (z : A) : z.x = 1 := by
   have ⟨x, a'⟩ := z

tests/lean/binderCacheIssue.lean.expected.out

@@ -1,4 +1,4 @@
-LNot.unpackFun : LNot ?m → ∀ (p : ?m), ¬?m p
+LNot.unpackFun.{u} {P : Sort u} {L : P → Prop} (K : LNot L) (p : P) : ¬L p
 Funtype.unpack : LNot ?m → ∀ (p : ?m), ¬?m p
-LNot.applyFun : LNot ?m → ∀ {p : ?m}, ¬?m p
+LNot.applyFun.{u} {P : Sort u} {L : P → Prop} (K : LNot L) {p : P} : ¬L p
 Funtype.apply : LNot ?m → ∀ {p : ?m}, ¬?m p

tests/lean/ctorUnivTooBig.lean

@@ -21,7 +21,7 @@ inductive Member : α → List α → Type u
   | head : Member a (a::as)
   | tail : Member a bs → Member a (b::bs)
 
-#check @Member.head
+#check Member.head
 end Ex1
 
 namespace Ex2

tests/lean/derivingRpcEncoding.lean

@@ -50,7 +50,7 @@ structure FooGeneric (α : Type) where
   b? : Option α
   deriving RpcEncodable, Inhabited
 
-#check @instRpcEncodableFooGeneric
+#check instRpcEncodableFooGeneric
 #eval test (FooGeneric Nat) default
 #eval test (FooGeneric Nat) { a := 3, b? := some 42 }
 
@@ -58,7 +58,7 @@ inductive BazInductive
   | baz (arr : Array Bar)
   deriving RpcEncodable, Inhabited
 
-#check @instRpcEncodableBazInductive
+#check instRpcEncodableBazInductive
 #eval test BazInductive ⟨#[default, default]⟩
 
 inductive FooInductive (α : Type) where
@@ -66,7 +66,7 @@ inductive FooInductive (α : Type) where
   | b : (n : Nat) → (a : α) → (m : Nat) → FooInductive α
   deriving RpcEncodable, Inhabited
 
-#check @instRpcEncodableFooInductive
+#check instRpcEncodableFooInductive
 #eval test (FooInductive BazInductive) (.a default default)
 #eval test (FooInductive BazInductive) (.b 42 default default)
 
@@ -80,20 +80,20 @@ inductive FooParam (n : Nat) where
   | a : Nat → FooParam n
   deriving RpcEncodable, Inhabited
 
-#check @instRpcEncodableFooParam
+#check instRpcEncodableFooParam
 #eval test (FooParam 10) (.a 42)
 
 inductive Unused (α : Type) | a
   deriving RpcEncodable, Inhabited
 
-#check @instRpcEncodableUnused
+#check instRpcEncodableUnused
 structure NoRpcEncodable
 #eval test (Unused NoRpcEncodable) default
 
 structure UnusedStruct (α : Type)
   deriving RpcEncodable, Inhabited
 
-#check @instRpcEncodableUnusedStruct
+#check instRpcEncodableUnusedStruct
 #eval test (UnusedStruct NoRpcEncodable) default
 
 deriving instance Repr, RpcEncodable for Empty

tests/lean/diamond2.lean

@@ -11,7 +11,7 @@ set_option structureDiamondWarning false
 
 structure Foo1 (α : Type) extends Bar (α → α), Baz α
 
-#check @Foo1.mk
+#check Foo1.mk
 
 def f1 (x : Nat) : Foo1 Nat :=
   { a := id
@@ -26,7 +26,7 @@ structure Boo2 (α : Type) extends Boo1 α where
 
 structure Foo2 (α : Type) extends Bar (α → α), Boo2 α
 
-#check @Foo2.mk
+#check Foo2.mk
 
 def f2 (v : Nat) : Foo2 Nat :=
   { a  := id

tests/lean/diamond5.lean

@@ -14,4 +14,4 @@ def D.toC (x : Nat) := x
 
 class D (α : Type) extends B α, C α
 
-#check @D.toC_1
+#check D.toC_1

tests/lean/diamond6.lean

@@ -14,7 +14,7 @@ class FooAC (α : Type) extends FooComm α, FooAssoc α where
   mul_comm (a b : α) : a * b = b * a
 
 set_option pp.all true
-#check @FooAC.mk
+#check FooAC.mk
 
 #print FooAC.toFooAssoc
 
@@ -24,7 +24,7 @@ class FooAssoc' (α : Type) extends FooAssoc α where
 class FooAC' (α : Type) extends FooComm α, FooAssoc' α where
   mul_comm (a b : α) : a * b = b * a
 
-#check @FooAC'.mk
+#check FooAC'.mk
 
 #print FooAC'.toFooAssoc'
 

tests/lean/diamond7.lean

@@ -17,7 +17,7 @@ class Monoid (α : Type u) extends Semigroup α, One α where
 class CommMonoid (α : Type u) extends Monoid α, CommSemigroup α
 
 set_option pp.all true
-#check @CommMonoid.mk
+#check CommMonoid.mk
 #print CommMonoid.toCommSemigroup
 
 class Inv (α : Type u) where
@@ -30,7 +30,7 @@ class Group (α : Type u) extends Monoid α, Inv α where
 
 class CommGroup (α : Type u) extends Group α, CommMonoid α
 
-#check @CommGroup.mk
+#check CommGroup.mk
 #print CommGroup.toCommMonoid
 
 class AddSemigroup (α : Type u) extends Add α where
@@ -87,6 +87,6 @@ class DivisionRing (α : Type u) extends Ring α, Inv α, ZeroNeOne α where
 class Field (α : Type u) extends DivisionRing α, CommRing α
 
 set_option pp.all false in
-#check @Field.mk
+#check Field.mk
 #print Field.toDivisionRing
 #print Field.toCommRing

tests/lean/heapSort.lean

@@ -173,6 +173,6 @@ termination_by _ => a.size
 decreasing_by assumption
 
 attribute [simp] Array.heapSort.loop
-#check @Array.heapSort.loop._eq_1
+#check Array.heapSort.loop._eq_1
 
 attribute [simp] BinaryHeap.heapifyDown

tests/lean/levelNGen.lean

@@ -1,6 +1,6 @@
 opaque test1 {α : Sort _} : α → Sort u_1
-#check @test1
+#check test1
 def test2 {α : Sort _} : α → Sort u_1 := sorry
-#check @test2
+#check test2
 variable {α : Sort _} in theorem test3 : α → Sort _ := sorry
-#check @test3
+#check test3

tests/lean/match1.lean.expected.out

@@ -46,6 +46,6 @@ fun x =>
   | #[] => 0
   | #[3, 4, 5] => 3
   | x => 4 : Array Nat → Nat
-g.match_1 : (motive : List ?m → Sort u_2) →
-  (x : List ?m) → ((a : ?m) → motive [a]) → ((x : List ?m) → motive x) → motive x
+g.match_1.{u_1, u_2} {α : Type u_1} (motive : List α → Sort u_2) (x✝ : List α) (h_1 : (a : α) → motive [a])
+  (h_2 : (x : List α) → motive x) : motive x✝
 fun e => nomatch e : Empty → False

tests/lean/openScoped.lean

@@ -1,4 +1,4 @@
-#check @epsilon -- Error
+#check epsilon -- Error
 
 noncomputable def foo1 (f g : Nat → Nat) : Nat :=
   if f = g then 1 else 2 -- Error
@@ -6,18 +6,18 @@ noncomputable def foo1 (f g : Nat → Nat) : Nat :=
 section
 open Classical
 
-#check @epsilon
+#check epsilon
 
 noncomputable def foo2 (f g : Nat → Nat) : Nat :=
   if f = g then 1 else 2 -- Ok
 end
 
-#check @epsilon -- Error
+#check epsilon -- Error
 
 section
 
 open scoped Classical
-#check @epsilon -- Error
+#check epsilon -- Error
 
 noncomputable def foo3 (f g : Nat → Nat) : Nat :=
   if f = g then 1 else 2 -- Ok

tests/lean/openScoped.lean.expected.out

@@ -1,6 +1,6 @@
-openScoped.lean:1:8-1:15: error: unknown identifier 'epsilon'
+openScoped.lean:1:7-1:14: error: unknown identifier 'epsilon'
 openScoped.lean:4:2-4:24: error: failed to synthesize instance
   Decidable (f = g)
 Classical.epsilon.{u} {α : Sort u} [h : Nonempty α] (p : α → Prop) : α
-openScoped.lean:15:8-15:15: error: unknown identifier 'epsilon'
-openScoped.lean:20:8-20:15: error: unknown identifier 'epsilon'
+openScoped.lean:15:7-15:14: error: unknown identifier 'epsilon'
+openScoped.lean:20:7-20:14: error: unknown identifier 'epsilon'

tests/lean/precissues.lean.expected.out

@@ -3,9 +3,9 @@ id fun x => x : ?m → ?m
 f 1 fun x => x : Nat
 0 : Nat
 f 1 fun x => x : Nat
-id : ?m → ?m
+id.{u} {α : Sort u} (a : α) : α
 precissues.lean:15:10: error: expected command
-id : ?m → ?m
+id.{u} {α : Sort u} (a : α) : α
 precissues.lean:17:10: error: expected command
 1 : Nat
 id
@@ -26,5 +26,5 @@ p ∧ ¬q : Prop
 ¬p = q : Prop
 id ¬p : Prop
 Nat → ∀ (a : Nat), a = a : Prop
-id : ?m → ?m
+id.{u} {α : Sort u} (a : α) : α
 precissues.lean:41:10: error: expected command

tests/lean/sizeof.lean

@@ -15,4 +15,4 @@ inductive InfTree (α : Type u)
 
 #reduce sizeOf <| InfTree.leaf 10
 
-#check @InfTree.node.sizeOf_spec
+#check InfTree.node.sizeOf_spec

tests/lean/strictImplicit.lean.expected.out

@@ -1,4 +1,4 @@
-g : ?m → ?m
+g {α : Type} (a : α) : α
 f ⦃α : Type⦄ (a : α) : α
 g 1 : Nat
 f 1 : Nat

tests/lean/varBinderUpdate.lean

@@ -8,8 +8,8 @@ def f (a : α) := a + a
 variable {α}
 def g (b : α) := b
 #check g 5
-#check @f
-#check @g
+#check f
+#check g
 end Ex1
 
 namespace Ex2
@@ -20,8 +20,8 @@ def f (a : α) := a
 def g (b : β) := b
 #check f Nat 5
 #check g 5
-#check @f
-#check @g
+#check f
+#check g
 variable (α)
 end Ex2
 
@@ -31,10 +31,10 @@ variable {α : Type}
 variable (f : α → α)
 variable (α)
 def g (a : α) := f a
-#check @g
+#check g
 variable {f}
 def h (a : α) := f a
-#check @h
+#check h
 end Ex3
 
 namespace Ex4