[ 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
Afficher les réponses par date