Private symbols are not unfolded

[NotBad4U]

I have a unification problem with the code below when code_S and S are private

symbol 𝑰 [a]: ℕ → τ a; 
private symbol code_S : Set;
private symbol S ≔ τ code_S;
private symbol a: S ≔ 𝑰 0;

I get the error:

The proof is not finished:
0. S ≡ τ ?498683
1. S ≡ τ ?498683
2. ?498683: Set
3. ?498683: Set

[fblanqui]

Please provide a standalone file.

[fblanqui]

symbol Set:TYPE;
injective symbol τ:Set → TYPE;
symbol ℕ:TYPE;
symbol 0:ℕ;
symbol 𝑰 [a]: ℕ → τ a;
private
symbol code_S : Set;
private
symbol S ≔ τ code_S;
private
symbol a: S ≔ 𝑰 0;
//symbol a0: S ≔ @𝑰 code_S 0;