{-# LANGUAGE GADTs #-}
{-# LANGUAGE Rank2Types #-}

-- | Pattern functors polymorphic in their top-level index type @ix@.
module Any (Any(..), mkAny, unwrapAnyF, AnyF(..), mkAnyF) where

import ShowFam
import Generics.MultiRec

-- | A value of some type in data family @s@, together with its witness.
data Any s where
  Any :: Ix s ix => s ix -> ix -> Any s

instance ShowFam s => Show (Any s) where
  show = showAny

showAny :: ShowFam s => Any s -> String
showAny (Any w x) = showFam w x

-- | Helper constructor.
mkAny :: Ix s ix => ix -> Any s
mkAny = Any index

-- | A value of some type in data family @s@ wrapped in an @f@, together with its witness.
data AnyF s f where
  AnyF :: (Ix s ix) => s ix -> f ix -> AnyF s f

-- | Helper constructor.
mkAnyF :: Ix s ix => r ix -> AnyF s r
mkAnyF = AnyF index

-- | Removes the value from its functor @f@.
unwrapAnyF :: (forall ix. Ix s ix => f ix -> ix) -> AnyF s f -> Any s
unwrapAnyF g (AnyF ix rix) = Any ix (g rix)