Test.hs

{-# LANGUAGE DataKinds, RankNTypes, ScopedTypeVariables, TypeFamilies, TypeOperators #-}
{-# OPTIONS_GHC -fconstraint-solver-iterations=10
                -fplugin TypeLevel.Rewrite
                -fplugin-opt=TypeLevel.Rewrite:TypeLevel.Append.RightIdentity
                -fplugin-opt=TypeLevel.Rewrite:TypeLevel.Append.RightAssociative #-}
module TypeLevel.Append.Test where

import TypeLevel.Append


ex1a :: (((as ++ '[]) ++ (bs ++ '[])) ~ (as ++ bs) => r)
     -> proxy as
     -> proxy bs
     -> r
ex1a r _ _ = r

ex1b :: ((as ++ bs) ~ ((as ++ '[]) ++ (bs ++ '[])) => r)
     -> proxy as
     -> proxy bs
     -> r
ex1b r _ _ = r

ex1c :: ((as ++ (bs ++ cs)) ~ (((as ++ '[]) ++ (bs ++ '[])) ++ (cs ++ '[])) => r)
     -> proxy as
     -> proxy bs
     -> proxy cs
     -> r
ex1c r _ _ _ = r

ex1d :: (proxy (as ++ bs) ~ proxy ((as ++ '[]) ++ (bs ++ '[])) => r)
     -> proxy as
     -> proxy bs
     -> r
ex1d r _ _ = r

ex1e :: proxy as
     -> proxy bs
     -> proxy (as ++ bs)
     -> proxy ((as ++ '[]) ++ (bs ++ '[]))
ex1e _ _ r = r


ex2a :: (((as ++ bs) ++ cs) ~ (as ++ (bs ++ cs)) => r)
     -> proxy as
     -> proxy bs
     -> proxy cs
     -> r
ex2a r _ _ _ = r

ex2b :: ((as ++ (bs ++ cs)) ~ ((as ++ bs) ++ cs) => r)
     -> proxy as
     -> proxy bs
     -> proxy cs
     -> r
ex2b r _ _ _ = r

ex2c :: ((as ++ (bs ++ (cs ++ ds))) ~ (((as ++ bs) ++ cs) ++ ds) => r)
     -> proxy as
     -> proxy bs
     -> proxy cs
     -> proxy ds
     -> r
ex2c r _ _ _ _ = r

ex2d :: (proxy (as ++ (bs ++ cs)) ~ proxy ((as ++ bs) ++ cs) => r)
     -> proxy as
     -> proxy bs
     -> proxy cs
     -> r
ex2d r _ _ _ = r

ex2e :: proxy as
     -> proxy bs
     -> proxy cs
     -> proxy (as ++ (bs ++ cs))
     -> proxy ((as ++ bs) ++ cs)
ex2e _ _ _ r = r

ex2f :: forall proxy xs as bs cs r. xs ~ ((as ++ bs) ++ cs)
     => (xs ~ (as ++ (bs ++ cs)) => r)
     -> proxy as
     -> proxy bs
     -> proxy cs
     -> r
ex2f r _ _ _ = r

ex2g :: (as ++ (bs ++ cs)) ~ cs
     => (((as ++ bs) ++ cs) ~ cs => r)
     -> proxy as
     -> proxy bs
     -> proxy cs
     -> r
ex2g r _ _ _ = r

ex2h :: forall proxy xs ys as bs cs r
      . ( ys ~ xs
        , xs ~ ((as ++ bs) ++ cs)
        )
     => (xs ~ (as ++ (bs ++ cs)) => r)
     -> proxy as
     -> proxy bs
     -> proxy cs
     -> r
ex2h r _ _ _ = r