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

Bonjour à tous,

J'ai récemment travaillé à ajouter l'élimination dépendante à Typer (4c632a1f, 8a7b7910), qui repose sur des égalités dans les expressions `case`. Pour les utiliser, on élimine éventuellement ces égalités avec `Eq.cast` (c'est ce que fait la macro `case_return_`, d'ailleurs). On dirait que dans certains cas de son utilisation (au niveau des types), il serait utile que les appels à `Eq.cast` puissent être réduits dans le calcul des WHNF, ce qui n'est pas le cas en ce moment.

Je me pose quelques questions quant à l'implantation de la WHNF de `Eq.cast`, sur lesquelles j'apprécierais vos commentaires. Aussi, pour rendre la discussion plus concrète, j'ai construit un petit exemple où l'unification échoue quand la réduction bloque sur un appel à `Eq.cast`.

Pour obtenir le code de l'exemple à partir de ce courriel, exécutez :

$ sed -n 's/^\s*> ?(.*)/\1/p' <email.txt >exemple.typer

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?

2. Exemple

Utilisons, au niveau des types, `decideBoolEq`, une fonction que l'on définit avec l'élimination dépendante, pour illustrer le problème.

Petite parenthèse, je vais utiliser le `case` builtin pour simplifier les affichages:

case_ = ##case_;

Prenons le type `Decidable` défini de cette façon:

Decidable = typecons (Decidable (ℓ ::: TypeLevel) (prop : Type_ ℓ)) (yes (p :: prop)) (no (p :: Not prop)); yes = datacons Decidable yes; no = datacons Decidable no;

Définissons `decideBoolEq`, qui prouve la décidabilité de l'égalité de booléens. On se sert des lemmes `true≠false` et `false≠true` qu'on définit au passage.

true≠false (p : Eq true false) = Eq_cast (p := p) (f := lambda tf -> case tf | true => True | false => False) (); % This is unit, an inhabitant of `True = Unit`.

false≠true (p : Eq false true) = true≠false (Eq_comm p);

decideBoolEq : (a : Bool) => (b : Bool) => Decidable (Eq a b); decideBoolEq = lambda (a : Bool) (b : Bool) => case a return (Decidable (Eq a b)) | true => (case b return (Decidable (Eq true b)) | true => yes (p := Eq_refl) | false => no (p := true≠false)) | false => (case b return (Decidable (Eq false b)) | true => no (p := false≠true) | false => yes (p := Eq_refl));

Note: Ici, on utilise la macro `case_return_`, qui insère les bons appels à `Eq.cast`.

Définissons maintenant une méthode d'accès pour obtenir la preuve d'un `Decidable`, qu'il soit vrai ou faux:

getProof : (l : TypeLevel) ≡> (prop : Type_ l) ≡> (d : Decidable prop) -> case d | yes => prop | no => Not prop; getProof d = case d return (case d | yes => prop | no => Not prop) | yes (p := p) => p | no (p := p) => p;

Ces définitions nous permettent de définir un terme qui fait échouer l'élaboration:

this_fails = (getProof (decideBoolEq : Decidable (Eq true true)) : Eq true true);

Voici l'erreur qu'on obtient:

% ./samples/exemple.typer:48:9:Error:(ELAB) Type mismatch (residue)! Context expected: % (Eq[257] ##TypeLevel.z typecons (Bool) (false) (true) true[210] true[210]) % but expression has type: % case (decideBoolEq[1] datacons Bool[211] true datacons Bool[211] true) | no _ => (Not[53] ##TypeLevel.z (Eq[259] ##TypeLevel.z typecons (Bool) (false) (true) true[212] true[212])) | yes _ => (Eq[259] ##TypeLevel.z typecons (Bool) (false) (true) true[212] true[212]) % can't unify: % (Eq[257] ##TypeLevel.z typecons (Bool) (false) (true) true[210] true[210]) % with: % case (decideBoolEq[1] datacons Bool[211] true datacons Bool[211] true) | no _ => (Not[53] ##TypeLevel.z (Eq[259] ##TypeLevel.z typecons (Bool) (false) (true) true[212] true[212])) | yes _ => (Eq[259] ##TypeLevel.z typecons (Bool) (false) (true) true[212] true[212]) % > Call: (getProof[0] ##TypeLevel.z (Eq[257] ##TypeLevel.z typecons (Bool) (false) (true) true[210] true[210]) (decideBoolEq[1] datacons Bool[211] true datacons Bool[211] true)) %

Pourquoi? On doit unifier le type de

getProof (decideBoolEq : Decidable (Eq true true))

qui est

case (decideBoolEq (a := true) (b := true)) | yes => Eq true true | no => Not (Eq true true)

avec `Eq true true`. Pour que cette unification fonctionne, il faut que `decideBoolEq (a := true) (b := true)` se réduise à un constructeur de `Decidable`, en l'occurence `yes`. Or, quand on regarde la première branche de `decideBoolEq`, on se rend compte qu'à cause de l'élimination dépendante, on obtient plutôt un appel à `Eq.cast`. Effectivement, en déboggant, j'obtiens le terme:

% (##Eq.cast % ##TypeLevel.z % ##TypeLevel.z % typecons (Bool) (false) (true) % true[210] % datacons Bool[211] true % (##Eq.refl % ##TypeLevel.z % Bool[211] % datacons Bool[211] true) % lambda (a : typecons (Bool) (false) (true)) -> % (Decidable[7] % ##TypeLevel.z % (Eq[258] ##TypeLevel.z typecons (Bool) (false) (true) a[0] datacons Bool[212] true)) % case datacons Bool[211] true % | false => (##Eq.cast ##TypeLevel.z ##TypeLevel.z typecons (Bool) (false) (true) false[210] datacons Bool[212] true <anon>[0] lambda (b : typecons (Bool) (false) (true)) -> (Decidable[8] ##TypeLevel.z (Eq[259] ##TypeLevel.z typecons (Bool) (false) (true) true[212] b[0])) (no[5] ##TypeLevel.z (Eq[258] ##TypeLevel.z typecons (Bool) (false) (true) true[211] false[210]) true≠false[4])) % | true => (##Eq.cast % ##TypeLevel.z % ##TypeLevel.z % typecons (Bool) (false) (true) % true[211] % datacons Bool[212] true % <anon>[0] % lambda (b : typecons (Bool) (false) (true)) -> % (Decidable[8] ##TypeLevel.z % (Eq[259] ##TypeLevel.z typecons (Bool) (false) (true) true[212] b[0])) % (yes[6] % ##TypeLevel.z % (Eq[258] ##TypeLevel.z typecons (Bool) (false) (true) datacons Bool[212] true datacons Bool[212] true) % (Eq_refl[216] ##TypeLevel.z typecons (Bool) (false) (true) datacons Bool[212] true))))

On constate que le `yes` que l'on cherche se trouve sous deux niveaux de `Eq.cast` à cause des deux niveaux de `case_return_` dans `decideBoolEq`. Ces deux appels à `Eq.cast` devraient pouvoir être réduits!

Jean-Alexandre