length-indexed lists

I'm a bit surprised to not see a structure like the following in the package:

```haskell
data L n a where
LNil :: L 0 a
(:.) :: (KnownNat n) => a -> L n a -> L (1 + n) a

infixr 5 :.

deriving instance (Show a) => Show (L n a)

instance (Eq a) => Eq (L n a) where
LNil == LNil = True
LNil == (_ :. _) = error "impossible"
(_ :. _) == LNil = error "impossible"
(a1 :. (t1 :: L p a)) == (a2 :. (t2 :: L q a)) = case plusIsCancellative @1 @p @q of
Sub Dict -> a1 == a2 && t1 == t2

deriving instance Functor (L n)

instance (KnownNat n) => Applicative (L n) where
pure :: forall a. a -> L n a
pure a = go LNil
where
go :: forall m. (KnownNat m, KnownNat n) => L m a -> L n a
go as = case sameNat (Proxy :: Proxy (m :: Nat)) (Proxy :: Proxy (n :: Nat)) of
Nothing -> case plusNat @1 @m of
Sub Dict -> go @ (1 + (m :: Nat)) (a :. as)
Just Refl -> as
LNil <*> LNil = LNil
LNil <*> _ = error "impossible"
_ <*> LNil = error "impossible"
f :. (fs :: L p (a -> b)) <*> a :. (as :: L q a) = case plusIsCancellative @1 @p @q of
Sub Dict -> f a :. (fs <*> as)

instance Foldable (L n) where
foldMap _ LNil = mempty
foldMap f (x :. xs) = f x <> foldMap f xs

instance (KnownNat n) => Additive (L n) where
zero = pure 0
liftU2 _ LNil LNil = LNil
liftU2 _ LNil _ = error "impossible"
liftU2 _ _ LNil = error "impossible"
liftU2 f (a:.(as :: L p a)) (b :. (bs :: L q a)) = case plusIsCancellative @1 @p @q of
Sub Dict -> f a b :. liftU2 f as bs
liftI2 _ LNil LNil = LNil
liftI2 _ LNil _ = error "impossible"
liftI2 _ _ LNil = error "impossible"
liftI2 f (a:.(as :: L p a)) (b :. (bs :: L q b)) = case plusIsCancellative @1 @p @q of
Sub Dict -> f a b :. liftI2 f as bs

instance (KnownNat n) => Metric (L n)
```

Compared to `Linear.V`, this allows us to write:

```shell
> Linear.Metric.dot (2 :. 3 :. 4 :. LNil) (5 :. 6 :. 7 :. LNil)
56
```

instead of:

```shell
> (reifyVectorNat (Data.Vector.fromList [2, 3, 4]) $ reifyVectorNat (Data.Vector.fromList [5, 6, 7]) $ \(v1 :: V (n :: Nat) Int) (v2 :: V (m :: Nat) Int) -> case sameNat (Proxy :: Proxy n) (Proxy :: Proxy m) of Just Refl -> Linear.Metric.dot v1 v2) :: Int
56
```

My implementation uses `GHC.TypeNats` but maybe it would be better to use peano numbers. It would mean that `plusCancellative` and `plusNat` could be removed. My implementation also incurs a dependency on `constraints` package, but the relevant parts could be inlined