...

...

Pour `x = cons 1 nil;`, son type de retour est :

---

**************** REPL --> eval_interactive --> lexprs ****************

---

x[0] --------------------------------------------------->>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> --------------------------------------------------->>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> (a : (##Type_ ##TypeLevel.z)) ≡> (inst : (let FromInteger : (α : Type[247]) -> Type[248]; FromInteger = typecons (FromInteger (α : Type[248])) (mkFromInteger (Integer[255] -> α[1])) in typecons (FromInteger (α : Type[248])) (mkFromInteger (Integer[255] -> α[1])) a[0])) => (List[158] ##TypeLevel.z a[1])

Vous pouvez m'expliquer la ligne suivante?

J'ai pas vu de "ligne suivante", donc je vais expliquer la ligne précédente à la place:

(a : (##Type_ ##TypeLevel.z))
≡> (inst : (let FromInteger : (α : Type[247]) -> Type[248];
                FromInteger = typecons (FromInteger (α : Type[248]))
                                       (mkFromInteger (Integer[255] -> α[1]))
            in (typecons (FromInteger (α : Type[248]))
                         (mkFromInteger (Integer[255] -> α[1])))
                   a[0]))
=> (List[158] ##TypeLevel.z a[1])

(j'ai juste rajouté des retour à la ligne et des espaces, plus 1(!) paire de parenthèses (celle qui s'ouvre juste après le `in`) qui manquait).

Donc, en gros:

(a : Type) ≡> (inst : FromInteger a) => List a

Ce qui signifie une liste de type `a` pour n'importe quel type `a` pour autant que c'est un type dans la type-classe `FromInteger`.

Est-ce normalement d'avoir une liste de type `a` pour n'importe quel type `a` ?

Vu que j'ai défini une liste d'entier. Le type de la liste doit être de type `Int ou ##Int` non ?

En fait, tu n'as pas défini une liste d'entiers. Tu a définis une liste qui contient un élément, cet élément étant représenté dans le code source par le litéral "1".

Le litéral "1" peut être un `Int`, ou un `Integer` ou un `Float`, ou potentiellement plein d'autres choses. Il a type:

(a : Type) ≡> (inst : FromInteger a) => a

Si tu veux une liste de `int`, alors il faut le spécifier explicitement, e.g.:

cons (1 : Int) nil

ou

(cons 1 nil) : List Int

Ce problème apparaît rarement dans un vrai programme, parce que ce `cons 1 nil` va être utilisé quelque part et ce "quelque part" va finir par spécifier quel genre de nombres on veut, mais dans la "repl" ce n'est pas le cas.

Il faudrait qu'on ajoute à la "repl" une règle qui prend un choix par défaut (e.g. ici on pourrait utiliser `Integer`) pour éviter ces situations, qui sont techniquement pas incorrectes mais n'en restent pas moins indésirables.

Stefan