From c0e8134b31132a1d4f052a517308161ad472f68e Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Sun, 10 Jan 2016 12:50:48 -0500
Subject: [PATCH 001/109] Move unification into its own section.

---
 src/Curve.hs | 29 ++++++++++++++++-------------
 1 file changed, 16 insertions(+), 13 deletions(-)

diff --git a/src/Curve.hs b/src/Curve.hs
index 47b2476..559667f 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -96,19 +96,6 @@ substitute name withTerm inScope = case out inScope of
   Application inA inB -> Term $ Application (substitute name withTerm inA) (substitute name withTerm inB)
   _ -> inScope
 
-unify :: Term' -> Term' -> Unification'
-unify expected actual = case (out expected, out actual) of
-  (_, Implicit) -> into expected
-  (Implicit, _) -> into actual
-
-  (Type, Type) -> into expected
-
-  (Variable n1, Variable n2) | n1 == n2 -> Unification $ Variable n2
-  (Application a1 b1, Application a2 b2) -> Unification $ Application (unify a1 a2) (unify b1 b2)
-  (Lambda i1 a1 b1, Lambda i2 a2 b2) | i1 == i2 -> Unification $ Lambda i2 (unify a1 a2) (unify b1 b2)
-
-  _ -> Conflict expected actual
-
 
 freeVariables :: Term' -> Set.Set Name
 freeVariables = cata inExpression
@@ -125,6 +112,22 @@ maxBoundVariable = cata (\ expression -> case expression of
   _ -> Nothing)
 
 
+-- Equality
+
+unify :: Term' -> Term' -> Unification'
+unify expected actual = case (out expected, out actual) of
+  (_, Implicit) -> into expected
+  (Implicit, _) -> into actual
+
+  (Type, Type) -> into expected
+
+  (Variable n1, Variable n2) | n1 == n2 -> Unification $ Variable n2
+  (Application a1 b1, Application a2 b2) -> Unification $ Application (unify a1 a2) (unify b1 b2)
+  (Lambda i1 a1 b1, Lambda i2 a2 b2) | i1 == i2 -> Unification $ Lambda i2 (unify a1 a2) (unify b1 b2)
+
+  _ -> Conflict expected actual
+
+
 -- Recursion schemes
 
 cata :: Functor f => (f a -> a) -> Term f -> a

From 78bb942d978c5dae4c845abd0f38a0ac8024dd12 Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Sun, 10 Jan 2016 12:51:02 -0500
Subject: [PATCH 002/109] Stub in a heading for typechecking.

---
 src/Curve.hs | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/Curve.hs b/src/Curve.hs
index 559667f..d46f254 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -112,6 +112,9 @@ maxBoundVariable = cata (\ expression -> case expression of
   _ -> Nothing)
 
 
+-- Typechecking
+
+
 -- Equality
 
 unify :: Term' -> Term' -> Unification'

From 670fe15a720dd8c88672e11fa5fa079281cff062 Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Sun, 10 Jan 2016 12:52:19 -0500
Subject: [PATCH 003/109] Add a type synonym for contexts.

---
 src/Curve.hs | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/Curve.hs b/src/Curve.hs
index d46f254..104b41d 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -4,6 +4,7 @@ module Curve where
 import Data.Functor.Classes
 import qualified Data.List as List
 import qualified Data.Set as Set
+import qualified Data.Map as Map
 
 data Name
   = Local Int
