diff --git a/LinearScan/Allocate.hs b/LinearScan/Allocate.hs
--- a/LinearScan/Allocate.hs
+++ b/LinearScan/Allocate.hs
@@ -142,8 +142,8 @@
                    (Morph.moveUnhandledToActive maxReg pre reg)}
       in
       let {cid = Cursor.curId maxReg sd} in
-      Context.context (Trace.ETryAllocateFreeReg ( reg) mres
-        ( (Prelude.fst cid)))
+      Context.context (Trace.ETryAllocateFreeReg (Prelude.id reg) mres
+        (Prelude.id (Prelude.fst cid)))
         (Context.ipure
           (case mres of {
             Prelude.Just n ->
@@ -211,8 +211,8 @@
            nextUsePos'' of {
      (,) reg mres ->
       let {cid = Cursor.curId maxReg sd} in
-      Context.context (Trace.EAllocateBlockedReg ( reg) mres
-        ( (Prelude.fst cid)))
+      Context.context (Trace.EAllocateBlockedReg (Prelude.id reg) mres
+        (Prelude.id (Prelude.fst cid)))
         (case case mres of {
                Prelude.Just n ->
                 (Prelude.<=) ((Prelude.succ) n)
@@ -236,7 +236,7 @@
                    (case mloc of {
                      Prelude.Just n ->
                       Context.context (Trace.EIntersectsWithFixedInterval n
-                        ( reg))
+                        (Prelude.id reg))
                         (Split.splitCurrentInterval maxReg pre
                           (Split.BeforePos n));
                      Prelude.Nothing -> Context.ipure ()}))
@@ -247,8 +247,8 @@
 morphlen_transport :: Prelude.Int -> ScanState.ScanStateDesc ->
                       ScanState.ScanStateDesc -> ScanState.IntervalId ->
                       ScanState.IntervalId
-morphlen_transport maxReg b b' = GHC.Base.id
-  
+morphlen_transport maxReg b b' =
+  Prelude.id
 
 mt_fst :: Prelude.Int -> ScanState.ScanStateDesc -> ScanState.ScanStateDesc
           -> ((,) ScanState.IntervalId PhysReg) -> (,) ScanState.IntervalId
@@ -291,8 +291,8 @@
               in
               Prelude.Right filtered_var0;
              Prelude.Nothing -> Prelude.Left ((:)
-              (Trace.ERegisterAssignmentsOverlap ( (Prelude.snd x))
-              ( (Prelude.fst x)) ((Prelude.succ) 0)) e)};
+              (Trace.ERegisterAssignmentsOverlap (Prelude.id (Prelude.snd x))
+              (Prelude.id (Prelude.fst x)) ((Prelude.succ) 0)) e)};
            Prelude.False -> Prelude.Right
             (case Prelude.not
                     (Interval.posWithinInterval
@@ -378,8 +378,8 @@
     in
     Prelude.Right filtered_var0;
    Prelude.False -> Prelude.Left ((:) (Trace.ERegisterAssignmentsOverlap
-    ( (Prelude.snd x)) ( (Prelude.fst x)) ((Prelude.succ) ((Prelude.succ)
-    0))) e)}
+    (Prelude.id (Prelude.snd x)) (Prelude.id (Prelude.fst x)) ((Prelude.succ)
+    ((Prelude.succ) 0))) e)}
 
 goInactive :: Prelude.Int -> Prelude.Int -> ScanState.ScanStateDesc -> ([]
               Trace.SSTrace) -> ScanState.ScanStateDesc -> ((,)
@@ -410,8 +410,8 @@
       in
       f filtered_var0;
      Prelude.Nothing -> Prelude.Left ((:) (Trace.ERegisterAssignmentsOverlap
-      ( (Prelude.snd x)) ( (Prelude.fst x)) ((Prelude.succ) ((Prelude.succ)
-      ((Prelude.succ) 0)))) e)};
+      (Prelude.id (Prelude.snd x)) (Prelude.id (Prelude.fst x))
+      ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) 0)))) e)};
    Prelude.False ->
     case Interval.posWithinInterval
            (
@@ -596,7 +596,7 @@
 determineAllocations :: Prelude.Int -> ScanState.ScanStateDesc -> []
                         Allocation
 determineAllocations maxReg sd =
-  Prelude.map (\x -> Build_Allocation ( (Prelude.fst x))
+  Prelude.map (\x -> Build_Allocation (Prelude.id (Prelude.fst x))
     (Interval.getIntervalDesc
       (
         (Vector0.vnth (ScanState.nextInterval maxReg sd)
diff --git a/LinearScan/Blocks.hs b/LinearScan/Blocks.hs
--- a/LinearScan/Blocks.hs
+++ b/LinearScan/Blocks.hs
@@ -41,7 +41,7 @@
 nat_of_varId :: Prelude.Int -> VarInfo -> Prelude.Int
 nat_of_varId maxReg v =
   case varId maxReg v of {
-   Prelude.Left n ->  n;
+   Prelude.Left n -> Prelude.id n;
    Prelude.Right v0 -> (Prelude.+) v0 maxReg}
 
 data OpKind =
diff --git a/LinearScan/Build.hs b/LinearScan/Build.hs
--- a/LinearScan/Build.hs
+++ b/LinearScan/Build.hs
@@ -144,7 +144,8 @@
       let {
        _top_assumption_ = compilePendingRanges b e
                             (List1.insert (coq_BoundedRange_leq b e) r
-                              (List1.sortBy (coq_BoundedRange_leq b e) ( rs)))}
+                              (List1.sortBy (coq_BoundedRange_leq b e)
+                                (Prelude.id rs)))}
       in
       let {
        _evar_0_0 = \_ _ ->
@@ -158,7 +159,7 @@
          (:) y ys -> rangesToBoundedRanges b e y ys}}
       in
       case List1.insert (coq_BoundedRange_leq b e) r
-             (List1.sortBy (coq_BoundedRange_leq b e) ( rs)) of {
+             (List1.sortBy (coq_BoundedRange_leq b e) (Prelude.id rs)) of {
        [] -> _evar_0_0 __ __;
        (:) x x0 -> _evar_0_1 x x0}}
     in
@@ -178,14 +179,15 @@
   IntMap.coq_IntMap_mergeWithKey (\_the_1st_wildcard_ brs srs2 ->
     let {
      _top_assumption_ = compilePendingRanges b e
-                          (List1.sortBy (coq_BoundedRange_leq b e) ( brs))}
+                          (List1.sortBy (coq_BoundedRange_leq b e)
+                            (Prelude.id brs))}
     in
     Prelude.Just
     (Range.coq_SortedRanges_cat ((Prelude.succ) (Ssrnat.double b))
       _top_assumption_ ((Prelude.succ) (Ssrnat.double e)) srs2))
     (IntMap.coq_IntMap_map (\brs ->
       compilePendingRanges b e
-        (List1.sortBy (coq_BoundedRange_leq b e) ( brs)))) (\sr ->
+        (List1.sortBy (coq_BoundedRange_leq b e) (Prelude.id brs)))) (\sr ->
     (Prelude.flip (Prelude.$)) __ (\_ ->
       IntMap.coq_IntMap_map
         (Range.transportSortedRanges ((Prelude.succ) (Ssrnat.double b))
@@ -297,7 +299,7 @@
                         in
                         let {
                          _evar_0_0 = \_the_2nd_wildcard_ rs -> Prelude.Just
-                          (NonEmpty.coq_NE_from_list br ( rs))}
+                          (NonEmpty.coq_NE_from_list br (Prelude.id rs))}
                         in
                         (\ns nc l -> case l of [x] -> ns x; (x:xs) -> nc x xs)
                           (\x ->
@@ -309,7 +311,7 @@
           let {
            _evar_0_0 = (Prelude.flip (Prelude.$)) _top_assumption_0 (\br ->
                          Prelude.Just
-                         (NonEmpty.coq_NE_from_list br ( range0)))}
+                         (NonEmpty.coq_NE_from_list br (Prelude.id range0)))}
           in
           case replaceFirst of {
            Prelude.True -> _evar_0_;
@@ -318,7 +320,7 @@
         let {
          _evar_0_0 = \_ -> Prelude.Just
           (NonEmpty.coq_NE_from_list (makeNewRange b pos e _top_assumption_)
-            ( range0))}
+            (Prelude.id range0))}
         in
         case upos_before_rend ( _top_assumption_0) _top_assumption_ of {
          Prelude.True -> _evar_0_ __;
@@ -342,7 +344,7 @@
   let {
    _evar_0_ = \range0 -> Prelude.Just
     (NonEmpty.coq_NE_from_list (makeNewRange b pos e _top_assumption_)
-      ( range0))}
+      (Prelude.id range0))}
   in
   let {
    _evar_0_0 = Prelude.Just ((:[]) (makeNewRange b pos e _top_assumption_))}
