DefunHigherDataCons.hs

{-# LANGUAGE PolyKinds, DataKinds, TypeApplications, TypeOperators, KindSignatures, GADTs, TypeFamilies, ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
-- ^ more extensions might be needed to do what I want to do, idk

-- Defunctionalized higher-order data constructors--are they possible?
module DefunHigherDataCons where

import Data.Kind
import Data.Singletons.TH

data Endo :: Type -> Type where
  -- A higher-order data constructor:
  MkEndo :: (a -> a) -> Endo a
  -- ^ Because of -XDataKinds, this also creates the /type constructor/ `'MkEndo :: (a -> a) -> Endo a`.
  -- But when doing type-level programming, a more useful type constructor would be `MkEndoSym1 :: (a ~> a) -> Endo a`.

-- Wrapping the above in `$(singletons [d| ... |])` causes errors, as do both of these:
-- $(genSingletons [''Endo])
-- $(genDefunSymbols [''Endo])

-- Which makes sense, since actually writing it out seems impossible. Is it?
type family MkEndoSym1 (f :: a ~> a) :: a where
  MkEndoSym1 f = ???