diff --git a/generics-mrsop-gdiff.cabal b/generics-mrsop-gdiff.cabal
--- a/generics-mrsop-gdiff.cabal
+++ b/generics-mrsop-gdiff.cabal
@@ -1,37 +1,42 @@
-name:                generics-mrsop-gdiff
+-- This file has been generated from package.yaml by hpack version 0.28.2.
+--
+-- see: https://github.com/sol/hpack
+--
+-- hash: 0efe06cb6c261c979c1bb69945d291c4d6d3d9eae84840801fabae96a8592ee2
 
--- The package version.  See the Haskell package versioning policy (PVP) 
--- for standards guiding when and how versions should be incremented.
--- https://wiki.haskell.org/Package_versioning_policy
--- PVP summary:      +------- breaking API changes
---                   | +----- non-breaking API additions
---                   | | +--- code changes with no API change
-version:             0.0.1
-license:             BSD3
-license-file:        LICENSE
-synopsis:            Reimplementation of the `gdiff` algorithm for `generics-mrsop`
-description:         Here we port the gdiff algorithm and library to work over the generics-mrsop, enabling code that relies on the later library to access the gdiff algorithm. 
-author:              Arian van Putten and Victor Miraldo
-maintainer:          arian.vanputten@gmail.com v.cacciarimiraldo@gmail.com
-category:            Generics
-build-type:          Simple
-cabal-version:       >=1.10
+name:           generics-mrsop-gdiff
+version:        0.0.2
+synopsis:       Reimplementation of the gdiff algorithm for generics-mrsop
+description:    Here we port the gdiff algorithm and library to work over the generics-mrsop, enabling code that relies on the later library to access the gdiff algorithm. Moreover, we also bring in the utilities for converting a gdiff patch into a more structured version, facilitating merging. For some literature on the topic check Arian's MSc thesis at <https://dspace.library.uu.nl/handle/1874/380853> or our TyDe 2017 paper at <https://victorcmiraldo.github.io/data/tyde2017.pdf>.
+category:       Generics
+homepage:       https://github.com/VictorCMiraldo/generics-mrsop-gdiff#readme
+bug-reports:    https://github.com/VictorCMiraldo/generics-mrsop-gdiff/issues
+author:         Arian van Putten and Victor Miraldo
+maintainer:     Victor Miraldo <v.cacciarimiraldo@gmail.com>
+license:        BSD3
+license-file:   LICENSE
+build-type:     Simple
+cabal-version:  >= 1.10
 
-library
-  ghc-options:
-    -O2 -Wall
+source-repository head
+  type: git
+  location: https://github.com/VictorCMiraldo/generics-mrsop-gdiff
 