@@ -405,7 +407,7 @@
               IntMap.IntMap PendingRanges
 handleVars maxReg varRefs b pos e ranges =
   let {
-   vars = Prelude.id 
+   vars = IntMap.coq_IntMap_map Prelude.id
             (IntMap.coq_IntMap_groupOn (Blocks.nat_of_varId maxReg) varRefs)}
   in
   IntMap.coq_IntMap_mergeWithKey (handleVars_combine maxReg b pos e)
diff --git a/LinearScan/Contravariant.hs b/LinearScan/Contravariant.hs
new file mode 100644
--- /dev/null
+++ b/LinearScan/Contravariant.hs
@@ -0,0 +1,37 @@
+{-# OPTIONS_GHC -cpp -XMagicHash #-}
+{- For Hugs, use the option -F"cpp -P -traditional" -}
+
+module LinearScan.Contravariant where
+
+
+import Debug.Trace (trace, traceShow, traceShowId)
+import qualified Prelude
+import qualified Data.IntMap
+import qualified Data.IntSet
+import qualified Data.List
+import qualified Data.Ord
+import qualified Data.Functor.Identity
+import qualified Hask.Utils
+
+
+
+#ifdef __GLASGOW_HASKELL__
+import qualified GHC.Base as GHC.Base
+import qualified GHC.Prim as GHC.Prim
+#else
+-- HUGS
+import qualified LinearScan.IOExts as IOExts
+#endif
+
+
+#ifdef __GLASGOW_HASKELL__
+type Any = GHC.Prim.Any
+#else
+-- HUGS
+type Any = ()
+#endif
+
+type Contravariant f =
+  () -> () -> (Any -> Any) -> f -> f
+  -- singleton inductive, whose constructor was Build_Contravariant
+  
diff --git a/LinearScan/Fintype.hs b/LinearScan/Fintype.hs
--- a/LinearScan/Fintype.hs
+++ b/LinearScan/Fintype.hs
@@ -107,14 +107,16 @@
 
 ordinal_subType :: Prelude.Int -> Eqtype.Coq_subType Prelude.Int
 ordinal_subType n =
-  Eqtype.SubType (unsafeCoerce ) (unsafeCoerce (\x _ ->  x)) (\_ k_S u ->
+  Eqtype.SubType (unsafeCoerce Prelude.id) (unsafeCoerce (\x _ ->  x))
+    (\_ k_S u ->
     case unsafeCoerce u of {
       x -> k_S x __})
 
 ordinal_eqMixin :: Prelude.Int -> Eqtype.Equality__Coq_mixin_of Prelude.Int
 ordinal_eqMixin n =
   Eqtype.Equality__Mixin (\x y ->
-    Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce ( x)) (unsafeCoerce ( y)))
+    Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce (Prelude.id x))
+      (unsafeCoerce (Prelude.id y)))
     (unsafeCoerce
       (Eqtype.val_eqP Ssrnat.nat_eqType (\x ->
         (Prelude.<=) ((Prelude.succ) (unsafeCoerce x)) n)
diff --git a/LinearScan/Interval.hs b/LinearScan/Interval.hs
--- a/LinearScan/Interval.hs
+++ b/LinearScan/Interval.hs
@@ -200,7 +200,7 @@
            Prelude.True -> Range.rbeg ( r);
            Prelude.False -> ibeg x});
         Prelude.False -> go rs0}}}
