diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c) 2018, Victor Miraldo and Alejandro Serrano
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * Neither the name of Victor Miraldo and Alejandro Serrano nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/generics-mrsop-gdiff.cabal b/generics-mrsop-gdiff.cabal
new file mode 100644
--- /dev/null
+++ b/generics-mrsop-gdiff.cabal
@@ -0,0 +1,39 @@
+name:                generics-mrsop-gdiff
+
+-- 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.0
+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
+
+library
+  ghc-options:
+    -O2 -Wall
+
+  exposed-modules: 
+    Generics.MRSOP.GDiff
+    Generics.MRSOP.GDiff.Util
+ 
+  -- Other library packages from which modules are imported.
+  build-depends:       base < 5,
+                       generics-mrsop >= 2.0.0
+  
+  -- Directories containing source files.
+  hs-source-dirs:      src
+  
+  -- Base language which the package is written in.
+  default-language:    Haskell2010
+  
diff --git a/src/Generics/MRSOP/GDiff.hs b/src/Generics/MRSOP/GDiff.hs
new file mode 100644
--- /dev/null
+++ b/src/Generics/MRSOP/GDiff.hs
@@ -0,0 +1,352 @@
+{-# LANGUAGE PolyKinds            #-}
+{-# LANGUAGE FlexibleContexts     #-}
+{-# LANGUAGE DataKinds            #-}
+{-# LANGUAGE TypeFamilies         #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE ConstraintKinds      #-}
+{-# LANGUAGE TypeApplications     #-}
+{-# LANGUAGE ScopedTypeVariables  #-}
+{-# LANGUAGE TypeOperators        #-}
+{-# LANGUAGE RankNTypes           #-}
+{-# LANGUAGE ViewPatterns         #-}
+{-# LANGUAGE GADTs                #-}
+-- |This module has been taken from arianvp/generics-mrsop-diff, it essentially
+-- isolates Arian's fixes over GDiff and adapts them to work over newer versions
+-- of generics-mrsop.
+--
+module Generics.MRSOP.GDiff
+  ( Cof(..)
+  , cofIdx , cofWitnessI , cofHeq
+  , ES(..)
+  , apply, apply' , applyES
+  , diff , diff'
+  , cost
+  ) where
+
+import Control.Monad
+import Data.Proxy
+import Data.Type.Equality  hiding (apply)
+import Generics.MRSOP.Base hiding (listPrfNP)
+import Generics.MRSOP.GDiff.Util
+import Generics.MRSOP.Util ( SNat
+                           , EqHO(..)
+                           , IsNat
+                           , (:++:)
+                           , Lkup
+                           , ShowHO(..)
+                           , Idx
+                           , El(..)
+                           , getSNat)
+
+-- | A 'Cof' represents a leaf of the flattened representation of our tree. Hence,
+-- it will be either a constructor of a particular datatype or an opaque value.
+data Cof (ki :: kon -> *) (codes :: [[[Atom kon]]]) :: Atom kon -> [Atom kon] -> * where
+  -- ^ A constructor tells us the type of its arguments and which type in the family it constructs
+  ConstrI :: (IsNat c, IsNat n) => Constr (Lkup n codes) c -> ListPrf (Lkup c (Lkup n codes)) -> Cof ki codes ('I n) (Lkup c (Lkup n codes))
+
+  -- ^ Requires no arguments to complete
+  ConstrK :: ki k -> Cof ki codes ('K k) '[]
+
+-- |Extracts a proxy from a 'Cof'
+cofWitnessI :: Cof ki codes ('I n) t -> Proxy n
+cofWitnessI _ = Proxy
+ 
+-- |Extracts an 'SNat' from a 'Cof'
+cofIdx :: forall ki codes xs n. IsNat n => Cof ki codes ('I n) xs -> SNat n
+cofIdx _ = getSNat @n Proxy
+
+-- |Values of type 'Cof' support heterogeneous equality checking.
+cofHeq :: (EqHO ki, TestEquality ki)
+       => Cof ki codes a t1
+       -> Cof ki codes b t2
+       -> Maybe (a :~: b, t1 :~: t2)
+cofHeq cx@(ConstrI x _) cy@(ConstrI y _) =
+  case testEquality (getSNat (cofWitnessI cx)) (getSNat (cofWitnessI cy)) of
+    Nothing -> Nothing
+    Just Refl ->
+      case testEquality x y of
+        Nothing -> Nothing
+        Just Refl -> Just (Refl, Refl)
+cofHeq (ConstrK x) (ConstrK y) =
+  case testEquality x y of
+    Just Refl ->
+      if eqHO x y
+        then Just (Refl, Refl)
+        else Nothing
+    Nothing -> Nothing
+cofHeq _ _ = Nothing
+
+-- |An edit script will insert, delete or copy 'Cof's. We keep the cost
+-- of the edit script annotated in the constructor
+data ES (ki :: kon -> *) (codes :: [[[Atom kon]]]) :: [Atom kon] -> [Atom kon] -> * where
+  ES0 :: ES ki codes '[] '[]
+  Ins :: Int -> Cof ki codes a t -> ES ki codes i          (t :++: j) -> ES ki codes i        (a ': j)
+  Del :: Int -> Cof ki codes a t -> ES ki codes (t :++: i) j          -> ES ki codes (a ': i) j
+  Cpy :: Int -> Cof ki codes a t -> ES ki codes (t :++: i) (t :++: j) -> ES ki codes (a ': i) (a ': j)
+
+{-# INLINE cost #-}
+cost :: ES ki codes txs tys -> Int
+cost ES0 = 0
+cost (Ins k _ _) = k
+cost (Del k _ _) = k
+cost (Cpy k _ _) = k
+
+{-# INLINE meet #-}
+meet :: ES ki codes txs tys -> ES ki codes txs tys -> ES ki codes txs tys
+meet d1 d2 = if cost d1 <= cost d2 then d1 else d2
+
+-- Heuristic:
+--
+--    many diffs have largely unchanged heads. Simply skip those
+--
+--    TODO: We can do the same with the tail in an imperative language
+--    however, we cant due to the way our diff structure is a stack,
+--
+--    TODO: We can even emit CpyTree's here, using hashing, but we'll
+--    also have to update the conversion to stdiff
+
+
+skipFront 
+  :: (TestEquality ki, EqHO ki)
+  => PoA ki (Fix ki codes) xs
+  -> PoA ki (Fix ki codes) ys
+  -> ES ki codes xs ys
+skipFront (x@(sopNA -> TagNA cx px) :* xs) (y@(sopNA -> TagNA cy py) :* ys) =
+  case cofHeq cx cy of
+    Just (Refl, Refl) ->
+      let c = skipFront (appendNP px xs) (appendNP py ys)
+       in Cpy (cost c) cx $ c
+    Nothing -> getDiff $ diffT (x :* xs) (y :* ys)
+skipFront xs ys = getDiff $ diffT xs ys
+
+-- |This is an edit script table; which is how we memoize computations
+-- to reuse them later. For more details check the last section in
+-- /A Type-safe diff for families of datatypes/, by /Lempsink and Loh/.
+data EST (ki :: kon -> *) (codes :: [[[Atom kon]]]) :: [Atom kon] -> [Atom kon] -> * where
+  NN :: ES ki codes '[] '[] 
+     -> EST ki codes '[] '[]
+  NC :: Cof ki codes y t
+     -> ES ki codes '[] (y ': tys)
+     -> EST ki codes '[] (t :++: tys)
+     -> EST ki codes '[] (y ': tys)
+  CN :: Cof ki codes x t
+     -> ES ki codes (x ': txs) '[]
+     -> EST ki codes (t :++: txs) '[]
+     -> EST ki codes (x ': txs) '[]
+  CC :: Cof ki codes x t1
+     -> Cof ki codes y t2
+     -> ES ki codes (x ': txs) (y ': tys)
+     -> EST ki codes (x ': txs) (t2 :++: tys)
+     -> EST ki codes (t1 :++: txs) (y ': tys)
+     -> EST ki codes (t1:++: txs) (t2 :++: tys)
+     -> EST ki codes (x ': txs) (y ': tys)
+
+
+getDiff :: EST ki codes rxs rys -> ES ki codes rxs rys
+getDiff (NN x) = x
+getDiff (NC _ x _) = x
+getDiff (CN _ x _) = x
+getDiff (CC _ _ x _ _ _) = x
+
+-- existential version of Cof, that hides its type
+data ViewNA ki codes a where
+  TagNA :: Cof ki codes a t -> PoA ki (Fix ki codes) t -> ViewNA ki codes a
+
+-- | Non-CC version of matchConstructor
+--
+-- A version of sop but over NA instead of Rep
+sopNA :: NA ki (Fix ki codes) a -> ViewNA ki codes a
+sopNA (NA_K k) = TagNA (ConstrK k) NP0
+sopNA (NA_I (Fix (sop -> Tag c poa))) = TagNA (ConstrI c (listPrfNP poa)) poa
+
+data DES ki codes a xs ys where 
+  DES :: Cof ki codes a t -> ES ki codes (a ': xs) ys -> EST ki codes (t :++: xs) ys -> DES ki codes a xs ys
+
+data IES ki codes a xs ys where 
+  IES :: Cof ki codes a t -> ES ki codes xs (a ': ys)-> EST ki codes xs (t :++: ys) -> IES ki codes a xs ys
+
+extractd :: EST ki codes (a ': xs) ys -> DES ki codes a xs ys
+extractd (CC f _ e _ i _) = DES f e i
+extractd (CN g d i) = DES g d i
+
+extracti :: EST ki codes xs (a ': ys) -> IES ki codes a xs ys
+extracti (CC _ g e i _ _) = IES g e i
+extracti (NC  g d i) = IES g d i
+
+diffT :: (EqHO ki, TestEquality ki)
+      => PoA ki (Fix ki codes) xs
+      -> PoA ki (Fix ki codes) ys
+      -> EST ki codes xs ys
+diffT NP0 NP0 = NN ES0
+diffT ((sopNA -> TagNA c poa) :* xs) NP0 =
+  let d = diffT (appendNP poa xs) NP0
+  in CN c (Del (1 + cost (getDiff d)) c (getDiff d)) d
+diffT NP0 ((sopNA -> TagNA c poa) :* ys) =
+  let i = diffT NP0 (appendNP poa ys)
+  in NC c (Ins (1 + cost (getDiff i)) c (getDiff i)) i
+diffT ((sopNA -> TagNA c1 poa1) :* xs) ((sopNA -> TagNA c2 poa2) :* ys) =
+  let 
+    i = extendi c1 c
+    d = extendd c2 c
+    c = diffT (appendNP poa1 xs) (appendNP poa2 ys)
+    es = bestDiffT c1 c2 i d c
+  in CC c1 c2 es i d c
+
+extendi 
+  :: (EqHO ki, TestEquality ki)
+  => Cof ki codes x t
+  -> EST ki codes (t :++: xs) ys
+  -> EST ki codes (x ': xs) ys
+extendi c1 i@(NN d) = CN c1 (Del (1 + cost d) c1 d) i
+extendi c1 i@(CN _ d _) =  CN c1 (Del (1 + cost d) c1 d) i
+extendi c1 d@NC{} =
+  case extracti d of
+    IES c2 _ c -> 
+      let i = extendi c1 c
+      in CC c1 c2 (bestDiffT c1 c2 i d c) i d c
+extendi c1 d@CC{} =
+  case extracti d of
+    IES c2 _ c -> 
+      let i = extendi c1 c
+      in CC c1 c2 (bestDiffT c1 c2 i d c) i d c
+  
+extendd
+  :: (TestEquality ki, EqHO ki) 
+  => Cof ki codes y t
+  -> EST ki codes xs (t :++: ys)
+  -> EST ki codes xs (y ': ys)
+extendd c1 i@(NN d) = NC c1 (Ins (1 + cost d) c1 d) i
+extendd c1 i@(NC _ d _) = NC c1 (Ins (1 + cost d) c1 d) i
+extendd c1 i@CN{} =
+  case extractd i of
+    DES c2 _ c -> 
+      let d = extendd c1 c 
+      in CC c2 c1 (bestDiffT c2 c1 i d c) i d c
+extendd c1 i@CC{} =
+  case extractd i of
+    DES c2 _ c -> 
+      let d = extendd c1 c
+      in CC c2 c1 (bestDiffT c2 c1 i d c) i d c
+
+bestDiffT
+  :: (EqHO ki, TestEquality ki)
+  => Cof ki codes x t1
+  -> Cof ki codes y t2
+  -> EST ki codes (x ': xs) (t2 :++: ys)
+  -> EST ki codes (t1 :++: xs) (y ': ys)
+  -> EST ki codes (t1 :++: xs) (t2 :++: ys)
+  -> ES ki codes (x ': xs) (y ': ys)
+bestDiffT cx cy i d c =
+  case cofHeq cx cy of
+    Just (Refl, Refl) ->
+      let c' = getDiff c
+      in Cpy (cost c') cx c'
+    Nothing -> 
+      let
+        i' = getDiff i
+        d' = getDiff d
+      in
+        meet (Ins (1 + cost i') cy i') (Del (1 + cost d') cx d')
+          
+matchCof :: (EqHO ki)
+         => Cof ki codes a t  -- NOTE: cof is a relation. not a function,
+         -> 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 (eqHO k k2) >> Just NP0
+
+-- 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
+insCof :: Cof ki codes a t
+       -> PoA ki (Fix ki codes) (t :++: xs)
+       -> PoA ki (Fix ki codes) (a ': xs)
+insCof (ConstrI c ispoa) xs =
+  let (poa, xs') = split ispoa xs
+   in NA_I (Fix $ inj c poa) :* xs'
+insCof (ConstrK k) xs = NA_K k :* xs 
+
+delCof :: EqHO ki
+       => Cof ki codes a t
+       -> PoA ki (Fix ki codes) (a ': xs)
+       -> Maybe (PoA ki (Fix ki codes) (t :++: xs))
+delCof c (x :* xs) = flip appendNP xs <$> matchCof c x
+
+
+apply :: forall ki fam codes ty1 ty2 ix1 ix2.
+         ( Family ki fam codes
+         , ix1 ~ Idx ty1 fam
+         , ix2 ~ Idx ty2 fam
+         , Lkup ix1 fam ~ ty1
+         , Lkup ix2 fam ~ ty2
+         , IsNat ix1
+         , IsNat ix2
+         ,  EqHO ki
+         , TestEquality ki
+         )
+      => ES ki codes '[ 'I ix1] '[ 'I ix2]
+      -> ty1
+      -> Maybe ty2
+apply es a =
+  case apply' es (deep a) of
+    Just (Fix x) ->
+      case dto @ix2 x of
+        El b -> Just b
+    Nothing -> Nothing
+
+apply' ::
+     (IsNat ix1, IsNat ix2,  EqHO ki)
+  => ES ki codes '[ 'I ix1] '[ 'I ix2]
+  -> Fix ki codes ix1
+  -> Maybe (Fix ki codes ix2)
+apply' es x = do
+  res <- applyES es (NA_I x :* NP0)
+  case res of
+    (NA_I y :* NP0) -> pure y
+
+applyES ::
+     EqHO ki
+  => ES ki codes xs ys
+  -> PoA ki (Fix ki codes) xs
+  -> Maybe (PoA ki (Fix ki codes) ys)
+applyES ES0 _ = Just NP0
+applyES (Ins _ c es) xs = insCof c <$> applyES es xs
+applyES (Del _ c es) xs = delCof c xs >>= applyES es
+applyES (Cpy _ c es) xs = insCof c <$> (delCof c xs >>= applyES es)
+
+
+-- When Showing, we do not know what the family that we're showing is,
+-- as edit scripts are not parameterised over the family.
+-- 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) = showHO k
+showCof x@(ConstrI c _) = constructorName . constrInfoLkup c $ datatypeInfo (Proxy @fam) (cofIdx x)
+
+instance (HasDatatypeInfo ki fam codes, ShowHO ki) =>
+         Show (ES ki codes xs ys) where
+  show ES0 = "ES0"
+  show (Ins _ c d) = "Ins " ++ showCof c ++ " $ " ++ show d
+  show (Del _ c d) = "Del " ++ showCof c ++ " $ " ++ show d
+  show (Cpy _ c d) = "Cpy " ++ showCof c ++ " $ " ++ show d
+
+diff :: forall fam ki codes ix1 ix2 ty1 ty2.
+        ( Family ki fam codes
+        , ix1 ~ Idx ty1 fam
+        , ix2 ~ Idx ty2 fam
+        , Lkup ix1 fam ~ ty1
+        , Lkup ix2 fam ~ ty2
+        , IsNat ix1
+        , IsNat ix2
+        ,  EqHO ki
+        , TestEquality ki
+        )
+     => ty1
+     -> ty2
+     -> ES ki codes '[ 'I ix1] '[ 'I ix2]
+diff a b = diff' (deep a) (deep b)
+
+diff' :: ( EqHO ki, IsNat ix1, IsNat ix2, TestEquality ki)
+      => Fix ki codes ix1
+      -> Fix ki codes ix2
+      -> ES ki codes '[ 'I ix1] '[ 'I ix2]
+diff' a b = skipFront (NA_I a :* NP0) (NA_I b :* NP0) 
diff --git a/src/Generics/MRSOP/GDiff/Util.hs b/src/Generics/MRSOP/GDiff/Util.hs
new file mode 100644
--- /dev/null
+++ b/src/Generics/MRSOP/GDiff/Util.hs
@@ -0,0 +1,56 @@
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE PolyKinds #-}
+
+-- | For the lack of a better name, here we put random stuff
+module Generics.MRSOP.GDiff.Util where
+
+import Generics.MRSOP.Base hiding (listPrfNP)
+import Generics.MRSOP.Util ((:++:))
+
+-- |Convenient constraint synonyms
+type L1 xs          = (IsList xs) 
+type L2 xs ys       = (IsList xs, IsList ys) 
+type L3 xs ys zs    = (IsList xs, IsList ys, IsList zs) 
+type L4 xs ys zs as = (IsList xs, IsList ys, IsList zs, IsList as) 
+
+data RList :: [k] -> * where
+  RList :: IsList ts => RList ts
+
+-- this seems more like "Coerce" to me
+{-# INLINE reify #-}
+reify :: ListPrf ts -> RList ts
+reify Nil      = RList
+reify (Cons x) = case reify x of RList -> RList
+
+-- |Proves that the index of a value of type 'NP' is a list.
+--  This is useful for pattern matching on said list without
+--  having to carry the product around.
+listPrfNP :: NP p xs -> ListPrf xs
+listPrfNP NP0       = Nil
+listPrfNP (_ :* xs) = Cons $ listPrfNP xs
+
+-- In Agda this would be:
+-- ++⁻ : {A : Set}
+--       {P : A -> Set}
+--       (xs : List A)
+--       {ys : List A} 
+--     → All P (xs ++ ys) → All P xs × All P ys
+-- ++⁻ []       p          = [] , p
+-- ++⁻ (x ∷ xs) (px ∷ pxs) = Prod.map (px ∷_) id (++⁻ _ pxs)
+--
+--   Note in particular, that xs is not an implicit argument,
+--   and that we explicitly pattern match on it.
+--
+--   In haskell, types and values are separated, but we can 
+--   carry around the Singleton LstPrf in order to
+--   discover on the type-level the list, by pattern matching
+split :: ListPrf xs -> NP p (xs :++: ys) -> (NP p xs, NP p ys)
+split Nil poa = (NP0, poa)
+split (Cons p) (x :* rs) =
+  let (xs, rest) = split p rs
+   in (x :* xs, rest)
+