Bonjour, J'essaie d'ajouter une extension à Typer pour séparer l'allocation de l’initialisation. Une primitive importante pour ça est Heap_unsafe-store-header : (addr : Int) -> ??? -> ##Heap Unit; où addr est l'adresse où le bloc a été alloué et ##Heap une sorte de ST pour le tas. Le problème est le deuxième argument, qui doit désigner un constructeur de valeur. En ce moment, on a par exemple cons : ?α -> List ?α -> List ?α; qui est impossible de distinguer d'une fonction par son type. J'aimerais donc introduire un nouveau type primitif, Datacons : (ℓ : TypeLevel) ≡> (t : Type_ ℓ) -> (arr : Type_ ℓ) -> Type_ ℓ; On aurait donc nil : (ℓ : TypeLevel) ≡> (α : Type ℓ) -> Datacons List (List α); nil = datacons List nil; cons : (ℓ : TypeLevel) ≡> (α : Type ℓ) -> Datacons List (α -> List α -> List α); cons = datacons List cons; Et la primitive présentée plus haut aurait le type Heap_unsafe-store-header : (addr : Int) -> Datacons ?τ ?τ-arr -> ##Heap Unit; Par contre, je vois deux façon d'ajouter ça à Typer. La première est de ne pas toucher à datacons et d'introduire une nouvelle forme spéciale pour avoir le Datacons lui-même plutôt que la fonction. La seconde est de changer datacons pour retourner un Datacons. Ça implique par contre qu'il faut ajouter à l'élaboration une coercition automatique du Datacons vers une fonction. Qu'est-ce que vous en pensez? Simon