{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Excluding where

import Control.DeepSeq
import Data.Kind
import GHC.Generics

-----
-- singletons machinery
-----

data family Sing :: k -> Type

class SingI (a :: k) where
  sing :: Sing a

data instance Sing :: Bool -> Type where
  SFalse :: Sing False
  STrue  :: Sing True

instance SingI False where
  sing = SFalse

instance SingI True where
  sing = STrue

-----
-- Type-level voodoo
-----

type family Unless (a :: Bool) (b :: Constraint) :: Constraint where
  Unless True  _ = ()
  Unless False b = b

type family Elem (x :: a) (xs :: [a]) :: Bool where
  Elem _ '[]    = False
  Elem x (x:_)  = True
  Elem x (y:xs) = Elem x xs

newtype Excluding :: [Type] -> Type -> Type where
  Excluding :: a -> Excluding excluded a

instance (Generic a, GNFData excluded (Rep a)) => NFData (Excluding excluded a) where
  rnf (Excluding x) = grnf @excluded $ from x

-----
-- Generics machinery
-----

class GNFData (excluded :: [Type]) f where
  grnf :: f a -> ()

instance GNFData e V1 where
  grnf x = case x of {}

instance GNFData e U1 where
  grnf U1 = ()

-- The important one!
instance ( Unless (Elem a excluded) (NFData a)
         , SingI (Elem a excluded) )
    => GNFData excluded (K1 i a) where
  grnf (K1 x) = case sing @Bool @(Elem a excluded) of
                  STrue  -> ()
                  SFalse -> rnf x
  {-# INLINEABLE grnf #-}

instance GNFData e a => GNFData e (M1 i c a) where
  grnf = grnf @e . unM1
  {-# INLINEABLE grnf #-}

instance (GNFData e a, GNFData e b) => GNFData e (a :*: b) where
  grnf (x :*: y) = grnf @e x `seq` grnf @e y
  {-# INLINEABLE grnf #-}

instance (GNFData e a, GNFData e b) => GNFData e (a :+: b) where
  grnf (L1 x) = grnf @e x
  grnf (R1 x) = grnf @e x
  {-# INLINEABLE grnf #-}

-----
-- Example
-----

data MyBigType
  = MyBigType {
      f1 :: Int
    , f2 :: Double
    , f3 :: (Int -> Char)
    , f4 :: Char
    } deriving stock Generic
      deriving NFData via (Excluding '[Int -> Char] MyBigType)

main :: IO ()
main = do
  let mbt = MyBigType 1 2.0 undefined '3'
  mbt `deepseq` putStrLn "Done"