Index: /sizechecking/Examples.hs
===================================================================
--- /sizechecking/Examples.hs	(revision 9)
+++ /sizechecking/Examples.hs	(revision 10)
@@ -210,4 +210,13 @@
 comp :: (SizedExp se)  => Size se ( (b->c) -> (a->b) -> a->c )
 comp = bind comps $ \f g x -> f `app` (g `app` x)
+
+test1s = Abs 2 $ AAbs 19 6 $ (Var 2) `App` (List (Var 19) (Var 6))
+test1 :: (SizedExp se)  => Size se (([a] -> [b]) -> [a] -> [b])
+test1 = bind test1s $ \f l -> match (f `app` l) nil (\x xs -> f `app` l)
+
+
+test2s = Abs 2 $ AAbs 18 5  $ appends `App` (Var 2 `App` (List (Var 18) (Var 5))) `App` (List (Var 18) (Var 5))
+test2 :: (SizedExp se)  => Size se (([a] -> [a]) -> [a] -> [a])
+test2 = bind test2s $ \f l -> append `app` (f `app` l) `app` l
 
 data TestCase = forall a . TestCase P.String (forall se. SizedExp se => Size se a)
Index: zechecking/L.hs
===================================================================
--- /sizechecking/L.hs	(revision 9)
+++ 	(revision )
@@ -1,203 +1,0 @@
-{-# Language GADTs, FlexibleInstances, FlexibleContexts, MultiParamTypeClasses, FunctionalDependencies, ScopedTypeVariables, TypeFamilies, NoMonomorphismRestriction #-}
-
-import Data.Char(ord, chr)
-import Control.Monad.State
---import Data.Supply
-
-data OpName = PLUS | MINUS | MUL
-data Bottom = Bottom
-  deriving Show
-
-{- Lambda calculus without free variables -}
-type Arr repr a b = repr a -> repr b
---type family Arr (repr :: * -> *) (a :: *) (b :: *) :: *
-
-class Lambda l where
-    labs    :: (l a -> l b) -> l (Arr l a b)
-    app     :: l (Arr l a b) -> l a -> l b
-    lit     :: Int -> l Int
-    op      :: l Int -> OpName -> l Int -> l Int
-
-class SizeExp l where
-    type List l :: * -> *
-    list    :: l Int -> l (Arr l Int b) -> l (List l b)
-    aabs    :: (l Int -> l (Arr l Int a) -> l b) -> l (Arr l (List l a) b)
-    shift   :: l (Arr l Int a) -> l Int -> l (Arr l Int a) -> l (Arr l Int a)
-    undef   :: l Bottom
-    unsized :: l ()
-
-instance Lambda l => Num (l Int) where
-    fromInteger = lit . fromIntegral
-    lhs + rhs   = op lhs PLUS rhs
-    lhs - rhs   = op lhs MINUS rhs
-    lhs * rhs   = op lhs MUL rhs
-    abs = error "abs is not implemented"
-    signum = error "signum is not implemented"
-
-{- Printing -}
-newtype LPrint a = LPrint { unPrint :: Int -> Int -> ShowS }
-
-instance Lambda LPrint where
-  lit x      = LPrint $ \_ -> return $ shows x
-  op m opc n = LPrint $ \p -> do
-    let (prec, lprec, rprec, c) = getPrec opc
-    l1 <- (unPrint m lprec)
-    l2 <- (unPrint n rprec)
-    return $ showParen (p>prec) $  l1 . showChar c . l2
-  app f v    = LPrint $ \p -> do
-    l1 <- unPrint f 6
-    l2 <- unPrint v 7
-    return $ showParen (p>6) $ l1 . showChar ' ' . l2
-  labs e      = LPrint $ \p v -> let
-    var = LPrint $ \_ -> return $ showVar v
-    l = unPrint (e var) 0 $ succ v
-    in showParen (p>0) $ showChar 'λ' . showVar v . showChar '.' . l
-
-instance SizeExp LPrint where
-  type List LPrint = []
-  aabs f   = LPrint $ \p v -> let 
-    v2 = succ v
-    var1 = LPrint $ \_ _ -> showVar v
-    var2 = LPrint $ \_ _ -> showVar v2
-    l = unPrint (f var1 var2) 0 (v+2)
-    in showParen (p>0) $ showChar 'Λ' . showVar v . showChar ',' . showVar v2 . showChar '.' . l
-  list s f = LPrint $ \p -> do
-    l1 <- unPrint s 9
-    l2 <- unPrint f 9
-    return $ showParen (p>0) $ showString "List " . l1 . showChar ' ' . l2
-  shift e1 s e2 = LPrint $ \p -> do
-    l1 <- unPrint e1 2
-    l2 <- unPrint s 2
-    l3 <- unPrint e2 2
-    return $ showParen (p>0) $ showString "Shift " . l1 .  showChar ' ' . l2 . showChar ' ' . l3
-  undef = LPrint $ \_ -> return $ showChar '┮'
-  unsized = LPrint $ \_ -> return $ showChar 'U'
-
-view :: LPrint a -> LPrint a
-view = id
-instance Show (LPrint a) where
-    showsPrec _ e = unPrint e 0 0
-
-showVar x = if x>28 
-    then showVar (x `div` 29) . showChar (chr $ ord 'a' + (x `mod` 29))
-    else showChar $ chr $ ord 'a' + x
-
-getPrec :: OpName -> (Int,Int,Int,Char)
-getPrec PLUS = (4,4,5,'+')
-getPrec MINUS = (4,4,5,'-')
-getPrec MUL = (5,5,6,'*')
-
-getVar :: State Int Int
-getVar = do { x <- get; put (x+1); return x }
-
-x = aabs (\s _ -> s) `app` list (lit 0) (labs $ \_ -> undef)
-y = list 0 $ labs $ \_ -> undef
-z = (labs $ \s -> s+1) `app` (lit 1+2)
-conss = labs $ \x -> aabs $ \ys yf -> list (ys + 1) $ shift yf ys (labs $ \_ -> x)
-concats = aabs $ \xs xf -> (aabs $ \ys yf -> list (xs+ys) $ shift xf xs yf)
-maps = labs $ \x -> aabs $ \ys yf -> list ys ( x `app` yf )
-l0 = list (lit 0) (labs $ \_ -> unsized)
-l1 = list (lit 1) (labs $ \_ -> unsized)
-l2 = list (lit 2) (labs $ \_ -> unsized)
-l00 = list (lit 0) (labs $ \_ -> list (lit 0) (labs $ \_ -> unsized))
-l10 = list (lit 1) (labs $ \_ -> list (lit 0) (labs $ \_ -> unsized))
-l01 = list (lit 0) (labs $ \_ -> list (lit 1) (labs $ \_ -> unsized))
-l11 = list (lit 1) (labs $ \_ -> list (lit 1) (labs $ \_ -> unsized))
-l12 = list (lit 1) (labs $ \_ -> list (lit 2) (labs $ \_ -> unsized))
-
-{- Evaluating -}
-newtype R a = R { unR :: a }
-instance Lambda R where
-  labs f      = R $ f 
-  app e1 e2   = (unR e1) e2
-  lit i       = R i
-  op e1 op e2 = let opm = case op of
-                                  PLUS  -> (+)
-                                  MINUS -> (-)
-                                  MUL   -> (*)
-                in R $ opm (unR e1) (unR e2)
-
-newtype RList a = RList { unList :: (Int, Int -> a)  }
-instance (Show a) => Show (RList a) where
-  show (RList (s,f)) = show (map f [0..s-1])
-
-instance SizeExp R where
-  type List R = RList
-  undef       = R $ Bottom
-  unsized     = R $ ()
-  list s f    = R $ RList (unR s, unR . (unR f) . R )
-  aabs e = R $ ( \(RList (s,f)) -> (e (R s) (R (R . f . unR))) ) . unR
-  shift a s c = R $ \i -> if (unR i)<(unR s) then unR a i else unR c i
-
--- Type level int to count arity
-data Zero
-data Succ a
-
-data Exp a where
-    Lit :: Int -> Exp Zero
-    Op  :: Exp Zero -> OpName -> Exp Zero -> Exp Zero
-    App :: Exp (Succ a) -> Exp Zero -> Exp a
-    Var :: Int -> Exp a
-
-instance Show (Exp a) where
-    showsPrec _ (Lit a)         = shows a
-    showsPrec p (Op lhs op rhs) =
-        let (prec, lprec, rprec, c) = getPrec op
-        in showParen (p>prec) $  showsPrec lprec lhs . showChar c . showsPrec rprec rhs
-    showsPrec p (App lhs rhs)   =
-        showParen (p>6) $ showsPrec 6 lhs . showChar ' ' . showsPrec 7 rhs
-    showsPrec _ (Var i)         = showVar i
-
-type IntExp = Exp Zero
-data Condition = Eq IntExp IntExp | Gt IntExp IntExp | Lt IntExp IntExp
-type SExp a = ([Condition], IntExp)
-newtype Compile a = Compile { unCompile :: SExp a }
-
---instance Lambda Compile where
---  labs :: (l a -> l b) -> l (a -> b)
---    labs f = Compile $ f
-
-
---{- Create a restricted deep embedding to work with the expression -}
---{- sized [a] to prove -}
---
---class Restricted a where
---    kind :: a -> Int
---
---instance Restricted Int where
---    kind _ = 0
---
---instance Restricted a => Restricted (Int -> a) where
---    kind _ = succ $ kind $ (undefined :: a)
---
---class Var l where
---    var :: Restricted a => Int -> l a
---
---showVar2 x = showChar '_' . showVar x
---
---newtype Count a = C { count :: Int }
---cnv :: Restricted a => Count a -> a
---cnv = undefined
---
---ckind :: (Restricted a) => Count a -> Int
---ckind = kind . cnv
---
---instance Var Count where
---    var _ = undefined
---
---instance Var LPrint where
---    var x = LPrint $ \_ -> return $ showVar2 x
---
---class MGS a where
---  mgs :: Supply Int -> a -> a
---  mgs = mgs' []
---  mgs' :: [Int] -> Supply Int -> a -> a
---
---instance MGS () where
---  mgs' _ _ _ = ()
---
---instance MGS a => MGS (RList a) where
---  mgs' bound supp  _ = RList (listsize, undefined)
---    where
---    (s1, s2, s3) = split3 supp
---    listsize = mgs' bound supp (undefined :: a)
Index: /sizechecking_branches/L.hs
===================================================================
--- /sizechecking_branches/L.hs	(revision 10)
+++ /sizechecking_branches/L.hs	(revision 10)
@@ -0,0 +1,209 @@
+{-# Language GADTs, FlexibleInstances, FlexibleContexts, MultiParamTypeClasses, FunctionalDependencies, ScopedTypeVariables, TypeFamilies, NoMonomorphismRestriction, OverlappingInstances #-}
+module L where
+
+import Data.Char(ord, chr)
+import Control.Monad.State
+--import Data.Supply
+
+data OpName = PLUS | MINUS | MUL
+data Bottom = Bottom
+  deriving Show
+
+{- Lambda calculus without free variables -}
+type Arr repr a b = repr a -> repr b
+
+class Lambda l where
+    labs    :: (l a -> l b) -> l (Arr l a b)
+    app     :: l (Arr l a b) -> l a -> l b
+    lit     :: Int -> l Int
+    op      :: l Int -> OpName -> l Int -> l Int
+
+class SizeExp l where
+    type List l :: * -> *
+    list    :: l Int -> l (Arr l Int b) -> l (List l b)
+    aabs    :: (l Int -> l (Arr l Int a) -> l b) -> l (Arr l (List l a) b)
+    shift   :: l (Arr l Int a) -> l Int -> l (Arr l Int a) -> l (Arr l Int a)
+    undef   :: l Bottom
+    unsized :: l ()
+
+instance Lambda l => Show (l a) where
+    showsPrec _ e = error "Error: no show"
+
+instance Lambda l => Eq (l a) where
+    (==) _ _ = error "Error: no eq"
+
+instance Lambda l => Num (l Int) where
+    fromInteger = lit . fromIntegral
+    lhs + rhs   = op lhs PLUS rhs
+    lhs - rhs   = op lhs MINUS rhs
+    lhs * rhs   = op lhs MUL rhs
+    abs = error "abs is not implemented"
+    signum = error "signum is not implemented"
+
+{- Printing -}
+newtype LPrint a = LPrint { unPrint :: Int -> Int -> ShowS }
+
+instance Lambda LPrint where
+  lit x      = LPrint $ \_ -> return $ shows x
+  op m opc n = LPrint $ \p -> do
+    let (prec, lprec, rprec, c) = getPrec opc
+    l1 <- (unPrint m lprec)
+    l2 <- (unPrint n rprec)
+    return $ showParen (p>prec) $  l1 . showChar c . l2
+  app f v    = LPrint $ \p -> do
+    l1 <- unPrint f 6
+    l2 <- unPrint v 7
+    return $ showParen (p>6) $ l1 . showChar ' ' . l2
+  labs e      = LPrint $ \p v -> let
+    var = LPrint $ \_ -> return $ showVar v
+    l = unPrint (e var) 0 $ succ v
+    in showParen (p>0) $ showChar 'λ' . showVar v . showChar '.' . l
+
+instance SizeExp LPrint where
+  type List LPrint = []
+  aabs f   = LPrint $ \p v -> let 
+    v2 = succ v
+    var1 = LPrint $ \_ _ -> showVar v
+    var2 = LPrint $ \_ _ -> showVar v2
+    l = unPrint (f var1 var2) 0 (v+2)
+    in showParen (p>0) $ showChar 'Λ' . showVar v . showChar ',' . showVar v2 . showChar '.' . l
+  list s f = LPrint $ \p -> do
+    l1 <- unPrint s 9
+    l2 <- unPrint f 9
+    return $ showParen (p>0) $ showString "List " . l1 . showChar ' ' . l2
+  shift e1 s e2 = LPrint $ \p -> do
+    l1 <- unPrint e1 2
+    l2 <- unPrint s 2
+    l3 <- unPrint e2 2
+    return $ showParen (p>0) $ showString "Shift " . l1 .  showChar ' ' . l2 . showChar ' ' . l3
+  undef = LPrint $ \_ -> return $ showChar '┮'
+  unsized = LPrint $ \_ -> return $ showChar 'U'
+
+view :: LPrint a -> LPrint a
+view = id
+instance Show (LPrint a) where
+    showsPrec _ e = unPrint e 0 0
+
+showVar x = if x>28 
+    then showVar (x `div` 29) . showChar (chr $ ord 'a' + (x `mod` 29))
+    else showChar $ chr $ ord 'a' + x
+
+getPrec :: OpName -> (Int,Int,Int,Char)
+getPrec PLUS = (4,4,5,'+')
+getPrec MINUS = (4,4,5,'-')
+getPrec MUL = (5,5,6,'*')
+
+getVar :: State Int Int
+getVar = do { x <- get; put (x+1); return x }
+
+x = aabs (\s _ -> s) `app` list (lit 0) (labs $ \_ -> undef)
+y = list 0 $ labs $ \_ -> undef
+z = (labs $ \s -> s+1) `app` (lit 1+2)
+conss = labs $ \x -> aabs $ \ys yf -> list (ys + 1) $ shift yf ys (labs $ \_ -> x)
+concats = aabs $ \xs xf -> (aabs $ \ys yf -> list (xs+ys) $ shift xf xs yf)
+maps = labs $ \x -> aabs $ \ys yf -> list ys ( x `app` yf )
+l0 = list (lit 0) (labs $ \_ -> unsized)
+l1 = list (lit 1) (labs $ \_ -> unsized)
+l2 = list (lit 2) (labs $ \_ -> unsized)
+l00 = list (lit 0) (labs $ \_ -> list (lit 0) (labs $ \_ -> unsized))
+l10 = list (lit 1) (labs $ \_ -> list (lit 0) (labs $ \_ -> unsized))
+l01 = list (lit 0) (labs $ \_ -> list (lit 1) (labs $ \_ -> unsized))
+l11 = list (lit 1) (labs $ \_ -> list (lit 1) (labs $ \_ -> unsized))
+l12 = list (lit 1) (labs $ \_ -> list (lit 2) (labs $ \_ -> unsized))
+
+{- Evaluating -}
+newtype R a = R { unR :: a }
+instance Lambda R where
+  labs f      = R $ f 
+  app e1 e2   = (unR e1) e2
+  lit i       = R i
+  op e1 op e2 = let opm = case op of
+                                  PLUS  -> (+)
+                                  MINUS -> (-)
+                                  MUL   -> (*)
+                in R $ opm (unR e1) (unR e2)
+
+newtype RList a = RList { unList :: (Int, Int -> a)  }
+instance (Show a) => Show (RList a) where
+  show (RList (s,f)) = show (map f [0..s-1])
+
+instance SizeExp R where
+  type List R = RList
+  undef       = R $ Bottom
+  unsized     = R $ ()
+  list s f    = R $ RList (unR s, unR . (unR f) . R )
+  aabs e = R $ ( \(RList (s,f)) -> (e (R s) (R (R . f . unR))) ) . unR
+  shift a s c = R $ \i -> if (unR i)<(unR s) then unR a i else unR c i
+
+-- Type level int to count arity
+data Zero
+data Succ a
+
+data Exp a where
+    Lit :: Int -> Exp Zero
+    Op  :: Exp Zero -> OpName -> Exp Zero -> Exp Zero
+    App :: Exp (Succ a) -> Exp Zero -> Exp a
+    Var :: Int -> Exp a
+
+instance Show (Exp a) where
+    showsPrec _ (Lit a)         = shows a
+    showsPrec p (Op lhs op rhs) =
+        let (prec, lprec, rprec, c) = getPrec op
+        in showParen (p>prec) $  showsPrec lprec lhs . showChar c . showsPrec rprec rhs
+    showsPrec p (App lhs rhs)   =
+        showParen (p>6) $ showsPrec 6 lhs . showChar ' ' . showsPrec 7 rhs
+    showsPrec _ (Var i)         = showVar i
+
+type IntExp = Exp Zero
+data Condition = Eq IntExp IntExp | Gt IntExp IntExp | Lt IntExp IntExp
+type SExp a = ([Condition], IntExp)
+newtype Compile a = Compile { unCompile :: SExp a }
+
+--instance Lambda Compile where
+--  labs :: (l a -> l b) -> l (a -> b)
+--    labs f = Compile $ f
+
+
+--{- Create a restricted deep embedding to work with the expression -}
+--{- sized [a] to prove -}
+--
+--class Restricted a where
+--    kind :: a -> Int
+--
+--instance Restricted Int where
+--    kind _ = 0
+--
+--instance Restricted a => Restricted (Int -> a) where
+--    kind _ = succ $ kind $ (undefined :: a)
+--
+--class Var l where
+--    var :: Restricted a => Int -> l a
+--
+--showVar2 x = showChar '_' . showVar x
+--
+--newtype Count a = C { count :: Int }
+--cnv :: Restricted a => Count a -> a
+--cnv = undefined
+--
+--ckind :: (Restricted a) => Count a -> Int
+--ckind = kind . cnv
+--
+--instance Var Count where
+--    var _ = undefined
+--
+--instance Var LPrint where
+--    var x = LPrint $ \_ -> return $ showVar2 x
+--
+--class MGS a where
+--  mgs :: Supply Int -> a -> a
+--  mgs = mgs' []
+--  mgs' :: [Int] -> Supply Int -> a -> a
+--
+--instance MGS () where
+--  mgs' _ _ _ = ()
+--
+--instance MGS a => MGS (RList a) where
+--  mgs' bound supp  _ = RList (listsize, undefined)
+--    where
+--    (s1, s2, s3) = split3 supp
+--    listsize = mgs' bound supp (undefined :: a)
Index: /sizechecking_branches/LL.hs
===================================================================
--- /sizechecking_branches/LL.hs	(revision 10)
+++ /sizechecking_branches/LL.hs	(revision 10)
@@ -0,0 +1,96 @@
+{-# Language GADTs, 
+        FlexibleInstances, 
+        FlexibleContexts, 
+        ScopedTypeVariables, 
+        TypeFamilies, 
+        NoMonomorphismRestriction,
+        OverlappingInstances #-}
+
+import Data.Char
+import Control.Monad.Instances()
+
+data OpName = PLUS | MINUS | MUL
+data Bottom = Bottom
+  deriving Show
+
+type family Arr (repr :: * -> *) (a :: *) (b :: *) :: *
+
+class Lambda l where
+    labs    :: (l a -> l b) -> l (Arr l a b)
+    app     :: l (Arr l a b) -> l a -> l b
+    lit     :: Int -> l Int
+    op      :: l Int -> OpName -> l Int -> l Int
+
+-- Required for Num
+instance Lambda l => Show (l a) where
+    showsPrec _ _ = error "Error: no show"
+
+-- Required for Num
+instance Lambda l => Eq (l a) where
+    (==) _ _ = error "Error: no eq"
+
+instance Lambda l => Num (l Int) where
+    fromInteger = lit . fromIntegral
+    lhs + rhs   = op lhs PLUS rhs
+    lhs - rhs   = op lhs MINUS rhs
+    lhs * rhs   = op lhs MUL rhs
+    abs = error "abs is not implemented"
+    signum = error "signum is not implemented"
+
+{- Printing -}
+showVar x = if x>28 
+    then showVar (x `div` 29) . showChar (chr $ ord 'a' + (x `mod` 29))
+    else showChar $ chr $ ord 'a' + x
+
+getPrec :: OpName -> (Int,Int,Int,Char)
+getPrec PLUS = (4,4,5,'+')
+getPrec MINUS = (4,4,5,'-')
+getPrec MUL = (5,5,6,'*')
+
+newtype LPrint a = LPrint { unPrint :: Int -> Int -> ShowS }
+type instance Arr LPrint a b = a -> b
+
+instance Lambda LPrint where
+  lit x      = LPrint $ \_ -> return $ shows x
+  op m opc n = LPrint $ \p -> do
+    let (prec, lprec, rprec, c) = getPrec opc
+    l1 <- unPrint m lprec
+    l2 <- unPrint n rprec
+    return $ showParen (p>prec) $  l1 . showChar c . l2
+  app f v    = LPrint $ \p -> do
+    l1 <- unPrint f 6
+    l2 <- unPrint v 7
+    return $ showParen (p>6) $ l1 . showChar ' ' . l2
+  labs e      = LPrint $ \p v -> let
+    var = LPrint $ \_ -> return $ showVar v
+    l = unPrint (e var) 0 $ succ v
+    in showParen (p>0) $ showChar 'λ' . showVar v . showChar '.' . l
+
+instance Show (LPrint a) where
+    showsPrec _ e = unPrint e 0 0
+
+view :: LPrint a -> LPrint a
+view = id
+
+{- Evaluating -}
+newtype R a = R { unR :: a }
+type instance Arr R a b = R a -> R b
+
+instance Lambda R where
+  labs        = R
+  app         = unR
+  lit         = R
+  op e1 op e2 = let opm = case op of
+                                  PLUS  -> (+)
+                                  MINUS -> (-)
+                                  MUL   -> (*)
+                in R $ opm (unR e1) (unR e2)
+
+newtype RList a = RList { unList :: (Int, Int -> a)  }
+
+instance (Show a) => Show (RList a) where
+  show (RList (s,f)) = show (map f [0..s-1])
+
+eval = unR
+
+z = labs ( \s -> s + 1) `app` ( 1 + lit 2)