diff --git a/packages.dhall b/packages.dhall
index 85fecd1..0a6fa38 100644
--- a/packages.dhall
+++ b/packages.dhall
@@ -104,9 +104,9 @@ let upstream =
 
 in  upstream
     with logict.repo = "https://dev.danilafe.com/Everything-I-Know-About-Types/logict.git"
-    with logict.version = "e19721af5e5fe172e93ebed1777e4718981516ef"
+    with logict.version = "880ade17dc5129975c16d211dc6ed3bddf2821c8"
     with logict.dependencies = [ "control", "lists", "maybe", "prelude", "transformers", "tuples" ]
     with unifyt.repo = "https://dev.danilafe.com/Everything-I-Know-About-Types/unifyt.git"
-    with unifyt.version = "590306964c59b8828b66b8d020283c8efaf2170b"
+    with unifyt.version = "ef3dabfa22a92b3983fc7f5c81614143c58972be"
     with unifyt.dependencies = [ "control", "foldable-traversable", "lazy", "maybe", "newtype", "ordered-collections", "prelude", "transformers", "tuples" ]
 
diff --git a/spago.dhall b/spago.dhall
index 1dcd689..84ef4b8 100644
--- a/spago.dhall
+++ b/spago.dhall
@@ -27,6 +27,7 @@ to generate this file without the comments in this block.
   , "parsing"
   , "prelude"
   , "strings"
+  , "tailrec"
   , "transformers"
   , "tuples"
   , "unifyt"
diff --git a/src/Language/Bergamot/Unifier.purs b/src/Language/Bergamot/Unifier.purs
index ca99d8f..6a978cd 100644
--- a/src/Language/Bergamot/Unifier.purs
+++ b/src/Language/Bergamot/Unifier.purs
@@ -4,6 +4,7 @@ import Prelude
 
 import Language.Bergamot.Rules (Metavariable, ProofTree(..), Rule(..), instantiate)
 import Language.Bergamot.Syntax (Expr(..), IntVar)
+import Language.Bergamot.Latex
 
 import Control.Plus (class Plus, empty)
 import Control.Apply (lift2)
@@ -18,9 +19,11 @@ import Control.Monad.Reader.Trans (ReaderT(..), runReaderT)
 import Control.Monad.Unify.Trans (UnifyT(..), runUnifyT)
 import Control.Monad.Logic.Trans (SFKT(..), runSFKTOnce, unSFKT)
 import Control.Monad.State.Trans (StateT(..), runStateT)
+import Control.Monad.Rec.Class (class MonadRec, Step(..), tailRecM)
 import Data.Traversable (traverse, oneOf)
+import Data.Foldable (oneOfMap)
 import Data.Tuple (fst)
-import Data.List (List(..), (:))
+import Data.List (List(..), (:), reverse)
 import Data.Newtype (class Newtype, un, over2)
 import Data.Maybe (Maybe)
 import Data.Bifunctor (rmap)
@@ -39,6 +42,7 @@ derive newtype instance Bind Unifier
 derive newtype instance Monad Unifier
 derive newtype instance MonadPlus Unifier
 derive newtype instance MonadUnify IntVar Expr Unifier
+derive newtype instance MonadRec Unifier
 
 -- >:(
 instance MonadAsk UnifierEnv Unifier where
@@ -80,23 +84,75 @@ matchBuiltin e@(Atom "isInt" (t : Nil)) =
         isIntProof i = MkProofTree { claim: e, rule: isIntRule i, witnesses: Nil }
 matchBuiltin _ = empty
 
-match :: Array (Rule Metavariable) -> Expr IntVar -> Unifier (ProofTree IntVar)
-match rs e = interleave (reify e >>= matchBuiltin) $ oneOf $ map (matchSingle e) rs
+type StackElement =
+    { done :: List (ProofTree IntVar)
+    , todo :: List (Expr IntVar)
+    , claim :: Expr IntVar
+    , rule :: Rule Metavariable
+    }
+
+type Stack = List StackElement
+
+type Acc =
+    { stack :: Stack
+    , rules :: Array (Rule Metavariable)
+    }
+
+rule :: Expr IntVar -> Rule Metavariable -> Unifier StackElement
+rule e r = do
+    MkRule {head, tail} <- instantiate r
+    _ <- unify e head
+    pure $ { done: Nil, todo: tail, claim: e, rule: r }
+
+rules :: Expr IntVar -> Array (Rule Metavariable) -> Unifier StackElement
+rules e rs = oneOfMap (rule e) rs
+
+step :: Acc -> Unifier (Step Acc (ProofTree IntVar))
+step {stack: Nil} = empty
+step acc@{stack: {done, todo: Nil, claim, rule: r} : xs} =
+    pure $ case xs of
+        Nil -> Done tree
+        Cons se xs' -> Loop acc {stack = se { done = tree : se.done } : xs'}
     where
-      matchSingle e' rule = spend $ do
-         MkRule {head, tail} <- instantiate rule
+        tree = MkProofTree { claim, rule: r, witnesses: reverse done }
+step acc@{stack: se@{todo: (e:es)} : xs} =
+    do
+        e' <- reify e
+        interleave (builtin e') (given e')
+    where
+        builtin e' = do
+            t <- matchBuiltin e'
+            pure $ Loop acc { stack = se { todo = es, done = t : se.done } : xs }
+        given e' = do
+            se' <- rules e' acc.rules
+            pure $ Loop acc { stack = se' : se { todo = es } : xs }
+
+
+-- Note: maybe it's the list / rule operations that are the problem, rather
+-- than the stack itself? In particular, could the oneOf be the issue?
+
+match' :: Array (Rule Metavariable) -> Expr IntVar -> Unifier (ProofTree IntVar)
+match' rs e = interleave (matchBuiltin e) do
+    firstElem <- rules e rs
+    tailRecM step { rules: rs, stack: firstElem : Nil }
+
+match :: Array (Rule Metavariable) -> Expr IntVar -> Unifier (ProofTree IntVar)
+match rs e = interleave (reify e >>= matchBuiltin) $ oneOfMap (matchSingle e) rs
+    where
+      matchSingle e' r = spend $ do
+         MkRule {head, tail} <- instantiate r
          _ <- unify e' head
          witnesses <- traverse (match rs) tail
-         pure $ MkProofTree { claim: e, rule: rule, witnesses: witnesses }
+         pure $ MkProofTree { claim: e, rule: r, witnesses: witnesses }
 
 reifyProofTree :: ProofTree IntVar -> Unifier (ProofTree IntVar)
-reifyProofTree (MkProofTree {claim, rule, witnesses}) = do
+reifyProofTree (MkProofTree {claim, rule: r, witnesses}) = do
     claim' <- reify claim
     witnesses' <- traverse reifyProofTree witnesses
-    pure $ MkProofTree $ { claim: claim', rule: rule, witnesses: witnesses' }
+    pure $ MkProofTree $ { claim: claim', rule: r, witnesses: witnesses' }
 
 query :: Expr Metavariable -> Unifier (ProofTree IntVar)
-query e = (join $ lift2 match (asks _.rules) (instantiate e)) >>= reifyProofTree
+query e = (join $ lift2 match' (asks _.rules) (instantiate e)) >>= reifyProofTree
 
 runUnifier :: forall a. Array (Rule Metavariable) -> Unifier a -> Maybe a
 runUnifier rs m = runSFKTOnce (fst <$> (runReaderT (runUnifyT $ un MkUnifier m) { rules: rs, fuel: 10 }))