-  in go ( (rds y))
+  in go (Prelude.id (rds y))
 
 divideIntervalRanges :: IntervalDesc -> Prelude.Int ->
                         ((,) Range.SortedRanges Range.SortedRanges)
@@ -328,7 +328,8 @@
      [] -> _evar_0_;
      (:) x x0 -> _evar_0_0 x x0}}
   in
-  case List1.span (\rd -> (Prelude.<=) (Range.rend ( rd)) before) ( (rds d)) of {
+  case List1.span (\rd -> (Prelude.<=) (Range.rend ( rd)) before)
+         (Prelude.id (rds d)) of {
    (,) x x0 -> _evar_0_ x x0 __}
 
 splitIntervalRanges :: IntervalDesc -> Prelude.Int ->
diff --git a/LinearScan/List1.hs b/LinearScan/List1.hs
--- a/LinearScan/List1.hs
+++ b/LinearScan/List1.hs
@@ -13,16 +13,15 @@
 import qualified Hask.Utils
 
 import qualified LinearScan.Eqtype as Eqtype
+import qualified LinearScan.Seq as Seq
 
 
 __ :: any
 __ = Prelude.error "Logical or arity value used"
 
 concat :: ([] ([] a1)) -> [] a1
-concat l =
-  case l of {
-   [] -> [];
-   (:) x xs -> (Prelude.++) x (concat xs)}
+concat =
+  Seq.flatten
 
 maybeLookup :: Eqtype.Equality__Coq_type -> ([]
                ((,) Eqtype.Equality__Coq_sort a1)) ->
diff --git a/LinearScan/Main.hs b/LinearScan/Main.hs
--- a/LinearScan/Main.hs
+++ b/LinearScan/Main.hs
@@ -56,14 +56,14 @@
        Prelude.Just x -> Prelude.Just (Interval.getIntervalDesc ( x));
        Prelude.Nothing -> Prelude.Nothing})
       (Vector0.vec_to_seq maxReg (ScanState.fixedIntervals maxReg sd)))
