diff --git a/Control/Category/Constrained.hs b/Control/Category/Constrained.hs
--- a/Control/Category/Constrained.hs
+++ b/Control/Category/Constrained.hs
@@ -1,25 +1,18 @@
 {-# LANGUAGE QuantifiedConstraints #-}
-{-# LANGUAGE InstanceSigs #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE TypeInType #-}
 {-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE UndecidableInstances #-}
-{-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TupleSections #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE ViewPatterns #-}
-{-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE RecursiveDo #-}
 {-# LANGUAGE LinearTypes #-}
 
 module Control.Category.Constrained where
@@ -215,7 +208,7 @@
   -- etc.
 
 instance Category (FUN x) where
-  id = \x -> x
+  id x = x
   f ∘ g = \x -> f (g x)
 
 instance Monoidal (FUN m) where
diff --git a/Control/Category/FreeSMC.hs b/Control/Category/FreeSMC.hs
--- a/Control/Category/FreeSMC.hs
+++ b/Control/Category/FreeSMC.hs
@@ -2,17 +2,13 @@
 {-# LANGUAGE QuantifiedConstraints #-}
 {-# OPTIONS_GHC -Wno-incomplete-patterns -Wno-overlapping-patterns #-}
 {-# LANGUAGE InstanceSigs #-}
-{-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE TypeInType #-}
 {-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE UndecidableInstances #-}
-{-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE TupleSections #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE ViewPatterns #-}
@@ -29,7 +25,7 @@
 import Data.Kind
 import Data.Type.Equality
 
-data Sho a b = Sho {fromSho :: Int -> ShowS}
+newtype Sho a b = Sho {fromSho :: Int -> ShowS}
 
 instance Show (Sho a b) where
   showsPrec d (Sho f) = f d
@@ -144,10 +140,10 @@
 commuteUnitors UL UR = id
 commuteUnitors UR UR = id
 commuteUnitors UR UL = id
-commuteUnitors (IL a) (IL b) = (commuteUnitors a b × id)
-commuteUnitors (IR a) (IR b) = (id × commuteUnitors a b)
-commuteUnitors (IR a) (IL b) = (U (IL b)) .  (U' (IR a))
-commuteUnitors (IL a) (IR b) = (U (IR b)) .  (U' (IL a))
+commuteUnitors (IL a) (IL b) = commuteUnitors a b × id
+commuteUnitors (IR a) (IR b) = id × commuteUnitors a b
+commuteUnitors (IR a) (IL b) = U (IL b) .  U' (IR a)
+commuteUnitors (IL a) (IR b) = U (IR b) .  U' (IL a)
 commuteUnitors UL (IR a) = U a . U' UL
 commuteUnitors UR (IL a) = U a . U' UR
 commuteUnitors (IR a) UL = U UL . U' a
@@ -177,27 +173,27 @@
     A -> A'
     A' -> A
 
-assocRight :: (Cat k obj x y) -> (Cat k obj x y)
+assocRight :: Cat k obj x y -> Cat k obj x y
 assocRight (a :.: (assocRight -> (b :.: c))) = (a :.: b) :.: c
 assocRight x = x
 
-rightView :: (obj a, obj c) => (Cat k obj a c) -> Cat k obj a c
+rightView :: (obj a, obj c) => Cat k obj a c -> Cat k obj a c
 rightView (assocRight -> (a :.: b)) = a :.: b
 rightView x = I :.: x
 
-assocLeft :: (Cat k obj x y) -> (Cat k obj x y)
+assocLeft :: Cat k obj x y -> Cat k obj x y
 assocLeft ((assocLeft -> (a :.: b)) :.: c) = a :.: (b :.: c)
 assocLeft x = x
 
-leftView :: (obj a, obj c) => (Cat k obj a c) -> Cat k obj a c
+leftView :: (obj a, obj c) => Cat k obj a c -> Cat k obj a c
 leftView (assocLeft -> (a :.: b)) = a :.: b
 leftView x = x :.: I
 
-pattern (:>:) ::  (obj x, obj y) => (obj b)  =>  (Cat k obj b y) -> (Cat k obj x b) -> Cat k obj x y
+pattern (:>:) ::  (obj x, obj y) => (obj b)  =>  Cat k obj b y -> Cat k obj x b -> Cat k obj x y
 pattern f :>: g <- (rightView -> f :.: g)
   where f :>: g = f . g
 
-pattern (:<:) ::  (obj x, obj y) => (obj b) => (Cat k obj b y) -> (Cat k obj x b) -> Cat k obj x y
+pattern (:<:) ::  (obj x, obj y) => (obj b) => Cat k obj b y -> Cat k obj x b -> Cat k obj x y
 pattern f :<: g <- (leftView -> f :.: g)
   where f :<: g = f . g
 
@@ -208,7 +204,7 @@
 
 evalM :: forall k a b con.
               (ProdObj con, forall x y. (con x, con y) => con (x,y), con (),
-               con ~ Obj k, Monoidal k, Obj k a, Obj k b) => Cat k (Obj k) a b -> (k a b)
+               con ~ Obj k, Monoidal k, Obj k a, Obj k b) => Cat k (Obj k) a b -> k a b
 evalM I          = id
 evalM (f :×: g)  = evalM f × evalM g
 evalM (f :.: g)  = evalM f . evalM g
@@ -221,7 +217,7 @@
 
 evalCartesian :: forall k a b con.
               (ProdObj con, forall x y. (con x, con y) => con (x,y), con (),
-               con ~ Obj k, Cartesian k, Obj k a, Obj k b) => Cat k (Obj k) a b -> (k a b)
+               con ~ Obj k, Cartesian k, Obj k a, Obj k b) => Cat k (Obj k) a b -> k a b
 evalCartesian = \case
   I -> id
   (f :×: g) -> evalCartesian f × evalCartesian g
@@ -237,20 +233,20 @@
 evalUnitor :: forall k a b con.
               (ProdObj con, forall x y. (con x, con y) => con (x,y), con (),
                con ~ Obj k, Monoidal k, Obj k a, Obj k b)
-           => Unitor (Obj k) a b -> (k a b)
+           => Unitor (Obj k) a b -> k a b
 evalUnitor UR = unitor
 evalUnitor UL = swap . unitor
-evalUnitor (IL x) = (evalUnitor x × id)
-evalUnitor (IR x) = (id × evalUnitor x)
+evalUnitor (IL x) = evalUnitor x × id
+evalUnitor (IR x) = id × evalUnitor x
 
 evalUnitor' :: forall k a b con.
               (ProdObj con, forall x y. (con x, con y) => con (x,y), con (),
                con ~ Obj k, Monoidal k, Obj k a, Obj k b)
-           => Unitor (Obj k) b a -> (k a b)
+           => Unitor (Obj k) b a -> k a b
 evalUnitor' UR = unitor'
 evalUnitor' UL = unitor' . swap
-evalUnitor' (IL x) = (evalUnitor' x × id)
-evalUnitor' (IR x) = (id × evalUnitor' x)
+evalUnitor' (IL x) = evalUnitor' x × id
+evalUnitor' (IR x) = id × evalUnitor' x
 -- eval Dup = dup
 -- eval Apply = apply
 -- eval (Curry f) = curry (eval f)
@@ -280,13 +276,13 @@
   unitor' = U' UR
 
 
-type Composer k con = forall a b c. (con a, con b, con c) => Cat k con b c -> Cat k con a b  -> (Cat k con a c)
+type Composer k con = forall a b c. (con a, con b, con c) => Cat k con b c -> Cat k con a b  -> Cat k con a c
 type PartialComposer k con = forall a b c. (con a, con b, con c) => Cat k con b c -> Cat k con a b  -> Alt Maybe (Cat k con a c)
 type ProtoSimplifier k con = (con (), ProdObj con, forall a b. (con a, con b) => con (a,b)) => Composer k con -> PartialComposer k con
-type Simplifier k con = (con (), ProdObj con, forall a b. (con a, con b) => con (a,b)) => forall a b. (con a, con b) =>  (Cat k con a b) -> (Cat k con a b)
+type Simplifier k con = (con (), ProdObj con, forall a b. (con a, con b) => con (a,b)) => forall a b. (con a, con b) =>  Cat k con a b -> Cat k con a b
 
 monoidalSimplify :: (con (), ProdObj con, forall α β. (con α, con β) => con (α,β)) => (con a, con b) => Cat k con a b -> Cat k con a b
-monoidalSimplify = mkSimplifier (\x -> monoidalRules x)
+monoidalSimplify = mkSimplifier monoidalRules
 
 monoidalRules :: forall k con. ProtoSimplifier k con
 monoidalRules  (.) = \ x y -> Alt (after x y) where
@@ -359,19 +355,6 @@
 neverEqual _ _ = Nothing
 
 
-
-
-{-
-
-closedCartesianRules :: forall k con. ProtoSimplifier k con
-closedCartesianRules (.) = \ x y -> Alt (after x y) where
-  after :: (con a, con b, con c) => Cat k con b  c -> Cat k con a b  -> Maybe (Cat k con a c)
-  
-  -- Incomplete support for apply/curry simplifier
-  Apply `after` (Curry f :×: I) = Just f
-  -- Apply `after` (Curry (g :>: R) :▵: f) = Just (g . f)
-  _ `after` _ = Nothing
--}
 mkSimplifier :: forall k con. ProtoSimplifier k con -> Simplifier k con
 mkSimplifier protoAfter = simplify where
    (...) :: Composer k con
diff --git a/Control/Category/Linear.hs b/Control/Category/Linear.hs
--- a/Control/Category/Linear.hs
+++ b/Control/Category/Linear.hs
@@ -3,20 +3,14 @@
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GADTs #-}
-{-# LANGUAGE GeneralizedNewtypeDeriving #-}
-{-# LANGUAGE InstanceSigs #-}
-{-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE LinearTypes #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE QuantifiedConstraints #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE StandaloneKindSignatures #-}
-{-# LANGUAGE TupleSections #-}
 {-# LANGUAGE TypeApplications #-}
-{-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeFamilyDependencies #-}
 {-# LANGUAGE TypeInType #-}
 {-# LANGUAGE TypeOperators #-}
@@ -24,12 +18,11 @@
 {-# LANGUAGE ViewPatterns #-}
 {-# LANGUAGE UnicodeSyntax #-}
 
-{-# OPTIONS_GHC -Wno-incomplete-patterns -Wno-overlapping-patterns #-}
 
 module Control.Category.Linear (
   -- Interface
   type P, unit, split, merge, pattern (:::),
-  encode, decode, reduce, (!:),
+  encode, decode, (!:),
   -- Helpers for cartesian categories
   ignore, copy, discard
 ) where
@@ -184,6 +177,7 @@
 -- | Perform all reduction steps and return intermediate states
 reductionSteps  :: (ProdObj con, forall α β. (con α, con β) => con (α,β), con (), 
                con a, con b) => R cat con a b -> [R cat con a b]
+reductionSteps st@(St _ Nil) = [st] -- done; and all the input is discarded
 reductionSteps st@(St _ (I :+ Nil)) = [st] -- done!
 reductionSteps st = st : reductionSteps (reductionStep st)
 
@@ -193,6 +187,16 @@
 
 rToFree :: (Obj cat ~ con, ProdObj con, forall α β. (con α, con β) => con (α,β), con (), con a, con b)
         => R cat con a b -> FreeSMC cat con a b
+rToFree (St done Nil) = unsafeCoerce done
+-- why is the above safe? (St _ Nil) means that the whole input is
+-- discarded/the whole expression has no free variable. In other
+-- words, the input is the unit type. So we can coerce. 
+--
+-- Other explanation:
+-- Our input is (f id), with f : (r `k` a) ⊸ r `k` b
+-- We know that (f id) starts with discard.  Because f is linear, (f
+-- id) can discard its input only if the input type is the unit in the
+-- first place, hence a=().
 rToFree (St done (I :+ Nil)) = done . unitor
 
 reduce  :: (Obj cat ~ con, ProdObj con, forall α β. (con α, con β) => con (α,β), con (),
@@ -223,13 +227,13 @@
     LT -> LT
     GT -> GT
     EQ -> EQ
-compareAtoms (P1) (_) = LT
-compareAtoms (_) (P1) = GT
-compareAtoms (P2) (_) = LT
-compareAtoms (_) (P2) = GT
-compareAtoms (Embed _) (_) = LT
-compareAtoms (_) (Embed _) = GT
-compareAtoms (E) (_) = LT
-compareAtoms (_) (E) = GT
+compareAtoms P1 _ = LT
+compareAtoms _ P1 = GT
+compareAtoms P2 _ = LT
+compareAtoms _ P2 = GT
+compareAtoms (Embed _) _ = LT
+compareAtoms _ (Embed _) = GT
+compareAtoms E _ = LT
+compareAtoms _ E = GT
 compareAtoms f g = error ("compareAtoms:\n" ++ showDbg 0 f "\n" ++ showDbg 0 g "" )
 
diff --git a/linear-smc.cabal b/linear-smc.cabal
--- a/linear-smc.cabal
+++ b/linear-smc.cabal
@@ -1,6 +1,6 @@
 Cabal-Version:  3.0
 name:           linear-smc
-version:        1.0.0
+version:        1.0.1
 category:       control
 synopsis:       Build SMC morphisms using linear types
 description: