constructor in used constants

Stream: lean4

[Adam Topaz]

I came across something curious today:

import Lean
open Lean

structure Foo where
  a : Nat

#check @Foo.mk
/-
Foo.mk : Nat → Foo
-/

#eval show MetaM Unit from do
  let some c := (← getEnv).find? `Foo.mk | unreachable!
  for d in c.getUsedConstantsAsSet do
    println! d
/-
Foo
Nat
Foo.mk

-/

Why does Foo.mk appear as a used constant in Foo.mk? Is this expected?

[Adam Topaz]

I mean, it's clear why this is the case, given the code for getUsedConstantsAsSet:

/-- Return all names appearing in the type or value of a `ConstantInfo`. -/
def getUsedConstantsAsSet (c : ConstantInfo) : NameSet :=
  c.type.getUsedConstantsAsSet ++ match c.value? with
  | some v => v.getUsedConstantsAsSet
  | none => match c with
    | .inductInfo val => .ofList val.ctors
    | .opaqueInfo val => val.value.getUsedConstantsAsSet
    | .ctorInfo val => ({} : NameSet).insert val.name
    | .recInfo val => .ofList val.all
    | _ => {}

I guess I'm curious why the ctorInfo case includes val.name.