Unrolling data with Backpack

A co-worker of mine had a random thought on IRC: Is data type “unrolling” a valid performance optimization? Used anywhere? Something like: data List a = Nil | Cons a {-# Unroll 10 #-} (List a) I thought, that sounds like the vec package I wrote. One module there uses the GADT definition data Vec (n :: Nat) a where VNil :: Vec 'Z a (:::) :: a -> Vec n a -> Vec ('S n) a which in some cases optimizes

[igrep]

長さが固定サイズのリストの要素をbackpackを使ってunpackしようという話