-    (Prelude.map (\i -> (,) ( (Prelude.fst i)) (Prelude.snd i))
+    (Prelude.map (\i -> (,) (Prelude.id (Prelude.fst i)) (Prelude.snd i))
       (ScanState.unhandled maxReg sd))
-    (Prelude.map (\i -> (,) ( (Prelude.fst i)) ( (Prelude.snd i)))
-      (ScanState.active maxReg sd))
-    (Prelude.map (\i -> (,) ( (Prelude.fst i)) ( (Prelude.snd i)))
-      (ScanState.inactive maxReg sd))
-    (Prelude.map (\i -> (,) ( (Prelude.fst i))
-      (Maybe.option_map (\x ->  x) (Prelude.snd i)))
+    (Prelude.map (\i -> (,) (Prelude.id (Prelude.fst i))
+      (Prelude.id (Prelude.snd i))) (ScanState.active maxReg sd))
+    (Prelude.map (\i -> (,) (Prelude.id (Prelude.fst i))
+      (Prelude.id (Prelude.snd i))) (ScanState.inactive maxReg sd))
+    (Prelude.map (\i -> (,) (Prelude.id (Prelude.fst i))
+      (Maybe.option_map (\x -> Prelude.id x) (Prelude.snd i)))
       (ScanState.handled maxReg sd))
 
 data Details blockType1 blockType2 =
diff --git a/LinearScan/Monad.hs b/LinearScan/Monad.hs
--- a/LinearScan/Monad.hs
+++ b/LinearScan/Monad.hs
@@ -14,7 +14,7 @@
 
 import qualified LinearScan.Applicative as Applicative
 import qualified LinearScan.Functor as Functor
-import qualified LinearScan.List1 as List1
+import qualified LinearScan.Seq as Seq
 
 
 __ :: any
@@ -92,5 +92,5 @@
 
 concatMapM :: (Applicative.Applicative a1) -> (a2 -> a1) -> ([] a2) -> a1
 concatMapM h f l =
-  Functor.fmap (Applicative.is_functor h) List1.concat (mapM h f l)
+  Functor.fmap (Applicative.is_functor h) Seq.flatten (mapM h f l)
 
diff --git a/LinearScan/Morph.hs b/LinearScan/Morph.hs
--- a/LinearScan/Morph.hs
+++ b/LinearScan/Morph.hs
@@ -139,7 +139,7 @@
           in
           let {
            _evar_0_0 = \_ -> Prelude.Left ((:)
-            (Trace.ECannotSpillIfRegisterRequired ( i)) e)}
+            (Trace.ECannotSpillIfRegisterRequired (Prelude.id i)) e)}
           in
           case Eqtype.eq_op
                  (Eqtype.option_eqType
@@ -178,7 +178,7 @@
         in
         let {
          _evar_0_0 = \_ -> Prelude.Left ((:) (Trace.ERegisterAlreadyAssigned
-          ( reg)) e)}
+          (Prelude.id reg)) e)}
         in
         case Prelude.not
                (Ssrbool.in_mem (unsafeCoerce reg)
diff --git a/LinearScan/Resolve.hs b/LinearScan/Resolve.hs
--- a/LinearScan/Resolve.hs
+++ b/LinearScan/Resolve.hs
@@ -102,13 +102,13 @@
 weakenResolvingMove :: Prelude.Int -> ResolvingMove -> ResolvingMoveSet
 weakenResolvingMove maxReg x =
   case x of {
-   Move fr fv tr -> RSMove ( fr) fv ( tr);
-   Spill fr tv b -> RSSpill ( fr) tv b;
-   Restore fv tr b -> RSRestore fv ( tr) b;
-   AllocReg fv tr -> RSAllocReg fv ( tr);
-   FreeReg fr tv -> RSFreeReg ( fr) tv;
-   AssignReg fv tr -> RSAssignReg fv ( tr);
-   ClearReg fr tv -> RSClearReg ( fr) tv;
+   Move fr fv tr -> RSMove (Prelude.id fr) fv (Prelude.id tr);
+   Spill fr tv b -> RSSpill (Prelude.id fr) tv b;
+   Restore fv tr b -> RSRestore fv (Prelude.id tr) b;
+   AllocReg fv tr -> RSAllocReg fv (Prelude.id tr);
+   FreeReg fr tv -> RSFreeReg (Prelude.id fr) tv;
+   AssignReg fv tr -> RSAssignReg fv (Prelude.id tr);
+   ClearReg fr tv -> RSClearReg (Prelude.id fr) tv;
    AllocStack tv -> RSAllocStack tv;
    FreeStack fv -> RSFreeStack fv;
    Looped x0 -> RSLooped (weakenResolvingMove maxReg x0)}
diff --git a/LinearScan/Seq.hs b/LinearScan/Seq.hs
--- a/LinearScan/Seq.hs
+++ b/LinearScan/Seq.hs
@@ -241,3 +241,7 @@
     (iota ((Prelude.succ) m) n'))
     n
 
+flatten :: ([] ([] a1)) -> [] a1
+flatten =
+  Prelude.foldr (Prelude.++) []
+
diff --git a/LinearScan/Spill.hs b/LinearScan/Spill.hs
--- a/LinearScan/Spill.hs
+++ b/LinearScan/Spill.hs
@@ -60,12 +60,12 @@
                          SpillCondition -> Trace.SpillConditionT
 coq_SpillConditionToT maxReg sd uid i x =
   case x of {
-   NewToHandled -> Trace.NewToHandledT ( uid);
-   UnhandledToHandled -> Trace.UnhandledToHandledT ( uid);
-   ActiveToHandled xid reg -> Trace.ActiveToHandledT ( xid)
-    ( (unsafeCoerce reg));
-   InactiveToHandled xid reg -> Trace.InactiveToHandledT ( xid)
-    ( (unsafeCoerce reg))}
+   NewToHandled -> Trace.NewToHandledT (Prelude.id uid);
+   UnhandledToHandled -> Trace.UnhandledToHandledT (Prelude.id uid);
+   ActiveToHandled xid reg -> Trace.ActiveToHandledT (Prelude.id xid)
+    (Prelude.id (unsafeCoerce reg));
+   InactiveToHandled xid reg -> Trace.InactiveToHandledT (Prelude.id xid)
+    (Prelude.id (unsafeCoerce reg))}
 
 optimalSplitPosition :: Interval.IntervalDesc -> Prelude.Int -> Prelude.Int
                         -> Prelude.Int
@@ -257,7 +257,8 @@
                                                           maxReg sd)
                                                         (ScanState.intervals
                                                           maxReg sd) 
