как преобразовать строки в синтаксическое дерево с помощью GADT

Я читал введение в GADT здесь, и мне понравилась идея ограничить программиста созданием синтаксического дерева только правильного типа, и я поместил эту идею в свой простой интерпретатор лямбда-исчисления. , но позже я понял, что не могу разобрать строку в это синтаксическое дерево, потому что одна функция синтаксического анализа должна возвращать разные типы синтаксического дерева в зависимости от ввода. Вот пример:

{-# LANGUAGE GADTs #-}
data Ident
data Lambda
data Application

data Expr a where
    Ident :: String -> Expr Ident
    Lambda :: Expr Ident -> Expr a -> Expr Lambda
    Application :: Expr a -> Expr a -> Expr Application

Прежде чем использовать GADT, я использовал это:

data Expr = Lambda Expr Expr
          | Ident String
          | Application Expr Expr

GADT дают здесь большое преимущество, потому что теперь я не могу создавать недопустимые синтаксические деревья, такие как Lambda (Application ..) .. .

Но с помощью GADT я не мог проанализировать строку и создать дерево разбора. Вот синтаксический анализатор для выражений Lambda, Ident и Application:

ident :: Parser (Expr Ident)
ident = ...

lambda :: Parser (Expr Lambda)
lambda = ...

application :: Parser (Expr Application)
application = ...

Теперь проблема в следующем:

expr = choice [ident, application, lambda]

Очевидно, что это не работает, так как каждый синтаксический анализатор возвращает разные типы.

Итак, есть ли способ проанализировать строку и создать синтаксическое дерево с помощью GADT?