Al final de la sección "5. OTT completo" deHacia la teoría del tipo de observación Los autores muestran cómo definir los tipos de datos indexados coercibles bajo constructores en OTT. La idea es básicamente convertir los tipos de datos indexados en parámetros así:

data IFin : ℕ -> Set where
  zero : ∀ {n} -> IFin (suc n)
  suc  : ∀ {n} -> IFin n -> IFin (suc n)

data PFin (m : ℕ) : Set where
  zero : ∀ {n} -> suc n ≡ m -> PFin m
  suc  : ∀ {n} -> suc n ≡ m -> PFin n -> PFin m

Conor también menciona esta técnica en la parte inferior deteoría de tipo observacional (entrega):

La solución, por supuesto, es hacer lo que hicieron las personas GADT y definir explícitamente a las familias inductivas hasta la igualdad proposicional. Y luego, por supuesto, puede transportarlos, por transisitividad.

Sin embargo, un verificador de tipo en Haskell es consciente de las restricciones de igualdad en el alcance y en realidad las usa durante la verificación de tipo. P.ej. podemos escribir

f :: a ~ b => a -> b
f x = x

No funciona así en la teoría de tipos, ya que no es suficiente tener una prueba dea ~ b en alcance para poder reescribir por esta ecuación: esa prueba también debe serrefl, porque en presencia de una hipótesis falsa, la comprobación de tipos se vuelve indecidible debido a problemas de terminación (algo comoesta) Entonces, cuando el patrón coincide enFin m en Haskellm se reescribe asuc n en cada rama, pero eso no puede suceder en la teoría de tipos, en cambio, te queda una prueba explícita desuc n ~ m. En OTT no es posible emparejar patrones en pruebas, por lo tanto, tampoco puede pretender que la prueba esrefl ni realmente requieren eso. Solo es posible suministrar la prueba acoerce o simplemente ignóralo.

Esto hace que sea muy difícil escribir algo que implique tipos de datos indexados. P.ej. las tres líneas habituales (incluida la firma de tipo)lookup para vectores se convierte en esta bestia:

vlookupₑ : ∀ {n m a} {α : Level a} {A : Univ α} -> ⟦ n ≅ m ⇒ fin n ⇒ vec A m ⇒ A ⟧
vlookupₑ         p (fzeroₑ q)       (vconsₑ r x xs)      = x
vlookupₑ {n} {m} p (fsucₑ {n′} q i) (vconsₑ {m′} r x xs) =
  vlookupₑ (left (suc n′) {m} {suc m′} (trans (suc n′) {n} {m} q p) r) i xs
vlookupₑ {n} {m} p (fzeroₑ {n′} q)  (vnilₑ r)            =
  ⊥-elim $ left (suc n′) {m} {0} (trans (suc n′) {n} {m} q p) r
vlookupₑ {n} {m} p (fsucₑ {n′} q i) (vnilₑ r)            =
  ⊥-elim $ left (suc n′) {m} {0} (trans (suc n′) {n} {m} q p) r

vlookup : ∀ {n a} {α : Level a} {A : Univ α} -> Fin n -> Vec A n -> ⟦ A ⟧
vlookup {n} = vlookupₑ (refl n)

Podría simplificarse un poco, ya que si dos elementos de un tipo de datos que tiene igualdad decidible son observablemente iguales, entonces también son iguales en el sentido intensional habitual, y los números naturales tienen igualdad decidible, por lo que podemos forzar todas las ecuaciones a sus contrapartes intensivas y el patrón coinciden con ellos, pero eso rompería algunas propiedades computacionales devlookup y es detallado de todos modos. Es casi imposible lidiar en casos más complicados con índices cuya igualdad no se puede decidir.

¿Es correcto mi razonamiento? ¿Cómo debe funcionar la coincidencia de patrones en OTT? Si esto es realmente un problema, ¿hay alguna forma de mitigarlo?