{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
module Data.GADT.HasFinitary where

import Data.Finitary
import GHC.TypeNats.Extra (SNat(SNat))
import GHC.Generics
import Data.Type.Equality ((:~:) (..))

class HasFinitary tag where
  withFinitary :: tag n -> (Finitary n => r) -> r

toSNat :: HasFinitary tag => tag a -> SNat (Cardinality a)
toSNat :: forall (tag :: * -> *) a.
HasFinitary tag =>
tag a -> SNat (Cardinality a)
toSNat tag a
ta = tag a
-> (Finitary a => SNat (Cardinality a)) -> SNat (Cardinality a)
forall n r. tag n -> (Finitary n => r) -> r
forall (tag :: * -> *) n r.
HasFinitary tag =>
tag n -> (Finitary n => r) -> r
withFinitary tag a
ta SNat (Cardinality a)
Finitary a => SNat (Cardinality a)
forall (n :: Nat). KnownNat n => SNat n
SNat

toInhabitants :: HasFinitary tag => tag a -> [a]
toInhabitants :: forall (tag :: * -> *) a. HasFinitary tag => tag a -> [a]
toInhabitants tag a
ta = tag a -> (Finitary a => [a]) -> [a]
forall n r. tag n -> (Finitary n => r) -> r
forall (tag :: * -> *) n r.
HasFinitary tag =>
tag n -> (Finitary n => r) -> r
withFinitary tag a
ta [a]
Finitary a => [a]
forall a. Finitary a => [a]
inhabitants

instance Finitary n => HasFinitary ((:~:) n) where
  withFinitary :: forall n r. (n :~: n) -> (Finitary n => r) -> r
withFinitary n :~: n
Refl Finitary n => r
body = r
Finitary n => r
body

instance (HasFinitary t1, HasFinitary t2) => HasFinitary ((:+:) t1 t2) where
  withFinitary :: forall n r. (:+:) t1 t2 n -> (Finitary n => r) -> r
withFinitary (:+:) t1 t2 n
tag Finitary n => r
body = case (:+:) t1 t2 n
tag of
    L1 t1 n
t1 -> t1 n -> (Finitary n => r) -> r
forall n r. t1 n -> (Finitary n => r) -> r
forall (tag :: * -> *) n r.
HasFinitary tag =>
tag n -> (Finitary n => r) -> r
withFinitary t1 n
t1 r
Finitary n => r
body
    R1 t2 n
t2 -> t2 n -> (Finitary n => r) -> r
forall n r. t2 n -> (Finitary n => r) -> r
forall (tag :: * -> *) n r.
HasFinitary tag =>
tag n -> (Finitary n => r) -> r
withFinitary t2 n
t2 r
Finitary n => r
body