Error when my inductive type have more than one parameter

[NotBad4U]

Hi! When I try to add a second parameter to the inductive type 𝕃, I get the error:

Cannot solve $130 □ ≡ $130 □

Here is a snippet of code to reproduce the problem:

symbol Prop : TYPE;
injective symbol Prf : Prop → TYPE;
builtin "Prop" ≔ Prop;
builtin "P" ≔ Prf;

symbol Set : TYPE; 
injective symbol τ : Set → TYPE;

(a:Set) (b:Set) inductive 𝕃:TYPE ≔
| □  : 𝕃 a b
| ⸬   : τ a → τ b → 𝕃 a b → 𝕃 a b;

Thank you in advance!

[amelieled]

The following is the translation from the second type-checker (me): τ b is not typable because b has type Prop and τ has type Set → TYPE.

[NotBad4U]

Sorry @amelieled I forgot to update the code in the issue (I just updated), there is an error even if b is a Set. @fblanqui is investigating the error.

[NotBad4U]

@fblanqui, any news about this bug? Maybe I can have a look if you give me some points to look at?

[fblanqui]

Sorry no. I am currently in Japan until June 11. I will try to look at that next week or when I am back.