Polymorphic seq

Using Coq
1

Hello.
I am reading “Mathematical Components”, 1.3.1

Inductive seq (A : Type) := nil | cons (hd : A) (tl : seq A).
… (seq nat) is the type of sequences of natural numbers, while (seq bool) is the type of sequences of booleans.
Check seq nat.
seq nat
: Set
Check seq bool.
seq bool
: Set
So far so good.
Check seq 5.
Error: The term “5” has type “nat” while it is expected to have type “Type”.
This is expected. But
Check seq true.
seq true
: Set
Is this a feature or a bug?

2

There’s a coercion from bool to Prop so it’s expected.