Is a type like "fixed-size list of 3 integers" really more useful than a type like "list of integers" plus a constraint "size must be 3"? I feel like the latter is more flexible. Does Lean have a type for "list containing only prime powers"?
You can wrap a base type with a proof which is called bundling
inductive PrimePower where | mk (n : Nat) (prf : IsPrimePower n)
So in this case the type checker will not allow construction unless the proof demonstrates they are prime powers
The prf part gets erased at runtime so there's no overhead. You could also use a constraint/refinement type like you talked about and it's more flexible as it relates to using list operations like map filter reverse etc.