Hi. You cannot partially apply a type family, as you try in
type family P (a :: *) (m :: Nat) (l :: Nat) :: * where P a m l = Vec a (Plus l m)
and then
p :: Proxy (P a m) p = Proxy
(The error message for this is not very good.) There are ways to work around this, for example with Richard's singletons library:
import Data.Proxy import Data.Singletons import Data.Singletons.Prelude
gfold :: Proxy (p :: TyFun Nat * -> *) -> (forall l . Proxy l -> a -> p $ l -> p $ S l) -> p $ Z -> Vec a k -> p $ k gfold _ f z Nil = z gfold p f z (x :> (xs :: Vec a l)) = f (Proxy :: Proxy l) x (gfold p f z xs)
data P (a :: *) (m :: Nat) (f :: TyFun Nat *) :: * type instance Apply (P a m) l = Vec a (Plus l m)
gconcat :: forall n m a . Vec a n -> Vec a m -> Vec a (Plus n m) gconcat xs ys = gfold (Proxy :: Proxy (P a m)) (const (:>)) ys xs
Rest as before. Cheers, Andres