CConst invariant (https://byorgey.wordpress.com/2023/07/13/compiling-to-intrinsically-typed-combinators#compiling-type-indexed-combinators-to-haskell)

TypedCombinators.hs

type family IsFun a where
  IsFun (_ -> _) = 'True
  IsFun _ = 'False

type NotFun a = IsFun a ~ 'False

data CTerm a where
  CFun :: (CTerm a -> CTerm b) -> CTerm (a -> b)
  CConst :: NotFun a => a -> CTerm a

instance Applicable CTerm where
  ($$) :: CTerm (a -> b) -> CTerm a -> CTerm b
  CFun f $$ x = f x
  
-- Couldn't match type ‘'True’ with ‘'False’ arising from a use of ‘CConst’
-- bad = CConst id

-- The TypeError type family can be used here for a better error message.


type family NoFunParams a where
  NoFunParams (a -> b) = (NotFun a, NoFunParams b)
  NoFunParams _ = ()

runCTerm :: NoFunParams a => CTerm a -> a