Inductively defined flat vectors

[ollef]

Now that there's some support for inductive families (#133), it would be cool if we could support definitions like the following:

type Vector n a where
  Nil : Vector Zero a
  Cons : forall n. a -> Vector n a -> Vector (Succ n) a

Note that there's no Ptr on the tail of the Cons, meaning that this is an inductive definition of a flat vector. To get there, we can use pattern-matching on indices in the generated size-computing function for Vector. That function should be something like:

Vector Zero a = unitTypeRep
Vector (Succ n) a = productTypeRep a (Vector n a)

This also relies on adopting detagging (a la Edwin Brady) to remove the need for constructor tags (since we know what constructor we have just from the n index) and doing forcing to remove the n argument to the Cons constructor (since it can be recovered from the index).