https://github.com/goldfirere/singletons/issues/274

SingConstrained.hs

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TemplateHaskellQuotes #-}
module SingConstrained where

import Control.Monad.Extra
import Data.List
import Data.Singletons.Prelude
import Language.Haskell.TH
import Language.Haskell.TH.Datatype
import Language.Haskell.TH.Desugar (tupleNameDegree_maybe, unboxedTupleNameDegree_maybe)

genSingConstrained :: Name -> Q [Dec]
genSingConstrained n = do
  DatatypeInfo { datatypeName    = d_name
               , datatypeVars    = d_vars
               , datatypeVariant = d_variant
               , datatypeCons    = d_cons
               } <- reifyDatatype n
  let noDataFamilies = fail "Data family instances are currently not supported"
  case d_variant of
    DataInstance    -> noDataFamilies
    NewtypeInstance -> noDataFamilies
    Datatype        -> pure ()
    Newtype         -> pure ()
  concatMapM from_con d_cons
  where
    from_con :: ConstructorInfo -> Q [Dec]
    from_con (ConstructorInfo { constructorName    = c_name
                              , constructorVars    = c_vars
                              , constructorContext = c_context
                              , constructorFields  = c_fields
                              , constructorVariant = c_variant
                              }) = do
      unless (null c_vars && null c_context) $
        fail $ unlines
          [ "GADTs or datatypes with existentially quantified"
          , "data constructors currently not supported"
          ]
      let sing_name   = singDataConName c_name
          constr_name = mkName (nameBase sing_name ++ "_")
      (constr_var_names, constr_args)
        <- case c_variant of
             NormalConstructor -> do ns <- replicateM (length c_fields) $ newName "n"
                                     return (ns, PrefixPatSyn ns)
             InfixConstructor  -> do n1 <- newName "n1"
                                     n2 <- newName "n2"
                                     return ([n1, n2], InfixPatSyn n1 n2)
             RecordConstructor fs -> return (fs, RecordPatSyn fs)
      let constr_tvs  = map VarT constr_var_names
          constr_exps = map VarE constr_var_names
          constr_pats = map VarP constr_var_names
          constr_type = ForallT [] [] $
                        ForallT [] (map (AppT (ConT ''SingI)) constr_tvs) $
                        ravel (map (AppT (ConT ''Sing)) constr_tvs) $
                        ConT ''Sing `AppT` foldl' AppT (PromotedT c_name) constr_tvs
          constr_expr = ExplBidir [ Clause constr_pats
                                           (NormalB (foldl' AppE (ConE sing_name) constr_exps))
                                           []
                                  ]
          mk_rhs_pat p = ViewP (VarE 'gen) (TupP [p, ConP 'SingInstance []])
          constr_pat  = ConP sing_name $ map mk_rhs_pat constr_pats

      return [ PatSynSigD constr_name constr_type
             , PatSynD    constr_name constr_args constr_expr constr_pat
             ]

gen :: Sing (a :: k) -> (Sing a, SingInstance a)
gen sing = (sing, singInstance sing)

-----
-- Taken directly from singletons
-----

singDataConName :: Name -> Name
singDataConName nm
  | nm == '[]                                      = 'SNil
  | nm == '(:)                                     = 'SCons
  | Just degree <- tupleNameDegree_maybe nm        = mkTupleDataName degree
  | Just degree <- unboxedTupleNameDegree_maybe nm = mkTupleDataName degree
  | otherwise                                      = prefixConName "S" "%" nm

mkTupleDataName :: Int -> Name
mkTupleDataName n = mkName $ "STuple" ++ (show n)

-- Put an uppercase prefix on a constructor name. Takes two prefixes:
-- one for identifiers and one for symbols.
--
-- This is different from 'prefixName' in that infix constructor names always
-- start with a colon, so we must insert the prefix after the colon in order
-- for the new name to be syntactically valid.
prefixConName :: String -> String -> Name -> Name
prefixConName pre tyPre n = case (nameBase n) of
    (':' : rest) -> mkName (':' : tyPre ++ rest)
    alpha -> mkName (pre ++ alpha)

ravel :: [Type] -> Type -> Type
ravel []    res = res
ravel (h:t) res = AppT (AppT ArrowT h) (ravel t res)

SingConstrainedExample.hs

{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -ddump-splices #-}
module SingConstrainedExample where

import Data.Singletons.TH
import SingConstrained

data N = Z | S N

$(return [])

$(genSingletons [''N])
$(genSingConstrained ''N)