No final da seção "5. OTT completo" doRumo à teoria do tipo observacional os autores mostram como definir tipos de dados indexados coercíveis em construtores no OTT. A ideia é basicamente transformar tipos de dados indexados em parâmetros assim:

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 também menciona essa técnica na parte inferior dateoria observacional do tipo (entrega):

A solução, é claro, é fazer o que o pessoal do GADT fez e definir famílias indutivas explicitamente até a igualdade proposicional. E então é claro que você pode transportá-los, por transisibilidade.

No entanto, um verificador de tipos no Haskell está ciente das restrições de igualdade no escopo e realmente as utiliza durante a verificação de tipos. Por exemplo. nós podemos escrever

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

Isso não funciona na teoria dos tipos, pois não basta ter uma prova dea ~ b no escopo para poder reescrever essa equação: essa prova também deve serrefl, porque, na presença de uma falsa hipótese, a verificação do tipo se torna indecidível devido a problemas de terminação (algo comoesta) Então, quando você padroniza a correspondênciaFin m em Haskellm é reescrito parasuc n em cada ramificação, mas isso não pode acontecer na teoria dos tipos. Em vez disso, você fica com uma prova explícita desuc n ~ m. No OTT, não é possível padronizar a correspondência nas provas; portanto, você não pode fingir que a prova érefl nem realmente exigem isso. Só é possível fornecer a prova paracoerce ou simplesmente ignore.

Isso torna muito difícil escrever qualquer coisa que envolva tipos de dados indexados. Por exemplo. as três linhas usuais (incluindo a assinatura de tipo)lookup para vetores se torna esta fera:

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)

Isso poderia ser um pouco simplificado, pois se dois elementos de um tipo de dados com igualdade decidível são observáveis iguais, eles também são iguais no sentido intensional usual e os números naturais têm igualdade decidível, para que possamos coagir todas as equações a suas contrapartes intensionais e padrões coincidem com eles, mas isso quebraria algumas propriedades computacionais devlookup e é detalhado de qualquer maneira. É quase impossível lidar em casos mais complicados com índices cuja igualdade não pode ser decidida.

Meu raciocínio está correto? Como a correspondência de padrões no OTT deve funcionar? Se esse é realmente um problema, existem maneiras de mitigá-lo?