Un cas que gère le tagless mais pas les GADT

Ton approche m'a faite rejouer avec les GADTs et les l'approche tagless finale et je viens enfin de résoudre un problème vieux comme le monde pour moi.

Je veux representer des expressions, genre "1 + 2 * x", qui peuvent contenir une "variable". Cela nous donne un ADT assez simple (Je le fais en Haskell, ce sera plus lisible que si je le faisais en OCaml, principalement parce que le Haskell est plus lisible, mais surtout parce que je ne maîtrise pas du tout l'écriture du OCaml et donc je ferais des erreurs ;):

data Expr = Add Expr Expr | Lit Int | Variable

L'expression "1 + x" précédente étant représentée par Add (Lit 1) Variable.

Je veux pouvoir évaluer mon expression :

eval :: Expr -> Int
eval (Lit i) = i
eval (Add e e') = eval e + eval e'
eval Variable = error "cannot evaluate a variable"

Suivez mon regard, j'aimerais dégager ce cas particulier. On va passer aux GADT pour représenter tout cela :

data Expr useVariable where
 Add :: Expr aUseVariable -> Expr bUseVariable -> Expr (FOr aUseVariable bUseVariable)
 Lit :: Int -> Expr SansVariable
 Variable :: Expr AvecVariable

Derrière se cache une fonction au niveau du type FOr :

type family FOr a b where
 FOr AvecVariable _ = AvecVariable
 For _ AvecVariable = AvecVariable
 For _ _ = SansVariable

Et ça cela marche, le type de Variable est bien Expr AvecVariable, le type de Add (Lit 1) (Lit 2) est bien Expr SansVariable et le type de Add Variable (Lit 4) est bien Expr AvecVariable.

Revenons à notre fonction eval :

eval :: Expr SansVariable -> Int
eval (Lit i) = i
eval (Add e e') = eval e + eval e'

Le type marque clairement que on ne peut évaluer qu'une expression SansVariable. Et le cas Variable n'est plus à écrire puisque il n'existe plus. Cependant cela ne marche pas. Pourquoi ?

Parce que Haskell (GHC 8.0) n'est pas capable de prouver que si (Add e e') est Expr SansVariable, alors e et e' le sont aussi. La preuve est triviale pour nous en regardant la fonction FOr, mais pas pour GHC.

Est-ce que OCaml sait faire ça ?

Comment feriez vous sinon ?

Note: la méthode TagLess final marche bien ici puisqu'il suffit de ne pas écrire d’implémentation d'eval pour Variable et le compilateur refusera de compiler un appel à eval sur un type qui contient des Variable. C'est cool ;)