[ J'ajoute typer@iro. ]
> Présentement, j'ai un type Exists défini comme suit :
>
> type Exists (l ::: TypeLevel) (t :: Type_ l) (f : t -> Type_ l) :
> Type_ l
> | exists (v : t) (f v);
[ Side notes:
Hmm... pourquoi `::` au lieu de `:::` pour `t`?
Ah, et les deux niveaux n'ont pas besoin d'être les mêmes, donc ça
devrait être:
type Exists (l₁ ::: TypeLevel) (l₂ ::: TypeLevel) (t :: Type_ l₁)
(f : t -> Type_ l₂)
: Type_ (l₁ ∪ l₂)
| exists (v : t) (f v);
que l'on devrait idéalement pouvoir écrire:
type Exists (f : ?t -> Type)
| exists (v : t) (f v);
Ah, et un "vrai" existentiel (un "weak sum" ∃ et non un "strong sum"
Σ) est "faible", donc ça devrait être:
type Exists (f : ?t -> Type)
| exists (f ?v);
A.K.A
type Exists (l₁ ::: TypeLevel) (l₂ ::: TypeLevel) (t :: Type_ l₁)
(f : t -> Type_ l₂)
: Type_ l₂
| exists (v ::: t) (f v);
]
> Je tente de le tester de cette façon :
>
> test4 : Exists (lambda (v : Int) -> Eq v 4);
> test4 = exists 4 Eq_refl;
>
> Étrangement, le type-checker refuse ce code :
>
> sl/logic.typer:36:17-36:24 Error:(ELAB) Type mismatch (residue)!
> Context expected:
> (?f↑0 (fromInteger ?t↑0 ?inst↑0 4))
> but expression has type:
> (Eq ?l↑0 ?t↑0 ?x↑0 ?x↑0)
> can't unify:
> (Eq ?l↑0 ?t↑0 ?x↑0 ?x↑0)
> with:
> (?f↑0 (fromInteger ?t↑0 ?inst↑0 4))
> > (Eq_refl ?l↑0 ?t↑0 ?x↑0)
> Compiler stopped after: 1 errors
>
> Pourtant, le deuxième paramètre de `exists` est de type `(lambda (v :
> Int) -> Eq v 4) 4`, qui se réduit en principe à `Eq 4 4`. Mais à en juger
> par le message d'erreur, au moment de vérifier `exists 4 Eq_refl`, le
> type-checker ne semble pas savoir ce que vaut `f`, et utilise une
> méta-variable à la place : `(?f↑0 (fromInteger ?t↑0 ?inst↑0 4))`.
En effet, on ne propage pas suffisamment bien l'information
fournie par ton annotation de type.
> Est-ce un problème dans ma définition, ou bien un bug dans Typer ?
Je pense que le mot clé est "residue": c'est pas exactement un bug mais
une partie non encore implémentée. L'unification n'échoue pas, mais
elle est incapable de résoudre le problème posé. On devrait alors
mettre cette équation de côté, poursuivre l'inférence, et ressayer
l'unification plus tard (quand `?f` aura été unifié avec ton annotation
explicite).
Stefan
