GADTs and match cases

Can you show us the definitions of the types index and level?
The compiler can deduce that the combinations Indexed _, Leveled _ and Leveled _, Indexed _ are impossible only if it can ensure that the types index and level are distinct.
If index and level are type aliases for the same type or, most probably, if they are both abstract, the compiler cannot ensure that they are distinct (see for instance, this previous discussion here: Unexpected GADT behavior when wrapping a type into a module).

Most probably, you do not rely on the fact that the type parameter of 'a t is either the type index or level themselves. Therefore, a solution can be to use another types to parameterize the result types of the constructors, for instance polymorphic variant types that are known to be distinct:

type _ t =
| Indexed : Ident.t * index -> [`index] t
| Leveled : Ident.t * level -> [`level] t