private and parameter

Stream: general

[Andrew Yang]

Consider this mwe

section
parameters (α : Type)
include α

private def foo : Type := α

#check foo /- foo : Type -/

example : Type := foo -- OK

example : Type := by exact foo
/-
invalid type ascription, term has type
  Type → Type
but is expected to have type
  Type
state:
α : Type
⊢ Type
-/

end

Lean seems to revert the parameters when private defs or lemmas are used in a tactic block.
It successfully compiles if private is removed. Is it really the case or am I missing something?

[Scott Morrison]

Given that using either parameters or private is discouraged, I'm not too surprised if there are bad interactions that haven't been noticed. :-(

[Mario Carneiro]

This is a known issue with parameters even without the private: parameters don't work inside tactics (they act like variables instead)