{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE GADTs                 #-}

module Generics.MultiRec.Any where

import Generics.MultiRec

data Any phi where
  Any :: phi ix -> ix -> Any phi

-- | Unify an 'Any' with an @a@.
matchAny :: forall phi ix. EqS phi => phi ix -> Any phi -> Maybe ix
matchAny p (Any w x) = match' w x p where
  match' :: EqS s => s b -> b -> s a -> Maybe a
  match' w x w' = case eqS w w' of
    Nothing -> Nothing
    Just Refl -> Just x