[Typer] Ajout de la WHNF de `Eq.cast`

[Stefan Monnier]

> 1. Question
>
>    Je me demande comment implanter la WHNF de `Eq.cast`, j'ai
>    l'impression, intuitivement, qu'il suffit de vérifier que son
>    argument `p` est bel et bien convertible à `Eq.refl` (autrement
>    dit, ce n'est pas simplement une variable/hypothèse), auquel cas,
>    il me paraît correct d'ignorer l'argument `f` et de se réduire à
>    l'argument explicite.
>
>    Évidemment, si `p` n'est pas convertible à `Eq.refl`, la réduction
>    doit bloquer.
>
>    Est-ce que cette approche peut causer des problèmes au niveau
>    théorique?

Ça ne va pas casser la cohérence de la logique (qui dans notre cas est
déjà cassée par le manque de termination-checker, de toute façon), non.

Par contre, ça pose un problème au moins conceptuel et potentiellement
pratique dans le sens que ça signifie qu'on ne peut pas faire cette
réduction après avoir effacé les argument effaçables.

Si on décide que l'effacement se fait après la vérification de types
(et donc que la convertibilité est vérifiée sur des termes
avant-effacement), alors cette règle ne pose aucun problème.  Si par
contre on aimerait faire l'effacement avant la vérification (ce qui
donne une notion de convertibilité un peu plus forte vu qu'elle va
permet de convertir des termes qui ont des parties effaçable
non-convertibles), ça pourrait poser problème.

Ceci dit, peut-être qu'on peut avoir le beurre et l'argent du beurre: en
fait, actuellement la notion de convertibilité "forte" (contrôlée par
la variable `conv_erase`) est utilisée sans effectuer l'effacement en
tant que tel, donc on peut utiliser la règle que tu suggères tout en
fermant les yeux sur les arguments effaçables lorsqu'on teste la
convertibilité de 2 termes.

La méta-théorie d'un tel système n'est probablement pas très jolie par
contre: `conv_erase` nous dirait normalement qqch comme

                    e₁ ≃ e₂
   -------------------------------------------
   Eq.cast _ _ _ _ _ e₁ ≃ Eq.cast _ _ _ _ _ e₂

quelque soient les arguments `_`, donc ça nous dit aussi que

    Eq.cast _ _ _ _ _ e₁ ≃ Eq.cast _ _ _ _ (Eq.refl _) e₁

et donc qu'on peut *toujours* réduire `Eq.cast` sans même regarder si la
preuve est `Eq.refl`, et ça on sait que c'est pas sound :-(

Donc en théorie `conv_erase` est incompatible avec la règle que tu
proposes, est-ce que ça s'applique aussi à notre
implantation de `conv_p`, je ne sais pas.

Mais, je ne vois pas de bonne alternative, alors: ¡Go for it!

> 2. Exemple

Merci pour l'exemple détaillé.  Je ne vois pas de manière satisfaisante
de résoudre ce problème autre que de faire la réduction que tu suggères.


        Stefan