How about this one for variadic structures? [0] data Rec (f :: k -> *) (ts :: [k...

How about this one for variadic structures? [0]

    data Rec (f :: k -> *) (ts :: [k]) where
      RNil :: Rec f '[]
      (:&) :: f t -> Rec f ts -> Rec f (t ': ts)

    infixr 9 :&

    data ElField f where
      Field :: KnownSymbol s => t -> ElField '(s, t)

    x :: Rec ElField ['("foo", Int), '("bar", String)]
    x = Field 3 :& Field "bar" :& RNil

It's an embedding of (variadic) typed records.

Anyway, I don't actually use GADT-driven embedded ASTs myself. They're just a pretty clear example.

[0] This is Jon Sterling's `vinyl` package in Haskell