Index: /sizechecking/branches/macs/Proof.hs
===================================================================
--- /sizechecking/branches/macs/Proof.hs	(revision 28)
+++ /sizechecking/branches/macs/Proof.hs	(revision 28)
@@ -0,0 +1,21 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module Proof where
+
+import Lambda
+import Ops
+import Size
+import Exp
+import SizedFun
+import qualified Prelude
+import Prelude (String, Int, ($), (.))
+
+
+data ZContext = ZContext {}
+data Constraint 
+newtype Z a = Z { unZ :: SizeExp }
+
+instance Size Q where
+instance Lambda Z where
+instance LOps Z where
+instance Exp Z where
Index: /sizechecking/branches/macs/Size.hs
===================================================================
--- /sizechecking/branches/macs/Size.hs	(revision 27)
+++ /sizechecking/branches/macs/Size.hs	(revision 28)
@@ -18,5 +18,4 @@
     unsized :: l Unsized
     bottom :: l a
-
 
 instance SContext s => Size (S s) where
Index: /sizechecking/branches/macs/SizedFun.hs
===================================================================
--- /sizechecking/branches/macs/SizedFun.hs	(revision 27)
+++ /sizechecking/branches/macs/SizedFun.hs	(revision 28)
@@ -11,9 +11,11 @@
 import qualified Data.Supply as S
 import Data.Lens.Light
+import Control.Monad.IO.Class
+
 
 class Infer a b where
 instance (Infer a b, Infer p q) => Infer (a->p) (b->q)
 instance Infer a b => Infer [a] [b]
-instance (a~b) => Infer a b
+instance a~b => Infer a b
 instance Infer Unsized Int
 
@@ -53,16 +55,5 @@
 
 instance SizedFun Q where
-    type SizeExp Q = S SBData
+    type SizeExp Q = S SData
     bind name size exp = exp
 
-data DeclSize b where
-  DeclSize :: Infer a b => S SData a -> DeclSize b
-
-instance Lambda DeclSize where
-instance LOps DeclSize where
-instance Exp DeclSize where
-instance SizedFun DeclSize where
-    type SizeExp DeclSize = S SData
-    bind name size exp = DeclSize size
-
---getDeclSize (DeclSize size) = size
Index: zechecking/branches/macs/Tests/BindTest.hs
===================================================================
--- /sizechecking/branches/macs/Tests/BindTest.hs	(revision 27)
+++ 	(revision )
@@ -1,16 +1,0 @@
-{-# LANGUAGE NoMonomorphismRestriction #-}
-
-module Tests.BindTest where
-
-import Lambda
-import SizedFun
-import Exp
-import Prelude ( ($), Int, (==), return, sequence, (>>=), and, (.), IO, Bool, String, const )
-import qualified Control.Monad
-import qualified Tests.SizeTest as S
-import qualified Tests.ExpTest as E
-
-addOne = bind "addone" S.testAddOne E.testAddOne
-
-concat = bind "concat" S.testConcat
-  (lam $ \l1 -> lam $ \l2 -> match l1 l2 $ \x xs -> cons x (concat `app` xs `app` l2))
Index: /sizechecking/branches/macs/Tests/ProofTest.hs
===================================================================
--- /sizechecking/branches/macs/Tests/ProofTest.hs	(revision 28)
+++ /sizechecking/branches/macs/Tests/ProofTest.hs	(revision 28)
@@ -0,0 +1,5 @@
+module Tests.ProofTest where
+
+import Tests.SizedFunTest
+import Proof
+
Index: /sizechecking/branches/macs/Tests/SizedFunTest.hs
===================================================================
--- /sizechecking/branches/macs/Tests/SizedFunTest.hs	(revision 28)
+++ /sizechecking/branches/macs/Tests/SizedFunTest.hs	(revision 28)
@@ -0,0 +1,16 @@
+{-# LANGUAGE NoMonomorphismRestriction #-}
+
+module Tests.SizedFunTest where
+
+import Lambda
+import SizedFun
+import Exp
+import Prelude ( ($), Int, (==), return, sequence, (>>=), and, (.), IO, Bool, String, const )
+import qualified Control.Monad
+import qualified Tests.SizeTest as S
+import qualified Tests.ExpTest as E
+
+addOne = bind "addone" S.testAddOne E.testAddOne
+
+concat = bind "concat" S.testConcat
+  (lam $ \l1 -> lam $ \l2 -> match l1 l2 $ \x xs -> cons x (concat `app` xs `app` l2))