-  exposed-modules: 
-    Generics.MRSOP.GDiff
-    Generics.MRSOP.GDiff.Util
- 
-  -- Other library packages from which modules are imported.
-  build-depends:       base < 5,
-                       generics-mrsop >= 2.2.0
-  
-  -- Directories containing source files.
-  hs-source-dirs:      src
-  
-  -- Base language which the package is written in.
-  default-language:    Haskell2010
-  
+library
+  exposed-modules:
+      Generics.MRSOP.GDiff
+      Generics.MRSOP.GDiff.Util
+      Generics.MRSOP.STDiff
+      Generics.MRSOP.STDiff.Compute
+      Generics.MRSOP.STDiff.Enum
+      Generics.MRSOP.STDiff.Merge
+      Generics.MRSOP.STDiff.Types
+  other-modules:
+      Paths_generics_mrsop_gdiff
+  hs-source-dirs:
+      src/
+  ghc-options: -Wall
+  build-depends:
+      base >=4.9 && <5
+    , generics-mrsop >=2.3.0
+  default-language: Haskell2010
diff --git a/src/Generics/MRSOP/GDiff.hs b/src/Generics/MRSOP/GDiff.hs
--- a/src/Generics/MRSOP/GDiff.hs
+++ b/src/Generics/MRSOP/GDiff.hs
@@ -1,4 +1,3 @@
-{-# LANGUAGE QuantifiedConstraints #-}
 {-# LANGUAGE PolyKinds            #-}
 {-# LANGUAGE FlexibleContexts     #-}
 {-# LANGUAGE DataKinds            #-}
@@ -17,7 +16,7 @@
 --
 module Generics.MRSOP.GDiff
   ( Cof(..)
-  , cofIdx , cofWitnessI , cofHeq
+  , cofIdx , cofWitnessI , cofHeq , matchCof
   , ES(..)
   , apply, apply' , applyES
   , diff , diff'
@@ -71,7 +70,7 @@
 cofHeq (ConstrK x) (ConstrK y) =
   case testEquality x y of
     Just Refl ->
-      if x == y
+      if eqHO x y
         then Just (Refl, Refl)
         else Nothing
     Nothing -> Nothing
@@ -255,7 +254,7 @@
          -> NA ki (Fix ki codes) a
          -> Maybe (PoA ki (Fix ki codes) t)
 matchCof (ConstrI c1 _) (NA_I (Fix x)) = match c1 x
-matchCof (ConstrK k) (NA_K k2) = guard (k == k2) >> Just Nil
+matchCof (ConstrK k) (NA_K k2) = guard (eqHO k k2) >> Just Nil
 
 -- we need to give Haskell a bit of a hint that Tyof codes c reduces to an IsList
 -- insCof is also really the only place where we _need_ IsList I think
@@ -328,7 +327,7 @@
 -- hence, we can not get the datatype info
 showCof :: forall ki fam codes a c.
      (HasDatatypeInfo ki fam codes, ShowHO ki) => Cof ki codes a c -> String
-showCof (ConstrK k) = show k
+showCof (ConstrK k) = showHO k
 showCof x@(ConstrI c _) = constructorName . constrInfoLkup c $ datatypeInfo (Proxy @fam) (cofIdx x)
 
 instance (HasDatatypeInfo ki fam codes, ShowHO ki) =>
diff --git a/src/Generics/MRSOP/GDiff/Util.hs b/src/Generics/MRSOP/GDiff/Util.hs
--- a/src/Generics/MRSOP/GDiff/Util.hs
+++ b/src/Generics/MRSOP/GDiff/Util.hs
@@ -1,9 +1,9 @@
-{-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeOperators   #-}
+{-# LANGUAGE TypeFamilies    #-}
+{-# LANGUAGE DataKinds       #-}
+{-# LANGUAGE GADTs           #-}
 {-# LANGUAGE ConstraintKinds #-}
-{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE PolyKinds       #-}
 
 -- | For the lack of a better name, here we put random stuff
 module Generics.MRSOP.GDiff.Util where
diff --git a/src/Generics/MRSOP/STDiff.hs b/src/Generics/MRSOP/STDiff.hs
new file mode 100644
--- /dev/null
+++ b/src/Generics/MRSOP/STDiff.hs
@@ -0,0 +1,104 @@
+{-# LANGUAGE ViewPatterns          #-}
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE RankNTypes            #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
+{-# LANGUAGE TypeApplications      #-}
+{-# LANGUAGE PolyKinds             #-}
+{-# LANGUAGE GADTs                 #-}
+module Generics.MRSOP.STDiff
+  ( module Generics.MRSOP.STDiff.Types
+  , apply , merge , diff
+  ) where
+
+import Data.Proxy
+import Data.Type.Equality hiding (apply)
+import Control.Monad
+import Generics.MRSOP.Base
+
+import Generics.MRSOP.STDiff.Types
+import Generics.MRSOP.STDiff.Merge
+import Generics.MRSOP.STDiff.Compute
+
+
+applyAt :: EqHO ki
+        => (At ki codes :*: NA ki (Fix ki codes)) a
+        -> Either String (NA ki (Fix ki codes) a)
+applyAt (AtSet (Trivial a' b) :*: NA_K a)  
+  | eqHO a' b  = pure (NA_K a)
+  | eqHO a' a  = pure (NA_K b)
+  | otherwise = Left "atom"
+applyAt (AtFix x :*: NA_I x') = NA_I <$> applyAlmu x x'
+
+applyAl
+  :: EqHO ki
+  => Al ki codes xs ys
+  -> PoA ki (Fix ki codes) xs
+  -> Either String (PoA ki (Fix ki codes) ys)
+applyAl A0 Nil = return Nil
+applyAl (AX dx dxs) (x :* xs) =
+  (:*) <$> applyAt (dx :*: x) <*> applyAl dxs xs
+applyAl (AIns x dxs) xs =
+  (x :*) <$> applyAl dxs xs 
+applyAl (ADel x dxs) (x' :* xs) =
+  if eqHO x x' then applyAl dxs xs else Left "al del"
+  -- applyAl dxs xs
+
+testEquality' :: (TestEquality f)
+              => f a -> f b -> Either String (a :~: b)
+testEquality' x y = case testEquality x y of
+  Just r -> Right r
+  Nothing -> Left "err"
+
+applySpine 
+  :: EqHO ki
+  => SNat ix
+  -> SNat iy
+  -> Spine ki codes (Lkup ix codes) (Lkup iy codes)
+  -> Rep ki (Fix ki codes) (Lkup ix codes)
+  -> Either String (Rep ki (Fix ki codes) (Lkup iy codes))
+applySpine _ _ Scp x = return x
+applySpine ix iy (SCns c1 dxs) (sop -> Tag c2 xs) =  do
+  Refl <- testEquality' ix iy
+  Refl <- testEquality' c1 c2
+  inj c2 <$> (mapNPM applyAt (zipNP dxs xs))
+applySpine _ _ (SChg c1 c2 al) (sop -> Tag c3 xs) = do
+  Refl <- testEquality' c1 c3
+  inj c2 <$> applyAl al xs
+
+insCtx
+  :: (IsNat ix, EqHO ki)
+  => InsCtx ki codes ix xs
+  -> Fix ki codes ix
+  -> Either String (PoA ki (Fix ki codes) xs)
+insCtx (H x x2) x1 = (\xi -> NA_I xi :* x2) <$> applyAlmu x x1
+insCtx (T x x2) x1 = (x :*) <$> insCtx x2 x1
+
+delCtx
+  :: (EqHO ki, IsNat ix)
+  => DelCtx ki codes ix xs
+  -> PoA ki (Fix ki codes) xs
+  -> Either String (Fix ki codes ix)
+delCtx (H spu _) (NA_I x :* _) = applyAlmu (unAlmuMin spu) x
+delCtx (T _ al)  (_ :* p)      = delCtx al p
+
+applyAlmu 
+  :: forall ki codes ix iy. (IsNat ix, IsNat iy, EqHO ki)
+  => Almu ki codes ix iy
+  -> Fix ki codes ix
+  -> Either String (Fix ki codes iy)
+applyAlmu (Spn spine) (Fix rep) = Fix <$> applySpine (getSNat (Proxy @ix)) (getSNat (Proxy @iy)) spine rep
+applyAlmu (Ins c ctx) f@(Fix _) = Fix . inj c <$> insCtx ctx f
+applyAlmu (Del c ctx) (Fix rep) = delCtx ctx <=< m2e . match c $ rep
+  where
+    m2e Nothing  = Left (show "del")
+    m2e (Just r) = Right r
+
+-- |Applies a patch to an element
+apply :: forall ki codes ix iy
+       . (IsNat ix, IsNat iy, EqHO ki)
+      => Almu ki codes ix iy
+      -> Fix ki codes ix
+      -> Maybe (Fix ki codes iy)
+apply almu x = case applyAlmu almu x of
+                 Left  _ -> Nothing
+                 Right y -> Just y
diff --git a/src/Generics/MRSOP/STDiff/Compute.hs b/src/Generics/MRSOP/STDiff/Compute.hs
new file mode 100644
--- /dev/null
+++ b/src/Generics/MRSOP/STDiff/Compute.hs
@@ -0,0 +1,365 @@
+{-# LANGUAGE ViewPatterns          #-}
+{-# LANGUAGE PolyKinds             #-}
+{-# LANGUAGE FlexibleContexts      #-}
+{-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE TypeFamilies          #-}
+{-# LANGUAGE ConstraintKinds       #-}
+{-# LANGUAGE TypeApplications      #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE RankNTypes            #-}
+{-# LANGUAGE GADTs                 #-}
+module Generics.MRSOP.STDiff.Compute where
+
+import Data.Function (on)
+import Data.Ord      (comparing)
+import Data.List     (maximumBy)
+import Data.Coerce
+import Data.Proxy
+import Data.Type.Equality
+import Data.Functor.Const
+
+import Generics.MRSOP.Base
+import Generics.MRSOP.AG
+
+import qualified Generics.MRSOP.GDiff as GDiff
+import           Generics.MRSOP.GDiff.Util
+import           Generics.MRSOP.STDiff.Types
+
+import Data.Maybe (fromJust)
+
+-- * Annotating Trees
+--
+-- $annotating
+--
+-- First we use /gdiff/ to annotate the source and destination
+-- forests before translating them to a 'Generics.MRSOP.STDiff.Almu'
+-- The idea being that the information comming from /gdiff/ is sufficient
+-- to know which constructors are copies and which have been modified.
+
+-- |Annotations to be placed throughout the tree.
+data Ann = Modify | Copy deriving Show
+
+-- |Adds an annotated constructor to a product of atoms.
+injCofAnn :: GDiff.Cof ki codes a t
+          -> Const ann ix
+          -> PoA ki (AnnFix ki codes (Const ann)) t
+          -> NA ki (AnnFix ki codes (Const ann)) a
+injCofAnn (GDiff.ConstrI c _) ann xs = NA_I (AnnFix (coerce ann) $ inj c xs)
+injCofAnn (GDiff.ConstrK k)   _   _  = NA_K k
+
+-- |Inserts an annotated constructor at the head of a
+-- product of atoms.
+insCofAnn :: GDiff.Cof ki codes a t
+          -> Const ann ix
+          -> PoA ki (AnnFix ki codes (Const ann)) (t :++: as)
+          -> PoA ki (AnnFix ki codes (Const ann)) (a ': as)
+insCofAnn (GDiff.ConstrK k)     _   xs = NA_K k :* xs
+insCofAnn (GDiff.ConstrI c prf) ann xs =
+  let (xs0, xs1) = split prf xs
+   in  injCofAnn (GDiff.ConstrI c prf) ann xs0 :* xs1
+
+{-
+ - In Agda, it would be the following. However, I'm not sure
+ - it is possible to carry around the IsJust constraint in Haskell
+ - hence, we will be partial instead
+ -  ann-source : ∀{txs tys}(xs : ⟦ txs ⟧A*)(p : ES txs tys)
+ -           → (hip : IsJust (applyES p xs))
+ -           → ⟦ txs ⟧Aₐ*
+ -
+ - However, it's morally total if you know beforehand that the
+ - patch is gonna apply. Which we know by construction everywhere we use this
+ - , so we can just `fromJust` it where appropriate
+ -
+ - WARNING: Morally dubious, but we know that this edit script was
+ - generated hte same time as the datatype, so it should never
+ - fail to apply
+ -
+ - TODO: Actually make it return Maybe and be honest
+ -}
+
+-- |Annotates the source of an edit script.
+annSrc :: (EqHO ki , IsNat ix)
+       => Fix ki codes ix -- ^ 
+       -> GDiff.ES ki codes '[ 'I ix] ys
+       -> AnnFix ki codes (Const Ann) ix
+annSrc x0 es0 = case annSrc' (NA_I x0 :* Nil) es0 of
+                  (NA_I y :* Nil) -> y
+  where
+    annSrc' :: EqHO ki
+        => PoA ki (Fix ki codes) xs
+        -> GDiff.ES ki codes xs ys
+        -> PoA ki (AnnFix ki codes (Const Ann)) xs
+    annSrc' _  GDiff.ES0 = Nil
+    annSrc' Nil _  = Nil
+    annSrc' xs (GDiff.Ins _ _ es) = annSrc' xs es
+    annSrc' (x :* xs) (GDiff.Del _ c es) =
+      let poa = fromJust $ GDiff.matchCof c x
+       in insCofAnn c (Const Modify) (annSrc' (appendNP poa xs) es)
+    annSrc' (x :* xs) (GDiff.Cpy _ c es) =
+      let poa = fromJust $ GDiff.matchCof c x
+       in insCofAnn c (Const Copy) (annSrc' (appendNP poa xs) es)
+
+-- |Annotates the destination of an edit script.
+annDest :: (EqHO ki , IsNat ix)
+        => Fix ki codes ix -- ^ 
+        -> GDiff.ES ki codes xs '[ 'I ix]
+        -> AnnFix ki codes (Const Ann) ix
+annDest x0 es0 = case annDest' (NA_I x0 :* Nil) es0 of
+                   (NA_I y :* Nil) -> y
+  where
+    annDest' :: EqHO ki
+             => PoA ki (Fix ki codes) ys
+             -> GDiff.ES ki codes xs ys
+             -> PoA ki (AnnFix ki codes (Const Ann)) ys
+    annDest' _  GDiff.ES0 = Nil
+    annDest' Nil _  = Nil
+    annDest' (x :* xs) (GDiff.Del _ _ es) = annDest' (x :* xs) es
+    annDest' (x :* xs) (GDiff.Ins _ c es)
+     = let poa = fromJust $ GDiff.matchCof c x
+       in insCofAnn c (Const Modify) (annDest' (appendNP poa xs) es)
+    annDest' (x :* xs) (GDiff.Cpy _ c es) =
+      let poa = fromJust $ GDiff.matchCof c x
+       in insCofAnn c (Const Copy) (annDest' (appendNP poa xs) es)
+
+-- * Differencing Annotated Trees
+--
+-- $diffann
+--
+-- Once we have annotated the trees on the source and destination of the
+-- edit script, we can easily diff them in the /stdiff/ style.
+--
+
+-- ** Stiff Patches
+--
+-- $stiffpatches
+--
+-- We call a patch /stiff/ if it has no copies. It is trivial
+-- to produce sauch a patch given two elements. We simply delete
+-- the entire source and insert the entire destination.
+
+stiffAlmu :: (TestEquality ki, EqHO ki)
+          => Fix ki codes ix -- ^
+          -> Fix ki codes iy
+          -> Almu ki codes ix iy
+stiffAlmu (Fix rep1) (Fix rep2) = Spn (stiffSpine rep1 rep2)
+
+stiffSpine :: (TestEquality ki, EqHO ki)
+           => Rep ki (Fix ki codes) xs -- ^ 
+           -> Rep ki (Fix ki codes) ys
+           -> Spine ki codes xs ys
+stiffSpine (sop -> Tag c1 p1) (sop -> Tag c2 p2) = SChg c1 c2 (stiffAl p1 p2)
+
+stiffAt :: (TestEquality ki, EqHO ki)
+        => NA ki (Fix ki codes) x -- ^ 
+        -> NA ki (Fix ki codes) x
+        -> At ki codes x
+stiffAt (NA_K x) (NA_K y) = AtSet (Trivial x y)
+stiffAt (NA_I x) (NA_I y) = AtFix (stiffAlmu x y)
+
+stiffAl :: (TestEquality ki, EqHO ki)
+        => PoA ki (Fix ki codes) xs -- ^
+        -> PoA ki (Fix ki codes) ys
+        -> Al ki codes xs ys
+stiffAl Nil Nil = A0
+stiffAl (x :* xs) Nil = ADel x (stiffAl xs Nil)
+stiffAl Nil (y :* ys) = AIns y (stiffAl Nil ys)
+stiffAl (x :* xs) (y :* ys) = 
+  case testEquality x y of
+    Just Refl -> AX (stiffAt x y) (stiffAl xs ys)
+    Nothing -> AIns y (ADel x (stiffAl xs ys))
+
+-- ** Copy Counting
+--
+-- $copycounting
+--
+-- In order to decide which path to follow from the roof to the
+-- leaves whenver we are faced with a choice, we will pre-compute
+-- the amount of copies present in each subtree.
+
+-- |Algebra for counting copies.
+copiesAlgebra :: Const Ann ix -- ^
+              -> Rep ki (Const Int) xs
+              -> Const Int ix
+copiesAlgebra (Const ann) r
+  = let inAnn = elimRep (const 0) getConst sum r
+     in Const $ case ann of
+                  Modify -> inAnn
+                  Copy   -> 1 + inAnn
+          
+
+-- |Annotates the tree with how many copies are underneath each node
+-- (inclusive with self)
+--
+-- > copies Copy = 1 + copies children
+-- > copies Modify = copies children
+--
+countCopies :: IsNat ix
+            => AnnFix ki codes (Const Ann) ix -- ^
+            -> AnnFix ki codes (Const Int :*: Const Ann) ix
+countCopies = synthesizeAnn (\ca r -> copiesAlgebra ca (mapRep getFst r) :*: ca)
+  where
+    getFst :: (a :*: b) x -> a x
+    getFst (x :*: _) = x
+
+-- |Returns whether or not a subtree constains any copies.
+hasCopies :: AnnFix ki codes (Const Int :*: chi) ix -> Bool
+hasCopies (AnnFix (Const x :*: _) _) = x > 0
+
+-- |Easily retrieves annotations
+myGetAnn :: (Const Int :*: Const Ann) x -> Ann
+myGetAnn (_ :*: Const ann) = ann
+
+myGetAnnAt :: NA ki (AnnFix ki codes (Const Int :*: Const Ann)) ('I x) -> Ann
+myGetAnnAt (NA_I (AnnFix ann _)) = myGetAnn ann
+
+-- |Easily retrieves annotations
+myGetCopies :: (Const Int :*: Const Ann) x -> Int
+myGetCopies (Const copies :*: _) = copies
+
+myForgetAnn :: NA ki (AnnFix ki codes (Const Int :*: Const Ann)) at
+            -> NA ki (Fix ki codes) at
+myForgetAnn = mapNA id forgetAnn
+
+-- ** Computing the Patch
+--
+-- $computing
+--
+-- Given trees annotated with information about each of their constructors
+-- and how many of those are supposed to be copied, we can finally
+-- deterministically translate two tress into a patch.
+
+data InsOrDel (ki :: kon -> *) (codes :: [[[Atom kon]]]) :: (Nat -> Nat -> *) -> * where
+  CtxIns :: InsOrDel ki codes (Almu ki codes)
+  CtxDel :: InsOrDel ki codes (AlmuMin ki codes)
+
+
+-- |Finds the element in the @PoA ... xs@ with the most copies
+-- and diff the given @AnnFix@.
+--
+-- PRECONDITION: The @PoA .. xs@ must contain at least one tree with
+--               a copy. Always guard this call with 'hasCopies'
+--
+--
+diffCtx :: forall ki codes p ix xs
+         . (EqHO ki, TestEquality ki, IsNat ix)
+        => InsOrDel ki codes p
+        -> AnnFix ki codes (Const Int :*: Const Ann) ix
+        -> PoA ki (AnnFix ki codes (Const Int :*: Const Ann)) xs
+        -> Ctx ki codes p ix xs
+diffCtx cid x xs
+ = let maxIdx  = fst $ maximumBy (comparing snd) zipped
+       zipped  = zip [0 .. ] elimmed
+       elimmed = elimNP (elimNA (const 0) (myGetCopies . getAnn)) xs
+    in drop' maxIdx xs
+  where
+      drop' :: Int
+            -> PoA ki (AnnFix ki codes (Const Int :*: Const Ann)) ys
+            -> Ctx ki codes p ix ys
+      drop' _ Nil = error "unreachable"
+      drop' 0 (NA_I y :* ys) =
+        case cid of
+          CtxIns -> H (diffAlmu x y)           (mapNP myForgetAnn ys)
+          CtxDel -> H (AlmuMin (diffAlmu y x)) (mapNP myForgetAnn ys)
+      drop' n (y :* ys) = T (myForgetAnn y) (drop' (n - 1) ys)
+
+-- | Takes two annotated trees, and produces a patch
+diffAlmu :: forall ki codes ix iy
+          . (EqHO ki, IsNat ix, IsNat iy, TestEquality ki)
+         => AnnFix ki codes (Const Int :*: Const Ann) ix -- ^ 
+         -> AnnFix ki codes (Const Int :*: Const Ann) iy
+         -> Almu ki codes ix iy
+diffAlmu x@(AnnFix ann1 rep1) y@(AnnFix ann2 rep2) =
+  case (myGetAnn ann1, myGetAnn ann2) of
+    (Copy, Copy) -> Spn (diffSpine (getSNat $ Proxy @ix) (getSNat $ Proxy @iy) rep1 rep2)
+    (Copy, Modify) -> 
+      if hasCopies y then diffIns x rep2 else stiffAlmu (forgetAnn x) (forgetAnn y)
+    (Modify, Copy) ->
+      if hasCopies x then diffDel rep1 y else stiffAlmu (forgetAnn x) (forgetAnn y)
+    (Modify, Modify) ->
+      if hasCopies x then diffDel rep1 y else stiffAlmu (forgetAnn x) (forgetAnn y)
+    where
+      diffIns :: AnnFix ki codes (Const Int :*: Const Ann) ix
+              -> Rep ki (AnnFix ki codes (Const Int :*: Const Ann)) (Lkup iy codes)
+              -> Almu ki codes ix iy
+      diffIns x1 rep = case sop rep of Tag c xs -> Ins c (diffCtx CtxIns x1 xs)
+
+      diffDel :: Rep ki (AnnFix ki codes (Const Int :*: Const Ann)) (Lkup ix codes)
+              -> AnnFix ki codes (Const Int :*: Const Ann) iy
+              -> Almu ki codes ix iy
+      diffDel rep x1 = case sop rep of Tag c xs -> Del c (diffCtx CtxDel x1 xs)
+
+-- | Takes two annotated 'Rep's, and produces a patch
+diffSpine :: forall ki codes ix iy
+           . (TestEquality ki, EqHO ki, IsNat ix, IsNat iy)
+          => SNat ix -- ^ We need these to identify the mutrec family 
+          -> SNat iy 
+          -> Rep ki (AnnFix ki codes (Const Int :*: Const Ann)) (Lkup ix codes)
+          -> Rep ki (AnnFix ki codes (Const Int :*: Const Ann)) (Lkup iy codes)
+          -> Spine ki codes (Lkup ix codes) (Lkup iy codes)
+diffSpine six siy s1@(sop -> Tag c1 p1) s2@(sop -> Tag c2 p2) =
+  case testEquality six siy of
+    Just Refl ->
+      if (eqHO `on` mapRep forgetAnn) s1 s2
+        then Scp
+        else case testEquality c1 c2 of
+                   Just Refl ->
+                     SCns c1 (mapNP (\(a :*: b) -> diffAt a b) (zipNP p1 p2))
+                   Nothing -> SChg c1 c2 (diffAl p1 p2)
+    Nothing -> SChg c1 c2 (diffAl p1 p2)
+
+
+diffAl :: forall ki codes xs ys
+        . (EqHO ki, TestEquality ki)
+       => PoA ki (AnnFix ki codes (Const Int :*: Const Ann)) xs -- ^
+       -> PoA ki (AnnFix ki codes (Const Int :*: Const Ann)) ys
+       -> Al ki codes xs ys
+diffAl Nil Nil = A0
+diffAl Nil (y :* ys) = AIns (mapNA id forgetAnn y) (diffAl Nil ys)
+diffAl (x :* xs) Nil = ADel (mapNA id forgetAnn x) (diffAl xs Nil)
+diffAl (x@(NA_K k1) :* xs) (y@(NA_K k2) :* ys) = 
+  case testEquality k1 k2 of
+    Just Refl -> AX (diffAt x y) (diffAl xs ys)
+    Nothing -> AIns (mapNA id forgetAnn y) (ADel (mapNA id forgetAnn x) (diffAl xs ys))
+diffAl (x@(NA_K _) :* xs) (y@(NA_I _) :* ys) = 
+  case myGetAnnAt y of
+    Modify -> AIns (mapNA id forgetAnn y) (diffAl (x :* xs) ys)
+    Copy -> ADel (mapNA id forgetAnn x) (diffAl xs (y :* ys))
+diffAl (x@(NA_I _) :* xs) (y@(NA_K _) :* ys) =
+  case myGetAnnAt x of
+    Modify -> ADel (mapNA id forgetAnn x) (diffAl xs (y :* ys))
+    Copy -> AIns (mapNA id forgetAnn y) (diffAl (x :* xs) ys)
+diffAl (x@(NA_I _) :* xs) (y@(NA_I _) :* ys) = 
+  case (myGetAnnAt x, myGetAnnAt y) of
+    (Modify, _) -> ADel (mapNA id forgetAnn x) (diffAl xs (y :* ys))
+    (Copy, Modify) -> AIns (mapNA id forgetAnn y) (diffAl (x :* xs) ys)
+    (Copy, Copy) -> 
+      case testEquality x y of
+        Just Refl -> AX (diffAt x y) (diffAl xs ys)
+        -- NOTE we added this case
+        Nothing -> AIns (mapNA id forgetAnn y) (ADel (mapNA id forgetAnn x) (diffAl xs ys))
+
+diffAt :: (EqHO ki, TestEquality ki)
+       => NA ki (AnnFix ki codes (Const Int :*: Const Ann)) a -- ^
+       -> NA ki (AnnFix ki codes (Const Int :*: Const Ann)) a
+       -> At ki codes a
+diffAt (NA_K x) (NA_K y) = AtSet (Trivial x y)
+diffAt (NA_I x) (NA_I y) = AtFix $ diffAlmu x y
+
+-- |The interface function which witnesses thecomplete pipeline.
+-- its implementation is straightforward:
+--
+-- > diff x y = let es = GDiff.diff' x y
+-- >                ax = countCopies $ annSrc  x es
+-- >                ay = countCopies $ annDest y es
+-- >             in diffAlmu ax ay
+--
+diff :: (EqHO ki , TestEquality ki , IsNat ix)
+     => Fix ki codes ix -- ^
+     -> Fix ki codes ix
+     -> Almu ki codes ix ix
+diff x y = let es = GDiff.diff' x y
+               ax = countCopies $ annSrc  x es
+               ay = countCopies $ annDest y es
+            in diffAlmu ax ay
+
diff --git a/src/Generics/MRSOP/STDiff/Enum.hs b/src/Generics/MRSOP/STDiff/Enum.hs
new file mode 100644
--- /dev/null
+++ b/src/Generics/MRSOP/STDiff/Enum.hs
@@ -0,0 +1,94 @@
+{-# LANGUAGE ViewPatterns          #-}
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE PolyKinds             #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
+{-# LANGUAGE GADTs                 #-}
+module Generics.MRSOP.STDiff.Enum (enumAlmu) where
+
+import Control.Monad
+import Control.Applicative
+import Data.Type.Equality
+
+import Generics.MRSOP.Base
+import Generics.MRSOP.STDiff.Types
+
+enumAt :: (MonadPlus m , TestEquality ki , EqHO ki)
+       => NA ki (Fix ki codes) at
+       -> NA ki (Fix ki codes) at
+       -> m (At ki codes at)
+enumAt (NA_I x) (NA_I y) = AtFix <$> enumAlmu x y
+enumAt (NA_K x) (NA_K y) = return $ AtSet (Trivial x y)
+
+enumAl :: (MonadPlus m , TestEquality ki , EqHO ki)
+       => PoA ki (Fix ki codes) p1
+       -> PoA ki (Fix ki codes) p2
+       -> m (Al ki codes p1 p2)
+enumAl Nil Nil = return A0
+enumAl (x :* xs) Nil = ADel x <$> enumAl xs Nil
+enumAl Nil (y :* ys) = AIns y <$> enumAl Nil ys
+enumAl (x :* xs) (y :* ys)
+  =     (ADel x <$> enumAl xs (y :* ys))
+    <|> (AIns y <$> enumAl (x :* xs) ys)
+    <|> case testEquality x y of
+          Just Refl -> AX <$> (enumAt x y) <*> enumAl xs ys
+          Nothing   -> mzero
+
+enumSpn :: (MonadPlus m , TestEquality ki , EqHO ki)
+        => SNat ix -> SNat iy
+        -> Rep ki (Fix ki codes) (Lkup ix codes)
+        -> Rep ki (Fix ki codes) (Lkup iy codes)
+        -> m (Spine ki codes (Lkup ix codes) (Lkup iy codes))
+enumSpn six siy (sop -> Tag cx px) (sop -> Tag cy py)
+  = case testEquality six siy of
+      Nothing -> SChg cx cy <$> enumAl px py
+      Just Refl -> 
+        case testEquality cx cy of
+           Nothing   -> SChg cx cy <$> enumAl px py
+           Just Refl -> if eqHO px py
+                        then return Scp
+                        else SCns cx <$> mapNPM (uncurry' enumAt) (zipNP px py)
+
+enumDelCtx :: forall m ki codes iy prod
+            . (MonadPlus m , TestEquality ki , EqHO ki , IsNat iy)
+           => PoA ki (Fix ki codes) prod
+           -> Fix ki codes iy
+           -> m (DelCtx ki codes iy prod)
+enumDelCtx Nil            _ = mzero
+enumDelCtx (NA_K x :* xs) f = T (NA_K x) <$> enumDelCtx xs f
+enumDelCtx (NA_I x :* xs) f
+  = (flip H xs . AlmuMin) <$> enumAlmu x f
+    <|> T (NA_I x) <$> enumDelCtx xs f
+
+enumInsCtx :: forall m ki codes iy prod
+            . (MonadPlus m , TestEquality ki , EqHO ki , IsNat iy)
+           => Fix ki codes iy
+           -> PoA ki (Fix ki codes) prod
+           -> m (InsCtx ki codes iy prod)
+enumInsCtx _ Nil            = mzero
+enumInsCtx f (NA_K x :* xs) = T (NA_K x) <$> enumInsCtx f xs
+enumInsCtx f (NA_I x :* xs) 
+  = (flip H xs) <$> enumAlmu f x
+    <|> T (NA_I x) <$> enumInsCtx f xs 
+    
+-- |Enumerates all possible patches that transform a value into another
+-- on a @MonadPlus@ instance; /WARNING: this function has impractical runtime performance and should not be used!!/
+enumAlmu :: forall m ki codes ix iy
+          . (MonadPlus m , TestEquality ki , EqHO ki , IsNat ix , IsNat iy)
+         => Fix ki codes ix
+         -> Fix ki codes iy
+         -> m (Almu ki codes ix iy)
+enumAlmu x y
+  =    enumDel (sop $ unFix x) y
+   <|> enumIns x (sop $ unFix y)
+   <|> Spn <$> enumSpn (snatFixIdx x) (snatFixIdx y) (unFix x) (unFix y)
+  where
+    enumDel :: View ki (Fix ki codes) (Lkup ix codes)
+            -> Fix ki codes iy
+            -> m (Almu ki codes ix iy)
+    enumDel (Tag c p) y0 = Del c <$> enumDelCtx p y0
+
+    enumIns :: Fix ki codes ix
+            -> View ki (Fix ki codes) (Lkup iy codes)
+            -> m (Almu ki codes ix iy)
+    enumIns x0 (Tag c p) = Ins c <$> enumInsCtx x0 p
diff --git a/src/Generics/MRSOP/STDiff/Merge.hs b/src/Generics/MRSOP/STDiff/Merge.hs
new file mode 100644
--- /dev/null
+++ b/src/Generics/MRSOP/STDiff/Merge.hs
@@ -0,0 +1,187 @@
+{-# LANGUAGE RankNTypes            #-}
+{-# LANGUAGE TypeApplications      #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
+{-# LANGUAGE GADTs                 #-}
+{-# LANGUAGE PolyKinds             #-}
+module Generics.MRSOP.STDiff.Merge (merge) where
+
+import Data.Proxy
+import Data.Type.Equality
+import Control.Monad (guard)
+
+import Generics.MRSOP.Base
+
+import Generics.MRSOP.STDiff.Types
+
+mergeAt :: EqHO ki
+        => At ki codes a
+        -> At ki codes a
+        -> Maybe (At ki codes a)
+mergeAt  (AtSet (Trivial k1 k2)) (AtSet (Trivial k3 k4)) = 
+   if eqHO k1 k2
+   then pure $ AtSet $ Trivial k3 k4
+   else if eqHO k3 k4
+   then pure $ AtSet $ Trivial k3 k4
+   else Nothing
+mergeAt (AtFix x) (AtFix y) = AtFix <$> mergeAlmu x y
+
+mergeAtAl :: EqHO ki
+          => NP (At ki codes) xs
+          -> Al ki codes xs ys
+          -> Maybe (Al ki codes xs ys)
+mergeAtAl Nil A0 = pure A0
+mergeAtAl xs (AIns at al) = AIns at <$> mergeAtAl xs al
+mergeAtAl (x :* xs) (ADel at al)
+  | identityAt x = ADel at <$> mergeAtAl xs al
+  | otherwise    = Nothing
+mergeAtAl (x :* xs) (AX at al) = AX <$> (mergeAt x at)  <*> mergeAtAl xs al
+
+identityAt :: (EqHO ki) => At ki codes a -> Bool
+identityAt (AtFix (Spn Scp)) = True
+identityAt (AtSet (Trivial k1 k2)) = eqHO k1 k2
+identityAt _ = False
+
+makeIdAt :: NA ki (Fix ki codes) a -> At ki codes a
+makeIdAt (NA_I _) = AtFix (Spn Scp)
+makeIdAt (NA_K k) = AtSet (Trivial k k)
+
+mergeAlAt :: EqHO ki
+          => Al ki codes xs ys
+          -> NP (At ki codes) xs
+          -> Maybe (NP (At ki codes) ys)
+mergeAlAt A0 Nil = pure Nil
+mergeAlAt (AIns at al) xs = (makeIdAt at :*) <$> mergeAlAt al xs
+mergeAlAt (ADel _  al) (x :* xs)
+  | identityAt x = mergeAlAt al xs
+  | otherwise    = Nothing
+mergeAlAt (AX a al)   (x :* xs) = (:*) <$> mergeAt a x <*> mergeAlAt al xs
+
+
+mergeAts :: EqHO ki
+         => NP (At ki codes) xs
+         -> NP (At ki codes) xs
+         -> Maybe (NP (At ki codes) xs)
+mergeAts Nil Nil = pure Nil
+mergeAts (x :* xs) (y :* ys) = (:*) <$> mergeAt x y <*> mergeAts xs ys
+
+mergeSpine :: EqHO ki
+           => SNat ix
+           -> SNat iy
+           -> Spine ki codes (Lkup ix codes) (Lkup iy codes)
+           -> Spine ki codes (Lkup ix codes) (Lkup iy codes)
+           -> Maybe (Spine ki codes (Lkup ix codes) (Lkup iy codes))
+mergeSpine _ _ Scp s = pure s
+mergeSpine _ _ _ Scp = pure Scp
+mergeSpine _ _ (SCns cx xs) (SCns cy ys) = do
+  Refl <- testEquality cx cy
+  SCns cx <$> mergeAts xs ys
+mergeSpine _ _ (SCns cx xs) (SChg cy cz al) = do
+  Refl <- testEquality cx cy
+  SChg cy cz <$> mergeAtAl xs al
+mergeSpine ix iy (SChg cx cy al) (SCns cz zs) = do
+  Refl <- testEquality ix iy
+  Refl <- testEquality cx cz
+  SCns cy <$> mergeAlAt al zs
+mergeSpine _ _ SChg{} SChg{} = Nothing
+
+mergeCtxAt :: forall ki codes ix iy xs
+            . (EqHO ki, IsNat ix, IsNat iy) 
+           => DelCtx ki codes iy xs
+           -> NP (At ki codes) xs
+           -> Maybe (Almu ki codes ix iy)
+mergeCtxAt (H (AlmuMin almu') _) (AtFix almu :* xs) = do
+  Refl <- testEquality (almuDest almu) (almuDest almu')
+  x <- mergeAlmu almu' almu
+  Refl <- testEquality (almuSrc x) (getSNat (Proxy @ix))
+  guard (and $ elimNP identityAt xs)
+  pure x
+mergeCtxAt (T _ ctx) (x :* xs) = do
+  guard (identityAt x)
+  mergeCtxAt ctx xs
+
+mergeAtCtx :: (EqHO ki, IsNat iy)
+           => NP (At ki codes) xs
+           -> DelCtx ki codes iy xs
+           -> Maybe (DelCtx ki codes iy xs)
+mergeAtCtx (AtFix almu :* xs) (H (AlmuMin almu') rest) = do
+  Refl <- testEquality (almuDest almu) (almuDest almu')
+  almu'' <- mergeAlmu almu almu'
+  guard (and $ elimNP identityAt xs)
+  pure $ H  (AlmuMin almu'') rest
+mergeAtCtx (x :* xs) (T a  ctx) = do
+   guard (identityAt x)
+   T a  <$> mergeAtCtx xs ctx
+mergeAtCtx Nil _ = error "unreachable" -- check x's type to be sure!
+
+almuDest :: forall ix iy ki codes. IsNat iy => Almu ki codes ix iy -> SNat iy
+almuDest _ = getSNat (Proxy @iy)
+
+almuSrc :: forall ix iy ki codes. IsNat ix => Almu ki codes ix iy -> SNat ix
+almuSrc _ = getSNat (Proxy @ix)
+
+mergeCtxAlmu :: (EqHO ki, IsNat ix )
+             => InsCtx ki codes ix xs
+             -> Almu ki codes ix ix
+             -> Maybe (NP (At ki codes) xs)
+mergeCtxAlmu (H almu' rest) almu = do 
+  Refl <- testEquality (almuDest almu) (almuDest almu')
+  x <- AtFix <$> mergeAlmu almu' almu
+  pure $ x :* mapNP makeIdAt rest
+mergeCtxAlmu (T a    ctx) almu = 
+  (makeIdAt a :*) <$> mergeCtxAlmu ctx almu
+
+mergeAlmuCtx :: (EqHO ki, IsNat ix)
+             => Almu ki codes ix ix
+             -> InsCtx ki codes ix xs
+             -> Maybe (InsCtx ki codes ix xs)
+mergeAlmuCtx almu (H almu' rest) = do
+  Refl <- testEquality (almuDest almu) (almuDest almu')
+  almu'' <- mergeAlmu almu almu'
+  pure (H almu'' rest)
+mergeAlmuCtx almu (T a ctx) = T a <$> mergeAlmuCtx almu ctx
+
+mergeAlmu :: forall ki codes ix iy
+           . (EqHO ki, IsNat ix, IsNat iy)
+          => Almu ki codes ix iy
+          -> Almu ki codes ix iy
+          -> Maybe (Almu ki codes ix iy)
+mergeAlmu (Ins _ _) (Ins _ _) = Nothing
+mergeAlmu (Ins c1 s1) (Spn s2) =  do
+  Refl <- testEquality (getSNat (Proxy @ix)) (getSNat (Proxy @iy))
+  Spn . SCns c1 <$> mergeCtxAlmu s1 (Spn s2)
+mergeAlmu (Ins c1 s1) (Del c2 s2) = do
+  Refl <- testEquality (getSNat (Proxy @ix)) (getSNat (Proxy @iy))
+  Spn . SCns c1 <$> mergeCtxAlmu s1 (Del c2 s2)
+mergeAlmu (Spn s1) (Ins c2 s2) = do
+  Refl <- testEquality (getSNat (Proxy @ix)) (getSNat (Proxy @iy))
+  Ins c2 <$> (mergeAlmuCtx (Spn s1) s2)
+mergeAlmu (Del c1 s1) (Ins c2 s2) = do
+  Refl <- testEquality (getSNat (Proxy @ix)) (getSNat (Proxy @iy))
+  Ins c2 <$> (mergeAlmuCtx (Del c1 s1) s2)
+
+mergeAlmu (Spn s1) (Spn s2) = Spn <$> mergeSpine (getSNat (Proxy @ix)) (getSNat (Proxy @iy)) s1 s2
+mergeAlmu (Spn Scp) (Del c2 s2) = pure $ Del c2 s2
+mergeAlmu (Spn (SCns c1 at1)) (Del c2 s2) = do
+  
+  Refl <- testEquality c1 c2
+  Del c1 <$> mergeAtCtx at1 s2
+mergeAlmu (Spn (SChg _ _ _)) (Del _ _) = Nothing
+mergeAlmu (Del _ _) (Spn Scp) = pure $ Spn Scp
+mergeAlmu (Del c1 s1) (Spn (SCns c2 at2)) = do
+  Refl <- testEquality c1 c2
+  mergeCtxAt s1 at2
+mergeAlmu (Del _ _) (Spn (SChg _ _ _)) = Nothing
+mergeAlmu (Del _ _) (Del _ _) = Nothing
+
+-- |Merges two patches in the /stdiff/ style. Satisfies the following
+-- postcondition:
+--
+-- > if merge p q == Just pq && merge q p == Just qp
+-- > then apply pq . q == apply qp . p
+--
+merge :: forall ki codes ix
+       . (EqHO ki, IsNat ix)
+      => Almu ki codes ix ix
+      -> Almu ki codes ix ix
+      -> Maybe (Almu ki codes ix ix)
+merge = mergeAlmu
diff --git a/src/Generics/MRSOP/STDiff/Types.hs b/src/Generics/MRSOP/STDiff/Types.hs
new file mode 100644
--- /dev/null
+++ b/src/Generics/MRSOP/STDiff/Types.hs
@@ -0,0 +1,185 @@
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE PolyKinds             #-}
+{-# LANGUAGE GADTs                 #-}
+module Generics.MRSOP.STDiff.Types where
+
+import Generics.MRSOP.Base
+
+-- * Functorial Changes
+--
+-- $functorialchanges
+--
+-- Represents changes on the /first layer/ of two values of
+-- mutually recursive families. For a more in-depth explanation
+-- of the datatypes and their meaning we refer the interested reader
+-- to the relevant literature:
+--
+--  - Miraldo, Dagand and Swierstra, TyDe 2017 <https://victorcmiraldo.github.io/data/tyde2017.pdf pdf>
+--  - van Putten, MSc thesis <https://dspace.library.uu.nl/handle/1874/380853>
+--
+
+-- |Represents a change between two opaque values. When they
+-- are equal represents a copy.
+data TrivialK (ki :: kon -> *) :: kon -> * where
+  Trivial :: ki kon -> ki kon -> TrivialK ki kon 
+
+-- |Represents a change between two atoms, where an atom is
+-- either a recursive or an opaque value.
+data At (ki :: kon -> *) (codes :: [[[Atom kon]]]) :: Atom kon -> * where
+  AtSet :: TrivialK ki kon                   -> At ki codes ('K kon)
+  AtFix :: (IsNat ix) => Almu ki codes ix ix -> At ki codes ('I ix)
+
+-- |Represents an alignment between two product of atoms.
+data Al (ki :: kon -> *) (codes :: [[[Atom kon]]]) :: [Atom kon] -> [Atom kon] -> * where
+  A0 :: Al ki codes '[] '[]
+  AX :: At ki codes x -> Al ki codes xs ys -> Al ki codes (x ': xs)  (x ': ys)
+  ADel :: NA ki (Fix ki codes) x -> Al ki codes xs ys -> Al ki codes (x ': xs) ys
+  AIns :: NA ki (Fix ki codes) x -> Al ki codes xs ys -> Al ki codes xs (x ': ys)
+
+-- |Represents a change at the coproduct structure.
+data Spine (ki :: kon -> *) (codes :: [[[Atom kon]]]) :: [[Atom kon]] -> [[Atom kon]] -> * where
+  Scp  :: Spine ki codes s1 s1
+  SCns :: Constr s1 c1 
+       -> NP (At ki codes) (Lkup c1 s1)
+       -> Spine ki codes s1 s1
+  SChg :: Constr s1 c1
+       -> Constr s2 c2
+       -> Al ki codes (Lkup c1 s1) (Lkup c2 s2)
+       -> Spine ki codes s1 s2
+
+-- * Fixpoint Changes
+--
+-- $fixpointchanges
+--
+-- The next datatypes represent a sequence of 'Spine', 'Al' and 'At' assembled
+-- coupled with operators to describe changes in the recursive structure such
+-- as inserting and deleting constructors.
+
+
+-- |Represents a /one-hole context/ over a @NP (NA ki (fix ki codes)) xs@ where
+-- the hole is in a distinguished element indexed by @'I ix@ and is filled
+-- with applying @p@ to the relevant indexes.
+data Ctx (ki :: kon -> *) (codes :: [[[Atom kon]]]) (p :: Nat -> Nat -> *)
+         (ix :: Nat) :: [Atom kon] -> * where
+  H :: IsNat iy
+    => p ix iy
+    -> PoA ki (Fix ki codes) xs
+    -> Ctx ki codes p ix ('I iy ': xs)
+  T :: NA ki (Fix ki codes) a
+    -> Ctx ki codes p ix xs
+    -> Ctx ki codes p ix (a ': xs)
+
+-- |Simple synonym for contexts.
+type InsCtx ki codes ix xs = Ctx ki codes (Almu ki codes) ix xs
+
+-- |A deletion context needs to swap the indexes in the hole, hence
+-- we use a newtype for that.
+type DelCtx ki codes ix xs = Ctx ki codes (AlmuMin ki codes) ix xs
+
+-- |The newtype used to swap the indexes to |Almu|.
+newtype AlmuMin ki codes ix iy = AlmuMin  { unAlmuMin :: Almu ki codes iy ix }
+
+-- |Represent recursive spines.
+data Almu (ki :: kon -> *) (codes :: [[[Atom kon]]]) :: Nat -> Nat -> * where
+  Spn :: Spine ki codes (Lkup ix codes) (Lkup iy codes) -> Almu ki codes ix iy
+  Ins :: Constr (Lkup iy codes) c
+      -> InsCtx ki codes ix (Lkup c (Lkup iy codes)) -- its an ix with an iy typed-hoed
+      -> Almu ki codes ix iy
+  Del :: IsNat iy
+      => Constr (Lkup ix codes) c
+      -> DelCtx ki codes iy (Lkup c (Lkup ix codes))
+      -> Almu ki codes ix iy
+
+{-
+
+{-
+instance (ShowHO ki) => Show (At ki codes at) where
+  show (AtSet t) = show t
+  show (AtFix a) = a
+
+instance ShowHO ki => Show (TrivialK ki x) where
+  show (Trivial x y) = show x ++ "|" ++ show y
+
+
+-}  
+
+
+
+{-
+instance (HasDatatypeInfo ki fam codes, Show1 ki) => Show (Al ki codes xs ys) where
+  show A0 = "A0"
+  show (AX x xs) = "(AX " ++ show1 x  ++ " " ++ show xs  ++ ")"
+  show (ADel x xs) = "(ADel " ++ show x  ++ " " ++ show xs  ++ ")"
+  show (AIns x xs) = "(AIns " ++ show x  ++ " " ++ show xs  ++ ")"
+-}
+
+{-
+instance (IsNat ix,IsNat iy, HasDatatypeInfo ki fam codes, Show1 ki) => Show (AlmuMin ki codes ix iy) where
+  show (AlmuMin x) = show x
+-}
+
+-- | An NP p xs, but there exists an x in xs such that h x
+--
+-- Note that:  NP p xs <=> Ctx' p p xs
+--
+-- and that the list is never empty, because it contains at
+-- least the pointed element
+--
+
+
+instance (IsNat ix, HasDatatypeInfo ki fam codes, Show1 ki) => Show (InsCtx ki codes ix xs) where
+  show (H p poa) = "(H " ++ show p ++ " " ++ show poa ++ ")"
+  show (T n c)   = "(T " ++ show n  ++ " " ++ show c ++ ")"
+instance (IsNat ix, HasDatatypeInfo ki fam codes, Show1 ki) => Show (DelCtx ki codes ix xs) where
+  show (H p poa) = "(H " ++ show p ++ " " ++ show poa ++ ")"
+  show (T n c)   = "(T " ++ show n  ++ " " ++ show c ++ ")"
+
+
+  -- TODO ins del
+
+
+instance forall ki fam codes ix iy. (IsNat ix, IsNat iy, Show1 ki, HasDatatypeInfo ki fam codes) => Show (Almu ki codes ix iy) where
+  show (Spn s) = "(Spn " ++ showSpine (getSNat @ix Proxy) (getSNat @iy Proxy) s ++ ")"
+  show (Ins c ic) = "(Ins " ++ showC c ++ " " ++ show ic ++ ")"
+    where showC c = constructorName . constrInfoLkup c $ (datatypeInfo (Proxy @fam) (getSNat @iy Proxy))
+  show (Del c ic) = "(Del " ++ showC c ++ " " ++ show ic ++ ")"
+    where showC c = constructorName . constrInfoLkup c $ (datatypeInfo (Proxy @fam) (getSNat @ix Proxy))
+
+instance (Show1 p) => Show1 (NP p) where
+  show1 np = parens . concat . intersperse " "  $ elimNP show1 np
+    where
+      parens x = "(" ++ x  ++ ")"
+
+
+showSpine :: forall ki fam codes ix iy. (Show1 ki, HasDatatypeInfo ki fam codes, IsNat ix,  IsNat iy) => SNat ix -> SNat iy -> Spine ki codes (Lkup ix codes) (Lkup iy codes) -> String
+showSpine six siy Scp = "Scp"
+showSpine six siy (SCns c x) =  "(Scns " ++ showC c six ++ " " ++ show1 x ++ ")" 
+    where showC c six = constructorName . constrInfoLkup c $ (datatypeInfo (Proxy @fam) six)
+showSpine six siy (SChg c1 c2 a) = "(SChg " ++ showCX  ++ " " ++ showCY ++ " " ++ show a  ++ ")"
+    where showCX = constructorName . constrInfoLkup c1 $ (datatypeInfo (Proxy @fam) six)
+          showCY = constructorName . constrInfoLkup c2 $ (datatypeInfo (Proxy @fam) siy)
+{-
+instance (HasDatatypeInfo ki fam codes, Show1 ki) => Show (Spine ki codes x y) where
+  show Scp = "COPY"
+  show (SCns c x) = "(Scns " ++ showC c ++ " " ++ show1 x ++ ")" 
+    where 
+      showC 
+      showC c = constructorName . consterInfoLookup c (datatypeInfo (Proxy @fam) (getSNat @ix Proxy))
+  show (SChg c1 c2 a) = "(SChg " ++ showC c1  ++ " " ++ showC c2  ++ " " ++ show a  ++ ")"
+    where showC c = constructorName . consterInfoLookup c (datatypeInfo (Proxy @fam) (getSNat @ix Proxy))
+-}
+
+-- OR what about:  ix iy
+guard' :: String -> Bool -> Either String ()
+guard' s False = Left s
+guard' _ True  = Right ()
+
+instance Show1 SNat where
+  show1 = show . go
+    where
+     go :: SNat n -> Int
+     go SZ = 0
+     go (SS s) = 1 + go s
+
+-}