existentials observe different behavior if using projections

Stream: new members

[Evan Gao]

(original issue: https://github.com/leanprover/lean4/issues/8520)
Sorry if the title seems weird because Zulip has word limit.
Anyway, my confusion is that, when defining an abstract type which contains some existentials, the semantics of extracting the underlying type and its methods vary depending on the way one extracts it(either pattern matching or invoking projection functions)
F is existentially quantified in AbstractStack:

inductive AbstractStack (β : Type u) where
  | mk {F : Type u -> Type u} [Inhabited β]
  : F β
  → (β -> F β -> F β)    -- push
  → (F β -> β × F β)     -- pop
  → AbstractStack β

def ListStack (s : List σ) : AbstractStack σ :=
  mk s cons snoc

Normally when extracting push and pop through pattern matching, we can observe that F is locally introduced, which can't escape its scope:

example : IO Unit := do
  let (mk s push pop) := ListStack [1,2,3,4,5]
  println! "{push 6 s}"   -- not cool. `F` is arbitrary
  println! "{pop s |>.1}" -- cool. `Nat` is concrete
-- This is expected behavior

However, through projection functions, we can directly extract the concrete type of a certain AbstractStack implementation, in this case ListStack:

def AbstractStack.F (s : AbstractStack σ) := s.1
def AbstractStack.push (s : AbstractStack σ) := s.4

#reduce -- yields (List, List.cons)
  let ls := show AbstractStack Unit from ListStack []
  (ls.F, ls.push)
#eval   -- yields [1,1,2]
  let ls := show AbstractStack.{0} Nat from ListStack []
  ls.push 1 [1,2]

From what I can see, this reveals the underlying implementation of ListStack and what's more important is that this behavior is different from extracting through pattern matching.