Concat.hs

{-# LANGUAGE TemplateHaskell, FlexibleContexts, FlexibleInstances, GADTs, DataKinds,
                     TypeInType, KindSignatures, InstanceSigs, TypeOperators,
                     ConstraintKinds, RankNTypes, ScopedTypeVariables, TypeFamilies,
                     UndecidableInstances, MultiParamTypeClasses, TypeApplications, PartialTypeSignatures #-}

$(singletons [d|
  data UNat = Zero | Succ UNat
    deriving (Eq)

  |])

class Concats (d:: UNat) (xs::[Nat]) (ys::[Nat]) where
  type ConcatShape d xs ys :: [Nat]

instance (xs ~ ys) => Concats 'Zero (x:xs) (y:ys) where
  type ConcatShape Zero (x:xs) (y:_) = (x + y : xs)

instance (x ~ y) => Concats ('Succ n) (x:xs) (y:ys) where
  type ConcatShape (Succ n) (x:xs) (_:ys) = x : ConcatShape n xs ys