@@ -114,6 +115,8 @@ maxBoundVariable = cata (\ expression -> case expression of
 
 -- Typechecking
 
+type Context = Map.Map Name Term'
+
 
 -- Equality
 

From a23775631a13f2fe538fbee82ea0cf8b8efd9420 Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Sun, 10 Jan 2016 12:54:31 -0500
Subject: [PATCH 004/109] Add a type synonym for inferers.

---
 src/Curve.hs | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/Curve.hs b/src/Curve.hs
index 104b41d..6ee63a1 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -116,6 +116,7 @@ maxBoundVariable = cata (\ expression -> case expression of
 -- Typechecking
 
 type Context = Map.Map Name Term'
+type Inferer = Context -> Unification'
 
 
 -- Equality

From af492e6df092494d0ccd139af5c961305813b44f Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Sun, 10 Jan 2016 12:54:37 -0500
Subject: [PATCH 005/109] Add a type synonym for checkers.

---
 src/Curve.hs | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/Curve.hs b/src/Curve.hs
index 6ee63a1..cd4c858 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -117,6 +117,7 @@ maxBoundVariable = cata (\ expression -> case expression of
 
 type Context = Map.Map Name Term'
 type Inferer = Context -> Unification'
+type Checker = Term' -> Inferer
 
 
 -- Equality

From 2e7cd74e681958d0494bb94c3ab775feffb0f4fb Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Sun, 10 Jan 2016 13:28:19 -0500
Subject: [PATCH 006/109] Remove the Inferer/Checker synonyms.

---
 src/Curve.hs | 2 --
 1 file changed, 2 deletions(-)

diff --git a/src/Curve.hs b/src/Curve.hs
index cd4c858..104b41d 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -116,8 +116,6 @@ maxBoundVariable = cata (\ expression -> case expression of
 -- Typechecking
 
 type Context = Map.Map Name Term'
-type Inferer = Context -> Unification'
-type Checker = Term' -> Inferer
 
 
 -- Equality

From 941e1e9a47fec2f557b21bae49b2794a0f52516a Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Sun, 10 Jan 2016 14:05:44 -0500
Subject: [PATCH 007/109] Add an Error case to Unification.

---
 src/Curve.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Curve.hs b/src/Curve.hs
index 104b41d..20ad5b8 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -22,7 +22,7 @@ data Expression term
 data Term f = Term { out :: f (Term f) }
 type Term' = Term Expression
 
-data Unification f = Unification (f (Unification f)) | Conflict (Term f) (Term f)
+data Unification f = Unification (f (Unification f)) | Conflict (Term f) (Term f) | Error String
 type Unification' = Unification Expression
 
 

From c9ec209349186e7cd052824b1de45c0eb7fed93f Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Sun, 10 Jan 2016 14:05:54 -0500
Subject: [PATCH 008/109] =?UTF-8?q?Errors=20don=E2=80=99t=20have=20a=20uni?=
 =?UTF-8?q?fied=20term.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/Curve.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Curve.hs b/src/Curve.hs
index 20ad5b8..d6a6147 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -73,7 +73,7 @@ into term = Unification $ into <$> out term
 
 unified :: Unification' -> Maybe Term'
 unified (Unification expression) = Term <$> traverse unified expression
-unified (Conflict _ _) = Nothing
+unified _ = Nothing
 
 
 -- Binding

From 8a7d3a87760490a5415cf9d722ab705bac0e167d Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Sun, 10 Jan 2016 14:05:59 -0500
Subject: [PATCH 009/109] Errors can equate.

---
 src/Curve.hs | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/Curve.hs b/src/Curve.hs
index d6a6147..ae78bec 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -196,6 +196,7 @@ instance Eq1 f => Eq (Term f) where
 instance Eq1 f => Eq (Unification f) where
   Unification a == Unification b = a `eq1` b
   Conflict a1 b1 == Conflict a2 b2 = a1 == a2 && b1 == b2
+  Error s1 == Error s2 = s1 == s2
   _ == _ = False
 
 instance Show Unification' where

From 484486b58d9ed5d933d6593cef7bdced5d4ccfb9 Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Sun, 10 Jan 2016 14:06:04 -0500
Subject: [PATCH 010/109] Errors can be shown.

---
 src/Curve.hs | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/Curve.hs b/src/Curve.hs
index ae78bec..d46f6cb 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -203,3 +203,4 @@ instance Show Unification' where
   show (Unification out) = show out
   show (Conflict a b) = "Expected: " ++ show a ++ "\n"
                      ++ "  Actual: " ++ show b ++ "\n"
+  show (Error s) = "Error: " ++ s

From 965b819c0e3328245b12dc0f18ba1c2f360648d8 Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Sun, 10 Jan 2016 15:05:58 -0500
Subject: [PATCH 011/109] Stub in typechecking.

---
 src/Curve.hs | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/src/Curve.hs b/src/Curve.hs
index d46f6cb..2da298f 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -117,6 +117,12 @@ maxBoundVariable = cata (\ expression -> case expression of
 
 type Context = Map.Map Name Term'
 
+check :: Term' -> Context -> Term' -> Unification'
+check expected context term = case (out term, out expected) of
+  (_, Implicit) -> Error $ "No rule to infer type of " ++ show term
+  (_, _) -> let unification = infer context term in
+    maybe unification (unify expected) $ unified unification
+
 
 -- Equality
 

From 4fb4753bf9b977f6264521aa8008124e15d46fa3 Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Sun, 10 Jan 2016 15:06:37 -0500
Subject: [PATCH 012/109] Inference.

---
 src/Curve.hs | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/Curve.hs b/src/Curve.hs
index 2da298f..a85de0c 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -117,6 +117,9 @@ maxBoundVariable = cata (\ expression -> case expression of
 
 type Context = Map.Map Name Term'
 
+infer :: Context -> Term' -> Unification'
+infer = check implicit
+
 check :: Term' -> Context -> Term' -> Unification'
 check expected context term = case (out term, out expected) of
   (_, Implicit) -> Error $ "No rule to infer type of " ++ show term

From e7e3a33b5afcc8af0e1398f6cdd00e08e6476682 Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Sun, 10 Jan 2016 15:06:42 -0500
Subject: [PATCH 013/109] Infer the type of type.

---
 src/Curve.hs | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/Curve.hs b/src/Curve.hs
index a85de0c..34705b6 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -122,6 +122,8 @@ infer = check implicit
 
 check :: Term' -> Context -> Term' -> Unification'
 check expected context term = case (out term, out expected) of
+  (Type, Implicit) -> Unification Type
+
   (_, Implicit) -> Error $ "No rule to infer type of " ++ show term
   (_, _) -> let unification = infer context term in
     maybe unification (unify expected) $ unified unification

From a2f893159b775a6efe86a80ca4bec6f943e12262 Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Sun, 10 Jan 2016 15:11:41 -0500
Subject: [PATCH 014/109] Infer the types of variables.

---
 src/Curve.hs | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/Curve.hs b/src/Curve.hs
index 34705b6..a5262fc 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -124,6 +124,8 @@ check :: Term' -> Context -> Term' -> Unification'
 check expected context term = case (out term, out expected) of
   (Type, Implicit) -> Unification Type
 
+  (Variable name, Implicit) -> maybe (Error $ "unexpectedly free variable " ++ show name) into (Map.lookup name context)
+
   (_, Implicit) -> Error $ "No rule to infer type of " ++ show term
   (_, _) -> let unification = infer context term in
     maybe unification (unify expected) $ unified unification

From 56d450730569ea355cae2181744179a7dd54903b Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Sun, 10 Jan 2016 15:18:10 -0500
Subject: [PATCH 015/109] Parameterize Unification by the type of conflicts.

Going to see if it can reasonably be a monad.
---
 src/Curve.hs | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/Curve.hs b/src/Curve.hs
index a5262fc..3fcd543 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -22,8 +22,8 @@ data Expression term
 data Term f = Term { out :: f (Term f) }
 type Term' = Term Expression
 
-data Unification f = Unification (f (Unification f)) | Conflict (Term f) (Term f) | Error String
-type Unification' = Unification Expression
+data Unification f term = Unification (f (Unification f term)) | Conflict term term | Error String
+type Unification' = Unification Expression Term'
 
 
 -- DSL for constructing terms
@@ -68,7 +68,7 @@ pi = lambda
 
 -- Unifications
 
-into :: Functor f => Term f -> Unification f
+into :: Functor f => Term f -> Unification f (Term f)
 into term = Unification $ into <$> out term
 
 unified :: Unification' -> Maybe Term'
@@ -206,7 +206,7 @@ showsType = showsLevel True
 instance Eq1 f => Eq (Term f) where
   a == b = out a `eq1` out b
 
-instance Eq1 f => Eq (Unification f) where
+instance (Eq1 f, Eq term) => Eq (Unification f term) where
   Unification a == Unification b = a `eq1` b
   Conflict a1 b1 == Conflict a2 b2 = a1 == a2 && b1 == b2
   Error s1 == Error s2 = s1 == s2

From d76d4fb35cffcf98e6c64322317516b3d46a99ee Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Sun, 10 Jan 2016 15:18:50 -0500
Subject: [PATCH 016/109] Unification is a Functor.

---
 src/Curve.hs | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/Curve.hs b/src/Curve.hs
index 3fcd543..93b10b0 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -23,6 +23,7 @@ data Term f = Term { out :: f (Term f) }
 type Term' = Term Expression
 
 data Unification f term = Unification (f (Unification f term)) | Conflict term term | Error String
+  deriving Functor
 type Unification' = Unification Expression Term'
 
 

From d1fe64239475339461be2695f73530b7adf6e735 Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Sun, 10 Jan 2016 15:19:42 -0500
Subject: [PATCH 017/109] Revert "Unification is a Functor."

This reverts commit d76d4fb35cffcf98e6c64322317516b3d46a99ee.
---
 src/Curve.hs | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/Curve.hs b/src/Curve.hs
index 93b10b0..3fcd543 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -23,7 +23,6 @@ data Term f = Term { out :: f (Term f) }
 type Term' = Term Expression
 
 data Unification f term = Unification (f (Unification f term)) | Conflict term term | Error String
-  deriving Functor
 type Unification' = Unification Expression Term'
 
 

From d657a6daa312354923d157292393649d00fa7dbf Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Sun, 10 Jan 2016 15:19:46 -0500
Subject: [PATCH 018/109] Revert "Parameterize Unification by the type of
 conflicts."

This reverts commit 56d450730569ea355cae2181744179a7dd54903b.
---
 src/Curve.hs | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/Curve.hs b/src/Curve.hs
index 3fcd543..a5262fc 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -22,8 +22,8 @@ data Expression term
 data Term f = Term { out :: f (Term f) }
 type Term' = Term Expression
 
-data Unification f term = Unification (f (Unification f term)) | Conflict term term | Error String
-type Unification' = Unification Expression Term'
+data Unification f = Unification (f (Unification f)) | Conflict (Term f) (Term f) | Error String
+type Unification' = Unification Expression
 
 
 -- DSL for constructing terms
@@ -68,7 +68,7 @@ pi = lambda
 
 -- Unifications
 
-into :: Functor f => Term f -> Unification f (Term f)
+into :: Functor f => Term f -> Unification f
 into term = Unification $ into <$> out term
 
 unified :: Unification' -> Maybe Term'
@@ -206,7 +206,7 @@ showsType = showsLevel True
 instance Eq1 f => Eq (Term f) where
   a == b = out a `eq1` out b
 
-instance (Eq1 f, Eq term) => Eq (Unification f term) where
+instance Eq1 f => Eq (Unification f) where
   Unification a == Unification b = a `eq1` b
   Conflict a1 b1 == Conflict a2 b2 = a1 == a2 && b1 == b2
   Error s1 == Error s2 = s1 == s2

From 63001ed5093c007f6c6b2ba6b92912420f460624 Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Sun, 10 Jan 2016 15:34:02 -0500
Subject: [PATCH 019/109] Add a Roll typeclass.

---
 src/Curve.hs | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/Curve.hs b/src/Curve.hs
index a5262fc..7859a4b 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -19,6 +19,9 @@ data Expression term
   | Application term term
   deriving (Show, Eq, Functor, Foldable, Traversable)
 
+class Roll g where
+  roll :: f (g f) -> g f
+
 data Term f = Term { out :: f (Term f) }
 type Term' = Term Expression
 

From 67bd56c2e2631edf254b7ebc68cbb9301441d009 Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Sun, 10 Jan 2016 15:34:33 -0500
Subject: [PATCH 020/109] Add a Roll instance for Term.

---
 src/Curve.hs | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/Curve.hs b/src/Curve.hs
index 7859a4b..64986e8 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -220,3 +220,6 @@ instance Show Unification' where
   show (Conflict a b) = "Expected: " ++ show a ++ "\n"
                      ++ "  Actual: " ++ show b ++ "\n"
   show (Error s) = "Error: " ++ s
+
+instance Roll Term where
+  roll = Term

From cd2a93550ff0ad09002c28149afe7ff8c4436bcf Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Sun, 10 Jan 2016 15:35:05 -0500
Subject: [PATCH 021/109] Add a Roll instance for Unification.

---
 src/Curve.hs | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/Curve.hs b/src/Curve.hs
index 64986e8..0f891a8 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -223,3 +223,6 @@ instance Show Unification' where
 
 instance Roll Term where
   roll = Term
+
+instance Roll Unification where
+  roll = Unification

From 3a6312d18555ccdd63bd5e2b6fdfec8f87078748 Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Sun, 10 Jan 2016 15:36:02 -0500
Subject: [PATCH 022/109] Generalize type' to Roll instances.

---
 src/Curve.hs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Curve.hs b/src/Curve.hs
index 0f891a8..9ef500f 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -31,8 +31,8 @@ type Unification' = Unification Expression
 
 -- DSL for constructing terms
 
-type' :: Term'
-type' = Term Type
+type' :: Roll f => f Expression
+type' = roll Type
 
 implicit :: Term'
 implicit = Term Implicit

From e2ef41ae34bc2ddc7ea8c7874adf0c2c3d94e635 Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Sun, 10 Jan 2016 15:36:24 -0500
Subject: [PATCH 023/109] Generalize implicit to Roll instances.

---
 src/Curve.hs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Curve.hs b/src/Curve.hs
index 9ef500f..d95c0fb 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -34,8 +34,8 @@ type Unification' = Unification Expression
 type' :: Roll f => f Expression
 type' = roll Type
 
-implicit :: Term'
-implicit = Term Implicit
+implicit :: Roll f => f Expression
+implicit = roll Implicit
 
 variable :: Name -> Term'
 variable = Term . Variable

From d9cac9a16523e3318605812e5e835d9715b04cbe Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Sun, 10 Jan 2016 15:36:51 -0500
Subject: [PATCH 024/109] Generalize variable to Roll instances.

---
 src/Curve.hs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Curve.hs b/src/Curve.hs
index d95c0fb..258acef 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -37,8 +37,8 @@ type' = roll Type
 implicit :: Roll f => f Expression
 implicit = roll Implicit
 
-variable :: Name -> Term'
-variable = Term . Variable
+variable :: Roll f => Name -> f Expression
+variable = roll . Variable
 
 local :: Int -> Term'
 local = variable . Local

From 382f4ed63d2a2f6c543252c2438d09beec85872f Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Sun, 10 Jan 2016 15:37:34 -0500
Subject: [PATCH 025/109] Change the type variable to r.

---
 src/Curve.hs | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/Curve.hs b/src/Curve.hs
index 258acef..c15be0d 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -31,13 +31,13 @@ type Unification' = Unification Expression
 
 -- DSL for constructing terms
 
-type' :: Roll f => f Expression
+type' :: Roll r => r Expression
 type' = roll Type
 
-implicit :: Roll f => f Expression
+implicit :: Roll r => r Expression
 implicit = roll Implicit
 
-variable :: Roll f => Name -> f Expression
+variable :: Roll r => Name -> r Expression
 variable = roll . Variable
 
 local :: Int -> Term'

From 8418a71d699b3deba122a154cf81e0a220b81816 Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Sun, 10 Jan 2016 15:37:42 -0500
Subject: [PATCH 026/109] Generalize local.

---
 src/Curve.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Curve.hs b/src/Curve.hs
index c15be0d..1c6949f 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -40,7 +40,7 @@ implicit = roll Implicit
 variable :: Roll r => Name -> r Expression
 variable = roll . Variable
 
-local :: Int -> Term'
+local :: Roll r => Int -> r Expression
 local = variable . Local
 
 global :: String -> Term'

From 5f33d83555f01cbceea8b4f209f7f34ea60dc9d3 Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Sun, 10 Jan 2016 15:37:52 -0500
Subject: [PATCH 027/109] Generalize global.

---
 src/Curve.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Curve.hs b/src/Curve.hs
index 1c6949f..cf5a6fb 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -43,7 +43,7 @@ variable = roll . Variable
 local :: Roll r => Int -> r Expression
 local = variable . Local
 
-global :: String -> Term'
+global :: Roll r => String -> r Expression
 global = variable . Global
 
 infixl 9 `apply`

From c03c36aaf1622c868c60469ef16c8b94deeccec0 Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Sun, 10 Jan 2016 15:40:05 -0500
Subject: [PATCH 028/109] Generalize apply.

---
 src/Curve.hs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Curve.hs b/src/Curve.hs
index cf5a6fb..cc06b9d 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -48,8 +48,8 @@ global = variable . Global
 
 infixl 9 `apply`
 
-apply :: Term' -> Term' -> Term'
-apply a = Term . Application a
+apply :: Roll r => r Expression -> r Expression -> r Expression
+apply a = roll . Application a
 
 infixr `lambda`
 

From 0037f1ee030c73b3e3ae0a0df20fa253545c005a Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Sun, 10 Jan 2016 15:50:51 -0500
Subject: [PATCH 029/109] Add a Catamorphable typeclass with an instance for
 Term.

---
 src/Curve.hs | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/src/Curve.hs b/src/Curve.hs
index cc06b9d..9628d21 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -22,6 +22,9 @@ data Expression term
 class Roll g where
   roll :: f (g f) -> g f
 
+class Catamorphable r where
+  cata :: Functor f => (f a -> a) -> r f -> a
+
 data Term f = Term { out :: f (Term f) }
 type Term' = Term Expression
 
@@ -152,8 +155,8 @@ unify expected actual = case (out expected, out actual) of
 
 -- Recursion schemes
 
-cata :: Functor f => (f a -> a) -> Term f -> a
-cata f = f . fmap (cata f) . out
+instance Catamorphable Term where
+  cata f = f . fmap (cata f) . out
 
 para :: Functor f => (f (Term f, a) -> a) -> Term f -> a
 para f = f . fmap fanout . out

From 71d47de62e4b0f4ad8d4a70b40de9ba295eff680 Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Sun, 10 Jan 2016 15:52:28 -0500
Subject: [PATCH 030/109] Add an Unroll typeclass.

---
 src/Curve.hs | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/Curve.hs b/src/Curve.hs
index 9628d21..bc5b52d 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -22,6 +22,9 @@ data Expression term
 class Roll g where
   roll :: f (g f) -> g f
 
+class Unroll r where
+  unroll :: r f -> f (r f)
+
 class Catamorphable r where
   cata :: Functor f => (f a -> a) -> r f -> a
 

From 10373608b7aaac396483ccc4e9a624f84a87bebc Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Sun, 10 Jan 2016 15:53:41 -0500
Subject: [PATCH 031/109] Add a `para` function w/default implementation for
 Unrollable types.

---
 src/Curve.hs | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/src/Curve.hs b/src/Curve.hs
index bc5b52d..80ffdd9 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -28,6 +28,11 @@ class Unroll r where
 class Catamorphable r where
   cata :: Functor f => (f a -> a) -> r f -> a
 
+  para :: (Unroll r, Functor f) => (f (r f, a) -> a) -> r f -> a
+  para f = f . fmap fanout . unroll
+    where fanout a = (a, para f a)
+
+
 data Term f = Term { out :: f (Term f) }
 type Term' = Term Expression
 
@@ -161,10 +166,6 @@ unify expected actual = case (out expected, out actual) of
 instance Catamorphable Term where
   cata f = f . fmap (cata f) . out
 
-para :: Functor f => (f (Term f, a) -> a) -> Term f -> a
-para f = f . fmap fanout . out
-  where fanout a = (a, para f a)
-
 
 -- Numerals
 

From da516ed3816440800432579a49deeaa957d33fac Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Sun, 10 Jan 2016 15:53:53 -0500
Subject: [PATCH 032/109] Generalize maxBoundVariable to Catamorphable terms.

---
 src/Curve.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Curve.hs b/src/Curve.hs
index 80ffdd9..be008da 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -120,7 +120,7 @@ freeVariables = cata inExpression
           Application a b -> a `Set.union` b
           _ -> mempty
 
-maxBoundVariable :: Term' -> Maybe Int
+maxBoundVariable :: Catamorphable r => r Expression -> Maybe Int
 maxBoundVariable = cata (\ expression -> case expression of
   Lambda n t _ -> max (Just n) t
   Application a b -> max a b

From 1622693210cfc96ffb9d2ba86461bee39804949b Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Sun, 10 Jan 2016 15:54:56 -0500
Subject: [PATCH 033/109] Add an Unroll instance for Term.

---
 src/Curve.hs | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/Curve.hs b/src/Curve.hs
index be008da..43547ce 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -231,5 +231,8 @@ instance Show Unification' where
 instance Roll Term where
   roll = Term
 
+instance Unroll Term where
+  unroll = out
+
 instance Roll Unification where
   roll = Unification

From efc1bd5afd1a635996e342042317758cd69de5e7 Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Sun, 10 Jan 2016 15:57:15 -0500
Subject: [PATCH 034/109] Replace the Catamorphable instance for Term with one
 for Unroll.

---
 src/Curve.hs | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/src/Curve.hs b/src/Curve.hs
index 43547ce..d52167e 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE DeriveFunctor, DeriveFoldable, DeriveTraversable, FlexibleInstances #-}
+{-# LANGUAGE DeriveFunctor, DeriveFoldable, DeriveTraversable, FlexibleInstances, UndecidableInstances #-}
 module Curve where
 
 import Data.Functor.Classes
@@ -32,6 +32,8 @@ class Catamorphable r where
   para f = f . fmap fanout . unroll
     where fanout a = (a, para f a)
 
+instance Unroll r => Catamorphable r where
+  cata f = f . fmap (cata f) . unroll
 
 data Term f = Term { out :: f (Term f) }
 type Term' = Term Expression
@@ -163,9 +165,6 @@ unify expected actual = case (out expected, out actual) of
 
 -- Recursion schemes
 
-instance Catamorphable Term where
-  cata f = f . fmap (cata f) . out
-
 
 -- Numerals
 

From d5e7cec65012ae8fd9dc9e970188e42d65c86887 Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Sun, 10 Jan 2016 15:58:39 -0500
Subject: [PATCH 035/109] Move the `para` implementation into the `Unroll`
 instance of `Catamorphable`.

---
 src/Curve.hs | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/src/Curve.hs b/src/Curve.hs
index d52167e..d176cad 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -28,13 +28,14 @@ class Unroll r where
 class Catamorphable r where
   cata :: Functor f => (f a -> a) -> r f -> a
 
-  para :: (Unroll r, Functor f) => (f (r f, a) -> a) -> r f -> a
-  para f = f . fmap fanout . unroll
-    where fanout a = (a, para f a)
+  para :: Functor f => (f (r f, a) -> a) -> r f -> a
 
 instance Unroll r => Catamorphable r where
   cata f = f . fmap (cata f) . unroll
 
+  para f = f . fmap fanout . unroll
+    where fanout a = (a, para f a)
+
 data Term f = Term { out :: f (Term f) }
 type Term' = Term Expression
 

From 2d95bc6817d7ec570e518b01b155a65cfd835015 Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Sun, 10 Jan 2016 15:59:03 -0500
Subject: [PATCH 036/109] Move the Catamorphable instance to the bottom.

---
 src/Curve.hs | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/src/Curve.hs b/src/Curve.hs
index d176cad..cdbc5a5 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -30,12 +30,6 @@ class Catamorphable r where
 
   para :: Functor f => (f (r f, a) -> a) -> r f -> a
 
-instance Unroll r => Catamorphable r where
-  cata f = f . fmap (cata f) . unroll
-
-  para f = f . fmap fanout . unroll
-    where fanout a = (a, para f a)
-
 data Term f = Term { out :: f (Term f) }
 type Term' = Term Expression
 
@@ -236,3 +230,9 @@ instance Unroll Term where
 
 instance Roll Unification where
   roll = Unification
+
+instance Unroll r => Catamorphable r where
+  cata f = f . fmap (cata f) . unroll
+
+  para f = f . fmap fanout . unroll
+    where fanout a = (a, para f a)

From 3658b6c2fc381043aa2552814eaaa09a533e068d Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Sun, 10 Jan 2016 16:00:29 -0500
Subject: [PATCH 037/109] Add a PartialUnroll typeclass.

---
 src/Curve.hs | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/Curve.hs b/src/Curve.hs
index cdbc5a5..dd20b90 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -25,6 +25,9 @@ class Roll g where
 class Unroll r where
   unroll :: r f -> f (r f)
 
+class PartialUnroll r where
+  unrollMaybe :: r f -> Maybe (f (r f))
+
 class Catamorphable r where
   cata :: Functor f => (f a -> a) -> r f -> a
 

From adebe6e87d44c2b25ae0b28061279e437c386beb Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Sun, 10 Jan 2016 16:00:36 -0500
Subject: [PATCH 038/109] Add a PartialUnroll instance for Unification.

---
 src/Curve.hs | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/Curve.hs b/src/Curve.hs
index dd20b90..eeecd26 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -239,3 +239,7 @@ instance Unroll r => Catamorphable r where
 
   para f = f . fmap fanout . unroll
     where fanout a = (a, para f a)
+
+instance PartialUnroll Unification where
+  unrollMaybe (Unification expression) = Just expression
+  unrollMaybe _ = Nothing

From ae64762ed9649dee2dbecb0c85e488e142570f58 Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Sun, 10 Jan 2016 16:01:26 -0500
Subject: [PATCH 039/109] Move the typeclasses down into their own section.

---
 src/Curve.hs | 31 +++++++++++++++++--------------
 1 file changed, 17 insertions(+), 14 deletions(-)

diff --git a/src/Curve.hs b/src/Curve.hs
index eeecd26..679644d 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -19,20 +19,6 @@ data Expression term
   | Application term term
   deriving (Show, Eq, Functor, Foldable, Traversable)
 
-class Roll g where
-  roll :: f (g f) -> g f
-
-class Unroll r where
-  unroll :: r f -> f (r f)
-
-class PartialUnroll r where
-  unrollMaybe :: r f -> Maybe (f (r f))
-
-class Catamorphable r where
-  cata :: Functor f => (f a -> a) -> r f -> a
-
-  para :: Functor f => (f (r f, a) -> a) -> r f -> a
-
 data Term f = Term { out :: f (Term f) }
 type Term' = Term Expression
 
@@ -178,6 +164,23 @@ showNumeral "" _ = ""
 showNumeral alphabet i = List.genericIndex alphabet <$> digits (List.genericLength alphabet) i
 
 
+-- Classes
+
+class Roll g where
+  roll :: f (g f) -> g f
+
+class Unroll r where
+  unroll :: r f -> f (r f)
+
+class PartialUnroll r where
+  unrollMaybe :: r f -> Maybe (f (r f))
+
+class Catamorphable r where
+  cata :: Functor f => (f a -> a) -> r f -> a
+
+  para :: Functor f => (f (r f, a) -> a) -> r f -> a
+
+
 -- Instances
 
 instance Show Name where

From 466d11233337a93205bdd9a35c31c3220e21ec7d Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Sun, 10 Jan 2016 16:24:03 -0500
Subject: [PATCH 040/109] Use the `local` constructor for the variable.

---
 src/Curve.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Curve.hs b/src/Curve.hs
index 679644d..a09e4d1 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -53,7 +53,7 @@ infixr `lambda`
 lambda :: Term' -> (Term' -> Term') -> Term'
 lambda t f = Term $ Lambda i t body
   where i = maybe 0 succ $ maxBoundVariable body
-        body = f (Term $ Variable $ Local i)
+        body = f (local i)
 
 infixr -->
 

From d83a75c0119641258c8c5844484f96cc929a46d1 Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Sun, 10 Jan 2016 16:24:12 -0500
Subject: [PATCH 041/109] `roll`.

---
 src/Curve.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Curve.hs b/src/Curve.hs
index a09e4d1..f88743f 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -51,7 +51,7 @@ apply a = roll . Application a
 infixr `lambda`
 
 lambda :: Term' -> (Term' -> Term') -> Term'
-lambda t f = Term $ Lambda i t body
+lambda t f = roll $ Lambda i t body
   where i = maybe 0 succ $ maxBoundVariable body
         body = f (local i)
 

From c645a1fa1c429bc9f6bd085b4a809d014c5299cd Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Sun, 10 Jan 2016 16:24:53 -0500
Subject: [PATCH 042/109] Handle errors in flipUnification.

---
 test/Spec.hs | 1 +
 1 file changed, 1 insertion(+)

diff --git a/test/Spec.hs b/test/Spec.hs
index 9a74ca9..5ae851b 100644
--- a/test/Spec.hs
+++ b/test/Spec.hs
@@ -81,3 +81,4 @@ main = hspec $ do
 
   where flipUnification (Conflict a b) = Conflict b a
         flipUnification (Unification out) = Unification $ flipUnification <$> out
+        flipUnification otherwise = otherwise

From 0d3f3d36e8be56af06714272fc581f6e268bcb15 Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Sun, 10 Jan 2016 16:25:31 -0500
Subject: [PATCH 043/109] Annotate a bunch of term types.

---
 test/Spec.hs | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/test/Spec.hs b/test/Spec.hs
index 5ae851b..c068f2d 100644
--- a/test/Spec.hs
+++ b/test/Spec.hs
@@ -46,7 +46,7 @@ main = hspec $ do
 
   describe "showsLevelPrec" $ do
     prop "parenthesizes right-nested applications" $
-      \ a b c -> show (apply a (apply b c)) `shouldBe` showsPrec 10 a " (" ++ showsPrec 10 (apply b c) ")"
+      \ a b c -> show (apply a (apply b c)) `shouldBe` showsPrec 10 a " (" ++ showsPrec 10 (apply b c :: Term') ")"
 
     prop "shows non-dependent function types with an arrow operator" $
       \ a b -> showsLevelPrec True 0 (Term $ Lambda 0 a b) "" `shouldBe` showsLevelPrec True 1 a " → " ++ showsType b ""
@@ -64,20 +64,20 @@ main = hspec $ do
       \ isType prec -> showsLevelPrec isType prec implicit "" `shouldBe` "_"
 
     prop "pretty-prints local variables alphabetically" $
-      \ i -> show (local i) `shouldBe` showNumeral ['a'..'z'] i
+      \ i -> show (local i :: Term') `shouldBe` showNumeral ['a'..'z'] i
 
     it "should format the identity function appropriately" $
       show (Term $ Lambda 1 type' $ Term $ Lambda 0 (local 1) (local 0)) `shouldBe` "λ b : Type . λ a : b . a"
 
   describe "DSL" $ do
     prop "apply associates leftwards" $
-      \ a b c -> a `apply` b `apply` c `shouldBe` (a `apply` b) `apply` c
+      \ a b c -> a `apply` b `apply` c `shouldBe` (a `apply` b) `apply` (c :: Term')
 
     prop "--> associates rightwards" $
-      \ a b c -> a --> b --> c `shouldBe` a --> (b --> c)
+      \ a b c -> a --> b --> c `shouldBe` a --> (b --> c :: Term')
 
     it "lambda avoids shadowing" $
-      show (type' `lambda` \ b -> b `lambda` id) `shouldBe` "λ b : Type . λ a : b . a"
+      show (type' `lambda` \ b -> b `lambda` id :: Term') `shouldBe` "λ b : Type . λ a : b . a"
 
   where flipUnification (Conflict a b) = Conflict b a
         flipUnification (Unification out) = Unification $ flipUnification <$> out

From 4d04400286968d61575733718dd9b941f08f3588 Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Sun, 10 Jan 2016 16:26:51 -0500
Subject: [PATCH 044/109] Remove the recursion schemes heading.

---
 src/Curve.hs | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/src/Curve.hs b/src/Curve.hs
index f88743f..de55164 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -147,9 +147,6 @@ unify expected actual = case (out expected, out actual) of
   _ -> Conflict expected actual
 
 
--- Recursion schemes
-
-
 -- Numerals
 
 digits :: Integral a => a -> a -> [a]

From 50140a38e294a4ddef003b137c9461040914a693 Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Sun, 10 Jan 2016 16:27:55 -0500
Subject: [PATCH 045/109] Total Unroll instances can be lowered to
 PartialUnroll instances.

---
 src/Curve.hs | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/Curve.hs b/src/Curve.hs
index de55164..be55855 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -234,6 +234,9 @@ instance Unroll Term where
 instance Roll Unification where
   roll = Unification
 
+instance Unroll r => PartialUnroll r where
+  unrollMaybe = Just . unroll
+
 instance Unroll r => Catamorphable r where
   cata f = f . fmap (cata f) . unroll
 

From 357e957277113cb75a12f708867ac818eb4d7a0c Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Sun, 10 Jan 2016 17:05:57 -0500
Subject: [PATCH 046/109] Generalize maxBoundVariable to PartialUnroll.

---
 src/Curve.hs | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/Curve.hs b/src/Curve.hs
index be55855..7acaad7 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -106,11 +106,11 @@ freeVariables = cata inExpression
           Application a b -> a `Set.union` b
           _ -> mempty
 
-maxBoundVariable :: Catamorphable r => r Expression -> Maybe Int
-maxBoundVariable = cata (\ expression -> case expression of
-  Lambda n t _ -> max (Just n) t
-  Application a b -> max a b
-  _ -> Nothing)
+maxBoundVariable :: PartialUnroll r => r Expression -> Maybe Int
+maxBoundVariable = foldl maximal Nothing . unrollMaybe
+  where maximal into (Lambda i t _) = max into $ max (Just i) (maxBoundVariable t)
+        maximal into (Application a b) = max into $ max (maxBoundVariable a) (maxBoundVariable b)
+        maximal into _ = into
 
 
 -- Typechecking

From 0cb5baa04f9f8b3b941e175190c3a31b9bf98ee0 Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Sun, 10 Jan 2016 17:06:11 -0500
Subject: [PATCH 047/109] Generalize lambda to Roll/PartialUnroll r.

---
 src/Curve.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Curve.hs b/src/Curve.hs
index 7acaad7..e2f9038 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -50,7 +50,7 @@ apply a = roll . Application a
 
 infixr `lambda`
 
-lambda :: Term' -> (Term' -> Term') -> Term'
+lambda :: (Roll r, PartialUnroll r) => r Expression -> (r Expression -> r Expression) -> r Expression
 lambda t f = roll $ Lambda i t body
   where i = maybe 0 succ $ maxBoundVariable body
         body = f (local i)

From 74ba982d54b8b1bcfceba6c437f06c37735c5720 Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Sun, 10 Jan 2016 17:06:54 -0500
Subject: [PATCH 048/109] Generalize --> to Roll/PartialUnroll.

---
 src/Curve.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Curve.hs b/src/Curve.hs
index e2f9038..99171da 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -57,7 +57,7 @@ lambda t f = roll $ Lambda i t body
 
 infixr -->
 
-(-->) :: Term' -> Term' -> Term'
+(-->) :: (Roll r, PartialUnroll r) => r Expression -> r Expression -> r Expression
 a --> b = a `lambda` const b
 
 infixr `pi`

From 4460e60b6c9f48797bffa6fe9ba4134e365ab7d6 Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Sun, 10 Jan 2016 17:15:27 -0500
Subject: [PATCH 049/109] Add an explicit instance of PartialUnroll for Term.

---
 src/Curve.hs | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/Curve.hs b/src/Curve.hs
index 99171da..c3e3504 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -231,12 +231,12 @@ instance Roll Term where
 instance Unroll Term where
   unroll = out
 
+instance PartialUnroll Term where
+  unrollMaybe = Just . unroll
+
 instance Roll Unification where
   roll = Unification
 
-instance Unroll r => PartialUnroll r where
-  unrollMaybe = Just . unroll
-
 instance Unroll r => Catamorphable r where
   cata f = f . fmap (cata f) . unroll
 

From e4390863a4602fda6e2071ccfe0fe412d4764f0c Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Sun, 10 Jan 2016 17:15:32 -0500
Subject: [PATCH 050/109] Generalize substitution to Roll/PartialUnroll.

---
 src/Curve.hs | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/src/Curve.hs b/src/Curve.hs
index c3e3504..4e2ff1b 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -88,13 +88,13 @@ rename old new term = Term $ case out term of
   Application a b -> Application (rename old new a) (rename old new b)
   other -> other
 
-substitute :: Int -> Term' -> Term' -> Term'
-substitute name withTerm inScope = case out inScope of
-  Variable (Local n) | n == name -> withTerm
-  Lambda n inType inBody -> if n == name
-    then Term $ Lambda n (substitute name withTerm inType) inBody
-    else Term $ Lambda n (substitute name withTerm inType) (substitute name withTerm inBody)
-  Application inA inB -> Term $ Application (substitute name withTerm inA) (substitute name withTerm inB)
+substitute :: (Roll r, PartialUnroll r) => Int -> r Expression -> r Expression -> r Expression
+substitute name withTerm inScope = case unrollMaybe inScope of
+  Just (Variable (Local n)) | n == name -> withTerm
+  Just (Lambda n inType inBody) -> if n == name
+    then roll $ Lambda n (substitute name withTerm inType) inBody
+    else roll $ Lambda n (substitute name withTerm inType) (substitute name withTerm inBody)
+  Just (Application inA inB) -> roll $ Application (substitute name withTerm inA) (substitute name withTerm inB)
   _ -> inScope
 
 

From 5492dcf2b076973078cde33bf7c4907d04954c90 Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Sun, 10 Jan 2016 17:15:40 -0500
Subject: [PATCH 051/109] Infer the types of lambdas.

---
 src/Curve.hs | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/Curve.hs b/src/Curve.hs
index 4e2ff1b..af545b8 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -126,6 +126,8 @@ check expected context term = case (out term, out expected) of
 
   (Variable name, Implicit) -> maybe (Error $ "unexpectedly free variable " ++ show name) into (Map.lookup name context)
 
+  (Lambda i t body, Implicit) -> unify t type' `lambda` \ v -> substitute i v (into body)
+
   (_, Implicit) -> Error $ "No rule to infer type of " ++ show term
   (_, _) -> let unification = infer context term in
     maybe unification (unify expected) $ unified unification

From 100f99e8427a1935ccfcaf0829b873f5372ed9a4 Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Sun, 10 Jan 2016 17:22:57 -0500
Subject: [PATCH 052/109] Use the constructors for unifying variables and
 applications.

---
 src/Curve.hs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Curve.hs b/src/Curve.hs
index af545b8..6f45a22 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -142,8 +142,8 @@ unify expected actual = case (out expected, out actual) of
 
   (Type, Type) -> into expected
 
-  (Variable n1, Variable n2) | n1 == n2 -> Unification $ Variable n2
-  (Application a1 b1, Application a2 b2) -> Unification $ Application (unify a1 a2) (unify b1 b2)
+  (Variable n1, Variable n2) | n1 == n2 -> variable n2
+  (Application a1 b1, Application a2 b2) -> unify a1 a2 `apply` unify b1 b2
   (Lambda i1 a1 b1, Lambda i2 a2 b2) | i1 == i2 -> Unification $ Lambda i2 (unify a1 a2) (unify b1 b2)
 
   _ -> Conflict expected actual

From cffca38919a29f76b19913d8003d5733720a8cb3 Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Sun, 10 Jan 2016 18:04:56 -0500
Subject: [PATCH 053/109] Generalize renaming to Roll/PartialUnroll.

---
 src/Curve.hs | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/src/Curve.hs b/src/Curve.hs
index 6f45a22..2e271bb 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -78,15 +78,15 @@ unified _ = Nothing
 
 -- Binding
 
-rename :: Int -> Int -> Term' -> Term'
+rename :: (Roll r, PartialUnroll r) => Int -> Int -> r Expression -> r Expression
 rename old new term | old == new = term
-rename old new term = Term $ case out term of
-  Variable (Local name) | name == old -> Variable $ Local new
-  Lambda name t b -> if name == old
+rename old new term = case unrollMaybe term of
+  Just (Variable (Local name)) | name == old -> local new
+  Just (Lambda name t b) -> roll $ if name == old
     then Lambda name (rename old new t) b
     else Lambda name (rename old new t) (rename old new b)
-  Application a b -> Application (rename old new a) (rename old new b)
-  other -> other
+  Just (Application a b) -> rename old new a `apply` rename old new b
+  _ -> term
 
 substitute :: (Roll r, PartialUnroll r) => Int -> r Expression -> r Expression -> r Expression
 substitute name withTerm inScope = case unrollMaybe inScope of

From 199dfbbcae9b2a18e4c53207b767ca42a1718e2b Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Sun, 10 Jan 2016 19:47:19 -0500
Subject: [PATCH 054/109] Stub in unification of arbitrary lambdas.

---
 src/Curve.hs | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/Curve.hs b/src/Curve.hs
index 2e271bb..fffeb40 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -145,6 +145,8 @@ unify expected actual = case (out expected, out actual) of
   (Variable n1, Variable n2) | n1 == n2 -> variable n2
   (Application a1 b1, Application a2 b2) -> unify a1 a2 `apply` unify b1 b2
   (Lambda i1 a1 b1, Lambda i2 a2 b2) | i1 == i2 -> Unification $ Lambda i2 (unify a1 a2) (unify b1 b2)
+  (Lambda i1 a1 b1, Lambda i2 a2 b2) -> Unification $ Lambda i1 (unify a1 a2) (rename fresh i1 (unify (rename i1 fresh b1) (rename i2 fresh b2)))
+    where fresh = 0
 
   _ -> Conflict expected actual
 

From 86878e701e8a514f0b9b82f6a6a6d2d9034c0e6d Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Sun, 10 Jan 2016 19:48:02 -0500
Subject: [PATCH 055/109] Arbitrary lambda unification subsumes no-renaming
 unification.

---
 src/Curve.hs | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/Curve.hs b/src/Curve.hs
index fffeb40..91405fe 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -144,7 +144,6 @@ unify expected actual = case (out expected, out actual) of
 
   (Variable n1, Variable n2) | n1 == n2 -> variable n2
   (Application a1 b1, Application a2 b2) -> unify a1 a2 `apply` unify b1 b2
-  (Lambda i1 a1 b1, Lambda i2 a2 b2) | i1 == i2 -> Unification $ Lambda i2 (unify a1 a2) (unify b1 b2)
   (Lambda i1 a1 b1, Lambda i2 a2 b2) -> Unification $ Lambda i1 (unify a1 a2) (rename fresh i1 (unify (rename i1 fresh b1) (rename i2 fresh b2)))
     where fresh = 0
 

From 17613a45c7315b461b8de086e63a61a729f54681 Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Sun, 10 Jan 2016 19:49:24 -0500
Subject: [PATCH 056/109] Define freeVariables with a lambda expression.

---
 src/Curve.hs | 11 +++++------
 1 file changed, 5 insertions(+), 6 deletions(-)

diff --git a/src/Curve.hs b/src/Curve.hs
index 91405fe..853dd1c 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -99,12 +99,11 @@ substitute name withTerm inScope = case unrollMaybe inScope of
 
 
 freeVariables :: Term' -> Set.Set Name
-freeVariables = cata inExpression
-  where inExpression expression = case expression of
-          Variable name -> Set.singleton name
-          Lambda i t b -> Set.delete (Local i) b `Set.union` t
-          Application a b -> a `Set.union` b
-          _ -> mempty
+freeVariables = cata $ \ expression -> case expression of
+  Variable name -> Set.singleton name
+  Lambda i t b -> Set.delete (Local i) b `Set.union` t
+  Application a b -> a `Set.union` b
+  _ -> mempty
 
 maxBoundVariable :: PartialUnroll r => r Expression -> Maybe Int
 maxBoundVariable = foldl maximal Nothing . unrollMaybe

From 83ef087306f65154528e894aa66b7bb976b595d9 Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Sun, 10 Jan 2016 19:51:36 -0500
Subject: [PATCH 057/109] Add a function to increment a name.

---
 src/Curve.hs | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/Curve.hs b/src/Curve.hs
index 853dd1c..fc535e6 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -111,6 +111,10 @@ maxBoundVariable = foldl maximal Nothing . unrollMaybe
         maximal into (Application a b) = max into $ max (maxBoundVariable a) (maxBoundVariable b)
         maximal into _ = into
 
+prime :: Name -> Name
+prime (Local i) = Local $ succ i
+prime (Global s) = Global $ s ++ "ʹ"
+
 
 -- Typechecking
 

From dfcd1a1ed0cd689b5ce064060997923988883378 Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Sun, 10 Jan 2016 19:51:46 -0500
Subject: [PATCH 058/109] Add a function to compute a fresh name given some
 predicate.

---
 src/Curve.hs | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/Curve.hs b/src/Curve.hs
index fc535e6..5d98242 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -111,6 +111,9 @@ maxBoundVariable = foldl maximal Nothing . unrollMaybe
         maximal into (Application a b) = max into $ max (maxBoundVariable a) (maxBoundVariable b)
         maximal into _ = into
 
+freshBy :: (Name -> Bool) -> Name -> Name
+freshBy isUsed name = if isUsed name then freshBy isUsed (prime name) else name
+
 prime :: Name -> Name
 prime (Local i) = Local $ succ i
 prime (Global s) = Global $ s ++ "ʹ"

From 334354301c38b9939502dfa3a419c2da250b0bdf Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Sun, 10 Jan 2016 19:53:50 -0500
Subject: [PATCH 059/109] Add a function to compute a fresh name given a set of
 names.

---
 src/Curve.hs | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/Curve.hs b/src/Curve.hs
index 5d98242..182958a 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -114,6 +114,9 @@ maxBoundVariable = foldl maximal Nothing . unrollMaybe
 freshBy :: (Name -> Bool) -> Name -> Name
 freshBy isUsed name = if isUsed name then freshBy isUsed (prime name) else name
 
+freshIn :: Set.Set Name -> Name -> Name
+freshIn names = freshBy (`Set.member` names)
+
 prime :: Name -> Name
 prime (Local i) = Local $ succ i
 prime (Global s) = Global $ s ++ "ʹ"

From 8d33b002716563bc77ce07d90a76216cb545f0a8 Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Sun, 10 Jan 2016 19:56:43 -0500
Subject: [PATCH 060/109] Pick a sensible fresh name given a set of names.

---
 src/Curve.hs | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/Curve.hs b/src/Curve.hs
index 182958a..805cf94 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -121,6 +121,9 @@ prime :: Name -> Name
 prime (Local i) = Local $ succ i
 prime (Global s) = Global $ s ++ "ʹ"
 
+pick :: Set.Set Name -> Name
+pick names = freshIn names (maximum $ Set.insert (Local 0) names)
+
 
 -- Typechecking
 

From 081897527b6aba8064284d42d24b6d95a2b54804 Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Sun, 10 Jan 2016 20:01:46 -0500
Subject: [PATCH 061/109] Generalize renaming to Names.

---
 src/Curve.hs | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/Curve.hs b/src/Curve.hs
index 805cf94..8091f9b 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -78,11 +78,11 @@ unified _ = Nothing
 
 -- Binding
 
-rename :: (Roll r, PartialUnroll r) => Int -> Int -> r Expression -> r Expression
+rename :: (Roll r, PartialUnroll r) => Name -> Name -> r Expression -> r Expression
 rename old new term | old == new = term
 rename old new term = case unrollMaybe term of
-  Just (Variable (Local name)) | name == old -> local new
-  Just (Lambda name t b) -> roll $ if name == old
+  Just (Variable name) | name == old -> variable new
+  Just (Lambda name t b) -> roll $ if Local name == old
     then Lambda name (rename old new t) b
     else Lambda name (rename old new t) (rename old new b)
   Just (Application a b) -> rename old new a `apply` rename old new b

From 4b6a1f5a5613cd350a7f39d6c5d9c5bd1a56b348 Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Sun, 10 Jan 2016 20:01:54 -0500
Subject: [PATCH 062/109] Select a fresh name.

---
 src/Curve.hs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Curve.hs b/src/Curve.hs
index 8091f9b..61107a4 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -156,8 +156,8 @@ unify expected actual = case (out expected, out actual) of
 
   (Variable n1, Variable n2) | n1 == n2 -> variable n2
   (Application a1 b1, Application a2 b2) -> unify a1 a2 `apply` unify b1 b2
-  (Lambda i1 a1 b1, Lambda i2 a2 b2) -> Unification $ Lambda i1 (unify a1 a2) (rename fresh i1 (unify (rename i1 fresh b1) (rename i2 fresh b2)))
-    where fresh = 0
+  (Lambda i1 a1 b1, Lambda i2 a2 b2) -> Unification $ Lambda i1 (unify a1 a2) (rename fresh (Local i1) (unify (rename (Local i1) fresh b1) (rename (Local i2) fresh b2)))
+    where fresh = pick (Set.union (freeVariables b1) (freeVariables b2))
 
   _ -> Conflict expected actual
 

From 3e59da42bc9894dd7aea4ed71d81eed3ac2fab3b Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Sun, 10 Jan 2016 23:42:23 -0500
Subject: [PATCH 063/109] Test that shadowed variables are not renamed.

---
 test/Spec.hs | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/test/Spec.hs b/test/Spec.hs
index c068f2d..9dc8c84 100644
--- a/test/Spec.hs
+++ b/test/Spec.hs
@@ -69,6 +69,10 @@ main = hspec $ do
     it "should format the identity function appropriately" $
       show (Term $ Lambda 1 type' $ Term $ Lambda 0 (local 1) (local 0)) `shouldBe` "λ b : Type . λ a : b . a"
 
+  describe "rename" $ do
+    prop "shadowed variables are not renamed" $
+      \ i t -> rename (Local i) (Local $ i + 1) (Term $ Lambda i t (local i)) `shouldBe` (Term $ Lambda i (rename (Local i) (Local $ i + 1) t) (local i))
+
   describe "DSL" $ do
     prop "apply associates leftwards" $
       \ a b c -> a `apply` b `apply` c `shouldBe` (a `apply` b) `apply` (c :: Term')

From f92cb88b2907ed7b561ef956194375f95b749d66 Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Sun, 10 Jan 2016 23:47:13 -0500
Subject: [PATCH 064/109] Test that prime is injective.

---
 test/Spec.hs | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/test/Spec.hs b/test/Spec.hs
index 9dc8c84..c288b59 100644
--- a/test/Spec.hs
+++ b/test/Spec.hs
@@ -73,6 +73,13 @@ main = hspec $ do
     prop "shadowed variables are not renamed" $
       \ i t -> rename (Local i) (Local $ i + 1) (Term $ Lambda i t (local i)) `shouldBe` (Term $ Lambda i (rename (Local i) (Local $ i + 1) t) (local i))
 
+  describe "prime" $ do
+    prop "injectivity over locals" $
+      \ i -> prime (Local i) `shouldNotBe` Local i
+
+    prop "injectivity over globals" $
+      \ s -> prime (Global s) `shouldNotBe` Global s
+
   describe "DSL" $ do
     prop "apply associates leftwards" $
       \ a b c -> a `apply` b `apply` c `shouldBe` (a `apply` b) `apply` (c :: Term')

From 997dac9c1a93602c11ee4b10df7f5e6d4003563c Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Sun, 10 Jan 2016 23:47:27 -0500
Subject: [PATCH 065/109] Test that renaming is injective.

---
 test/Spec.hs | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/test/Spec.hs b/test/Spec.hs
index c288b59..efa0810 100644
--- a/test/Spec.hs
+++ b/test/Spec.hs
@@ -73,6 +73,9 @@ main = hspec $ do
     prop "shadowed variables are not renamed" $
       \ i t -> rename (Local i) (Local $ i + 1) (Term $ Lambda i t (local i)) `shouldBe` (Term $ Lambda i (rename (Local i) (Local $ i + 1) t) (local i))
 
+    prop "renaming is injective" $
+      \ n term -> rename (prime n) n (rename n (prime n) term) `shouldBe` (term :: Term')
+
   describe "prime" $ do
     prop "injectivity over locals" $
       \ i -> prime (Local i) `shouldNotBe` Local i

From c3de2e5c93c5ae2e16d5a5f3bbb26a3f1a54c70d Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Sun, 10 Jan 2016 23:49:37 -0500
Subject: [PATCH 066/109] Generalize the test of renaming with shadowed
 variables to arbitrary bodies.

---
 test/Spec.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/test/Spec.hs b/test/Spec.hs
index efa0810..c744d14 100644
--- a/test/Spec.hs
+++ b/test/Spec.hs
@@ -71,7 +71,7 @@ main = hspec $ do
 
   describe "rename" $ do
     prop "shadowed variables are not renamed" $
-      \ i t -> rename (Local i) (Local $ i + 1) (Term $ Lambda i t (local i)) `shouldBe` (Term $ Lambda i (rename (Local i) (Local $ i + 1) t) (local i))
+      \ i t body -> rename (Local i) (Local $ i + 1) (Term $ Lambda i t body) `shouldBe` (Term $ Lambda i (rename (Local i) (Local $ i + 1) t) body)
 
     prop "renaming is injective" $
       \ n term -> rename (prime n) n (rename n (prime n) term) `shouldBe` (term :: Term')

From bbde0cc064c0272e52dea25fb31a3175ea0e99d2 Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Sun, 10 Jan 2016 23:51:13 -0500
Subject: [PATCH 067/109] Factor out the priming.

---
 test/Spec.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/test/Spec.hs b/test/Spec.hs
index c744d14..3a9e2f4 100644
--- a/test/Spec.hs
+++ b/test/Spec.hs
@@ -71,7 +71,7 @@ main = hspec $ do
 
   describe "rename" $ do
     prop "shadowed variables are not renamed" $
-      \ i t body -> rename (Local i) (Local $ i + 1) (Term $ Lambda i t body) `shouldBe` (Term $ Lambda i (rename (Local i) (Local $ i + 1) t) body)
+      \ i t body -> let name = Local i in rename name (prime name) (Term $ Lambda i t body) `shouldBe` (Term $ Lambda i (rename name (prime name) t) body)
 
     prop "renaming is injective" $
       \ n term -> rename (prime n) n (rename n (prime n) term) `shouldBe` (term :: Term')

From cd4d342f2765ea94d405af4ec692fccef6243c25 Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Sun, 10 Jan 2016 23:59:41 -0500
Subject: [PATCH 068/109] Reconstruct the expected term from Unifications.

---
 src/Curve.hs | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/src/Curve.hs b/src/Curve.hs
index 61107a4..27e7995 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -75,6 +75,11 @@ unified :: Unification' -> Maybe Term'
 unified (Unification expression) = Term <$> traverse unified expression
 unified _ = Nothing
 
+expected :: Unification' -> Term'
+expected (Unification out) = Term $ expected <$> out
+expected (Conflict a _) = a
+expected _ = implicit
+
 
 -- Binding
 

From 36a72ca8b196644524ef5f0da47ecaf3264bf6fa Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Sun, 10 Jan 2016 23:59:48 -0500
Subject: [PATCH 069/109] Reconstruct the actual term from Unifications.

---
 src/Curve.hs | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/src/Curve.hs b/src/Curve.hs
index 27e7995..b3926dd 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -80,6 +80,11 @@ expected (Unification out) = Term $ expected <$> out
 expected (Conflict a _) = a
 expected _ = implicit
 
+actual :: Unification' -> Term'
+actual (Unification out) = Term $ actual <$> out
+actual (Conflict _ b) = b
+actual _ = implicit
+
 
 -- Binding
 

From 57839086bf1cd1e5f8c51b0f81eb661f14c66a4d Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Mon, 11 Jan 2016 00:05:56 -0500
Subject: [PATCH 070/109] Stub in a test helper for replacing terms deeply.

---
 test/Spec.hs | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/test/Spec.hs b/test/Spec.hs
index 3a9e2f4..9dbbfc5 100644
--- a/test/Spec.hs
+++ b/test/Spec.hs
@@ -96,3 +96,5 @@ main = hspec $ do
   where flipUnification (Conflict a b) = Conflict b a
         flipUnification (Unification out) = Unification $ flipUnification <$> out
         flipUnification otherwise = otherwise
+
+        replace needle withTerm inHaystack = if needle == inHaystack then withTerm else Term $ replace needle withTerm <$> out inHaystack

From e17b61963c43b01cb31fe5a00b8fed1401cdd4eb Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Mon, 11 Jan 2016 00:07:25 -0500
Subject: [PATCH 071/109] Test that the expected term is recoverable.

---
 test/Spec.hs | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/test/Spec.hs b/test/Spec.hs
index 9dbbfc5..1b8ce03 100644
--- a/test/Spec.hs
+++ b/test/Spec.hs
@@ -37,6 +37,9 @@ main = hspec $ do
     prop "symmetry" $
       \ a b -> a `unify` b `shouldBe` flipUnification (b `unify` a)
 
+    prop "expected term is recoverable" $ forAll (replace implicit type' <$> arbitrary) $
+      \ a b -> expected (a `unify` b) `shouldBe` a
+
   describe "freeVariables" $ do
     prop "variables are free in themselves" $
       \ name -> freeVariables (variable name) `shouldBe` Set.singleton name

From 4def13c4d6f1fbfca8fd08dfb9ee2520ad74ae9e Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Mon, 11 Jan 2016 00:07:34 -0500
Subject: [PATCH 072/109] Test that the actual term is recoverable.

---
 test/Spec.hs | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/test/Spec.hs b/test/Spec.hs
index 1b8ce03..f0ee4be 100644
--- a/test/Spec.hs
+++ b/test/Spec.hs
@@ -40,6 +40,9 @@ main = hspec $ do
     prop "expected term is recoverable" $ forAll (replace implicit type' <$> arbitrary) $
       \ a b -> expected (a `unify` b) `shouldBe` a
 
+    prop "actual term is recoverable" $ forAll (replace implicit type' <$> arbitrary) $
+      \ a b -> actual (a `unify` b) `shouldBe` b
+
   describe "freeVariables" $ do
     prop "variables are free in themselves" $
       \ name -> freeVariables (variable name) `shouldBe` Set.singleton name

From 7ad1a9331a8fa20fd7ff0d9ab3e7f53dd8c92f76 Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Mon, 11 Jan 2016 00:11:20 -0500
Subject: [PATCH 073/109] Section header for naming.

---
 src/Curve.hs | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/Curve.hs b/src/Curve.hs
index b3926dd..c47f0f7 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -121,6 +121,9 @@ maxBoundVariable = foldl maximal Nothing . unrollMaybe
         maximal into (Application a b) = max into $ max (maxBoundVariable a) (maxBoundVariable b)
         maximal into _ = into
 
+
+-- Naming
+
 freshBy :: (Name -> Bool) -> Name -> Name
 freshBy isUsed name = if isUsed name then freshBy isUsed (prime name) else name
 

From 5fef46eb8539e0a3f22b85f9c12e52fe304d87fe Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Mon, 11 Jan 2016 00:11:25 -0500
Subject: [PATCH 074/109] Alpha equivalence.

---
 src/Curve.hs | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/src/Curve.hs b/src/Curve.hs
index c47f0f7..7dc56fb 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -122,6 +122,14 @@ maxBoundVariable = foldl maximal Nothing . unrollMaybe
         maximal into _ = into
 
 
+alphaEquivalent :: Term' -> Term' -> Bool
+alphaEquivalent a b | a == b = True
+alphaEquivalent (Term (Application a1 b1)) (Term (Application a2 b2)) = alphaEquivalent a1 a2 && alphaEquivalent b1 b2
+alphaEquivalent (Term (Lambda i1 t1 b1)) (Term (Lambda i2 t2 b2)) = alphaEquivalent t1 t2 && alphaEquivalent (rename (Local i1) fresh b1) (rename (Local i2) fresh b2)
+  where fresh = pick (Set.union (freeVariables b1) (freeVariables b2))
+alphaEquivalent _ _ = False
+
+
 -- Naming
 
 freshBy :: (Name -> Bool) -> Name -> Name

From d28d51f08d0f1a2c5931f007badbf49db06b760e Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Mon, 11 Jan 2016 00:12:29 -0500
Subject: [PATCH 075/109] Test recovery of expected/actual terms up to
 renaming.

---
 test/Spec.hs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/test/Spec.hs b/test/Spec.hs
index f0ee4be..6ee3949 100644
--- a/test/Spec.hs
+++ b/test/Spec.hs
@@ -38,10 +38,10 @@ main = hspec $ do
       \ a b -> a `unify` b `shouldBe` flipUnification (b `unify` a)
 
     prop "expected term is recoverable" $ forAll (replace implicit type' <$> arbitrary) $
-      \ a b -> expected (a `unify` b) `shouldBe` a
+      \ a b -> expected (a `unify` b) `shouldSatisfy` alphaEquivalent a
 
     prop "actual term is recoverable" $ forAll (replace implicit type' <$> arbitrary) $
-      \ a b -> actual (a `unify` b) `shouldBe` b
+      \ a b -> actual (a `unify` b) `shouldSatisfy` alphaEquivalent b
 
   describe "freeVariables" $ do
     prop "variables are free in themselves" $

From 21d491965361b2a957d3e4f33236164bf6d72e8f Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Mon, 11 Jan 2016 00:25:35 -0500
Subject: [PATCH 076/109] Test actual/expected terms by replacing.

---
 test/Spec.hs | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/test/Spec.hs b/test/Spec.hs
index 6ee3949..e8d3c20 100644
--- a/test/Spec.hs
+++ b/test/Spec.hs
@@ -37,11 +37,11 @@ main = hspec $ do
     prop "symmetry" $
       \ a b -> a `unify` b `shouldBe` flipUnification (b `unify` a)
 
-    prop "expected term is recoverable" $ forAll (replace implicit type' <$> arbitrary) $
-      \ a b -> expected (a `unify` b) `shouldSatisfy` alphaEquivalent a
+    prop "expected term is recoverable" $
+      \ a b -> expected (replace implicit type' a `unify` b) `shouldSatisfy` alphaEquivalent (replace implicit type' a)
 
-    prop "actual term is recoverable" $ forAll (replace implicit type' <$> arbitrary) $
-      \ a b -> actual (a `unify` b) `shouldSatisfy` alphaEquivalent b
+    prop "actual term is recoverable" $
+      \ a b -> actual (a `unify` replace implicit type' b) `shouldSatisfy` alphaEquivalent (replace implicit type' b)
 
   describe "freeVariables" $ do
     prop "variables are free in themselves" $

From b45dd2809e89bb62b6b69188cddafde4c833a493 Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Mon, 11 Jan 2016 00:25:56 -0500
Subject: [PATCH 077/109] Test that identical terms are alpha-equivalent.

---
 test/Spec.hs | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/test/Spec.hs b/test/Spec.hs
index e8d3c20..8c35a94 100644
--- a/test/Spec.hs
+++ b/test/Spec.hs
@@ -43,6 +43,10 @@ main = hspec $ do
     prop "actual term is recoverable" $
       \ a b -> actual (a `unify` replace implicit type' b) `shouldSatisfy` alphaEquivalent (replace implicit type' b)
 
+  describe "alphaEquivalent" $ do
+    prop "identical terms are alpha-equivalent" $
+      \ a -> a `alphaEquivalent` a `shouldBe` True
+
   describe "freeVariables" $ do
     prop "variables are free in themselves" $
       \ name -> freeVariables (variable name) `shouldBe` Set.singleton name

From cab0752da17bc9e39f04dd365e50d8ff87549664 Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Mon, 11 Jan 2016 00:29:21 -0500
Subject: [PATCH 078/109] Test that free variables are alpha-equivalent.

---
 test/Spec.hs | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/test/Spec.hs b/test/Spec.hs
index 8c35a94..7a25bcc 100644
--- a/test/Spec.hs
+++ b/test/Spec.hs
@@ -47,6 +47,9 @@ main = hspec $ do
     prop "identical terms are alpha-equivalent" $
       \ a -> a `alphaEquivalent` a `shouldBe` True
 
+    prop "free variables are alpha-equivalent" $
+      \ n -> variable n `alphaEquivalent` variable (prime n) `shouldBe` True
+
   describe "freeVariables" $ do
     prop "variables are free in themselves" $
       \ name -> freeVariables (variable name) `shouldBe` Set.singleton name

From 142c0541747d6ca15659c162265814cfa2702474 Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Mon, 11 Jan 2016 00:30:43 -0500
Subject: [PATCH 079/109] Variables are alpha equivalent.

---
 src/Curve.hs | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/Curve.hs b/src/Curve.hs
index 7dc56fb..7b68305 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -124,6 +124,7 @@ maxBoundVariable = foldl maximal Nothing . unrollMaybe
 
 alphaEquivalent :: Term' -> Term' -> Bool
 alphaEquivalent a b | a == b = True
+alphaEquivalent (Term (Variable _)) (Term (Variable _)) = True
 alphaEquivalent (Term (Application a1 b1)) (Term (Application a2 b2)) = alphaEquivalent a1 a2 && alphaEquivalent b1 b2
 alphaEquivalent (Term (Lambda i1 t1 b1)) (Term (Lambda i2 t2 b2)) = alphaEquivalent t1 t2 && alphaEquivalent (rename (Local i1) fresh b1) (rename (Local i2) fresh b2)
   where fresh = pick (Set.union (freeVariables b1) (freeVariables b2))

From 0e80009747951b37ab66bbf3f9c4392a5e3751be Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Mon, 11 Jan 2016 00:30:53 -0500
Subject: [PATCH 080/109] Generate lambdas more often.

---
 test/Spec.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/test/Spec.hs b/test/Spec.hs
index 7a25bcc..e611ba9 100644
--- a/test/Spec.hs
+++ b/test/Spec.hs
@@ -14,7 +14,7 @@ instance Arbitrary (Term Expression) where
               (4, pure (Term Type))
             : (4, pure (Term Implicit))
             : (1, Term <$> (Application <$> inScope names <*> inScope names))
-            : (1, Term <$> (Lambda (length names) <$> inScope names <*> inScope (Local (length names) : names)))
+            : (2, Term <$> (Lambda (length names) <$> inScope names <*> inScope (Local (length names) : names)))
             : ((,) 4 . pure . Term . Variable <$> names)
 
   shrink term = filter (/= term) $ case out term of

From 804bd99ff96a2e1b7e78eb53b5ca1c67bbc12182 Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Mon, 11 Jan 2016 00:57:03 -0500
Subject: [PATCH 081/109] Fix a test name.

---
 test/Spec.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/test/Spec.hs b/test/Spec.hs
index e611ba9..3aba962 100644
--- a/test/Spec.hs
+++ b/test/Spec.hs
@@ -70,7 +70,7 @@ main = hspec $ do
     prop "shows dependent function types with a binding arrow operator" $
       \ a n -> showsType (Term $ Lambda n a (local n)) "" `shouldBe` "(" ++ shows (Local n) " : " ++ showsType a ") → " ++ showsType (local n) ""
 
-    prop "parentheses left-nested non-dependent function types" $
+    prop "parenthesizes left-nested non-dependent function types" $
       \ a b c -> showsLevelPrec True 0 (Term $ Lambda 0 (Term $ Lambda 1 a b) c) "" `shouldBe` "(" ++ showsLevelPrec True 0 (Term $ Lambda 1 a b) ") → " ++ showsType c ""
 
     prop "pretty-prints Implicit as _ at any level and precedence" $

From 36202739ed44154b029dc35bb4e821651234a289 Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Mon, 11 Jan 2016 01:09:10 -0500
Subject: [PATCH 082/109] Unify free variables.

---
 src/Curve.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Curve.hs b/src/Curve.hs
index 7b68305..3e19f00 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -176,7 +176,7 @@ unify expected actual = case (out expected, out actual) of
 
   (Type, Type) -> into expected
 
-  (Variable n1, Variable n2) | n1 == n2 -> variable n2
+  (Variable _, Variable _) -> into expected
   (Application a1 b1, Application a2 b2) -> unify a1 a2 `apply` unify b1 b2
   (Lambda i1 a1 b1, Lambda i2 a2 b2) -> Unification $ Lambda i1 (unify a1 a2) (rename fresh (Local i1) (unify (rename (Local i1) fresh b1) (rename (Local i2) fresh b2)))
     where fresh = pick (Set.union (freeVariables b1) (freeVariables b2))

From d9d121b46ee19b35140e9cbd9ec8ad41be4adf15 Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Mon, 11 Jan 2016 01:09:24 -0500
Subject: [PATCH 083/109] Unify lambdas up to renaming.

---
 src/Curve.hs | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/Curve.hs b/src/Curve.hs
index 3e19f00..12f6904 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -178,8 +178,7 @@ unify expected actual = case (out expected, out actual) of
 
   (Variable _, Variable _) -> into expected
   (Application a1 b1, Application a2 b2) -> unify a1 a2 `apply` unify b1 b2
-  (Lambda i1 a1 b1, Lambda i2 a2 b2) -> Unification $ Lambda i1 (unify a1 a2) (rename fresh (Local i1) (unify (rename (Local i1) fresh b1) (rename (Local i2) fresh b2)))
-    where fresh = pick (Set.union (freeVariables b1) (freeVariables b2))
+  (Lambda i a1 b1, Lambda _ a2 b2) -> Unification $ Lambda i (unify a1 a2) (unify b1 b2)
 
   _ -> Conflict expected actual
 

From 0c0d58dbcc5ee5512d70beb7e6116c7d1133532c Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Mon, 11 Jan 2016 01:09:51 -0500
Subject: [PATCH 084/109] Alpha-equivalence is defined up to renaming.

---
 src/Curve.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Curve.hs b/src/Curve.hs
index 12f6904..331a7a0 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -126,7 +126,7 @@ alphaEquivalent :: Term' -> Term' -> Bool
 alphaEquivalent a b | a == b = True
 alphaEquivalent (Term (Variable _)) (Term (Variable _)) = True
 alphaEquivalent (Term (Application a1 b1)) (Term (Application a2 b2)) = alphaEquivalent a1 a2 && alphaEquivalent b1 b2
-alphaEquivalent (Term (Lambda i1 t1 b1)) (Term (Lambda i2 t2 b2)) = alphaEquivalent t1 t2 && alphaEquivalent (rename (Local i1) fresh b1) (rename (Local i2) fresh b2)
+alphaEquivalent (Term (Lambda i1 t1 b1)) (Term (Lambda i2 t2 b2)) = alphaEquivalent t1 t2 && alphaEquivalent b1 b2
   where fresh = pick (Set.union (freeVariables b1) (freeVariables b2))
 alphaEquivalent _ _ = False
 

From f66ea9954b28fbf9e4a172a521339eefc02f2f06 Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Mon, 11 Jan 2016 01:10:04 -0500
Subject: [PATCH 085/109] Remove some unused terms.

---
 src/Curve.hs | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/Curve.hs b/src/Curve.hs
index 331a7a0..3919422 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -126,8 +126,7 @@ alphaEquivalent :: Term' -> Term' -> Bool
 alphaEquivalent a b | a == b = True
 alphaEquivalent (Term (Variable _)) (Term (Variable _)) = True
 alphaEquivalent (Term (Application a1 b1)) (Term (Application a2 b2)) = alphaEquivalent a1 a2 && alphaEquivalent b1 b2
-alphaEquivalent (Term (Lambda i1 t1 b1)) (Term (Lambda i2 t2 b2)) = alphaEquivalent t1 t2 && alphaEquivalent b1 b2
-  where fresh = pick (Set.union (freeVariables b1) (freeVariables b2))
+alphaEquivalent (Term (Lambda _ t1 b1)) (Term (Lambda _ t2 b2)) = alphaEquivalent t1 t2 && alphaEquivalent b1 b2
 alphaEquivalent _ _ = False
 
 

From a5e5a2aa6ec5b585dc71e2810b674bfa892346dd Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Tue, 12 Jan 2016 02:07:05 -0500
Subject: [PATCH 086/109] As an experiment, represent errors with conflicts.

---
 src/Curve.hs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Curve.hs b/src/Curve.hs
index 3919422..d859d88 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -157,11 +157,11 @@ check :: Term' -> Context -> Term' -> Unification'
 check expected context term = case (out term, out expected) of
   (Type, Implicit) -> Unification Type
 
-  (Variable name, Implicit) -> maybe (Error $ "unexpectedly free variable " ++ show name) into (Map.lookup name context)
+  (Variable name, Implicit) -> maybe (Conflict implicit implicit) into (Map.lookup name context)
 
   (Lambda i t body, Implicit) -> unify t type' `lambda` \ v -> substitute i v (into body)
 
-  (_, Implicit) -> Error $ "No rule to infer type of " ++ show term
+  (_, Implicit) -> Conflict implicit implicit
   (_, _) -> let unification = infer context term in
     maybe unification (unify expected) $ unified unification
 

From d00104f5960320b20108cfb82b775640f8e2f04a Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Tue, 12 Jan 2016 02:07:38 -0500
Subject: [PATCH 087/109] Remove the Error case from Unification.

---
 src/Curve.hs | 4 +---
 test/Spec.hs | 1 -
 2 files changed, 1 insertion(+), 4 deletions(-)

diff --git a/src/Curve.hs b/src/Curve.hs
index d859d88..6502630 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -22,7 +22,7 @@ data Expression term
 data Term f = Term { out :: f (Term f) }
 type Term' = Term Expression
 
-data Unification f = Unification (f (Unification f)) | Conflict (Term f) (Term f) | Error String
+data Unification f = Unification (f (Unification f)) | Conflict (Term f) (Term f)
 type Unification' = Unification Expression
 
 
@@ -251,14 +251,12 @@ instance Eq1 f => Eq (Term f) where
 instance Eq1 f => Eq (Unification f) where
   Unification a == Unification b = a `eq1` b
   Conflict a1 b1 == Conflict a2 b2 = a1 == a2 && b1 == b2
-  Error s1 == Error s2 = s1 == s2
   _ == _ = False
 
 instance Show Unification' where
   show (Unification out) = show out
   show (Conflict a b) = "Expected: " ++ show a ++ "\n"
                      ++ "  Actual: " ++ show b ++ "\n"
-  show (Error s) = "Error: " ++ s
 
 instance Roll Term where
   roll = Term
diff --git a/test/Spec.hs b/test/Spec.hs
index 3aba962..0f7be9f 100644
--- a/test/Spec.hs
+++ b/test/Spec.hs
@@ -108,6 +108,5 @@ main = hspec $ do
 
   where flipUnification (Conflict a b) = Conflict b a
         flipUnification (Unification out) = Unification $ flipUnification <$> out
-        flipUnification otherwise = otherwise
 
         replace needle withTerm inHaystack = if needle == inHaystack then withTerm else Term $ replace needle withTerm <$> out inHaystack

From bb2052a1940c888d243f4072669e0799fb61b446 Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Tue, 12 Jan 2016 02:10:38 -0500
Subject: [PATCH 088/109] Typecheck applications in suspension.

---
 src/Curve.hs | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/Curve.hs b/src/Curve.hs
index 6502630..00eabb9 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -159,6 +159,9 @@ check expected context term = case (out term, out expected) of
 
   (Variable name, Implicit) -> maybe (Conflict implicit implicit) into (Map.lookup name context)
 
+  (Application a b, Implicit) -> case infer context a of
+    other -> other `apply` infer context b
+
   (Lambda i t body, Implicit) -> unify t type' `lambda` \ v -> substitute i v (into body)
 
   (_, Implicit) -> Conflict implicit implicit

From e384d66776a259d94484b0988fb42d54db776c6d Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Tue, 12 Jan 2016 02:12:32 -0500
Subject: [PATCH 089/109] Typecheck applications of functions in suspension.

---
 src/Curve.hs | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/src/Curve.hs b/src/Curve.hs
index 00eabb9..b5dc5c7 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -159,8 +159,10 @@ check expected context term = case (out term, out expected) of
 
   (Variable name, Implicit) -> maybe (Conflict implicit implicit) into (Map.lookup name context)
 
-  (Application a b, Implicit) -> case infer context a of
-    other -> other `apply` infer context b
+  (Application a b, Implicit) -> let a' = infer context a in case a' of
+    Unification (Lambda _ from to) -> case unified from of
+      _ -> a' `apply` infer context b
+    _ -> a' `apply` infer context b
 
   (Lambda i t body, Implicit) -> unify t type' `lambda` \ v -> substitute i v (into body)
 

From 0df897a6b6d41093ce04cb5d68da3e44eae79555 Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Tue, 12 Jan 2016 02:14:09 -0500
Subject: [PATCH 090/109] Stub in an applySubstitution function.

---
 src/Curve.hs | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/Curve.hs b/src/Curve.hs
index b5dc5c7..ab19fac 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -107,6 +107,9 @@ substitute name withTerm inScope = case unrollMaybe inScope of
   Just (Application inA inB) -> roll $ Application (substitute name withTerm inA) (substitute name withTerm inB)
   _ -> inScope
 
+applySubstitution :: Roll r => r Expression -> r Expression -> r Expression
+applySubstitution _ inScope = inScope
+
 
 freeVariables :: Term' -> Set.Set Name
 freeVariables = cata $ \ expression -> case expression of

From d12d486cc574215168d33447e5430fbca68f4618 Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Tue, 12 Jan 2016 02:15:24 -0500
Subject: [PATCH 091/109] Substitute inside lambdas.

---
 src/Curve.hs | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/src/Curve.hs b/src/Curve.hs
index ab19fac..bb7a2a3 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -107,8 +107,10 @@ substitute name withTerm inScope = case unrollMaybe inScope of
   Just (Application inA inB) -> roll $ Application (substitute name withTerm inA) (substitute name withTerm inB)
   _ -> inScope
 
-applySubstitution :: Roll r => r Expression -> r Expression -> r Expression
-applySubstitution _ inScope = inScope
+applySubstitution :: (Roll r, PartialUnroll r) => r Expression -> r Expression -> r Expression
+applySubstitution withTerm body = case unrollMaybe body of
+  Just (Lambda i _ inScope) -> substitute i withTerm inScope
+  _ -> body
 
 
 freeVariables :: Term' -> Set.Set Name

From 740901b4ce8fe70b2cf535f4962e2f5820bf8bbd Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Tue, 12 Jan 2016 02:15:37 -0500
Subject: [PATCH 092/109] Remove overlapped patterns.

---
 src/Curve.hs | 2 --
 1 file changed, 2 deletions(-)

diff --git a/src/Curve.hs b/src/Curve.hs
index bb7a2a3..1d30adc 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -78,12 +78,10 @@ unified _ = Nothing
 expected :: Unification' -> Term'
 expected (Unification out) = Term $ expected <$> out
 expected (Conflict a _) = a
-expected _ = implicit
 
 actual :: Unification' -> Term'
 actual (Unification out) = Term $ actual <$> out
 actual (Conflict _ b) = b
-actual _ = implicit
 
 
 -- Binding

From 9229ceb3d535a1f55d0db952fc40086490354f19 Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Tue, 12 Jan 2016 02:16:16 -0500
Subject: [PATCH 093/109] Substitute in application types.

---
 src/Curve.hs | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/Curve.hs b/src/Curve.hs
index 1d30adc..7ae07d3 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -164,6 +164,7 @@ check expected context term = case (out term, out expected) of
 
   (Application a b, Implicit) -> let a' = infer context a in case a' of
     Unification (Lambda _ from to) -> case unified from of
+      Just from -> applySubstitution (check from context b) to
       _ -> a' `apply` infer context b
     _ -> a' `apply` infer context b
 

From e3e85a462c35fcfea1fde72d2d999d09db92b322 Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Tue, 12 Jan 2016 02:19:16 -0500
Subject: [PATCH 094/109] Test the equivalence of checking against implicit &
 inference.

---
 test/Spec.hs | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/test/Spec.hs b/test/Spec.hs
index 0f7be9f..6ffdf9c 100644
--- a/test/Spec.hs
+++ b/test/Spec.hs
@@ -57,6 +57,10 @@ main = hspec $ do
     prop "lambdas are shadowing" $
       \ name t b -> freeVariables (Term (Lambda name t b)) `shouldSatisfy` Set.notMember (Local name)
 
+  describe "check" $ do
+    prop "checking against implicit is inference" $
+      \ term -> check implicit mempty term `shouldBe` infer mempty term
+
   describe "showsLevelPrec" $ do
     prop "parenthesizes right-nested applications" $
       \ a b c -> show (apply a (apply b c)) `shouldBe` showsPrec 10 a " (" ++ showsPrec 10 (apply b c :: Term') ")"

From ed623e62a599df075d7bfe943f24212211be92b8 Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Tue, 12 Jan 2016 02:20:34 -0500
Subject: [PATCH 095/109] Check lambda types against Type, rather than unifying
 against it.

---
 src/Curve.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Curve.hs b/src/Curve.hs
index 7ae07d3..bd67d51 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -168,7 +168,7 @@ check expected context term = case (out term, out expected) of
       _ -> a' `apply` infer context b
     _ -> a' `apply` infer context b
 
-  (Lambda i t body, Implicit) -> unify t type' `lambda` \ v -> substitute i v (into body)
+  (Lambda i t body, Implicit) -> check type' context t `lambda` \ v -> substitute i v (into body)
 
   (_, Implicit) -> Conflict implicit implicit
   (_, _) -> let unification = infer context term in

From 2ede00c87503667610b29fe4e2a40cc63d8944d6 Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Tue, 12 Jan 2016 02:22:52 -0500
Subject: [PATCH 096/109] Test that free variables do not typecheck.

---
 test/Spec.hs | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/test/Spec.hs b/test/Spec.hs
index 6ffdf9c..12e281d 100644
--- a/test/Spec.hs
+++ b/test/Spec.hs
@@ -61,6 +61,9 @@ main = hspec $ do
     prop "checking against implicit is inference" $
       \ term -> check implicit mempty term `shouldBe` infer mempty term
 
+    prop "infers free variables as conflicts" $
+      \ name -> infer mempty (variable name) `shouldBe` Conflict implicit implicit
+
   describe "showsLevelPrec" $ do
     prop "parenthesizes right-nested applications" $
       \ a b c -> show (apply a (apply b c)) `shouldBe` showsPrec 10 a " (" ++ showsPrec 10 (apply b c :: Term') ")"

From 912e8a720436d826e54b9f1c54e0bdf92633a138 Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Tue, 12 Jan 2016 02:24:35 -0500
Subject: [PATCH 097/109] Test the inference of bound variables.

---
 test/Spec.hs | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/test/Spec.hs b/test/Spec.hs
index 12e281d..29e220c 100644
--- a/test/Spec.hs
+++ b/test/Spec.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE FlexibleInstances #-}
+import qualified Data.Map as Map
 import qualified Data.Set as Set
 import Test.Hspec
 import Test.Hspec.QuickCheck
@@ -64,6 +65,9 @@ main = hspec $ do
     prop "infers free variables as conflicts" $
       \ name -> infer mempty (variable name) `shouldBe` Conflict implicit implicit
 
+    prop "infers bound variables from the context" $
+      \ name t -> infer (Map.singleton name t) (variable name) `shouldBe` into t
+
   describe "showsLevelPrec" $ do
     prop "parenthesizes right-nested applications" $
       \ a b c -> show (apply a (apply b c)) `shouldBe` showsPrec 10 a " (" ++ showsPrec 10 (apply b c :: Term') ")"

From 19b097a3ff50fee09755efb47522ca3e69aaebdb Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Tue, 12 Jan 2016 02:26:46 -0500
Subject: [PATCH 098/109] Test that inferred types are checked.

---
 test/Spec.hs | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/test/Spec.hs b/test/Spec.hs
index 29e220c..fcabe1b 100644
--- a/test/Spec.hs
+++ b/test/Spec.hs
@@ -68,6 +68,9 @@ main = hspec $ do
     prop "infers bound variables from the context" $
       \ name t -> infer (Map.singleton name t) (variable name) `shouldBe` into t
 
+    prop "checks inferred types" $
+      \ name t -> check t (Map.singleton name t) (variable name) `shouldBe` into t
+
   describe "showsLevelPrec" $ do
     prop "parenthesizes right-nested applications" $
       \ a b c -> show (apply a (apply b c)) `shouldBe` showsPrec 10 a " (" ++ showsPrec 10 (apply b c :: Term') ")"

From 0d0358c8b7e609afcb5edfa56c81224a59b2b9fb Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Tue, 12 Jan 2016 02:28:25 -0500
Subject: [PATCH 099/109] Test the inference of simple function types.

---
 test/Spec.hs | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/test/Spec.hs b/test/Spec.hs
index fcabe1b..7cfb38e 100644
--- a/test/Spec.hs
+++ b/test/Spec.hs
@@ -71,6 +71,9 @@ main = hspec $ do
     prop "checks inferred types" $
       \ name t -> check t (Map.singleton name t) (variable name) `shouldBe` into t
 
+    prop "infers function types" $
+      \ i -> infer mempty (Term $ Lambda i type' type') `shouldBe` type' --> type'
+
   describe "showsLevelPrec" $ do
     prop "parenthesizes right-nested applications" $
       \ a b c -> show (apply a (apply b c)) `shouldBe` showsPrec 10 a " (" ++ showsPrec 10 (apply b c :: Term') ")"

From 57ad2a5de24e24e6e978a2ff880d566283ea592b Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Tue, 12 Jan 2016 02:31:31 -0500
Subject: [PATCH 100/109] Simplify the test of simple function type inference.

---
 test/Spec.hs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/test/Spec.hs b/test/Spec.hs
index 7cfb38e..b0932ec 100644
--- a/test/Spec.hs
+++ b/test/Spec.hs
@@ -71,8 +71,8 @@ main = hspec $ do
     prop "checks inferred types" $
       \ name t -> check t (Map.singleton name t) (variable name) `shouldBe` into t
 
-    prop "infers function types" $
-      \ i -> infer mempty (Term $ Lambda i type' type') `shouldBe` type' --> type'
+    it "infers function types" $
+      infer mempty (type' `lambda` const type') `shouldBe` type' --> type'
 
   describe "showsLevelPrec" $ do
     prop "parenthesizes right-nested applications" $

From 7c7063506cb51d764c7fd308e9134d6edccc7f9f Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Tue, 12 Jan 2016 02:34:29 -0500
Subject: [PATCH 101/109] Typecheck the bodies of lambdas.

---
 src/Curve.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Curve.hs b/src/Curve.hs
index bd67d51..a619e78 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -168,7 +168,7 @@ check expected context term = case (out term, out expected) of
       _ -> a' `apply` infer context b
     _ -> a' `apply` infer context b
 
-  (Lambda i t body, Implicit) -> check type' context t `lambda` \ v -> substitute i v (into body)
+  (Lambda i t body, Implicit) -> check type' context t `lambda` \ v -> substitute i v (infer (Map.insert (Local i) t context) body)
 
   (_, Implicit) -> Conflict implicit implicit
   (_, _) -> let unification = infer context term in

From b3ed734811c76db4112852f467e79105dcd78e51 Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Tue, 12 Jan 2016 02:35:14 -0500
Subject: [PATCH 102/109] Add another test of simple function type inference.

---
 test/Spec.hs | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/test/Spec.hs b/test/Spec.hs
index b0932ec..b0a7630 100644
--- a/test/Spec.hs
+++ b/test/Spec.hs
@@ -71,9 +71,12 @@ main = hspec $ do
     prop "checks inferred types" $
       \ name t -> check t (Map.singleton name t) (variable name) `shouldBe` into t
 
-    it "infers function types" $
+    it "infers constant function types" $
       infer mempty (type' `lambda` const type') `shouldBe` type' --> type'
 
+    it "infers function types" $
+      infer mempty (type' `lambda` id) `shouldBe` type' --> type'
+
   describe "showsLevelPrec" $ do
     prop "parenthesizes right-nested applications" $
       \ a b c -> show (apply a (apply b c)) `shouldBe` showsPrec 10 a " (" ++ showsPrec 10 (apply b c :: Term') ")"

From 0e8a9281d6e3f2357afe5e87b0b122b1aa1f96ee Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Tue, 12 Jan 2016 02:41:25 -0500
Subject: [PATCH 103/109] =?UTF-8?q?Test=20the=20inference=20of=20`identity?=
 =?UTF-8?q?`=E2=80=99s=20type.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 test/Spec.hs | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/test/Spec.hs b/test/Spec.hs
index b0a7630..57914ca 100644
--- a/test/Spec.hs
+++ b/test/Spec.hs
@@ -77,6 +77,9 @@ main = hspec $ do
     it "infers function types" $
       infer mempty (type' `lambda` id) `shouldBe` type' --> type'
 
+    it "infers pi types" $
+      infer mempty (type' `lambda` \ a -> a `lambda` id) `shouldBe` (type' `lambda` \ a -> a --> a)
+
   describe "showsLevelPrec" $ do
     prop "parenthesizes right-nested applications" $
       \ a b c -> show (apply a (apply b c)) `shouldBe` showsPrec 10 a " (" ++ showsPrec 10 (apply b c :: Term') ")"

From 5ff72a453e7034f2405bc105cadbfbefb0f75cb6 Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Tue, 12 Jan 2016 02:43:32 -0500
Subject: [PATCH 104/109] =?UTF-8?q?Test=20the=20inference=20of=20`constant?=
 =?UTF-8?q?`=E2=80=99s=20type.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 test/Spec.hs | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/test/Spec.hs b/test/Spec.hs
index 57914ca..e858a15 100644
--- a/test/Spec.hs
+++ b/test/Spec.hs
@@ -77,9 +77,12 @@ main = hspec $ do
     it "infers function types" $
       infer mempty (type' `lambda` id) `shouldBe` type' --> type'
 
-    it "infers pi types" $
+    it "infers identity’s type" $
       infer mempty (type' `lambda` \ a -> a `lambda` id) `shouldBe` (type' `lambda` \ a -> a --> a)
 
+    it "infers constant’s type" $
+      infer mempty (type' `lambda` \ a -> type' `lambda` \ b -> a `lambda` \ a' -> b `lambda` const a') `shouldBe` (type' `lambda` \ a -> type' `lambda` \ b -> a --> b --> a)
+
   describe "showsLevelPrec" $ do
     prop "parenthesizes right-nested applications" $
       \ a b c -> show (apply a (apply b c)) `shouldBe` showsPrec 10 a " (" ++ showsPrec 10 (apply b c :: Term') ")"

From 4bb7cc442e13a1996df13eb1dfd5a6ea853066f4 Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Tue, 12 Jan 2016 03:11:40 -0500
Subject: [PATCH 105/109] Use the parameter type, and not its type, as the
 domain.

---
 src/Curve.hs | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/Curve.hs b/src/Curve.hs
index a619e78..f8457c8 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -168,7 +168,9 @@ check expected context term = case (out term, out expected) of
       _ -> a' `apply` infer context b
     _ -> a' `apply` infer context b
 
-  (Lambda i t body, Implicit) -> check type' context t `lambda` \ v -> substitute i v (infer (Map.insert (Local i) t context) body)
+  (Lambda i t body, Implicit) -> (check type' context t >> into t) `lambda` \ v -> substitute i v (infer (Map.insert (Local i) t context) body)
+    where (>>) (Unification _) b = b
+          (>>) a _ = a
 
   (_, Implicit) -> Conflict implicit implicit
   (_, _) -> let unification = infer context term in

From 318fea5206de16f631a7b028b2ad73b529d8a441 Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Tue, 12 Jan 2016 03:12:02 -0500
Subject: [PATCH 106/109] Shadow >> infix.

---
 src/Curve.hs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Curve.hs b/src/Curve.hs
index f8457c8..a9713bb 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -169,8 +169,8 @@ check expected context term = case (out term, out expected) of
     _ -> a' `apply` infer context b
 
   (Lambda i t body, Implicit) -> (check type' context t >> into t) `lambda` \ v -> substitute i v (infer (Map.insert (Local i) t context) body)
-    where (>>) (Unification _) b = b
-          (>>) a _ = a
+    where Unification _ >> b = b
+          a >> _ = a
 
   (_, Implicit) -> Conflict implicit implicit
   (_, _) -> let unification = infer context term in

From 90d1f24f3f5db4454a7f4724b8246e2e07e0e81b Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Tue, 12 Jan 2016 03:24:32 -0500
Subject: [PATCH 107/109] Check lambdas against types.

---
 src/Curve.hs | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/Curve.hs b/src/Curve.hs
index a9713bb..a6ea96d 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -173,6 +173,9 @@ check expected context term = case (out term, out expected) of
           a >> _ = a
 
   (_, Implicit) -> Conflict implicit implicit
+  
+  (Lambda {}, Type) -> check (type' --> type') context term
+
   (_, _) -> let unification = infer context term in
     maybe unification (unify expected) $ unified unification
 

From 180c8fefd37b7aca4768fd094e04b1f6bdf83872 Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Tue, 12 Jan 2016 03:26:20 -0500
Subject: [PATCH 108/109] Make the >> definition available to all cases.

---
 src/Curve.hs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Curve.hs b/src/Curve.hs
index a6ea96d..ee64ac7 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -169,8 +169,6 @@ check expected context term = case (out term, out expected) of
     _ -> a' `apply` infer context b
 
   (Lambda i t body, Implicit) -> (check type' context t >> into t) `lambda` \ v -> substitute i v (infer (Map.insert (Local i) t context) body)
-    where Unification _ >> b = b
-          a >> _ = a
 
   (_, Implicit) -> Conflict implicit implicit
   
@@ -178,6 +176,8 @@ check expected context term = case (out term, out expected) of
 
   (_, _) -> let unification = infer context term in
     maybe unification (unify expected) $ unified unification
+  where Unification _ >> b = b
+        a >> _ = a
 
 
 -- Equality

From c3bb9be7c7b040680eb043b23ccdbe2d041927ac Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@github.com>
Date: Tue, 12 Jan 2016 03:26:36 -0500
Subject: [PATCH 109/109] Strip some leading indentation.

---
 src/Curve.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Curve.hs b/src/Curve.hs
index ee64ac7..974ac6e 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -171,7 +171,7 @@ check expected context term = case (out term, out expected) of
   (Lambda i t body, Implicit) -> (check type' context t >> into t) `lambda` \ v -> substitute i v (infer (Map.insert (Local i) t context) body)
 
   (_, Implicit) -> Conflict implicit implicit
-  
+
   (Lambda {}, Type) -> check (type' --> type') context term
 
   (_, _) -> let unification = infer context term in