diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,29 @@
+Copyright (c) 2024, Alejandro Serrano
+
+
+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 the copyright holder nor the names of its
+      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
+HOLDER 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/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,52 @@
+# Unification for `unbound-generics`
+
+This package implements (first-order) unification by reusing the framework of [`unbound-generics`](https://hackage.haskell.org/package/unbound-generics).
+
+To use it, declare your data types as usual, including the generically-derived instances for alpha-equivalence (`Alpha`) and substitution (`Subst`) from `unbound-generics`.
+In addition to those, ask for a new instance of `Unify` with the same arguments as `Subst`, that is, the type from which we build variables, and the type we want to unify.
+
+The packages provides a function `unify` which works on a `Unification` monad. This monad is parametrized by the type we draw variables from. That means you can have as many types as you want, but there should be a single type of variables. In many cases the compiler fails to infer that argument to the `Unification` monad, so we recommend enabling `TypeApplications` for that matter.
+
+The result of `unify` is either a single value which is an instance of both arguments, or a `UnificationError`. That error explains where the process has failed by a `Path` consisting of constructor, fields, and indices; and a cause.
+
+---
+
+This is an example in which `Type` is the one we draw variables from. Since we also use `TypeConstructor` inside the `TyCon` constructor, we also need to "request" to derive `Unify Type TypeConstructor`.
+
+```haskell
+type TypeVar = Name Type
+
+data Type = TyVar { var :: TypeVar }
+          | TyFun { args :: [Type], ret :: Type }
+          | TyCon { con :: TypeConstructor, args :: [Type] }
+          deriving (Eq, Show, Generic, Typeable)
+
+data TypeConstructor = TyConInt | TyConBool deriving (Eq, Show, Generic)
+
+pattern TyInt, TyBool :: Type
+pattern TyInt  = TyCon TyConInt []
+pattern TyBool = TyCon TyConBool []
+
+instance Alpha Type
+instance Alpha TypeConstructor
+
+instance Subst Type Type where
+  isvar (TyVar v) = Just $ SubstName v
+  isvar _ = Nothing
+instance Subst Type TypeConstructor
+
+instance Unify Type Type
+instance Unify Type TypeConstructor
+```
+
+Here are some example runs, using the explicitly-typed version of `runUnification` to declare that we are using `Type`-variables. To create new variables we use the usual `s2n` function from `unbound-generics`.
+
+```haskell
+>>> runUnification @Type $ let x = s2n "x" in unify' (TyFun [TyVar x] TyInt) (TyFun [TyVar x] (TyVar x))
+( Right (TyFun {args = [TyCon {con = TyConInt, args = []}], ret = TyCon {con = TyConInt, args = []}})
+, fromList [(x,TyCon {con = TyConInt, args = []})] )
+
+>>> runUnification @Type $ let x = s2n "x" in unify' (TyFun [TyVar x] TyInt) (TyFun [TyBool] (TyVar x))
+( Left ([PathConstructor "TyFun", PathSelector "ret", PathConstructor "TyCon", PathSelector "con"], DifferentConstructor)
+, fromList [(x,TyCon {con = TyConBool, args = []})] )
+```
diff --git a/src/Unbound/Generics/Unify.hs b/src/Unbound/Generics/Unify.hs
new file mode 100644
--- /dev/null
+++ b/src/Unbound/Generics/Unify.hs
@@ -0,0 +1,164 @@
+{-# language DefaultSignatures, UndecidableInstances, GADTs, MultiWayIf, AllowAmbiguousTypes #-}
+-- | Unification for @unbound-generics@
+module Unbound.Generics.Unify (
+  -- * Main unification functions
+  unify', Unify(..),
+  -- ** Information about errors
+  UnificationError, UnificationErrorCause(..),
+  Path, PathElement(..),
+  -- * Unification as a monad
+  Unification(..),
+  -- ** Base implementation
+  UnificationM, runUnification,
+  -- ** Including fresh creation
+  UnificationFreshM, runUnificationFresh,
+  -- ** As a monad transformer
+  UnificationMT, runUnificationT,
+  -- * Generic methods
+  GUnify(..)
+) where
+
+import Data.Bifunctor
+import Control.Monad (forM)
+import Control.Monad.Trans.State
+import Data.Functor.Identity
+import Data.Map
+import GHC.Generics
+import Unbound.Generics.LocallyNameless
+
+-- | Path to navigate to a unification error.
+type UnificationError = (Path, UnificationErrorCause)
+
+-- | Potential causes for unification errors.
+data UnificationErrorCause where
+  OccursCheck          :: (Name t) -> t -> UnificationErrorCause
+  DifferentConstructor :: UnificationErrorCause
+  DifferentListLength  :: UnificationErrorCause
+
+instance Show UnificationErrorCause where
+  show OccursCheck {}       = "OccursCheck"
+  show DifferentConstructor = "DifferentConstructor"
+  show DifferentListLength  = "DifferentListLength"
+
+type Path = [PathElement]
+-- | Ways to navigate within a value.
+data PathElement
+  = PathConstructor String | PathSelector String | PathIndex Int
+  deriving (Eq, Show)
+
+-- | Stateful storage of substitutions as required for unification.
+--
+-- The substitution operates only on terms and variables of type 't'.
+class Monad m => Unification t m where
+  -- | Obtain the current substitution.
+  currentSubst :: m (Map (Name t) t)
+  -- | Add a new substitution.
+  recordSubst  :: Name t -> t -> m ()
+
+applySubst :: forall t a m. (Unification t m, Subst t a) => a -> m a
+applySubst term = do
+  current <- currentSubst @t @m
+  pure $ foldlWithKey (\t v u -> subst v u t) term current
+
+type UnificationM t = UnificationMT t Identity
+type UnificationFreshM t = UnificationMT t FreshM
+
+runUnification :: forall t a. UnificationM t a -> (a, Map (Name t) t)
+runUnification action = runIdentity (runUnificationT action)
+
+runUnificationFresh :: forall t a. UnificationFreshM t a -> (a, Map (Name t) t)
+runUnificationFresh action = runFreshM (runUnificationT action)
+
+runUnificationT :: forall t m a. Monad m => UnificationMT t m a -> m (a, Map (Name t) t)
+runUnificationT action = runStateT (unUnificationMT action) empty
+
+newtype UnificationMT t m a 
+  = UnificationMT { unUnificationMT :: StateT (Map (Name t) t) m a }
+  deriving (Functor, Applicative, Monad)
+
+instance (Monad m) => Unification t (UnificationMT t m) where
+  currentSubst = UnificationMT $ get
+  recordSubst v t = UnificationMT $ modify (insert v t)
+
+-- | Tries to unify two terms, giving back a common term, or a unification error.
+--
+-- This variant requires the terms to be of the same type 't' as the variables within them.
+unify' :: forall t m. (Unification t m, Unify t t) => t -> t -> m (Either UnificationError t)
+unify' = unify @t
+
+-- | Declares the ability to unify values of type 'a' containing variables of type 't'.
+class Subst t a => Unify t a where
+  -- | Tries to unify two terms, giving back a common term, or a unification error.
+  unify :: Unification t m => a -> a -> m (Either UnificationError a)
+
+  default unify :: forall m. (Generic a, GUnify t (Rep a), Unification t m)
+                 => a -> a -> m (Either UnificationError a)
+  unify x y = do
+    x' <- applySubst @t x
+    y' <- applySubst @t y
+    result <- unifyIsvar x' y'
+    case result of
+      Left e -> pure $ Left e
+      Right r -> Right <$> applySubst @t r
+
+    where
+      unifyIsvar x y
+        | Just (SubstName v1) <- isvar @t @a x
+        , Just (SubstName v2) <- isvar @t @a y
+        = if | v1 == v2  -> Right <$> applySubst @t x
+             | v1  < v2  -> do { recordSubst v1 y ; Right <$> applySubst @t x }
+             | otherwise -> do { recordSubst v2 x ; Right <$> applySubst @t y }
+        -- do occurs check!!
+        | Just (SubstName v) <- isvar @t @a x = do { recordSubst v y ; Right <$> applySubst @t x }
+        | Just (SubstName v) <- isvar @t @a y = do { recordSubst v x ; Right <$> applySubst @t y }
+        | otherwise = unify_ x y
+
+      unify_ :: a -> a -> m (Either UnificationError a)
+      unify_ x y = fmap to <$> gunify @t @(Rep a) @m (from x) (from y)
+
+instance {-# overlaps #-} Unify t (Name t) where
+  unify = error "should have never arrived here"
+
+-- required because otherwise strings are matched as lists
+instance {-# overlaps #-} Unify t String where
+  unify x y
+    | x == y    = pure $ Right x
+    | otherwise = pure $ Left ([], DifferentConstructor)
+
+instance {-# overlaps #-} (Unify t a) => Unify t [a] where
+  unify xlst ylst
+    | length xlst /= length ylst = pure $ Left ([], DifferentListLength)
+    | otherwise = sequence <$> forM (zip3 [0 .. ] xlst ylst) (\(i, x,  y) -> first (first (PathIndex i :)) <$> unify @t x y)
+
+-- | Implementation of unification using @GHC.Generics@.
+class GUnify t f where
+  gunify :: Unification t m => f a -> f a -> m (Either UnificationError (f a))
+
+instance GUnify t U1 where
+  gunify _ _ = pure $ Right U1
+
+instance (Unify t a) => GUnify t (K1 i a) where
+  gunify (K1 x) (K1 y) = fmap K1 <$> unify @t x y
+
+instance GUnify t f => GUnify t (D1 d f) where
+  gunify (M1 x) (M1 y) = fmap M1 <$> gunify @t x y
+
+instance (Constructor c, GUnify t f) => GUnify t (C1 c f) where
+  gunify c@(M1 x) (M1 y) = bimap (first (PathConstructor (conName c) :)) M1 <$> gunify @t x y
+
+instance (Selector s, GUnify t f) => GUnify t (S1 s f) where
+  gunify c@(M1 x) (M1 y) = 
+    case selName c of
+      ""  -> fmap M1 <$> gunify @t x y
+      con -> bimap (first (PathSelector con :)) M1 <$> gunify @t x y
+
+instance (GUnify t f, GUnify t g) => GUnify t (f :*: g) where
+  gunify (x1 :*: x2) (y1 :*: y2) = do
+    r1 <- gunify @t x1 y1
+    r2 <- gunify @t x2 y2
+    pure $ (:*:) <$> r1 <*> r2
+
+instance (GUnify t f, GUnify t g) => GUnify t (f :+: g) where
+  gunify (R1 x) (R1 y) = fmap R1 <$> gunify @t x y
+  gunify (L1 x) (L1 y) = fmap L1 <$> gunify @t x y
+  gunify _ _ = pure $ Left ([], DifferentConstructor)
diff --git a/unbound-generics-unify.cabal b/unbound-generics-unify.cabal
new file mode 100644
--- /dev/null
+++ b/unbound-generics-unify.cabal
@@ -0,0 +1,23 @@
+cabal-version:      3.0
+name:               unbound-generics-unify
+version:            0.1.0.0
+synopsis:           Unification based on unbound-generics
+-- description:
+license:            BSD-3-Clause
+license-file:       LICENSE
+author:             Alejandro Serrano
+maintainer:         trupill@gmail.com
+-- copyright:
+category:           Language
+build-type:         Simple
+extra-source-files: README.md
+
+common warnings
+    ghc-options: -Wall
+
+library
+    import:           warnings
+    exposed-modules:  Unbound.Generics.Unify
+    build-depends:    base >= 4.16 && < 5, unbound-generics ^>= 0.4.4, containers >= 0.7, transformers >= 0.6
+    hs-source-dirs:   src
+    default-language: GHC2021