-                                                        ( i1_1))) ( uid)
+                                                        ( i1_1)))
+                                                    (Prelude.id uid) 
                                                     ( i1_0))
                                                   (ScanState.fixedIntervals
                                                     maxReg sd) us'
@@ -281,11 +282,12 @@
                                              _evar_0_3 = \_ _ -> Prelude.Left
                                               ((:)
                                               (Trace.ECannotModifyHandledInterval
-                                              ( uid)) e3)}
+                                              (Prelude.id uid)) e3)}
                                             in
                                             case Prelude.not
                                                    (Ssrbool.in_mem
-                                                     (unsafeCoerce ( uid))
+                                                     (unsafeCoerce
+                                                       (Prelude.id uid))
                                                      (Ssrbool.mem
                                                        (Seq.seq_predType
                                                          (Fintype.ordinal_eqType
@@ -320,7 +322,7 @@
                                                         maxReg sd)
                                                       (ScanState.intervals
                                                         maxReg sd) ( i1_1)))
-                                                  ( xid) ( i1_0))
+                                                  (Prelude.id xid) ( i1_0))
                                                 (ScanState.fixedIntervals
                                                   maxReg sd) unh'
                                                 (Prelude.map Prelude.id
@@ -361,11 +363,12 @@
                                              _evar_0_4 = \_ _ -> Prelude.Left
                                               ((:)
                                               (Trace.ECannotModifyHandledInterval
-                                              ( xid)) e3)}
+                                              (Prelude.id xid)) e3)}
                                             in
                                             case Prelude.not
                                                    (Ssrbool.in_mem
-                                                     (unsafeCoerce ( xid))
+                                                     (unsafeCoerce
+                                                       (Prelude.id xid))
                                                      (Ssrbool.mem
                                                        (Seq.seq_predType
                                                          (Fintype.ordinal_eqType
@@ -400,7 +403,7 @@
                                                         maxReg sd)
                                                       (ScanState.intervals
                                                         maxReg sd) ( i1_1)))
-                                                  ( xid) ( i1_0))
+                                                  (Prelude.id xid) ( i1_0))
                                                 (ScanState.fixedIntervals
                                                   maxReg sd) unh'
                                                 (Prelude.map Prelude.id
@@ -441,11 +444,12 @@
                                              _evar_0_5 = \_ _ -> Prelude.Left
                                               ((:)
                                               (Trace.ECannotModifyHandledInterval
-                                              ( xid)) e3)}
+                                              (Prelude.id xid)) e3)}
                                             in
                                             case Prelude.not
                                                    (Ssrbool.in_mem
-                                                     (unsafeCoerce ( xid))
+                                                     (unsafeCoerce
+                                                       (Prelude.id xid))
                                                      (Ssrbool.mem
                                                        (Seq.seq_predType
                                                          (Fintype.ordinal_eqType
@@ -575,7 +579,7 @@
              in
              let {
               _evar_0_1 = \_ -> Prelude.Left ((:)
-               (Trace.EIntervalBeginsBeforeUnhandled ( uid)) e)}
+               (Trace.EIntervalBeginsBeforeUnhandled (Prelude.id uid)) e)}
              in
              case (Prelude.<=) beg (Interval.ibeg d) of {
               Prelude.True -> _evar_0_0 __;
diff --git a/LinearScan/Split.hs b/LinearScan/Split.hs
--- a/LinearScan/Split.hs
+++ b/LinearScan/Split.hs
@@ -78,8 +78,8 @@
                           Prelude.Either ([] Trace.SSTrace)
                           ScanState.ScanStateSig
 splitUnhandledInterval maxReg sd uid beg us pos e =
-  (Prelude.flip (Prelude.$)) ((:) (Trace.ESplitUnhandledInterval ( uid)
-    (coq_SplitPositionToT pos)) e) (\e2 ->
+  (Prelude.flip (Prelude.$)) ((:) (Trace.ESplitUnhandledInterval
+    (Prelude.id uid) (coq_SplitPositionToT pos)) e) (\e2 ->
     let {
      _evar_0_ = \_nextInterval_ ints _fixedIntervals_ unh _active_ _inactive_ _handled_ uid0 us0 ->
       let {int = Vector0.vnth _nextInterval_ ints uid0} in
@@ -175,8 +175,8 @@
                             in
                             let {
                              _evar_0_0 = \_ _ -> Prelude.Left ((:)
-                              (Trace.ECannotModifyHandledInterval ( uid0))
-                              e2)}
+                              (Trace.ECannotModifyHandledInterval
+                              (Prelude.id uid0)) e2)}
                             in
                             case Prelude.not
                                    (Ssrbool.in_mem (unsafeCoerce uid0)
@@ -220,7 +220,7 @@
               let {_evar_0_2 = \_ -> Prelude.Right _top_assumption_} in
               let {
                _evar_0_3 = \_ -> Prelude.Left ((:)
-                (Trace.ENoValidSplitPosition ( uid0)) e)}
+                (Trace.ENoValidSplitPosition (Prelude.id uid0)) e)}
               in
               case (Prelude.<=) ((Prelude.succ) 0)
                      (Data.List.length
@@ -239,7 +239,7 @@
         in
         let {
          _evar_0_1 = \_ -> Prelude.Left ((:) (Trace.ENoValidSplitPosition
-          ( uid0)) e)}
+          (Prelude.id uid0)) e)}
         in
         case (Prelude.<=) beg (Interval.ibeg ( int)) of {
          Prelude.True -> _evar_0_0 __;
@@ -267,8 +267,8 @@
      _evar_0_0 = \_top_assumption_ ->
       let {
        _evar_0_0 = \uid beg us ->
-        (Prelude.flip (Prelude.$)) ((:) (Trace.ESplitCurrentInterval 
-          ( uid) (coq_SplitPositionToT pos)) e) (\e2 _ _ _ _ ->
+        (Prelude.flip (Prelude.$)) ((:) (Trace.ESplitCurrentInterval
+          (Prelude.id uid) (coq_SplitPositionToT pos)) e) (\e2 _ _ _ _ ->
           let {
            _evar_0_0 = \_nextInterval_ intervals0 fints unhandled0 _active_ _inactive_ _handled_ uid0 us0 _top_assumption_0 ->
             let {_evar_0_0 = \err -> Prelude.Left err} in
@@ -305,7 +305,7 @@
                                  ([] Trace.SSTrace) ScanState.ScanStateSig
 splitActiveOrInactiveInterval maxReg sd uid beg us xid pos reg hin e =
   (Prelude.flip (Prelude.$)) ((:) (Trace.ESplitActiveOrInactiveInterval
-    ( xid)
+    (Prelude.id xid)
     (case hin of {
       Prelude.Left _ -> Prelude.True;
       Prelude.Right _ -> Prelude.False}) (coq_SplitPositionToT pos)) e)
@@ -361,8 +361,8 @@
                               in
                               let {
                                _evar_0_0 = \_ _ -> Prelude.Left ((:)
-                                (Trace.ECannotModifyHandledInterval ( xid0))
-                                e2)}
+                                (Trace.ECannotModifyHandledInterval
+                                (Prelude.id xid0)) e2)}
                               in
                               case Prelude.not
                                      (Ssrbool.in_mem (unsafeCoerce xid0)
@@ -420,7 +420,7 @@
           in
           let {
            _evar_0_1 = \_ -> Prelude.Left ((:) (Trace.ENoValidSplitPosition
-            ( xid0)) e2)}
+            (Prelude.id xid0)) e2)}
           in
           case (Prelude.<=) beg (Interval.ibeg ( int)) of {
            Prelude.True -> _evar_0_0 __;
@@ -473,8 +473,8 @@
               let {
                _evar_0_1 = \aid aids iHaids ->
                 (Prelude.flip (Prelude.$)) ((:)
-                  (Trace.ESplitAssignedIntervalForReg ( aid) ( reg)
-                  (coq_SplitPositionToT pos)) e) (\e2 ->
+                  (Trace.ESplitAssignedIntervalForReg (Prelude.id aid)
+                  (Prelude.id reg) (coq_SplitPositionToT pos)) e) (\e2 ->
                   let {
                    _evar_0_1 = \_ ->
                     let {
@@ -524,11 +524,11 @@
                                         (ScanState.nextInterval maxReg
                                           _top_assumption_3))
                                       (Fintype.ordinal_eqType maxReg))
-                                    (unsafeCoerce ((,) ( aid) reg))
+                                    (unsafeCoerce ((,) (Prelude.id aid) reg))
                                     (unsafeCoerce
                                       (ScanState.active maxReg
                                         _top_assumption_3)))) ((:) ((,)
-                                ( aid) reg)
+                                (Prelude.id aid) reg)
                                 (ScanState.inactive maxReg _top_assumption_3))
                                 (ScanState.handled maxReg _top_assumption_3)}
                               in
@@ -547,7 +547,8 @@
                            in
                             _evar_0_3 __}
                          in
