Bonjour tout le monde,
J’aimerais signaler ce qui me semble être un bug. Il s’agit d’une boucle infinie lors du typechecking.
Je n’arrive pas à reproduire le bug en construisant un exemple plus simple, ce qui indique que je
n’ai toujours pas bien compris la chose exacte qui déclenche ce bug. Donc, je vous invite à aller
voir le code sur ma branche qui s’appelle `quot-types/normalisation`. Je précise que j’ai contourné
le problème dans la version actuelle du code, je vais vous expliquer comment le reproduire. C’est
la fonction `ee'≡id` dans le fichier `samples/quotient_normalisation.typer` qui pose problème. Le problème
se trouve dans l’annotation de type de cette fonction, pour une raison x ou y, le calcul de la WHNF de
l’expression suivante pourrait nous mener à une boucle infinie:
```
Eq (e (p := isSetA) (r := r) (i := i)
(e' (p := isSetA) (r := r) (i := i) s))
s
```
En investiguant davantage, je me suis rendu compte que le vrai coupable est la fonction `Sigma_η` que
j’ai définie dans `btl/pervasive.typer`. Voici la ‘chaîne de dépendance entre `ee’≡id` et `Sigma_η`:
```
ee'≡id ⇨ e ⇨ Qnorm_eq ⇨ Σ≡Prop ⇨ Sigma_η
```
Maintenant, regardons la fonction `Sigma_η`, elle contient un `case` qui fait une élimination
dépendante en utilisant la preuve d’égalité qui est insérée dans le contexte, on peut y accéder avec
`##DeBruijn 0`. Le problème se produit lorsqu’on met cette preuve d’égalité dans une variable d’un
`let`. Par exemple, si on définit `Sigma_η` comme suit,
```
Sigma_η : (A : Type_ ?) ≡> (P : (a : A) -> Type_ ?)
≡> (p : Sigma A P) -> Eq p (sigma (B := P) p.fst p.snd);
Sigma_η p = case p
| sigma x y =>
let
branch≡p : Eq (sigma (B := P) x y) p;
branch≡p = ##DeBruijn 0;
in
Eq_cast (x := sigma (B := P) x y) (y := p)
(p := branch≡p) %% Proof of Eq (sigma x y) p
(f := lambda x -> Eq x (sigma (B := P) x.fst x.snd))
%% Proof of Eq (sigma x y) (sigma x y).fst (sigma x y).snd
Eq_refl;
```
on se retrouve avec une boucle infinie lors du typechecking de `ee’≡id`, ça ne nuit pas au typechecking
des autres fonctions par contre.
Pour l’instant, je suis toujours pas sûr pourquoi le calcul de la WHNF de la fonction ci-dessus pourrait être
problématique, ça pourrait être lié à la façon dont on insère la preuve d’égalité dans l’environnement.
J'investiguerai davantage quand j’aurai le temps. Est-ce que vous avez déjà rencontré quelque chose de
similaire?
James
