Thinking about http://mazzo.li/posts/customizable-data-types.html

ConfData.hs

{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE GADTs                #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE PolyKinds            #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ConstraintKinds      #-}

import Data.Constraint
import Data.Function

data Var'
data Sum'
data Zro'

type family Apply (f :: *) (ix :: *) :: * where
  Apply Var' ix = Var ix
  Apply Sum' ix = Sum ix
  Apply Zro' ix = Zro ix

type AllFamilies = Var' ': Sum' ': Zro' ': '[]

data Expr ix where
  Var ::                Var ix                        -> Expr ix
  Sum :: Sum ix ~ () => [Expr ix]                     -> Expr ix
  Add ::                Expr ix -> Expr ix            -> Expr ix
  Zro :: Zro ix ~ () =>                                  Expr ix

type family AllEq (ps :: [*]) (x :: *) (y :: *) :: Constraint where
  AllEq '[]       x y = ()
  AllEq (p ': ps) x y = (Apply p x ~ Apply p y, AllEq ps x y)

type family (:-:) (xs :: [k]) (x :: k) :: [k] where
  '[]       :-: x = '[]
  (x ': xs) :-: x = xs
  (y ': xs) :-: x = y ': (xs :-: x)

data Stage1 -- Right after parsing
data Stage2 -- After renaming
data Stage3 -- After desugaring

type family Var ix :: * where
  Var Stage1 = String
  Var Stage2 = Int
  Var Stage3 = Int

type True  = ()
type False = Int

type family Sum ix :: * where
  Sum Stage1 = True
  Sum Stage2 = True
  Sum Stage3 = False

type family Zro ix :: * where
  Zro Stage1 = True
  Zro Stage2 = True
  Zro Stage3 = True

type family Diff (xs :: [k]) (ys :: [k]) :: [k] where
  Diff xs '[]       = xs
  Diff xs (y ': ys) = Diff (xs :-: y) ys

type Change  x  ix ix' = AllEq (AllFamilies :-: x) ix ix'
type Changes xs ix ix' = AllEq (Diff AllFamilies xs) ix ix'

inlineSum :: Sum ix' ~ False
          => Zro ix' ~ True
          => Change Sum' ix ix'
          => Expr ix -> Expr ix'
inlineSum (Var v)   = Var v
inlineSum (Sum vs)  = foldr Add Zro $ fmap inlineSum vs
inlineSum (Add x y) = (Add `on` inlineSum) x y
inlineSum Zro       = Zro