-                         case Ssrbool.in_mem (unsafeCoerce ((,) ( aid) reg))
+                         case Ssrbool.in_mem
+                                (unsafeCoerce ((,) (Prelude.id aid) reg))
                                 (Ssrbool.mem
                                   (Seq.seq_predType
                                     (Eqtype.prod_eqType
@@ -568,7 +569,7 @@
                   in
                   let {
                    _evar_0_2 = \_ -> Prelude.Left ((:)
-                    (Trace.ECannotSplitSingleton ( aid)) e2)}
+                    (Trace.ECannotSplitSingleton (Prelude.id aid)) e2)}
                   in
                   case (Prelude.<=) beg
                          (splitPosition
@@ -608,7 +609,7 @@
                              PhysReg -> Prelude.Int -> Morph.SState () 
                              () ()
 splitActiveIntervalForReg maxReg pre reg pos =
-  Context.context (Trace.ESplitActiveIntervalForReg ( reg)
+  Context.context (Trace.ESplitActiveIntervalForReg (Prelude.id reg)
     (coq_SplitPositionToT (BeforePos pos)))
     (splitAssignedIntervalForReg maxReg pre reg (BeforePos pos) Prelude.True)
 
@@ -617,7 +618,8 @@
                                   () () ()
 splitAnyInactiveIntervalForReg maxReg pre reg pos e ss =
   (Prelude.flip (Prelude.$)) ((:) (Trace.ESplitAnyInactiveIntervalForReg
-    ( reg) (coq_SplitPositionToT (EndOfLifetimeHole pos))) e) (\e2 ->
+    (Prelude.id reg) (coq_SplitPositionToT (EndOfLifetimeHole pos))) e)
+    (\e2 ->
     (Prelude.flip (Prelude.$)) (\s ->
       splitAssignedIntervalForReg maxReg s reg (EndOfLifetimeHole pos)
         Prelude.False) (\_top_assumption_ ->
diff --git a/LinearScan/Verify.hs b/LinearScan/Verify.hs
--- a/LinearScan/Verify.hs
+++ b/LinearScan/Verify.hs
@@ -297,8 +297,8 @@
            (unsafeCoerce alloc) (unsafeCoerce reg)) of {
    Prelude.True ->
     errorT maxReg mDict pc (AllocationDoesNotMatch var
-      (reg)
-      (alloc) pos idx);
+      (Maybe.option_map (Maybe.option_map Prelude.id) reg)
+      (Maybe.option_map (Maybe.option_map Prelude.id) alloc) pos idx);
    Prelude.False -> Applicative.pure (State0.coq_StateT_Applicative mDict) ()}
 
 reserveReg :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId -> PhysReg ->
@@ -326,11 +326,12 @@
             (Prelude.not
               (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce v)
                 (unsafeCoerce var)))
-            (errorT maxReg mDict pc (RegAlreadyReservedToVar ( reg) v var));
+            (errorT maxReg mDict pc (RegAlreadyReservedToVar (Prelude.id reg)
+              v var));
          Prelude.Nothing ->
           Applicative.pure (State0.coq_StateT_Applicative mDict) ()}})
       (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict))
