MapDict.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module MapDict where

import Generics.SOP
import Generics.SOP.Dict

type family Map (f :: k -> l) (xs :: [k]) :: [l] where
  Map _f '[]       = '[]
  Map  f (x ': xs) = f x ': Map f xs

mapDict :: forall f xs . Proxy f -> SList xs -> Dict SListI (Map f xs)
mapDict pf SNil  = Dict
mapDict pf SCons = goCons (sList :: SList xs)
  where
    goCons :: forall y ys . SList (y ': ys) -> Dict SListI (Map f (y ': ys))
    goCons SCons = withDict (mapDict pf (sList :: SList ys)) Dict