Add Index built-in type-family (#19238)

Proposal: Add Index, a built-in type-family allowing indexing of a type-level list with a Nat without requiring intermediate coercion steps.

It is equivalent to the following user-defined type family:

      type family Index n xs where
          Index 0 (x:_)  = x
          Index n (_:xs) = Index (n-1) xs

But the resulting is much less verbose. For example in the new IndexFamily test we get the following Core:

      x :: Index 4 '[Float, Double, String, Char, Int, Word]
      x = IndexFamily.x1
          `cast` (Sub (Sym (IndexDef (<4>_N,
                                      <'[Float, Double, String, Char, Int, Word]>_N)))
                  :: Int ~R# Index 4 '[Float, Double, String, Char, Int, Word])
    
    instead of the following one with the user-defined family:
    
      x :: Index 4 '[Float, Double, String, Char, Int, Word]
      x = IndexFamily.x1
          `cast` (Sub (Sym (IndexFamily.D:R:Index[0]
                                <*>_N <Int>_N <'[Word]>_N))
                  ; (Index <*>_N (Sym (SubDef (<1>_N, <1>_N))) <'[Int, Word]>_N)_R
                  ; Sub (Sym (IndexFamily.D:R:Index[1]
                                  <*>_N <1>_N <Char>_N <'[Int, Word]>_N))
                  ; (Index
                       <*>_N (Sym (SubDef (<2>_N, <1>_N))) <'[Char, Int, Word]>_N)_R
                  ; Sub (Sym (IndexFamily.D:R:Index[1]
                                  <*>_N <2>_N <[Char]>_N <'[Char, Int, Word]>_N))
                  ; (Index
                       <*>_N
                       (Sym (SubDef (<3>_N, <1>_N)))
                       <'[[Char], Char, Int, Word]>_N)_R
                  ; Sub (Sym (IndexFamily.D:R:Index[1]
                                  <*>_N <3>_N <Double>_N <'[String, Char, Int, Word]>_N))
                  ; (Index
                       <*>_N
                       (Sym (SubDef (<4>_N, <1>_N)))
                       <'[Double, [Char], Char, Int, Word]>_N)_R
                  ; Sub (Sym (IndexFamily.D:R:Index[1]
                                  <*>_N <4>_N <Float>_N <'[Double, String, Char, Int, Word]>_N))
                  :: Int ~R# Index 4 '[Float, Double, String, Char, Int, Word])

Note that if we manage to generate smaller coercions for the user-defined family (cf #8095), we will just have to remove the built-in axioms. In the mean time, the built-in family is needed, e.g. to define generic sums.