From e84ba37142462c0ddb377ea7fc5d73accaa6d053 Mon Sep 17 00:00:00 2001
From: Roman Cheplyaka <roma@ro-che.info>
Date: Tue, 4 Jul 2017 18:47:19 +0300
Subject: [PATCH 1/2] Correct README to README.md in the cabal file

---
 unification-fd.cabal | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/unification-fd.cabal b/unification-fd.cabal
index 7a2d951..6f1907e 100644
--- a/unification-fd.cabal
+++ b/unification-fd.cabal
@@ -30,7 +30,7 @@ Tested-With:
     GHC == 7.4.2, GHC == 7.6.3, GHC == 7.8.4, GHC == 7.10.3, GHC == 8.0.2
 
 Extra-source-files:
-    AUTHORS, README, CHANGELOG
+    AUTHORS, README.md, CHANGELOG
 Source-Repository head
     Type:     darcs
     Location: http://community.haskell.org/~wren/unification-fd

From 0f2b39fc0cca41a0b4c61b643fdb0bd468950639 Mon Sep 17 00:00:00 2001
From: Roman Cheplyaka <roma@ro-che.info>
Date: Tue, 15 May 2018 15:45:33 +0100
Subject: [PATCH 2/2] Introduce freshenAndFree

---
 src/Control/Unification.hs | 43 ++++++++++++++++++++++++++++++++++++++
 1 file changed, 43 insertions(+)

diff --git a/src/Control/Unification.hs b/src/Control/Unification.hs
index 0cb4211..6da36d0 100644
--- a/src/Control/Unification.hs
+++ b/src/Control/Unification.hs
@@ -71,6 +71,7 @@ module Control.Unification
     , getFreeVarsAll
     , applyBindingsAll
     , freshenAll
+    , freshenAndFree
     -- subsumesAll -- to ensure that there's a single coherent substitution allowing the schema to subsume all the terms in some collection.
 
     -- * Helper functions
@@ -386,6 +387,48 @@ freshenAll ts0 = evalStateT (mapM loop ts0) IM.empty
                                 modify' $ IM.insert i (Right v')
                                 return v'
 
+-- | Like 'freshenAll', but also ignore any existing bindings affecting the
+-- terms.
+--
+-- This is useful when the terms come from a different binding environment
+-- and have had their bindings applied.
+--
+-- Then 'freshenAndFree' ensures that no free variables are or will be
+-- accidentally captured in the current environment.
+--
+-- For instance, let's say you inferred the type of @id = λx.x@ as @UVar 1 -> UVar 1@.
+-- You may store this type in an interface file of some kind.
+-- Next time your program is run, it is asked to typecheck another term,
+-- which involves @id@. From the interface file you find that @id@ has type
+-- @UVar 1 -> UVar 1@, but what does @UVar 1@ refer to? It is supposed to
+-- be free (because the type of @id@ had its bindings applied before
+-- exporting, see 'applyBindings'). But in the current binding environment,
+-- @UVar 1@ may be already used to refer to something else, resulting in
+-- a variable capture. Applying 'freshenAndFree' returns an
+-- alpha-equivalent term, say, @UVar 17 -> UVar 17@, such that 17 is
+-- a fresh free variable in the current environment.
+freshenAndFree
+    ::  ( BindingMonad t v m
+        , Traversable s
+        )
+    => s (UTerm t v)        -- ^
+    -> m (s (UTerm t v)) -- ^
+freshenAndFree ts0 = evalStateT (mapM loop ts0) IM.empty
+    where
+    loop t0 = do
+        t0 <- lift $ semiprune t0
+        case t0 of
+            UTerm t -> UTerm <$> mapM loop t
+            UVar  v -> do
+                let i = getVarID v
+                seenVars <- get
+                case IM.lookup i seenVars of
+                    Just t -> return t
+                    Nothing -> do
+                        v' <- lift $ UVar <$> freeVar
+                        put $! IM.insert i v' seenVars
+                        return v'
+
 ----------------------------------------------------------------
 ----------------------------------------------------------------
 -- BUG: have to give the signatures for Haddock :(