diff --git a/FMCt.cabal b/FMCt.cabal
index ec9a539..9f4a2ed 100644
--- a/FMCt.cabal
+++ b/FMCt.cabal
@@ -13,7 +13,8 @@ extra-source-files:     CHANGELOG.md,
                         
 common common-specs     
   Ghc-Options:          -Wno-name-shadowing
-                        -- -Wall
+                        -Wall
+                        -Wno-unuused-top-binds
                         -- -Wcompat
                         -- -Wincomplete-uni-patterns
                         -- -Wredundant-constraints
diff --git a/src/FMCt/Evaluator.hs b/src/FMCt/Evaluator.hs
index 1ef908a..a062166 100644
--- a/src/FMCt/Evaluator.hs
+++ b/src/FMCt/Evaluator.hs
@@ -1,26 +1,24 @@
 {-#LANGUAGE ScopedTypeVariables#-}
 module FMCt.Evaluator
-  ( eval
+  ( Binds
+  , Memory
+  , State
+  , emptyMem
+  , eval
   , eval1
-  , tCheck'
   , eval1'
   , evalToString
+  , tCheck'
   , tryEval1
-  , State
-  , Binds
-  , Memory
-  , emptyMem
   ) where
 
-import Control.DeepSeq
-import Control.Exception (try, IOException, catch)
+import Control.Exception (try, IOException)
 import Data.Map (Map, (!?))
-import FMCt.Syntax (Tm(..), Lo(..), Vv, Type(..))
+import FMCt.Syntax (Tm(..), Lo(..), Vv )
 import Text.Read (readMaybe)
-import FMCt.TypeChecker (typeCheck, Derivation, TError)
+import FMCt.TypeChecker (typeCheck, TError)
 import qualified Control.Exception as E
 import qualified Data.Map as M
-import Control.Monad (void)
 
 -- | Memory is a Map between a location and a list of Terms.
 type Memory = Map Lo [Tm]
@@ -40,16 +38,9 @@ push t l (m,b) = case m !? l of
                Nothing -> (M.insert l [t]   m, b)
                Just x  -> (M.insert l (t:x) m, b)
 
--- | Pops a term from λ location to a given location
-pushL :: Lo -> State -> State
-pushL l st@(m,b) = case m !? Ho of
-                     Nothing     -> error "Empty Stack when attempting to pop λ location"                    
-                     Just (x:xs) -> push x l (M.insert Ho xs m, b)
-                     Just _      -> error "Empty Stack when attempting to pop λ location"
-
 -- | Binds a term to a value and puts in the memory
 bind :: Vv -> Lo -> State -> State
-bind vv l st@(m,b) = case m !? l of
+bind vv l (m,b) = case m !? l of
                    Nothing      -> error $ "Empty Location " ++ show l
                    Just []      -> error $ "Empty Location " ++ show l
                    Just (x:xs)  -> (M.insert l xs m, M.insert vv [x] b)
@@ -68,40 +59,43 @@ pop n l st@(m,b)
 -- | Hacky way to add numbers - TODO: refactor
 adds :: String -> String -> String
 adds x y = case (readMaybe x :: Maybe Int, readMaybe y :: Maybe Int) of
-             (Just x, Just y) -> show $ x + y
+             (Just x', Just y') -> show $ x' + y'
              _                -> x ++ y
 
+-- | Hacky way to add numbers - TODO: refactor
 add :: State -> State
-add st@(m,b) = t
+add (m,b) = t
   where
     t = case m !? Ho of
-      Just []       -> error "Empty Stack"
+      Nothing       -> error "Not enough numbers to add! Empty Stack!"
+      Just []       -> error "Not enough numbers to add! Empty Stack!"
+      Just [_]      -> error "Not enough numbers to add!"
       Just (x:y:xs) -> case (x, y) of
-                         (V x _ , V y _) -> push (V (x `adds` y) St) Ho (M.insert Ho xs m, b)
+                         (V x' _ , V y' _) -> push (V (x' `adds` y') St) Ho (M.insert Ho xs m, b)
+                         (_,_) -> error $ "Cannot add these terms"
+
         
 evaluate :: Tm -> State -> State
 evaluate (V "+" c) m = evaluate c $ add (pop 2 Ho m)
-  where
-    intermediary = add $ pop 2 Ho m
     
 evaluate St         m = m                  -- does nothing
-evaluate (V x c) st@(m,b) = evaluate c nt -- places value @ lambda pos
+evaluate (V x c) st@(_,b) = evaluate c nt -- places value @ lambda pos
   where
-    nt = if unbound then push (V x St) Ho st
+    nt = if unbound
+         then push (V x St) Ho st
          else push (head et) Ho st
-    et = case b !? x of
-           Just x -> x
-           _      -> error "This should have never happened - pushing unbound"
-    unbound = case b !? x of
-                Nothing -> True
-                _       -> False                
-evaluate (B v ty lo tm) m = evaluate tm (bind v lo m)        -- pops and binds the term
-evaluate (P te l t') st@(m,b) = evaluate t' (push te l st)   -- pushes the term
---evaluate (E t    t') st@(m,b) = evaluate t' (evaluate t st)  -- evaluates the term 
+              
+    et = maybe (error "This should have never happened - pushing unbound") id $
+         b !? x
+         
+    unbound = maybe False (const True) $ b !? x 
+
+evaluate (B v _ lo tm) m = evaluate tm (bind v lo m)        -- pops and binds the term
+evaluate (P te l t') st  = evaluate t' (push te l st)   -- pushes the term
 
 -- | The Empty FMCt Evaluator state.
 emptyMem :: State
-emptyMem = (M.empty, M.empty)
+emptyMem = (,) M.empty M.empty
 
 -- | Takes a list of terms and evaluates them one after another starting from
 -- the head.
@@ -138,7 +132,7 @@ evalToString  term = do
   tc <- tCheck' term
   case tc of
     Left e -> pure $ show e
-    Right x -> pure . show $ eval1 term
+    Right _ -> pure . show $ eval1 term
 
 -- | Evaluates a term and fails safely.
 tryEval1 :: Tm -> IO (Either IOException State)
@@ -146,29 +140,4 @@ tryEval1 term = do
   x :: Either IOException State <- try $ E.evaluate $ eval1 term
   return x
 
-evalIO :: State -> IO ()
-evalIO st@(m,b) = case m !? Out of
-                    Just (x:xs)  -> print (show x)
-                      >> evalIO (M.insert Out xs m, b)
-                    Just []      -> return ()
-                    Nothing      -> return ()
-
--- Some simple examples
-ex7 = eval1 $                  -- [1.2.*].<x:t>.x.3.4
-      P (V "1" $ V "2" St) La  -- [1 . 2 . *]
-      (B "x" (TVec [] :=> TVec [TLoc Ho $ TCon "a"]) La             -- <x:t> 
-        $ V "x"                -- x
-        $ V "3"                -- 3
-        $ V "4"                -- 4
-        $ V "+"                -- +
-        $ V "+"                -- +
-        St)                    -- Star
-      
-ex8 = eval1          -- 1 . 2 . <x:t>_ . x . +
-      (V "1"         -- 1
-       $ V "2"       -- 2
-       $ B "x" (TVec [TLoc Ho $ TCon "a"]) Ho -- <x>
-       $ V "x"       -- x
-       $ V "+" St)   -- +
-
 
diff --git a/src/FMCt/Examples.hs b/src/FMCt/Examples.hs
index 0b15599..2739ad4 100644
--- a/src/FMCt/Examples.hs
+++ b/src/FMCt/Examples.hs
@@ -1,10 +1,16 @@
+{-# OPTIONS_GHC -Wno-unused-top-binds -Wno-missing-signatures#-}
 module FMCt.Examples
-  (examplesList)
+  ( examplesList
+  , pEx
+  , runPEx
+  )
 where
 import FMCt.Parsing (parseFMC) 
 import FMCt.TypeChecker (derive, fuse, consumes, consume)
-import FMCt.Syntax (T, Type(..), Lo(..))
+import FMCt.Syntax (T, Type(..), Lo(..), Tm(..))
+import FMCt.Evaluator
 
+examplesList :: [String]
 examplesList = [term1]
   where
   term1 :: String 
@@ -61,3 +67,35 @@ exCons' = (TCon "a" :=> TVec[TCon "b"]) `consume` (TCon "b" :=> TCon "c")
 -- | Wrapped in two vectors.
 exCons'' = (TCon "a" :=> TVec[TVec[TCon "b"]]) `consume` (TCon "b" :=> TCon "c")
 exCons2 = (TCon "a" :=> TCon "b") `consume` (TCon "" :=> TCon "c")
+
+--------------------------------------------------------------------------------
+-- parse example
+runPEx = parseFMC <$> pEx
+pEx = [pEx1, pEx2, pEx3, pEx4, pEx5]
+  where
+    pEx1 =  "x . y . [*]. [*] . <x:((int,bool))>"
+    pEx2 =  "x . y . [*]. [*] . <x:_>"
+    pEx3 =  "x . y . [*]. [*] . <x:(a(int,bool) => (int))>"
+    pEx4 =  "x . y . [*]. [*] . <x:(a(a) => (a) => (b))>"  -- higher order type 
+    pEx5 =  "x . y . [*]. [*] . <x:(a(ab,b) => (int)), (b(int))>"
+
+
+
+--------------------------------------------------------------------------------
+-- Some simple Evaluator examples
+ex7 = eval1 $                  -- [1.2.*].<x:t>.x.3.4
+      P (V "1" $ V "2" St) La  -- [1 . 2 . *]
+      (B "x" (TVec [] :=> TVec [TLoc Ho $ TCon "a"]) La             -- <x:t> 
+        $ V "x"                -- x
+        $ V "3"                -- 3
+        $ V "4"                -- 4
+        $ V "+"                -- +
+        $ V "+"                -- +
+        St)                    -- Star
+      
+ex8 = eval1          -- 1 . 2 . <x:t>_ . x . +
+      (V "1"         -- 1
+       $ V "2"       -- 2
+       $ B "x" (TVec [TLoc Ho $ TCon "a"]) Ho -- <x>
+       $ V "x"       -- x
+       $ V "+" St)   -- +
diff --git a/src/FMCt/Parsing.hs b/src/FMCt/Parsing.hs
index 2b3ac48..8c2b669 100644
--- a/src/FMCt/Parsing.hs
+++ b/src/FMCt/Parsing.hs
@@ -3,19 +3,23 @@ module FMCt.Parsing
     , parseType
     , parseFMCtoString
     , parseFMC'
+    , PError(..)
     )
 where
 import Control.Monad (void)
-import Control.Exception hiding (try)
-
-import FMCt.Syntax (Tm(..), Lo(..), T(..), Type(..))
+import qualified Control.Exception as E
+import Control.Exception (Exception)
+import FMCt.Syntax (Tm(..), Lo(..), T, Type(..))
 import Text.ParserCombinators.Parsec
 
+data PError = PTermErr String
+            | PTypeErr String
+            deriving Show
+instance Exception PError
+
 -- | Main Parsing Function. (Unsafe)
 parseFMC :: String -> Tm
-parseFMC x = case parse term "FMCParser" x of
-  Right x -> x
-  Left  e -> error $ show e
+parseFMC x = either (E.throw . PTermErr . show) id $ parse term "FMCParser" x 
 
 -- | Main Parsing Function. (Safe)
 parseFMC' :: String -> Either ParseError Tm
@@ -23,15 +27,12 @@ parseFMC' x = parse term "FMCParser" x
 
 -- | Utility Parsing Function used for the FMCt-Web.
 parseFMCtoString :: String -> String
-parseFMCtoString x = case parse term "FMCParser" x of
-  Right x -> show x
-  Left  e -> show e
+parseFMCtoString x = either show show $ parse term "FMCParser" x 
 
 -- | Type Parser.
 parseType :: String -> T
-parseType x = case parse termType "TypeParser" x of
-  Right x -> x
-  Left  e -> error $ show e
+parseType x = either (E.throw . PTypeErr . show)  id $  parse termType "TypeParser" x 
+
 
 -- | Term Parser.
 term :: Parser Tm
@@ -90,7 +91,7 @@ type TConstant = String
 typeConstant :: Parser TConstant
 typeConstant = many1 alpha <> many alphaNumeric
 
-
+{-
 -- | Home Constants are constants that are on the lambda row
 --
 -- Examples:
@@ -99,7 +100,7 @@ homeType :: Parser T
 homeType = do
   typeC <- between (char '(') (char ')') termType
   return $ TLoc La typeC
-
+-}
 -- | Constant Type
 --
 -- Example:
@@ -144,11 +145,11 @@ emptyType = do
     void (char 'e') <|> spaces
     return $ TCon ""
 
-nestedType :: Parser T
-nestedType = do
-  l <- location
-  ts <- between (spaces >> char '(' >> spaces) (spaces >> char ')' >> spaces) termType
-  return $ TLoc l ts
+-- nestedType :: Parser T
+-- nestedType = do
+--   l <- location
+--   ts <- between (spaces >> char '(' >> spaces) (spaces >> char ')' >> spaces) termType
+--   return $ TLoc l ts
 
 higherType :: Parser T
 higherType = do
@@ -175,9 +176,3 @@ alphaNumeric = alpha <|> numeric
 operators :: Parser Char
 operators = oneOf "+-/%=!?"
 
--- parse example
-ex1 = parseTest term "x . y . [*]. [*] . <x:((int,bool))>"
-ex2 = parseTest term "x . y . [*]. [*] . <x:_>"
-ex3 = parseTest term "x . y . [*]. [*] . <x:(a(int,bool) => (int))>"
-ex4 = parseTest term "x . y . [*]. [*] . <x:(a(a) => (a) => (b))>"  -- higher order type 
-ex5 = parseTest term "x . y . [*]. [*] . <x:(a(ab,b) => (int)), (b(int))>"
diff --git a/src/FMCt/Pretty.hs b/src/FMCt/Pretty.hs
index fd42527..0541ea0 100644
--- a/src/FMCt/Pretty.hs
+++ b/src/FMCt/Pretty.hs
@@ -12,13 +12,14 @@ printStack (m,b) = "Memory: \n" ++ printer mem ++ "Bindings: \n" ++ printer bin
     mem = M.toList m
     bin = M.toList b
     printer [] = ""
-    printer (x@(l,ts):xs) = show l ++ "[" ++ show ts ++ "]" ++ "\n" ++ printer xs
+    printer ((l,ts):xs) = show l ++ "[" ++ show ts ++ "]" ++ "\n" ++ printer xs
 
-printOutput (m,b) = "Output: \n" ++ printer out
+printOutput :: State -> String 
+printOutput (m,_) = "Output: \n" ++ printer out
   where
     out = maybe [] reverse (m M.!? Out)
-    printer x = case x of
-      [] -> ""
+    printer = \case 
+      []     -> ""
       (x:xs) -> show x ++ "\n" ++ printer xs
     
     
diff --git a/src/FMCt/Syntax.hs b/src/FMCt/Syntax.hs
index 6a60783..934543b 100644
--- a/src/FMCt/Syntax.hs
+++ b/src/FMCt/Syntax.hs
@@ -39,14 +39,28 @@ type T = Type String
 
 -- | Type data structure
 data Type a = TCon a             -- ^ Type Constant.
-            | TVar a             -- ^ Type Variable - (like haskell forall - WIP)
+--            | TVar a             -- ^ Type Variable - (like haskell forall - WIP)
             | TVec [Type a]      -- ^ Type Vector 
             | TLoc Lo (Type a)   -- ^ Location Parametrised Type.
             | Type a :=> Type a  -- ^ A FMC Type.
             deriving (Eq, Ord)
 
--- | TypedTerms
-type TTm = (Tm, T)
+
+instance Semigroup T where
+  TVec []       <> x              = x
+  x             <> TVec[]         = x
+  TCon ""       <> x              = x
+  x             <> TCon ""        = x
+  xx@(TCon _)   <> yy@(TCon _)    = TVec [xx,yy]
+  TVec x        <> TVec y         = TVec $ x ++ y
+  xx@(TLoc l x) <> yy@(TLoc l' y) | l == l' = TLoc l $ x <> y
+                                  | otherwise = TVec [xx,yy]
+  xx <> yy                        = TVec [xx,yy]
+
+instance Monoid T where
+  mempty = TCon ""
+
+
 
 --------------------------------------------
 -- Location = {out, in, rnd, nd, x, γ, λ} --
@@ -60,9 +74,9 @@ data Lo = Out              -- ^ User Output Location - can only be pushed to.
         | Ho               -- ^ Home stack : γ ∈ A.
         | La               -- ^ Default push Location: λ ∈ A.
         | Lo  String       -- ^ any other location: x ∈ A.
-        | InInt            -- ^ User Input Location for Ints
-        | InBool           -- ^ User Input Location for Bools
-        | InChar           -- ^ User Input Location for Chars
+--        | InInt            -- ^ User Input Location for Ints
+--        | InBool           -- ^ User Input Location for Bools
+--        | InChar           -- ^ User Input Location for Chars
         deriving (Eq, Ord)
   
 --------------------------------------------------------------------------------
@@ -81,7 +95,7 @@ instance Show (Type String)  where
   show x = case x of
     TCon "" -> " "
     TCon y -> y
-    TVec x -> mconcat ["(", init $ mconcat $ (flip (++) ",") <$> show <$> x , ")"]
+    TVec _x -> mconcat ["(", init $ mconcat $ (flip (++) ",") <$> show <$> _x , ")"]
     TLoc l y -> show l ++ "(" ++ show y ++ ")"
     t1 :=> t2 -> mconcat ["(", show t1, " => ", show t2, ")"]
 
@@ -92,11 +106,3 @@ instance Show Tm where
     V v t -> v ++ "." ++ show t -- untyped version
     St          -> "*"
 
-instance Functor Type where
-  fmap f term
-    = case term of
-        TCon x   -> TCon $ f x
-        TVar x   -> TVar $ f x
-        TLoc l x -> TLoc l $ f <$> x
-        a :=> b  -> (f <$> a) :=> (f <$> b)
-                  
diff --git a/src/FMCt/TypeChecker.hs b/src/FMCt/TypeChecker.hs
index 25fcf14..73acb89 100644
--- a/src/FMCt/TypeChecker.hs
+++ b/src/FMCt/TypeChecker.hs
@@ -11,14 +11,7 @@ module FMCt.TypeChecker
   )
 where
 
-import Control.DeepSeq
 import FMCt.Syntax
-import Data.List (sort)
-import qualified Data.Map as M
-import FMCt.Parsing (parseType, parseFMC)
-import Text.Read (readMaybe)
-import Data.Monoid
-import Control.Monad.State
 import Control.Exception
 
 -- | Typechecking Errors.
@@ -36,29 +29,13 @@ type Context = [(Term, T)]
 type Judgement = (Context, Term, T)
 
 data Derivation
-  = Star        Judgement
-  | Variable    Judgement
-  | Abstraction Judgement Derivation
-  | Application Judgement Derivation
-  | Fusion      Judgement Derivation Derivation
+  = Star        !Judgement
+  | Variable    !Judgement
+  | Abstraction !Judgement !Derivation
+  | Application !Judgement !Derivation
+  | Fusion      !Judgement !Derivation !Derivation
 
 type Term = Tm
-type TypedTerm = (Term, T)
-type TVariable = String
-
-instance Semigroup T where
-  TVec []       <> x              = x
-  x             <> TVec[]         = x
-  TCon ""       <> x              = x
-  x             <> TCon ""        = x
-  xx@(TCon x)   <> yy@(TCon y)    = TVec [xx,yy]
-  TVec x        <> TVec y         = TVec $ x ++ y
-  xx@(TLoc l x) <> yy@(TLoc l' y) | l == l' = TLoc l $ x <> y
-                                  | otherwise = TVec [xx,yy]
-  xx <> yy                        = TVec [xx,yy]
-
-instance Monoid T where
-  mempty = TCon ""
 
 --------------------------------------------------------------------------------
 -- TypeCheck Function
@@ -68,6 +45,7 @@ typeCheck = derive
 
 --------------------------------------------------------------------------------
 -- Aux Functions
+getJudgement :: Derivation -> Judgement
 getJudgement = \case
   Star j -> j
   Variable j -> j
@@ -77,7 +55,7 @@ getJudgement = \case
 
 freshTypeVar :: [T]
 freshTypeVar = TCon <$> [ mconcat $ [[x],[z],show y]
-                        | y <- [1..]
+                        | y <- [1..] :: [Integer]
                         , x <- ['A'..'Z']
                         , z <- ['A'..'Z']
                         ]
@@ -88,8 +66,8 @@ freshVarTypes =  TVec . (:[]) <$> freshTypeVar
 splitStream :: [a] -> ([a],[a])
 splitStream x = (,) l r
   where
-    l = snd <$> (filter ( odd . fst ) $ zip [1..] x)
-    r = snd <$> (filter ( not . odd . fst ) $ zip [1..] x)              
+    l = snd <$> (filter ( odd . fst ) $ zip ([1..] :: [Integer]) x)
+    r = snd <$> (filter ( not . odd . fst ) $ zip ([1..] :: [Integer]) x)              
 
 --------------------------------------------------------------------------------
 --
@@ -101,12 +79,7 @@ fuseTypesD dL dR = ty
     tR = (getJType . getJudgement) dR :: T 
     ty = fuse tL tR 
 
-newtype MT = MT T
-
-toMT :: T -> MT
-toMT x@(t1 :=> t2) = MT x
-toMT _             = error "Not Machine Type"
-                                                                           
+getJType :: Judgement -> T
 getJType (_,_,x) = x
 
 -- | Second step is to add our known variables to the context
@@ -136,7 +109,7 @@ derive = derive' freshVarTypes [(St, TCon [] :=> TCon [])]
     mergeCtx ox oy = makeSet ox oy
       where
         makeSet [] x  = x
-        makeSet (t@(term,ty):xs)  [] = t : makeSet xs oy 
+        makeSet (t:xs) [] = t : makeSet xs oy 
         makeSet t@((term,ty):xs) ((term',ty'):ys)
           = if term /= term' then makeSet t ys
             else if ty == ty' then makeSet xs oy
@@ -160,7 +133,7 @@ derive = derive' freshVarTypes [(St, TCon [] :=> TCon [])]
             where
               ty = getType term ctx
 
-          V x St -> Variable (ctx, term, ty)
+          V _ St -> Variable (ctx, term, ty)
             where
               ty = getType term ctx
 
@@ -206,43 +179,43 @@ derive = derive' freshVarTypes [(St, TCon [] :=> TCon [])]
 
 fuse :: T -> T -> T
 fuse = \case
-  x@(TCon "") -> normaliseT
+  TCon "" -> normaliseT
 
-  x@(TVec []) -> normaliseT
+  TVec [] -> normaliseT
   
   x@(TCon _)  -> \case
-    y@(TCon "")      ->  x
+    TCon ""          ->  x
     y@(TCon _)       -> TVec [x,y]
-    y@(TVec [])      -> TVec [x]
-    yy@(TVec (y:ys)) -> fuse (fuse x y) (TVec ys)
-    y@(TLoc l t)     -> TVec [x,y]
-    y@(t1 :=> t2)    -> either (throw . ErrWrongT) normaliseT $ consume y (mempty :=> x)
+    TVec []          -> TVec [x]
+    TVec (y:ys)      -> fuse (fuse x y) (TVec ys)
+    y@(TLoc _ _)     -> TVec [x,y]
+    y@(_ :=> _)    -> either (throw . ErrWrongT) normaliseT $ consume y (mempty :=> x)
     
-  xxx@(TVec xx@(x:xs))  -> \case
-    y@(TCon "")      -> xxx
+  xxx@(TVec xx@(x:_))  -> \case
+    TCon ""          -> xxx
     y@(TCon _)       -> TVec $ xx ++ [y]
-    y@(TVec [])      -> xxx
-    yy@(TVec (y:ys)) -> fuse (fuse xxx y) (TVec ys)
-    y@(TLoc l t)     -> TVec [x,y]
-    y@(t1 :=> t2)    -> either (throw . ErrWrongT) normaliseT $ consume y (mempty :=> xxx)
+    TVec []          -> xxx
+    TVec (y:ys)      -> fuse (fuse xxx y) (TVec ys)
+    y@(TLoc _ _)     -> TVec [x,y]
+    y@(_ :=> _)      -> either (throw . ErrWrongT) normaliseT $ consume y (mempty :=> xxx)
     
   x@(TLoc l t) -> \case
-    y@(TCon "")      -> x
+    TCon ""          -> x
     y@(TCon _)       -> TVec $ x : y : []
-    y@(TVec [])      -> x
-    yy@(TVec (y:ys)) -> fuse (fuse x y) (TVec ys)
+    TVec []          -> x
+    TVec (y:ys)      -> fuse (fuse x y) (TVec ys)
     y@(TLoc l' t')   -> if l == l'
                         then TLoc l $ fuse t t'
                         else TVec [x,y]
-    y@(t1 :=> t2)    -> either (throw . ErrWrongT) normaliseT $ consume y (mempty :=> x)
+    y@(_ :=> _)    -> either (throw . ErrWrongT) normaliseT $ consume y (mempty :=> x)
 
-  x@(t1 :=> t2)  -> \case
-    y@(TCon "")      -> x
+  x@(_ :=> _)  -> \case
+    TCon ""          -> x
     y@(TCon _)       -> fuse (mempty :=> y) x
-    y@(TVec [])      -> x
-    yy@(TVec (y:ys)) -> fuse (fuse x y) (TVec ys)
-    y@(TLoc l' t')   -> fuse (mempty :=> y) x
-    y@(t1' :=> t2')  -> either (throw . ErrWrongT) normaliseT $ consume x y
+    TVec []          -> x
+    TVec (y:ys)      -> fuse (fuse x y) (TVec ys)
+    y@(TLoc _ _)     -> fuse (mempty :=> y) x
+    y@(_ :=> _)      -> either (throw . ErrWrongT) normaliseT $ consume x y
 
 consumes :: T
           -- ^ Requires - What the term will consume
@@ -268,10 +241,11 @@ consumes = \case
       in (,) res2 (left1 <> left2)        
     yy          -> (xx,yy)
 
-  xxx@(TVec xx@(x:xs)) -> \case
-    TCon "" -> (,) xxx mempty
-    TVec [] -> (,) xxx mempty
-    yyy@(TVec yy@(y:ys)) -> let
+  xxx@(TVec (x:xs)) -> \case
+    TCon ""     -> (,) xxx mempty
+    TVec []     -> (,) xxx mempty
+    TVec (y:ys) ->
+      let
         (res1,left1) = consumes xxx y
         (res2,left2) = consumes res1 (TVec ys)
       in
@@ -291,11 +265,7 @@ consumes = \case
       if l == l'
       then
         let              
-          (res, left) = consumes t t'
-                        
-          res' = if res == mempty || res == TVec []
-                 then mempty
-                 else TLoc l res
+          (res, left) = consumes t t'                       
                      
           left' = if left == mempty || left == TVec []
                   then mempty
@@ -309,7 +279,7 @@ consumes = \case
     -- TLoc doesn't interact with any other type.
     y       -> (,) x y
 
-  x@(tIn :=> tOut) ->
+  x@(_ :=> _) ->
     \y ->
       if x == y
       then (,) mempty mempty
@@ -317,18 +287,16 @@ consumes = \case
 
 -- | Normalise gets rid of empty Types at locations.
 normaliseT :: T -> T
-normaliseT x@(TCon _)         = x
-normaliseT x@(TVec [])        = mempty
-normaliseT (TLoc _ (TVec [])) = mempty
-normaliseT (TLoc _ (TCon "")) = mempty
-normaliseT (TVec (x:[]))      = normaliseT x
-normaliseT (t1 :=> t2)        = normaliseT t1 :=> normaliseT t2
-normaliseT (TVec x)           = TVec $ fEmpty $ normaliseT <$> x
-  where
-    fEmpty :: [T] -> [T]
-    fEmpty = filter (not . aux)
-    aux x = x == (mempty :: T) || x == TCon "" || x == TVec []
-normaliseT x                  = id x -- Just to be sure it gets through.
+normaliseT = \case
+  x@(TCon _)        -> x
+  TVec []           -> mempty
+  TLoc _ (TVec [])  -> mempty
+  TLoc _ (TCon "")  -> mempty
+  TVec (x:[])       -> normaliseT x
+  t1 :=> t2         -> normaliseT t1 :=> normaliseT t2
+  TVec x            -> TVec $ fEmpty $ normaliseT <$> x
+    where fEmpty = filter (not . aux); aux y = y == TCon "" || y == TVec []
+  x -> id x -- Just to be sure it gets through.
 
 -- | Consume                                 
 consume :: T -> T -> Either String T
@@ -356,10 +324,9 @@ consume t1@(tIn :=> tOut) t2@(tIn' :=> tOut') = result
             , ". Resulting Type: "
             , show intermediary
             ]
+consume _ _ = (throw . ErrWrongT) $ "Cannot consume types which are not of the form (* => *)"
 
 -- Show Instance
-type DisplayLine = (( Int, Int, Int), [String])
-
 instance Show Derivation where
   show d = unlines (reverse strs)
     where      
@@ -381,65 +348,30 @@ instance Show Derivation where
       showD :: Derivation -> (Int,Int,Int,[String])
       showD (Star j) = (0,k,0,[s,showL 0 k 0]) where s = showJ j; k = length s
       showD (Variable j) = (0,k,0,[s,showL 0 k 0]) where s = showJ j; k = length s
-      showD (Abstraction j d) = addrule (showJ j) (showD d)
-      showD (Application j d) = addrule (showJ j) (showD d)
-      showD (Fusion j d e) = addrule (showJ j) (sidebyside (showD d) (showD e))
+      showD (Abstraction j d') = addrule (showJ j) (showD d')
+      showD (Application j d') = addrule (showJ j) (showD d')
+      showD (Fusion j d' e) = addrule (showJ j) (sidebyside (showD d') (showD e))
 
       addrule :: String -> (Int,Int,Int,[String]) -> (Int,Int,Int,[String])
       addrule x (l,m,r,xs)
-        | k <= m     = (ll,k,rr, (replicate ll ' ' ++ x ++ replicate rr ' ')
-                                 : showL  l m r
-                                 : xs)
+        | k <= m
+        = (ll,k,rr, (replicate ll ' ' ++ x ++ replicate rr ' ') : showL  l m r : xs)
 
         | k <= l+m+r
-        = ( ll
-          , k
-          , rr
-          , (replicate ll ' ' ++ x ++ replicate rr ' ')
-            : showL ll k rr
-            : xs
-          )
+        = ( ll , k , rr , (replicate ll ' ' ++ x ++ replicate rr ' ') : showL ll k rr : xs )
 
         | otherwise
-        = ( 0
-          , k
-          , 0
-          , x
-            : replicate k '-'
-            : [ replicate (-ll) ' '
-                ++ y
-                ++ replicate (-rr) ' '
-              | y <- xs
-              ]
-          )
-        where
-          k = length x
-          i = div (m - k) 2
-          ll = l+i
-          rr = r+m-k-i
+        = ( 0 , k , 0 , x : replicate k '-' : [ replicate (-ll) ' ' ++ y ++ replicate (-rr) ' ' | y <- xs ] )
+        where k = length x; i = div (m - k) 2; ll = l+i; rr = r+m-k-i
 
       extend :: Int -> [String] -> [String]
-      extend i strs = strs ++ repeat (replicate i ' ')
+      extend i strs' = strs' ++ repeat (replicate i ' ')
 
-      sidebyside
-        :: (Int,Int,Int,[String])
-        -> (Int,Int,Int,[String])
-        -> (Int,Int,Int,[String])
+      sidebyside :: (Int,Int,Int,[String]) -> (Int,Int,Int,[String]) -> (Int,Int,Int,[String])
         
       sidebyside (l1,m1,r1,d1) (l2,m2,r2,d2)
         | length d1 > length d2
-        = ( l1
-          , m1+r1+2+l2+m2
-          , r2
-          , [ x ++ "  " ++ y
-            | (x,y) <- zip d1 (extend (l2+m2+r2) d2)
-            ]
-          )
+        = ( l1, m1+r1+2+l2+m2, r2, [ x ++ "  " ++ y | (x,y) <- zip d1 (extend (l2+m2+r2) d2)])
+        
         | otherwise
-        = ( l1
-          , m1+r1+2+l2+m2
-          , r2
-          , [ x ++ "  " ++ y
-            | (x,y) <- zip (extend (l1+m1+r1) d1) d2
-            ]
-          )
+        = ( l1 , m1+r1+2+l2+m2 , r2 , [ x ++ " " ++ y | (x,y) <- zip (extend (l1+m1+r1) d1) d2])