Bonjour,
Decidable est définit comme suit
Decidable = typecons (Decidable (prop : Type_ ?ℓ)) (true (p ::: prop)) (false (p ::: Not prop));
Ce qui est élaboré en
Decidable' = lambda (ℓ : TypeLevel) ≡> typecons (Decidable (prop : Type_ ?ℓ)) …
C'est problématique parce que Typer n'élabore pas les lambda dans les datacons. Le code suivant est rejeté parce que Decidable n'est pas un type.
yes = datacons Decidable true;
Je propose le changement [0], qui instancie les arguments implicites dans les datacons, mais plus j'y pense, plus je me rends compte que ce n'est pas la bonne solution à ce problème. (Je pense quand même que ce changement est correct, mais pour d'autres circonstances.) Decidable ne devrait-il pas être définit comme
Decidable'' = typecons (Decidable (ℓ ::: TypeLevel) (t : Type_ ℓ)) …
Mes deux questions sont: - Quelle est la différence sémantique entre les deux formulations? - Si la première est incorrecte, est-ce que l'élaboration des typecons devrait être changé pour que l'élaboration du code le plus naturel donne "la bonne chose".
Bon typage Simon
[0]: https://gitlab.com/monnier/typer/-/commit/da12222203e536730456fefc0eaa2f2464...