-    (addMove maxReg mDict pc (Resolve.RSAllocReg var ( reg)))
+    (addMove maxReg mDict pc (Resolve.RSAllocReg var (Prelude.id reg)))
 
 isReserved :: Prelude.Int -> (Monad.Monad a1) -> PhysReg -> Verified 
               a1 a2 (Prelude.Maybe Blocks.VarId)
@@ -346,7 +347,7 @@
 checkReservation maxReg mDict pc reg var =
   Monad.bind (State0.coq_StateT_Monad mDict) (\st ->
     let {
-     err = errorT maxReg mDict pc (VarNotReservedForReg var ( reg)
+     err = errorT maxReg mDict pc (VarNotReservedForReg var (Prelude.id reg)
              (Lens.view (Lens.stepdownl' (\_ -> reservation))
                (Vector0.vnth maxReg (rsAllocs maxReg st) reg))
              ((Prelude.succ) 0))}
@@ -377,12 +378,12 @@
               (Lens.set (\_ -> reservation) Prelude.Nothing))
             (rsStack maxReg st))) mDict;
        Prelude.Nothing ->
-        errorT maxReg mDict pc (VarNotReservedForReg var ( reg)
+        errorT maxReg mDict pc (VarNotReservedForReg var (Prelude.id reg)
           (Lens.view (Lens.stepdownl' (\_ -> reservation))
             (Vector0.vnth maxReg (rsAllocs maxReg st) reg)) ((Prelude.succ)
           ((Prelude.succ) 0)))})
       (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict))
-    (addMove maxReg mDict pc (Resolve.RSFreeReg ( reg) var))
+    (addMove maxReg mDict pc (Resolve.RSFreeReg (Prelude.id reg) var))
 
 clearReg :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId -> UseVerifier ->
             PhysReg -> Blocks.VarId -> Verified a1 a2 ()
@@ -402,7 +403,8 @@
             (rsStack maxReg st))) mDict;
        Prelude.Nothing ->
         let {
-         err = errorT maxReg mDict pc (VarNotResidentForReg var ( reg)
+         err = errorT maxReg mDict pc (VarNotResidentForReg var
+                 (Prelude.id reg)
                  (Lens.view (Lens.stepdownl' (\_ -> residency))
                    (Vector0.vnth maxReg (rsAllocs maxReg st) reg))
                  ((Prelude.succ) ((Prelude.succ) 0)))}
@@ -416,7 +418,7 @@
            Prelude.Nothing ->
             Applicative.pure (State0.coq_StateT_Applicative mDict) ()}}})
       (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict))
