Inductive families/indexed types

[ollef]

So we can do more dependently typed goodness. If this is done, we can potentially also allow e.g.:

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).

[ollef]

Preliminary support was added in #133.