content: {-# LANGUAGE DataKinds              #-}
  {-# LANGUAGE GADTs                  #-}
  {-# LANGUAGE TypeFamilyDependencies #-}
  {-# LANGUAGE TypeOperators          #-}
  {-# LANGUAGE ViewPatterns           #-}
  {-# LANGUAGE UndecidableInstances   #-}
  
  module T16512a where
  
  import Data.Kind
    ( Type )
  
  -- HOAS representation
  data AST (a :: Type) :: Type where
    (:$) :: AST ( a -> b ) -> AST a -> AST b
    -- Lam :: ( AST a -> AST b ) -> AST ( a -> b )
    -- PrimOp :: PrimOp op a => AST a
    -- ...
  
  data ASTs (as :: [Type]) :: Type where
    NilASTs :: ASTs '[]
    ConsAST :: AST a -> ASTs as -> ASTs (a ': as)
  
  type family ListVariadic (as :: [Type]) (b :: Type) = (r :: Type) | r -> as b where
    ListVariadic (a ': as) b = a -> ListVariadic as b
    -- ListVariadic '[] ()     = ()
    -- ListVariadic '[] Bool   = Bool
    -- ListVariadic '[] Word   = Word
    -- ListVariadic '[] Int    = Int
    -- ListVariadic '[] Float  = Float
    -- ListVariadic '[] Double = Double
    -- ...
  
  data AnApplication b where
    AnApplication :: AST (ListVariadic as b) -> ASTs as -> AnApplication b
  
  unapply :: AST b -> AnApplication b
  unapply (f :$ a)
    = case unapply f of
          AnApplication g as ->
            AnApplication g (a `ConsAST` as)
  -- no other cases with this simplified AST
  