-    (addMove maxReg mDict pc (Resolve.RSClearReg ( reg) var))
+    (addMove maxReg mDict pc (Resolve.RSClearReg (Prelude.id reg) var))
 
 assignReg :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId -> UseVerifier ->
              PhysReg -> Blocks.VarId -> Verified a1 a2 ()
@@ -447,7 +449,8 @@
             (rsAllocs maxReg st));
        Prelude.Nothing ->
         let {
-         err = errorT maxReg mDict pc (VarNotReservedForReg var ( reg)
+         err = errorT maxReg mDict pc (VarNotReservedForReg var
+                 (Prelude.id reg)
                  (Lens.view (Lens.stepdownl' (\_ -> reservation))
                    (Vector0.vnth maxReg (rsAllocs maxReg st) reg))
                  ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) 0))))}
@@ -461,7 +464,7 @@
            Prelude.Nothing ->
             Applicative.pure (State0.coq_StateT_Applicative mDict) ()}}})
       (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict))
-    (addMove maxReg mDict pc (Resolve.RSAssignReg var ( reg)))
+    (addMove maxReg mDict pc (Resolve.RSAssignReg var (Prelude.id reg)))
 
 isResident :: Prelude.Int -> (Monad.Monad a1) -> PhysReg -> Verified 
               a1 a2 (Prelude.Maybe Blocks.VarId)
@@ -479,8 +482,8 @@
   Monad.bind (State0.coq_StateT_Monad mDict) (\st ->
     Monad.bind (State0.coq_StateT_Monad mDict) (\res ->
       let {
-       err = errorT maxReg mDict pc (VarNotResidentForReg var ( reg) res
-               ((Prelude.succ) 0))}
+       err = errorT maxReg mDict pc (VarNotResidentForReg var
+               (Prelude.id reg) res ((Prelude.succ) 0))}
       in
       case useVerifier of {
        VerifyEnabledStrict ->
@@ -649,7 +652,8 @@
             case Lens.view (Lens.stepdownl' (\_ -> reservation))
                    (Vector0.vnth maxReg (rsAllocs maxReg st) reg) of {
              Prelude.Just v ->
-              errorT maxReg mDict pc (PhysRegAlreadyReservedForVar ( reg) v);
+              errorT maxReg mDict pc (PhysRegAlreadyReservedForVar
+                (Prelude.id reg) v);
              Prelude.Nothing ->
               case Prelude.filter (\i ->
                      Eqtype.eq_op
@@ -663,7 +667,7 @@
                 errorT maxReg mDict pc (AllocationDoesNotMatch
                   (Interval.ivar (Allocate.intVal maxReg x)) Prelude.Nothing
                   (Prelude.Just
-                  ((Allocate.intReg maxReg x)))
+                  (Maybe.option_map Prelude.id (Allocate.intReg maxReg x)))
                   (Prelude.pred pc) 0)}})
             (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict));
        Prelude.Right var ->
@@ -708,7 +712,8 @@
             case Lens.view (Lens.stepdownl' (\_ -> reservation))
                    (Vector0.vnth maxReg (rsAllocs maxReg st) reg) of {
              Prelude.Just v ->
-              errorT maxReg mDict pc (PhysRegAlreadyReservedForVar ( reg) v);
+              errorT maxReg mDict pc (PhysRegAlreadyReservedForVar
+                (Prelude.id reg) v);
              Prelude.Nothing ->
               case Prelude.filter (\i ->
                      Eqtype.eq_op
@@ -722,7 +727,7 @@
                 errorT maxReg mDict pc (AllocationDoesNotMatch
                   (Interval.ivar (Allocate.intVal maxReg x)) Prelude.Nothing
                   (Prelude.Just
-                  ((Allocate.intReg maxReg x)))
+                  (Maybe.option_map Prelude.id (Allocate.intReg maxReg x)))
                   (Prelude.pred pc) 0)}})
             (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict));
        Prelude.Right var ->
diff --git a/linearscan.cabal b/linearscan.cabal
--- a/linearscan.cabal
+++ b/linearscan.cabal
@@ -1,5 +1,5 @@
 name:          linearscan
-version:       0.11
+version:       0.11.1
 synopsis:      Linear scan register allocator, formally verified in Coq
 homepage:      http://github.com/jwiegley/linearscan
 license:       BSD3
@@ -60,20 +60,19 @@
     LinearScan.Build
     LinearScan.Choice
     LinearScan.Class
-    LinearScan.Context
     LinearScan.Const
+    LinearScan.Context
+    LinearScan.Contravariant
     LinearScan.Cursor
     LinearScan.Datatypes
-    -- LinearScan.Either
-    -- LinearScan.Either0
     LinearScan.Eqtype
     LinearScan.Fintype
     LinearScan.Functor
     LinearScan.Graph
     LinearScan.Identity
+    LinearScan.Interval
     LinearScan.IntMap
     LinearScan.IntSet
-    LinearScan.Interval
     LinearScan.Lens
     LinearScan.Lib
     LinearScan.List0