No title

1
2
3
4
5
6
7
8
9
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeOperators #-}

data Rec :: (a -> *) -> (a -> *) -> [a] -> * where
  RNil :: Rec f g '[]
  (:&) :: (f a -> g a) -> Rec f g as -> Rec f g (a ': as)