{-# LANGUAGE GADTs
           , TypeFamilies
           , TypeOperators
           , KindSignatures
           , MultiParamTypeClasses
           , EmptyDataDecls
           , FlexibleInstances
           #-}

module ListRep where

import Generics.MultiRec.Elems.One

data ListU :: (* -> *) -> * -> * -> * where
    List :: ListU (Elems a) [a] Zero

type instance PF ListU = (U :+: I (Elem Zero) :*: I (Rec Zero)) :>: Zero

instance Fam ListU (Elems a) where
    from List [] = Tag (L U)
    from List (x : xs) = Tag (R (I (CL (E0 x)) :*: I (CR (R0 List xs))))
    to List (Tag (L U)) = []
    to List (Tag (R (I (CL (E0 x)) :*: I (CR (R0 List xs))))) = x : xs

instance El (Proof (ListU (Elems a))) Zero where
  proof = Proof List

instance EqS (Proof (ListU (Elems a))) where
  eqS (Proof List) (Proof List) = Just Refl

instance EqS2 (ListU (Elems a)) where
  eqS2 List List = Just (Refl, Refl)