Impossible to pattern match on Ctxs and discover _what_ constructor it is pointing to

Given the definition of `Ctxs`:

```haskell
data Ctx :: (kon -> *) -> [*] -> [[Atom kon]] -> Nat -> * where
Ctx :: Constr c n
-> NPHole ki fam ix (Lkup n c)
-> Ctx ki fam c ix
data Ctxs :: (kon -> *) -> [*] -> [[[Atom kon]]] -> Nat -> Nat -> * where
Nil :: Ctxs ki fam cs ix ix
Cons :: (IsNat ix , IsNat a , IsNat b)
=> Ctx ki fam (Lkup ix cs) b -> Ctxs ki fam cs a ix
-> Ctxs ki fam cs a b
```

and me wanting to visualize the Constructor the hole is pointing to

We will need to somehow call :
```haskell
datatypeInfo :: (IsNat ix)
=> Proxy fam -> SNat ix -> DatatypeInfo (Lkup ix codes)
```

However, When we pattern match on `Cons`, and want to call `datatypeInfo`,
How do we ever discover the `SNat ix` that we need to supply? Because
`ix` is existential in `Ctxs` we can't call `getSNat (Proxy :: Proxy ix)`

So there is no what for us to visualize the Constructor inside `Ctx`

```haskell
case ctxs of
Nil -> ""
Cons (Ctx c h) ctxs ->
constructorName (constrInfoLkup c (datatypeInfo (Proxy :: Proxy fam)) ????)
```

Start with the Ctxs, Cons, Ctx, and datatypeInfo definitions shown in the issue, then trace how the existential ix is represented when matching on Cons. Done means establishing a documented or implementable way to obtain the needed SNat ix and identify the constructor referenced by each Ctx.

Written by the indexing model from the issue text.