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