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

[Barszcz Jean-Alexandre]

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