From 5eaa216b9be609104adfe9a3cdd7d1ec4c29190a Mon Sep 17 00:00:00 2001
From: Ilya Yanok <ilya.yanok@gmail.com>
Date: Mon, 15 May 2017 12:06:37 +0200
Subject: [PATCH 1/6] SimpleFP-v2: make it compile with GHC8 and lts-8.13

Mostly changing Eq1 instances to work with transformers-5
---
 src/Continuations/Core/Term.hs    |  17 +++--
 src/Dependent/Monadic/Equality.hs |  62 +++++++++------
 src/Require/Core/Parser.hs        |   4 +-
 src/Require/Core/Term.hs          | 123 +++++++++++++++++-------------
 src/Simple/Monadic/Equality.hs    |   8 +-
 src/Utils/ABT.hs                  |  11 ++-
 src/Utils/Telescope.hs            |   6 +-
 7 files changed, 132 insertions(+), 99 deletions(-)

diff --git a/src/Continuations/Core/Term.hs b/src/Continuations/Core/Term.hs
index 5edb16a..a2823af 100644
--- a/src/Continuations/Core/Term.hs
+++ b/src/Continuations/Core/Term.hs
@@ -142,14 +142,15 @@ instance Bizippable PatternFF where
 
 
 instance Bitraversable PatternFF where
-  bisequenceA (ConPat c ps) =
-    ConPat c <$> sequenceA [ (,) plic <$> p
-                           | (plic,p) <- ps
-                           ]
-  bisequenceA (AssertionPat m) =
-    AssertionPat <$> m
-  bisequenceA MakeMeta =
-    pure MakeMeta
+  bitraverse f g = biseq . bimap f g where
+    biseq (ConPat c ps) =
+      ConPat c <$> sequenceA [ (,) plic <$> p
+                             | (plic,p) <- ps
+                             ]
+    biseq (AssertionPat m) =
+      AssertionPat <$> m
+    biseq MakeMeta =
+      pure MakeMeta
 
 
 -- | 'PatternF' is the type of pattern shaped containers for terms. The
diff --git a/src/Dependent/Monadic/Equality.hs b/src/Dependent/Monadic/Equality.hs
index 71ec4a6..bd7ce84 100644
--- a/src/Dependent/Monadic/Equality.hs
+++ b/src/Dependent/Monadic/Equality.hs
@@ -15,6 +15,7 @@ import Dependent.Core.Term
 
 import Data.Functor.Classes
 
+import Utils.ABT
 
 
 
@@ -22,42 +23,53 @@ import Data.Functor.Classes
 
 
 instance Eq1 TermF where
-  eq1 (Defined n) (Defined n') =
+  liftEq eq (Defined n) (Defined n') =
     n == n'
-  eq1 (Ann m t) (Ann m' t') =
-    m == m' && t == t'
-  eq1 Type Type = True
-  eq1 (Fun arg sc) (Fun arg' sc') =
-    arg == arg' && sc == sc'
-  eq1 (Lam sc) (Lam sc') =
-    sc == sc'
-  eq1 (App f x) (App f' x') =
-    f == f' && x == x'
-  eq1 (Con c as) (Con c' as') =
-    c == c' && as == as'
-  eq1 (Case as mot cls) (Case as' mot' cls') =
-    as == as' && eq1 mot mot' &&
-      length cls == length cls' && and (zipWith eq1 cls cls')
-  eq1 _ _ = False
+  liftEq eq (Ann m t) (Ann m' t') =
+    eq m m' && eq t t'
+  liftEq eq Type Type = True
+  liftEq eq (Fun arg sc) (Fun arg' sc') =
+    eq arg arg' && eq sc sc'
+  liftEq eq (Lam sc) (Lam sc') =
+    eq sc sc'
+  liftEq eq (App f x) (App f' x') =
+    eq f f' && eq x x'
+  liftEq eq (Con c as) (Con c' as') =
+    c == c' && liftEq eq as as'
+  liftEq eq (Case as mot cls) (Case as' mot' cls') =
+    liftEq eq as as' && liftEq eq mot mot' &&
+      length cls == length cls' && and (zipWith (liftEq eq) cls cls')
+  liftEq _ _ _ = False
 
 
 instance Eq1 CaseMotiveF where
-  eq1 (CaseMotive t) (CaseMotive t') = eq1 t t'
+  liftEq eq (CaseMotive t) (CaseMotive t') = liftEq eq t t'
 
 
 instance Eq1 ClauseF where
-  eq1 (Clause pscs bsc) (Clause pscs' bsc') =
-    length pscs == length pscs' && and (zipWith eq1 pscs pscs') &&
-      bsc == bsc'
+  liftEq eq (Clause pscs bsc) (Clause pscs' bsc') =
+    length pscs == length pscs' && and (zipWith (liftEq eq) pscs pscs') &&
+      eq bsc bsc'
 
 
 instance Eq1 PatternF where
-  eq1 (PatternF x) (PatternF y) = x == y
+  liftEq eq (PatternF x) (PatternF x') = eqScopes eq x x'
+    where
+      eqScopes :: (a -> b -> Bool) -> Scope (PatternFF a) -> Scope (PatternFF b) -> Bool
+      eqScopes eq' = liftScopeEq (liftABTEq $ liftEq2 eq' (eqScopes eq'))
 
 
 instance Eq a => Eq1 (PatternFF a) where
-  eq1 (ConPat c ps) (ConPat c' ps') =
-    c == c' && ps == ps'
-  eq1 (AssertionPat m) (AssertionPat m') =
+  liftEq eq (ConPat c ps) (ConPat c' ps') =
+    c == c' && liftEq eq ps ps'
+  liftEq eq (AssertionPat m) (AssertionPat m') =
     m == m'
-  eq1 _ _ = False
\ No newline at end of file
+  liftEq _ _ _ = False
+
+instance Eq2 PatternFF where
+  liftEq2 eq eq' (ConPat c ps) (ConPat c' ps') =
+    c == c' && liftEq eq' ps ps'
+  liftEq2 eq eq' (AssertionPat m) (AssertionPat m') =
+    eq m m'
+  liftEq2 _ _ _ _ =
+    False
diff --git a/src/Require/Core/Parser.hs b/src/Require/Core/Parser.hs
index 43e9cb0..9eaed5d 100644
--- a/src/Require/Core/Parser.hs
+++ b/src/Require/Core/Parser.hs
@@ -19,8 +19,8 @@ import Require.Core.DeclArg
 import Require.Core.Term
 import Require.Core.Program
 
-import Debug
-
+--import Debug
+debug_ = const $ return ()
 
 
 
diff --git a/src/Require/Core/Term.hs b/src/Require/Core/Term.hs
index 2b41660..defaf1c 100644
--- a/src/Require/Core/Term.hs
+++ b/src/Require/Core/Term.hs
@@ -64,45 +64,45 @@ data TermF r
 
 
 instance Eq1 TermF where
-  eq1 (Defined n) (Defined n') =
+  liftEq _ (Defined n) (Defined n') =
     n == n'
-  eq1 (Ann m t) (Ann m' t') =
-    m == m' && t == t'
-  eq1 Type Type =
+  liftEq eq (Ann m t) (Ann m' t') =
+    eq m m' && eq t t'
+  liftEq _ Type Type =
     True
-  eq1 (Fun plic a sc) (Fun plic' a' sc') =
-    plic == plic' && a == a' && sc == sc'
-  eq1 (Lam plic sc) (Lam plic' sc') =
-    plic == plic' && sc == sc'
-  eq1 (App plic f x) (App plic' f' x') =
-    plic == plic' && f == f' && x == x'
-  eq1 (Con c ms) (Con c' ms') =
-    c == c' && ms == ms'
-  eq1 (Case ms motive clauses) (Case ms' motive' clauses') =
-    ms == ms' && eq1 motive motive'
+  liftEq eq (Fun plic a sc) (Fun plic' a' sc') =
+    plic == plic' && eq a a' && eq sc sc'
+  liftEq eq (Lam plic sc) (Lam plic' sc') =
+    plic == plic' && eq sc sc'
+  liftEq eq (App plic f x) (App plic' f' x') =
+    plic == plic' && eq f f' && eq x x'
+  liftEq eq (Con c ms) (Con c' ms') =
+    c == c' && liftEq (\(p,a) (p',a') -> p == p' && eq a a') ms ms'
+  liftEq eq (Case ms motive clauses) (Case ms' motive' clauses') =
+    liftEq eq ms ms' && liftEq eq motive motive'
       && length clauses == length clauses'
-      && all (uncurry eq1) (zip clauses clauses')
-  eq1 (RecordType fields tele) (RecordType fields' tele') =
-    fields == fields' && eq1 tele tele'
-  eq1 (RecordCon fs) (RecordCon fs') =
-    fs == fs'
-  eq1 (RecordProj m x) (RecordProj m' x') =
-    x == x' && m == m'
-  eq1 (QuotedType resets a) (QuotedType resets' a') =
-    resets == resets' && a == a'
-  eq1 (Quote m) (Quote m') =
-    m == m'
-  eq1 (Unquote m) (Unquote m') =
-    m == m'
-  eq1 (Continue m) (Continue m') =
-    m == m'
-  eq1 (Shift res m) (Shift res' m') =
-    res == res' && m == m'
-  eq1 (Reset res m) (Reset res' m') =
-    res == res' && m == m'
-  eq1 (Require a sc) (Require a' sc') =
-    a == a' && sc == sc'
-  eq1 _ _ =
+      && all (uncurry $ liftEq eq) (zip clauses clauses')
+  liftEq eq (RecordType fields tele) (RecordType fields' tele') =
+    fields == fields' && liftEq eq tele tele'
+  liftEq eq (RecordCon fs) (RecordCon fs') =
+    liftEq (\(n,a) (n',a') -> n == n' && eq a a') fs fs'
+  liftEq eq (RecordProj m x) (RecordProj m' x') =
+    x == x' && eq m m'
+  liftEq eq (QuotedType resets a) (QuotedType resets' a') =
+    resets == resets' && eq a a'
+  liftEq eq (Quote m) (Quote m') =
+    eq m m'
+  liftEq eq (Unquote m) (Unquote m') =
+    eq m m'
+  liftEq eq (Continue m) (Continue m') =
+    eq m m'
+  liftEq eq (Shift res m) (Shift res' m') =
+    res == res' && eq m m'
+  liftEq eq (Reset res m) (Reset res' m') =
+    res == res' && eq m m'
+  liftEq eq (Require a sc) (Require a' sc') =
+    eq a a' && eq sc sc'
+  liftEq _ _ _ =
     False
 
 
@@ -124,8 +124,8 @@ newtype CaseMotiveF r = CaseMotive (BindingTelescope r)
 
 
 instance Eq1 CaseMotiveF where
-  eq1 (CaseMotive tele) (CaseMotive tele') =
-    eq1 tele tele'
+  liftEq eq (CaseMotive tele) (CaseMotive tele') =
+    liftEq eq tele tele'
 
 
 type CaseMotive = CaseMotiveF (Scope TermF)
@@ -137,10 +137,10 @@ data ClauseF r
 
 
 instance Eq1 ClauseF where
-  eq1 (Clause ps sc) (Clause ps' sc') =
+  liftEq eq (Clause ps sc) (Clause ps' sc') =
     length ps == length ps'
-      && all (uncurry eq1) (zip ps ps')
-      && sc == sc'
+      && all (uncurry $ liftEq eq) (zip ps ps')
+      && eq sc sc'
 
 
 type Clause = ClauseF (Scope TermF)
@@ -172,15 +172,24 @@ data PatternFF a r
 
 
 instance Eq a => Eq1 (PatternFF a) where
-  eq1 (ConPat c ps) (ConPat c' ps') =
-    c == c' && ps == ps'
-  eq1 (AssertionPat m) (AssertionPat m') =
+  liftEq eq (ConPat c ps) (ConPat c' ps') =
+    c == c' && liftEq (\(p,a) (p',a') -> p == p' && eq a a') ps ps'
+  liftEq eq (AssertionPat m) (AssertionPat m') =
     m == m'
-  eq1 MakeMeta MakeMeta =
+  liftEq eq MakeMeta MakeMeta =
     True
-  eq1 _ _ =
+  liftEq eq _ _ =
     False
 
+instance Eq2 PatternFF where
+  liftEq2 eq eq' (ConPat c ps) (ConPat c' ps') =
+    c == c' && liftEq (\(p,a) (p',a') -> p == p' && eq' a a') ps ps'
+  liftEq2 eq eq' (AssertionPat m) (AssertionPat m') =
+    eq m m'
+  liftEq2 eq eq' MakeMeta MakeMeta =
+    True
+  liftEq2 _ _ _ _ =
+    False
 
 instance Bifunctor PatternFF where
   bimap _ g (ConPat s xs) = ConPat s [ (plic,g x) | (plic,x) <- xs ]
@@ -210,14 +219,15 @@ instance Bizippable PatternFF where
 
 
 instance Bitraversable PatternFF where
-  bisequenceA (ConPat c ps) =
-    ConPat c <$> sequenceA [ (,) plic <$> p
-                           | (plic,p) <- ps
-                           ]
-  bisequenceA (AssertionPat m) =
-    AssertionPat <$> m
-  bisequenceA MakeMeta =
-    pure MakeMeta
+  bitraverse f g = biseq . bimap f g where
+    biseq (ConPat c ps) =
+      ConPat c <$> sequenceA [ (,) plic <$> p
+                             | (plic,p) <- ps
+                             ]
+    biseq (AssertionPat m) =
+      AssertionPat <$> m
+    biseq MakeMeta =
+      pure MakeMeta
 
 
 -- | 'PatternF' is the type of pattern shaped containers for terms. The
@@ -229,7 +239,10 @@ newtype PatternF a = PatternF { unwrapPatternF :: Scope (PatternFF a) }
 
 
 instance Eq1 PatternF where
-  eq1 (PatternF x) (PatternF x') = x == x'
+  liftEq eq (PatternF x) (PatternF x') = eqScopes eq x x'
+    where
+      eqScopes :: (a -> b -> Bool) -> Scope (PatternFF a) -> Scope (PatternFF b) -> Bool
+      eqScopes eq' = liftScopeEq (liftABTEq $ liftEq2 eq' (eqScopes eq'))
 
 
 type Pattern = ABT (PatternFF Term)
diff --git a/src/Simple/Monadic/Equality.hs b/src/Simple/Monadic/Equality.hs
index c4a65f7..b561223 100644
--- a/src/Simple/Monadic/Equality.hs
+++ b/src/Simple/Monadic/Equality.hs
@@ -22,8 +22,8 @@ import Data.Functor.Classes
 
 
 instance Eq1 TypeF where
-  eq1 (TyCon c) (TyCon c') =
+  liftEq _ (TyCon c) (TyCon c') =
     c == c'
-  eq1 (Fun a b) (Fun a' b') =
-    a == a' && b == b'
-  eq1 _ _ = False
\ No newline at end of file
+  liftEq eq (Fun a b) (Fun a' b') =
+    eq a a' && eq b b'
+  liftEq _ _ _ = False
diff --git a/src/Utils/ABT.hs b/src/Utils/ABT.hs
index ad075a4..da2064c 100644
--- a/src/Utils/ABT.hs
+++ b/src/Utils/ABT.hs
@@ -726,8 +726,15 @@ instance Eq1 f => Eq (Scope f) where
 
 
 
-
-
+-- needed for Eq1 PatternF instance
+liftABTEq :: (f (Scope f) -> g (Scope g) -> Bool) -> ABT f -> ABT g -> Bool
+liftABTEq _ (Var x) (Var y) = x == y
+liftABTEq eq (In x) (In y) = eq x y
+liftABTEq _ _ _ = False
+
+liftScopeEq :: (ABT f -> ABT g -> Bool) -> Scope f -> Scope g -> Bool
+liftScopeEq eq (Scope ns _ x) (Scope ns' _ y) =
+  length ns == length ns' && eq x y
 
 
 -- * Zipping
diff --git a/src/Utils/Telescope.hs b/src/Utils/Telescope.hs
index c9d5029..2b73567 100644
--- a/src/Utils/Telescope.hs
+++ b/src/Utils/Telescope.hs
@@ -35,7 +35,7 @@ data Telescope a
 
 
 instance Eq1 Telescope where
-  eq1 (Telescope as) (Telescope as') = as == as'
+  liftEq eq (Telescope as) (Telescope as') = liftEq eq as as'
 
 
 namesTelescope :: Telescope (Scope f) -> [String]
@@ -153,8 +153,8 @@ data BindingTelescope a
 
 
 instance Eq1 BindingTelescope where
-  eq1 (BindingTelescope as b) (BindingTelescope as' b') =
-    as == as' && b == b'
+  liftEq eq (BindingTelescope as b) (BindingTelescope as' b') =
+    liftEq eq as as' && eq b b'
 
 
 namesBindingTelescope :: BindingTelescope (Scope f) -> [String]

From d6338206c96e97bcdffc16bf262b7ebdaaed495b Mon Sep 17 00:00:00 2001
From: Ilya Yanok <ilya.yanok@gmail.com>
Date: Mon, 15 May 2017 12:07:53 +0200
Subject: [PATCH 2/6] SimpleFP-v2: add stack.yaml

---
 stack.yaml | 35 +++++++++++++++++++++++++++++++++++
 1 file changed, 35 insertions(+)
 create mode 100644 stack.yaml

diff --git a/stack.yaml b/stack.yaml
new file mode 100644
index 0000000..f87eddc
--- /dev/null
+++ b/stack.yaml
@@ -0,0 +1,35 @@
+# For more information, see: http://docs.haskellstack.org/en/stable/yaml_configuration.html
+
+# Specifies the GHC version and set of packages available (e.g., lts-3.5, nightly-2015-09-21, ghc-7.10.2)
+resolver: lts-8.13
+
+# Local packages, usually specified by relative directory name
+packages:
+- '.'
+
+# Packages to be pulled from upstream that are not in the resolver (e.g., acme-missiles-0.3)
+extra-deps: []
+
+# Override default flag values for local packages and extra-deps
+flags: {}
+
+# Extra package databases containing global packages
+extra-package-dbs: []
+
+# Control whether we use the GHC we find on the path
+# system-ghc: true
+
+# Require a specific version of stack, using version ranges
+# require-stack-version: -any # Default
+# require-stack-version: >= 1.0.0
+
+# Override the architecture used by stack, especially useful on Windows
+# arch: i386
+# arch: x86_64
+
+# Extra directories used by stack for building
+# extra-include-dirs: [/path/to/dir]
+# extra-lib-dirs: [/path/to/dir]
+
+# Allow a newer minor version of GHC than the snapshot specifies
+# compiler-check: newer-minor

From 1af13abf35fd0457e8664927e3acaf361f407308 Mon Sep 17 00:00:00 2001
From: Ilya Yanok <ilya.yanok@gmail.com>
Date: Mon, 15 May 2017 12:08:14 +0200
Subject: [PATCH 3/6] dependent: add example that show we can (wrongly) prove
 injectivity

---
 src/Dependent/Eq.sfp | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)
 create mode 100644 src/Dependent/Eq.sfp

diff --git a/src/Dependent/Eq.sfp b/src/Dependent/Eq.sfp
new file mode 100644
index 0000000..4ac7dcc
--- /dev/null
+++ b/src/Dependent/Eq.sfp
@@ -0,0 +1,20 @@
+
+data Eq (a : Type) (x : a) (y : a) where
+| Refl (a : Type) (x : a) : Eq a x x
+end
+
+let inj :
+  (a : Type) ->
+  (b : Type) ->
+  (f : a -> b) ->
+  (x : a) ->
+  (y : a) ->
+  (eq : Eq b (f x) (f y)) ->
+  Eq a x y =
+  \a -> \b -> \f -> \x -> \y -> \eq ->
+  case y || eq
+  motive (y' : a) || (eq' : Eq b (f x) (f y')) || Eq a x y'
+  of
+  | .x || Refl .b .(f x) -> Refl a x
+  end
+end

From c76d50e740247d80c6c1b9063c5bca6a35062731 Mon Sep 17 00:00:00 2001
From: Ilya Yanok <ilya.yanok@gmail.com>
Date: Tue, 30 May 2017 13:20:21 +0200
Subject: [PATCH 4/6] Dependent: add example of (wrongly) proving equality for
 any pair of values of the same type

---
 src/Dependent/EqAny.sfp | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)
 create mode 100644 src/Dependent/EqAny.sfp

diff --git a/src/Dependent/EqAny.sfp b/src/Dependent/EqAny.sfp
new file mode 100644
index 0000000..0b008f6
--- /dev/null
+++ b/src/Dependent/EqAny.sfp
@@ -0,0 +1,17 @@
+
+data Eq (a : Type) (x : a) (y : a) where
+| Refl (a : Type) (x : a) : Eq a x x
+end
+
+let anyEq :
+  (a : Type) ->
+  (x : a) ->
+  (y : a) ->
+  Eq a x y =
+  \a -> \x -> \y ->
+  case y 
+  motive (y' : a) || Eq a x y'
+  of
+  | .x -> Refl a x
+  end
+end

From 4478f717cbfc8353cb82448ad4ec020862b15664 Mon Sep 17 00:00:00 2001
From: Ilya Yanok <ilya.yanok@gmail.com>
Date: Fri, 2 Jun 2017 17:43:58 +0200
Subject: [PATCH 5/6] typecheck: fix assertion patterns checking

Before this commit assertion patterns are only checked to have the
required type. That is not enough, as the value provided in the
assertion pattern is used to determine the result type of the clause, so
we have to ensure the value provided in the assertion pattern is indeed
the only option, otherwise the type checking will become unsound
(see src/Dependent/EqAny.sfp for an example).

This patch adds checking for the assertion patterns. To achieve this we
return new meta variable as the pattern value and save a pair (meta,
assertion pattern value) for the later. By the end of clause pattern
checking this new meta variable should be solved to exactly the value
provided, otherwise it's an error.

This fixes all the affected variants EXCEPT Dependent.Monadic, since we
rely on the unification to solve the constraint for us.
---
 src/Continuations/Unification/TypeChecking.hs | 46 +++++++++++-----
 src/Dependent/Unification/TypeChecking.hs     | 52 ++++++++++++-------
 .../Unification/TypeChecking.hs               | 46 +++++++++++-----
 src/Modular/Unification/TypeChecking.hs       | 46 +++++++++++-----
 src/OpenDefs/Unification/TypeChecking.hs      | 46 +++++++++++-----
 src/Quasiquote/Unification/TypeChecking.hs    | 46 +++++++++++-----
 src/Record/Unification/TypeChecking.hs        | 46 +++++++++++-----
 src/Require/Unification/TypeChecking.hs       | 46 +++++++++++-----
 8 files changed, 271 insertions(+), 103 deletions(-)

diff --git a/src/Continuations/Unification/TypeChecking.hs b/src/Continuations/Unification/TypeChecking.hs
index acf260d..6ef08e4 100644
--- a/src/Continuations/Unification/TypeChecking.hs
+++ b/src/Continuations/Unification/TypeChecking.hs
@@ -978,7 +978,7 @@ checkifyCaseMotive (CaseMotive tele) =
 
 checkifyPattern :: Pattern
                 -> NormalTerm
-                -> TypeChecker (Pattern,ElaboratedTerm)
+                -> TypeChecker (Pattern,ElaboratedTerm,[(Term,Term)])
 checkifyPattern (Var (Bound _ _)) _ =
   error "A bound variable should not be the subject of pattern type checking."
 checkifyPattern (Var (Free x)) t =
@@ -986,12 +986,13 @@ checkifyPattern (Var (Free x)) t =
      unifyHelper t (NormalTerm t')  -- @t'@ is guaranteed to be normal
      return ( Var (Free x)
             , ElaboratedTerm (Var (Free x))
+            , []
             )
 checkifyPattern (Var (Meta _)) _ =
   error "Metavariables should not be the subject of pattern type checking."
 checkifyPattern (In (ConPat c ps)) (NormalTerm t) =
   do (ec,ConSig plics (BindingTelescope ascs bsc)) <- typeInSignature c
-     (ps',elms') <-
+     (ps',elms',cs) <-
        checkifyPatterns
          (zip plics ascs)
          bsc
@@ -1000,17 +1001,21 @@ checkifyPattern (In (ConPat c ps)) (NormalTerm t) =
      let ms' = [ (plic,m') | (plic, ElaboratedTerm m') <- elms' ]
      return ( conPatH ec ps'
             , ElaboratedTerm (conH ec ms')
+            , cs
             )
 checkifyPattern (In (AssertionPat m)) t =
   do ElaboratedTerm m' <- checkify m t
+     mv <- nextElab nextMeta
      return ( In (AssertionPat m')
-            , ElaboratedTerm m'
+            , ElaboratedTerm (Var $ Meta mv)
+            , [(Var $ Meta mv, m')]
             )
 checkifyPattern (In MakeMeta) _ =
   do meta <- nextElab nextMeta
      let x = Var (Meta meta)
      return ( In (AssertionPat x)
             , ElaboratedTerm x
+            , []
             )
 
 
@@ -1049,6 +1054,7 @@ checkifyPatterns :: [(Plicity,Scope TermF)]
                  -> Term
                  -> TypeChecker ( [(Plicity,Pattern)]
                                 , [(Plicity,ElaboratedTerm)]
+                                , [(Term,Term)]
                                 )
 checkifyPatterns ascs0 bsc ps0 t =
   do argsToCheck <- accArgsToCheck [] ascs0 ps0
@@ -1062,33 +1068,36 @@ checkifyPatterns ascs0 bsc ps0 t =
               return (eqs,ret')
          ret' -> return ([],ret')
      unifyHelper (NormalTerm ret') (NormalTerm t)
-     psms' <- forM argsToCheck $ \(plic,p0,mToElabInto,a) ->
+     (ps',ms',cs) <- unzip3 <$> forM argsToCheck (\(plic,p0,mToElabInto,a) ->
                 case p0 of
                   Nothing ->
                     do subMToElabInto <- substitute mToElabInto
                        em' <- evaluate subMToElabInto
                        return ( (plic, In (AssertionPat (normTerm em')))
                               , (plic, ElaboratedTerm (normTerm em'))
+                              , []
                               )
                   Just p ->
                     do subMToElabInto <- substitute mToElabInto
                        eMToElabInto <- evaluate subMToElabInto
                        suba <- substitute a
                        ea <- evaluate suba
-                       (p',ElaboratedTerm m') <- checkifyPattern p ea
+                       (p',ElaboratedTerm m',cs) <- checkifyPattern p ea
                        subm' <- substitute m'
                        em' <- evaluate subm'
                        unifyHelper eMToElabInto em'
                        return ( (plic, p')
                               , (plic, ElaboratedTerm (normTerm em'))
+                              , cs
                               )
+                                                 )
      forM_ eqs $ \(l,r) ->
        do subl <- substitute l
           el <- evaluate subl
           subr <- substitute r
           er <- evaluate subr
           unifyHelper el er
-     return $ unzip psms'
+     return (ps',ms',concat cs)
   where
     accArgsToCheck :: [(Plicity,Maybe Pattern,Term,Term)]
                    -> [(Plicity,Scope TermF)]
@@ -1160,21 +1169,34 @@ checkifyPatternsCaseMotive :: [Pattern]
                            -> CaseMotive
                            -> TypeChecker ([Pattern], ElaboratedTerm)
 checkifyPatternsCaseMotive ps0 (CaseMotive (BindingTelescope ascs bsc)) =
-  do (ps',ms') <- go [] ps0 ascs
+  do (ps',ms',cs) <- go [] ps0 ascs
+     forM_ cs (\(l,r) -> do
+                  subl <- substitute l
+                  el <- evaluate subl
+                  subr <- substitute r
+                  er <- evaluate subr
+                  s <- getElab substitution
+                  unifyHelper el er
+                  s' <- getElab substitution
+                  when (length s /= length s') $
+                    throwError $ "Solving the constraint "
+                    ++ pretty (normTerm el) ++ " == "
+                    ++ pretty (normTerm er) ++ " produced new metavar resolution"
+              )
      return (ps', ElaboratedTerm (instantiate bsc ms'))
   where
     go :: [Term]
        -> [Pattern]
        -> [Scope TermF]
-       -> TypeChecker ([Pattern],[Term])
+       -> TypeChecker ([Pattern],[Term],[(Term,Term)])
     go _ [] [] =
-      return ([],[])
+      return ([],[],[])
     go acc (p:ps) (sc:scs) =
       do subt <- substitute (instantiate sc acc)
          et <- evaluate subt
-         (p',ElaboratedTerm m') <- checkifyPattern p et
-         (ps',ms') <- go (acc ++ [m']) ps scs
-         return (p':ps', m':ms')
+         (p',ElaboratedTerm m',cs) <- checkifyPattern p et
+         (ps',ms',cs') <- go (acc ++ [m']) ps scs
+         return (p':ps', m':ms', cs ++ cs')
     go _ _ _ =
       error $ "The auxiliary function 'go' in 'checkPatternsCaseMotive'"
            ++ " should always have equal number of args for its patterns and"
diff --git a/src/Dependent/Unification/TypeChecking.hs b/src/Dependent/Unification/TypeChecking.hs
index 73ab0dc..eeb02f4 100644
--- a/src/Dependent/Unification/TypeChecking.hs
+++ b/src/Dependent/Unification/TypeChecking.hs
@@ -318,14 +318,14 @@ checkifyCaseMotive (CaseMotive tele) = checkifyTelescope tele
 
 checkifyPattern :: Pattern
                 -> NormalTerm
-                -> TypeChecker Term
+                -> TypeChecker (Term, [(Term,Term)])
 checkifyPattern (Var (Bound _ _)) _ =
   error "A bound variable should not be the subject of pattern type checking."
 
 checkifyPattern (Var (Free x)) t =
   do t' <- typeInContext x
      unifyHelper t (NormalTerm t')  -- @t'@ is guaranteed to be normal
-     return $ Var (Free x)
+     return (Var (Free x), [])
 checkifyPattern (Var (Meta _)) _ =
   error "Metavariables should not be the subject of pattern type checking."
 checkifyPattern (In (ConPat c ps)) t =
@@ -336,14 +336,15 @@ checkifyPattern (In (ConPat c ps)) t =
        $ throwError $ "The constructor " ++ c ++ " expects " ++ show lascs
                    ++ " " ++ (if lascs == 1 then "arg" else "args")
                    ++ " but was given " ++ show lps
-     (ms,ret) <- checkifyPatterns (map instantiate0 ps) consig
+     (ms,ret,cs) <- checkifyPatterns (map instantiate0 ps) consig
      subret <- substitute ret
      eret <- evaluate subret
      unifyHelper eret t
-     return $ conH c ms
+     return (conH c ms, cs)
 checkifyPattern (In (AssertionPat m)) t =
   do checkify m t
-     return m
+     mv <- nextElab nextMeta
+     return (Var $ Meta mv, [(Var $ Meta mv, m)])
 
 
 
@@ -365,19 +366,19 @@ checkifyPattern (In (AssertionPat m)) t =
 
 checkifyPatterns :: [Pattern]
                  -> ConSig
-                 -> TypeChecker ([Term], Term)
+                 -> TypeChecker ([Term], Term, [(Term, Term)])
 checkifyPatterns ps0 (ConSig (BindingTelescope ascs bsc)) =
-  do ms <- go [] ps0 ascs
-     return (ms, instantiate bsc ms)
+  do (ms, cs) <- go [] ps0 ascs
+     return (ms, instantiate bsc ms, cs)
   where
-    go :: [Term] -> [Pattern] -> [Scope TermF] -> TypeChecker [Term]
-    go _ [] [] = return []
+    go :: [Term] -> [Pattern] -> [Scope TermF] -> TypeChecker ([Term],[(Term, Term)])
+    go _ [] [] = return ([], [])
     go acc (p:ps) (sc:scs) =
       do subt <- substitute (instantiate sc acc)
          et <- evaluate subt
-         m <- checkifyPattern p et
-         ms <- go (acc ++ [m]) ps scs
-         return $ m:ms
+         (m, cs) <- checkifyPattern p et
+         (ms, cs') <- go (acc ++ [m]) ps scs
+         return (m:ms, cs ++ cs')
     go _ _ _ =
       error $ "The auxiliary function 'go' in 'checkPatterns' should always"
            ++ " have equal number of args for its patterns and scopes. This"
@@ -404,21 +405,34 @@ checkifyPatternsCaseMotive :: [Pattern]
                            -> CaseMotive
                            -> TypeChecker Term
 checkifyPatternsCaseMotive ps0 (CaseMotive (BindingTelescope ascs bsc)) =
-  do ms <- go [] ps0 ascs
+  do (ms, cs) <- go [] ps0 ascs
+     forM_ cs (\(l,r) -> do
+                  subl <- substitute l
+                  el <- evaluate subl
+                  subr <- substitute r
+                  er <- evaluate subr
+                  s <- getElab substitution
+                  unifyHelper el er
+                  s' <- getElab substitution
+                  when (length s /= length s') $
+                    throwError $ "Solving the constraint "
+                    ++ pretty (normTerm el) ++ " == "
+                    ++ pretty (normTerm er) ++ " produced new metavar resolution"
+              )
      return $ instantiate bsc ms
   where
     go :: [Term]
        -> [Pattern]
        -> [Scope TermF]
-       -> TypeChecker [Term]
+       -> TypeChecker ([Term], [(Term, Term)])
     go _ [] [] =
-      return []
+      return ([], [])
     go acc (p:ps) (sc:scs) =
       do subt <- substitute (instantiate sc acc)
          et <- evaluate subt
-         m <- checkifyPattern p et
-         ms <- go (acc ++ [m]) ps scs
-         return $ m:ms
+         (m,cs) <- checkifyPattern p et
+         (ms,cs') <- go (acc ++ [m]) ps scs
+         return (m:ms, cs ++ cs')
     go _ _ _ =
       error $ "The auxiliary function 'go' in 'checkPatternsCaseMotive'"
            ++ " should always have equal number of args for its patterns and"
diff --git a/src/DependentImplicit/Unification/TypeChecking.hs b/src/DependentImplicit/Unification/TypeChecking.hs
index 155664f..301d0a3 100644
--- a/src/DependentImplicit/Unification/TypeChecking.hs
+++ b/src/DependentImplicit/Unification/TypeChecking.hs
@@ -668,7 +668,7 @@ checkifyCaseMotive (CaseMotive tele) =
 
 checkifyPattern :: Pattern
                 -> NormalTerm
-                -> TypeChecker (Pattern,ElaboratedTerm)
+                -> TypeChecker (Pattern,ElaboratedTerm,[(Term,Term)])
 checkifyPattern (Var (Bound _ _)) _ =
   error "A bound variable should not be the subject of pattern type checking."
 checkifyPattern (Var (Free x)) t =
@@ -676,6 +676,7 @@ checkifyPattern (Var (Free x)) t =
      unifyHelper t (NormalTerm t')  -- @t'@ is guaranteed to be normal
      return ( Var (Free x)
             , ElaboratedTerm (Var (Free x))
+            , []
             )
 checkifyPattern (Var (Meta _)) _ =
   error "Metavariables should not be the subject of pattern type checking."
@@ -683,7 +684,7 @@ checkifyPattern (In (ConPat _ _)) (NormalTerm (In Type)) =
   throwError "Cannot pattern match on a type."
 checkifyPattern (In (ConPat c ps)) (NormalTerm t) =
   do ConSig plics (BindingTelescope ascs bsc) <- typeInSignature c
-     (ps',elms') <-
+     (ps',elms',cs) <-
        checkifyPatterns
          (zip plics ascs)
          bsc
@@ -692,17 +693,21 @@ checkifyPattern (In (ConPat c ps)) (NormalTerm t) =
      let ms' = [ (plic,m') | (plic, ElaboratedTerm m') <- elms' ]
      return ( conPatH c ps'
             , ElaboratedTerm (conH c ms')
+            , cs
             )
 checkifyPattern (In (AssertionPat m)) t =
   do ElaboratedTerm m' <- checkify m t
+     mv <- nextElab nextMeta
      return ( In (AssertionPat m')
-            , ElaboratedTerm m'
+            , ElaboratedTerm (Var $ Meta mv)
+            , [(Var $ Meta mv, m')]
             )
 checkifyPattern (In MakeMeta) _ =
   do meta <- nextElab nextMeta
      let x = Var (Meta meta)
      return ( In (AssertionPat x)
             , ElaboratedTerm x
+            , []
             )
 
 
@@ -741,6 +746,7 @@ checkifyPatterns :: [(Plicity,Scope TermF)]
                  -> Term
                  -> TypeChecker ( [(Plicity,Pattern)]
                                 , [(Plicity,ElaboratedTerm)]
+                                , [(Term,Term)]
                                 )
 checkifyPatterns ascs0 bsc ps0 t =
   do argsToCheck <- accArgsToCheck [] ascs0 ps0
@@ -754,33 +760,36 @@ checkifyPatterns ascs0 bsc ps0 t =
               return (eqs,ret')
          ret' -> return ([],ret')
      unifyHelper (NormalTerm ret') (NormalTerm t)
-     psms' <- forM argsToCheck $ \(plic,p0,mToElabInto,a) ->
+     (ps',ms',cs) <- unzip3 <$> forM argsToCheck (\(plic,p0,mToElabInto,a) ->
                 case p0 of
                   Nothing ->
                     do subMToElabInto <- substitute mToElabInto
                        em' <- evaluate subMToElabInto
                        return ( (plic, In (AssertionPat (normTerm em')))
                               , (plic, ElaboratedTerm (normTerm em'))
+                              , []
                               )
                   Just p ->
                     do subMToElabInto <- substitute mToElabInto
                        eMToElabInto <- evaluate subMToElabInto
                        suba <- substitute a
                        ea <- evaluate suba
-                       (p',ElaboratedTerm m') <- checkifyPattern p ea
+                       (p',ElaboratedTerm m',cs) <- checkifyPattern p ea
                        subm' <- substitute m'
                        em' <- evaluate subm'
                        unifyHelper eMToElabInto em'
                        return ( (plic, p')
                               , (plic, ElaboratedTerm (normTerm em'))
+                              , cs
                               )
+                                                 )
      forM_ eqs $ \(l,r) ->
        do subl <- substitute l
           el <- evaluate subl
           subr <- substitute r
           er <- evaluate subr
           unifyHelper el er
-     return $ unzip psms'
+     return (ps',ms',concat cs)
   where
     accArgsToCheck :: [(Plicity,Maybe Pattern,Term,Term)]
                    -> [(Plicity,Scope TermF)]
@@ -852,21 +861,34 @@ checkifyPatternsCaseMotive :: [Pattern]
                            -> CaseMotive
                            -> TypeChecker ([Pattern], ElaboratedTerm)
 checkifyPatternsCaseMotive ps0 (CaseMotive (BindingTelescope ascs bsc)) =
-  do (ps',ms') <- go [] ps0 ascs
+  do (ps',ms',cs) <- go [] ps0 ascs
+     forM_ cs (\(l,r) -> do
+                  subl <- substitute l
+                  el <- evaluate subl
+                  subr <- substitute r
+                  er <- evaluate subr
+                  s <- getElab substitution
+                  unifyHelper el er
+                  s' <- getElab substitution
+                  when (length s /= length s') $
+                    throwError $ "Solving the constraint "
+                    ++ pretty (normTerm el) ++ " == "
+                    ++ pretty (normTerm er) ++ " produced new metavar resolution"
+              )
      return (ps', ElaboratedTerm (instantiate bsc ms'))
   where
     go :: [Term]
        -> [Pattern]
        -> [Scope TermF]
-       -> TypeChecker ([Pattern],[Term])
+       -> TypeChecker ([Pattern],[Term],[(Term,Term)])
     go _ [] [] =
-      return ([],[])
+      return ([],[],[])
     go acc (p:ps) (sc:scs) =
       do subt <- substitute (instantiate sc acc)
          et <- evaluate subt
-         (p',ElaboratedTerm m') <- checkifyPattern p et
-         (ps',ms') <- go (acc ++ [m']) ps scs
-         return (p':ps', m':ms')
+         (p',ElaboratedTerm m',cs) <- checkifyPattern p et
+         (ps',ms',cs') <- go (acc ++ [m']) ps scs
+         return (p':ps', m':ms', cs ++ cs')
     go _ _ _ =
       error $ "The auxiliary function 'go' in 'checkPatternsCaseMotive'"
            ++ " should always have equal number of args for its patterns and"
diff --git a/src/Modular/Unification/TypeChecking.hs b/src/Modular/Unification/TypeChecking.hs
index f36d86e..168571a 100644
--- a/src/Modular/Unification/TypeChecking.hs
+++ b/src/Modular/Unification/TypeChecking.hs
@@ -706,7 +706,7 @@ checkifyCaseMotive (CaseMotive tele) =
 
 checkifyPattern :: Pattern
                 -> NormalTerm
-                -> TypeChecker (Pattern,ElaboratedTerm)
+                -> TypeChecker (Pattern,ElaboratedTerm,[(Term,Term)])
 checkifyPattern (Var (Bound _ _)) _ =
   error "A bound variable should not be the subject of pattern type checking."
 checkifyPattern (Var (Free x)) t =
@@ -714,12 +714,13 @@ checkifyPattern (Var (Free x)) t =
      unifyHelper t (NormalTerm t')  -- @t'@ is guaranteed to be normal
      return ( Var (Free x)
             , ElaboratedTerm (Var (Free x))
+            , []
             )
 checkifyPattern (Var (Meta _)) _ =
   error "Metavariables should not be the subject of pattern type checking."
 checkifyPattern (In (ConPat c ps)) (NormalTerm t) =
   do (ec,ConSig plics (BindingTelescope ascs bsc)) <- typeInSignature c
-     (ps',elms') <-
+     (ps',elms',cs) <-
        checkifyPatterns
          (zip plics ascs)
          bsc
@@ -728,17 +729,21 @@ checkifyPattern (In (ConPat c ps)) (NormalTerm t) =
      let ms' = [ (plic,m') | (plic, ElaboratedTerm m') <- elms' ]
      return ( conPatH ec ps'
             , ElaboratedTerm (conH ec ms')
+            , cs
             )
 checkifyPattern (In (AssertionPat m)) t =
   do ElaboratedTerm m' <- checkify m t
+     mv <- nextElab nextMeta
      return ( In (AssertionPat m')
-            , ElaboratedTerm m'
+            , ElaboratedTerm (Var $ Meta mv)
+            , [(Var $ Meta mv, m')]
             )
 checkifyPattern (In MakeMeta) _ =
   do meta <- nextElab nextMeta
      let x = Var (Meta meta)
      return ( In (AssertionPat x)
             , ElaboratedTerm x
+            , []
             )
 
 
@@ -777,6 +782,7 @@ checkifyPatterns :: [(Plicity,Scope TermF)]
                  -> Term
                  -> TypeChecker ( [(Plicity,Pattern)]
                                 , [(Plicity,ElaboratedTerm)]
+                                , [(Term,Term)]
                                 )
 checkifyPatterns ascs0 bsc ps0 t =
   do argsToCheck <- accArgsToCheck [] ascs0 ps0
@@ -790,33 +796,36 @@ checkifyPatterns ascs0 bsc ps0 t =
               return (eqs,ret')
          ret' -> return ([],ret')
      unifyHelper (NormalTerm ret') (NormalTerm t)
-     psms' <- forM argsToCheck $ \(plic,p0,mToElabInto,a) ->
+     (ps',ms',cs) <- unzip3 <$> forM argsToCheck (\(plic,p0,mToElabInto,a) ->
                 case p0 of
                   Nothing ->
                     do subMToElabInto <- substitute mToElabInto
                        em' <- evaluate subMToElabInto
                        return ( (plic, In (AssertionPat (normTerm em')))
                               , (plic, ElaboratedTerm (normTerm em'))
+                              , []
                               )
                   Just p ->
                     do subMToElabInto <- substitute mToElabInto
                        eMToElabInto <- evaluate subMToElabInto
                        suba <- substitute a
                        ea <- evaluate suba
-                       (p',ElaboratedTerm m') <- checkifyPattern p ea
+                       (p',ElaboratedTerm m',cs) <- checkifyPattern p ea
                        subm' <- substitute m'
                        em' <- evaluate subm'
                        unifyHelper eMToElabInto em'
                        return ( (plic, p')
                               , (plic, ElaboratedTerm (normTerm em'))
+                              , cs
                               )
+                                                 )
      forM_ eqs $ \(l,r) ->
        do subl <- substitute l
           el <- evaluate subl
           subr <- substitute r
           er <- evaluate subr
           unifyHelper el er
-     return $ unzip psms'
+     return (ps',ms',concat cs)
   where
     accArgsToCheck :: [(Plicity,Maybe Pattern,Term,Term)]
                    -> [(Plicity,Scope TermF)]
@@ -888,21 +897,34 @@ checkifyPatternsCaseMotive :: [Pattern]
                            -> CaseMotive
                            -> TypeChecker ([Pattern], ElaboratedTerm)
 checkifyPatternsCaseMotive ps0 (CaseMotive (BindingTelescope ascs bsc)) =
-  do (ps',ms') <- go [] ps0 ascs
+  do (ps',ms',cs) <- go [] ps0 ascs
+     forM_ cs (\(l,r) -> do
+                  subl <- substitute l
+                  el <- evaluate subl
+                  subr <- substitute r
+                  er <- evaluate subr
+                  s <- getElab substitution
+                  unifyHelper el er
+                  s' <- getElab substitution
+                  when (length s /= length s') $
+                    throwError $ "Solving the constraint "
+                    ++ pretty (normTerm el) ++ " == "
+                    ++ pretty (normTerm er) ++ " produced new metavar resolution"
+              )
      return (ps', ElaboratedTerm (instantiate bsc ms'))
   where
     go :: [Term]
        -> [Pattern]
        -> [Scope TermF]
-       -> TypeChecker ([Pattern],[Term])
+       -> TypeChecker ([Pattern],[Term],[(Term,Term)])
     go _ [] [] =
-      return ([],[])
+      return ([],[],[])
     go acc (p:ps) (sc:scs) =
       do subt <- substitute (instantiate sc acc)
          et <- evaluate subt
-         (p',ElaboratedTerm m') <- checkifyPattern p et
-         (ps',ms') <- go (acc ++ [m']) ps scs
-         return (p':ps', m':ms')
+         (p',ElaboratedTerm m',cs) <- checkifyPattern p et
+         (ps',ms',cs') <- go (acc ++ [m']) ps scs
+         return (p':ps', m':ms', cs ++ cs')
     go _ _ _ =
       error $ "The auxiliary function 'go' in 'checkPatternsCaseMotive'"
            ++ " should always have equal number of args for its patterns and"
diff --git a/src/OpenDefs/Unification/TypeChecking.hs b/src/OpenDefs/Unification/TypeChecking.hs
index 00b476b..3080b75 100644
--- a/src/OpenDefs/Unification/TypeChecking.hs
+++ b/src/OpenDefs/Unification/TypeChecking.hs
@@ -802,7 +802,7 @@ checkifyCaseMotive (CaseMotive tele) =
 
 checkifyPattern :: Pattern
                 -> NormalTerm
-                -> TypeChecker (Pattern,ElaboratedTerm)
+                -> TypeChecker (Pattern,ElaboratedTerm,[(Term,Term)])
 checkifyPattern (Var (Bound _ _)) _ =
   error "A bound variable should not be the subject of pattern type checking."
 checkifyPattern (Var (Free x)) t =
@@ -810,12 +810,13 @@ checkifyPattern (Var (Free x)) t =
      unifyHelper t (NormalTerm t')  -- @t'@ is guaranteed to be normal
      return ( Var (Free x)
             , ElaboratedTerm (Var (Free x))
+            , []
             )
 checkifyPattern (Var (Meta _)) _ =
   error "Metavariables should not be the subject of pattern type checking."
 checkifyPattern (In (ConPat c ps)) (NormalTerm t) =
   do (ec,ConSig plics (BindingTelescope ascs bsc)) <- typeInSignature c
-     (ps',elms') <-
+     (ps',elms',cs) <-
        checkifyPatterns
          (zip plics ascs)
          bsc
@@ -824,17 +825,21 @@ checkifyPattern (In (ConPat c ps)) (NormalTerm t) =
      let ms' = [ (plic,m') | (plic, ElaboratedTerm m') <- elms' ]
      return ( conPatH ec ps'
             , ElaboratedTerm (conH ec ms')
+            , cs
             )
 checkifyPattern (In (AssertionPat m)) t =
   do ElaboratedTerm m' <- checkify m t
+     mv <- nextElab nextMeta
      return ( In (AssertionPat m')
-            , ElaboratedTerm m'
+            , ElaboratedTerm (Var $ Meta mv)
+            , [(Var $ Meta mv, m')]
             )
 checkifyPattern (In MakeMeta) _ =
   do meta <- nextElab nextMeta
      let x = Var (Meta meta)
      return ( In (AssertionPat x)
             , ElaboratedTerm x
+            , []
             )
 
 
@@ -873,6 +878,7 @@ checkifyPatterns :: [(Plicity,Scope TermF)]
                  -> Term
                  -> TypeChecker ( [(Plicity,Pattern)]
                                 , [(Plicity,ElaboratedTerm)]
+                                , [(Term,Term)]
                                 )
 checkifyPatterns ascs0 bsc ps0 t =
   do argsToCheck <- accArgsToCheck [] ascs0 ps0
@@ -886,33 +892,36 @@ checkifyPatterns ascs0 bsc ps0 t =
               return (eqs,ret')
          ret' -> return ([],ret')
      unifyHelper (NormalTerm ret') (NormalTerm t)
-     psms' <- forM argsToCheck $ \(plic,p0,mToElabInto,a) ->
+     (ps',ms',cs) <- unzip3 <$> forM argsToCheck (\(plic,p0,mToElabInto,a) ->
                 case p0 of
                   Nothing ->
                     do subMToElabInto <- substitute mToElabInto
                        em' <- evaluate subMToElabInto
                        return ( (plic, In (AssertionPat (normTerm em')))
                               , (plic, ElaboratedTerm (normTerm em'))
+                              , []
                               )
                   Just p ->
                     do subMToElabInto <- substitute mToElabInto
                        eMToElabInto <- evaluate subMToElabInto
                        suba <- substitute a
                        ea <- evaluate suba
-                       (p',ElaboratedTerm m') <- checkifyPattern p ea
+                       (p',ElaboratedTerm m',cs) <- checkifyPattern p ea
                        subm' <- substitute m'
                        em' <- evaluate subm'
                        unifyHelper eMToElabInto em'
                        return ( (plic, p')
                               , (plic, ElaboratedTerm (normTerm em'))
+                              , cs
                               )
+                                                 )
      forM_ eqs $ \(l,r) ->
        do subl <- substitute l
           el <- evaluate subl
           subr <- substitute r
           er <- evaluate subr
           unifyHelper el er
-     return $ unzip psms'
+     return (ps',ms',concat cs)
   where
     accArgsToCheck :: [(Plicity,Maybe Pattern,Term,Term)]
                    -> [(Plicity,Scope TermF)]
@@ -984,21 +993,34 @@ checkifyPatternsCaseMotive :: [Pattern]
                            -> CaseMotive
                            -> TypeChecker ([Pattern], ElaboratedTerm)
 checkifyPatternsCaseMotive ps0 (CaseMotive (BindingTelescope ascs bsc)) =
-  do (ps',ms') <- go [] ps0 ascs
+  do (ps',ms',cs) <- go [] ps0 ascs
+     forM_ cs (\(l,r) -> do
+                  subl <- substitute l
+                  el <- evaluate subl
+                  subr <- substitute r
+                  er <- evaluate subr
+                  s <- getElab substitution
+                  unifyHelper el er
+                  s' <- getElab substitution
+                  when (length s /= length s') $
+                    throwError $ "Solving the constraint "
+                    ++ pretty (normTerm el) ++ " == "
+                    ++ pretty (normTerm er) ++ " produced new metavar resolution"
+              )
      return (ps', ElaboratedTerm (instantiate bsc ms'))
   where
     go :: [Term]
        -> [Pattern]
        -> [Scope TermF]
-       -> TypeChecker ([Pattern],[Term])
+       -> TypeChecker ([Pattern],[Term],[(Term,Term)])
     go _ [] [] =
-      return ([],[])
+      return ([],[],[])
     go acc (p:ps) (sc:scs) =
       do subt <- substitute (instantiate sc acc)
          et <- evaluate subt
-         (p',ElaboratedTerm m') <- checkifyPattern p et
-         (ps',ms') <- go (acc ++ [m']) ps scs
-         return (p':ps', m':ms')
+         (p',ElaboratedTerm m',cs) <- checkifyPattern p et
+         (ps',ms',cs') <- go (acc ++ [m']) ps scs
+         return (p':ps', m':ms', cs ++ cs')
     go _ _ _ =
       error $ "The auxiliary function 'go' in 'checkPatternsCaseMotive'"
            ++ " should always have equal number of args for its patterns and"
diff --git a/src/Quasiquote/Unification/TypeChecking.hs b/src/Quasiquote/Unification/TypeChecking.hs
index 9aecff6..da876ce 100644
--- a/src/Quasiquote/Unification/TypeChecking.hs
+++ b/src/Quasiquote/Unification/TypeChecking.hs
@@ -872,7 +872,7 @@ checkifyCaseMotive (CaseMotive tele) =
 
 checkifyPattern :: Pattern
                 -> NormalTerm
-                -> TypeChecker (Pattern,ElaboratedTerm)
+                -> TypeChecker (Pattern,ElaboratedTerm,[(Term,Term)])
 checkifyPattern (Var (Bound _ _)) _ =
   error "A bound variable should not be the subject of pattern type checking."
 checkifyPattern (Var (Free x)) t =
@@ -880,12 +880,13 @@ checkifyPattern (Var (Free x)) t =
      unifyHelper t (NormalTerm t')  -- @t'@ is guaranteed to be normal
      return ( Var (Free x)
             , ElaboratedTerm (Var (Free x))
+            , []
             )
 checkifyPattern (Var (Meta _)) _ =
   error "Metavariables should not be the subject of pattern type checking."
 checkifyPattern (In (ConPat c ps)) (NormalTerm t) =
   do (ec,ConSig plics (BindingTelescope ascs bsc)) <- typeInSignature c
-     (ps',elms') <-
+     (ps',elms',cs) <-
        checkifyPatterns
          (zip plics ascs)
          bsc
@@ -894,17 +895,21 @@ checkifyPattern (In (ConPat c ps)) (NormalTerm t) =
      let ms' = [ (plic,m') | (plic, ElaboratedTerm m') <- elms' ]
      return ( conPatH ec ps'
             , ElaboratedTerm (conH ec ms')
+            , cs
             )
 checkifyPattern (In (AssertionPat m)) t =
   do ElaboratedTerm m' <- checkify m t
+     mv <- nextElab nextMeta
      return ( In (AssertionPat m')
-            , ElaboratedTerm m'
+            , ElaboratedTerm (Var $ Meta mv)
+            , [(Var $ Meta mv, m')]
             )
 checkifyPattern (In MakeMeta) _ =
   do meta <- nextElab nextMeta
      let x = Var (Meta meta)
      return ( In (AssertionPat x)
             , ElaboratedTerm x
+            , []
             )
 
 
@@ -943,6 +948,7 @@ checkifyPatterns :: [(Plicity,Scope TermF)]
                  -> Term
                  -> TypeChecker ( [(Plicity,Pattern)]
                                 , [(Plicity,ElaboratedTerm)]
+                                , [(Term,Term)]
                                 )
 checkifyPatterns ascs0 bsc ps0 t =
   do argsToCheck <- accArgsToCheck [] ascs0 ps0
@@ -956,33 +962,36 @@ checkifyPatterns ascs0 bsc ps0 t =
               return (eqs,ret')
          ret' -> return ([],ret')
      unifyHelper (NormalTerm ret') (NormalTerm t)
-     psms' <- forM argsToCheck $ \(plic,p0,mToElabInto,a) ->
+     (ps',ms',cs) <- unzip3 <$> forM argsToCheck (\(plic,p0,mToElabInto,a) ->
                 case p0 of
                   Nothing ->
                     do subMToElabInto <- substitute mToElabInto
                        em' <- evaluate subMToElabInto
                        return ( (plic, In (AssertionPat (normTerm em')))
                               , (plic, ElaboratedTerm (normTerm em'))
+                              , []
                               )
                   Just p ->
                     do subMToElabInto <- substitute mToElabInto
                        eMToElabInto <- evaluate subMToElabInto
                        suba <- substitute a
                        ea <- evaluate suba
-                       (p',ElaboratedTerm m') <- checkifyPattern p ea
+                       (p',ElaboratedTerm m',cs) <- checkifyPattern p ea
                        subm' <- substitute m'
                        em' <- evaluate subm'
                        unifyHelper eMToElabInto em'
                        return ( (plic, p')
                               , (plic, ElaboratedTerm (normTerm em'))
+                              , cs
                               )
+                                                 )
      forM_ eqs $ \(l,r) ->
        do subl <- substitute l
           el <- evaluate subl
           subr <- substitute r
           er <- evaluate subr
           unifyHelper el er
-     return $ unzip psms'
+     return (ps',ms',concat cs)
   where
     accArgsToCheck :: [(Plicity,Maybe Pattern,Term,Term)]
                    -> [(Plicity,Scope TermF)]
@@ -1054,21 +1063,34 @@ checkifyPatternsCaseMotive :: [Pattern]
                            -> CaseMotive
                            -> TypeChecker ([Pattern], ElaboratedTerm)
 checkifyPatternsCaseMotive ps0 (CaseMotive (BindingTelescope ascs bsc)) =
-  do (ps',ms') <- go [] ps0 ascs
+  do (ps',ms',cs) <- go [] ps0 ascs
+     forM_ cs (\(l,r) -> do
+                  subl <- substitute l
+                  el <- evaluate subl
+                  subr <- substitute r
+                  er <- evaluate subr
+                  s <- getElab substitution
+                  unifyHelper el er
+                  s' <- getElab substitution
+                  when (length s /= length s') $
+                    throwError $ "Solving the constraint "
+                    ++ pretty (normTerm el) ++ " == "
+                    ++ pretty (normTerm er) ++ " produced new metavar resolution"
+              )
      return (ps', ElaboratedTerm (instantiate bsc ms'))
   where
     go :: [Term]
        -> [Pattern]
        -> [Scope TermF]
-       -> TypeChecker ([Pattern],[Term])
+       -> TypeChecker ([Pattern],[Term],[(Term,Term)])
     go _ [] [] =
-      return ([],[])
+      return ([],[],[])
     go acc (p:ps) (sc:scs) =
       do subt <- substitute (instantiate sc acc)
          et <- evaluate subt
-         (p',ElaboratedTerm m') <- checkifyPattern p et
-         (ps',ms') <- go (acc ++ [m']) ps scs
-         return (p':ps', m':ms')
+         (p',ElaboratedTerm m',cs) <- checkifyPattern p et
+         (ps',ms',cs') <- go (acc ++ [m']) ps scs
+         return (p':ps', m':ms', cs ++ cs')
     go _ _ _ =
       error $ "The auxiliary function 'go' in 'checkPatternsCaseMotive'"
            ++ " should always have equal number of args for its patterns and"
diff --git a/src/Record/Unification/TypeChecking.hs b/src/Record/Unification/TypeChecking.hs
index 89095ff..38b6d4f 100644
--- a/src/Record/Unification/TypeChecking.hs
+++ b/src/Record/Unification/TypeChecking.hs
@@ -802,7 +802,7 @@ checkifyCaseMotive (CaseMotive tele) =
 
 checkifyPattern :: Pattern
                 -> NormalTerm
-                -> TypeChecker (Pattern,ElaboratedTerm)
+                -> TypeChecker (Pattern,ElaboratedTerm,[(Term,Term)])
 checkifyPattern (Var (Bound _ _)) _ =
   error "A bound variable should not be the subject of pattern type checking."
 checkifyPattern (Var (Free x)) t =
@@ -810,12 +810,13 @@ checkifyPattern (Var (Free x)) t =
      unifyHelper t (NormalTerm t')  -- @t'@ is guaranteed to be normal
      return ( Var (Free x)
             , ElaboratedTerm (Var (Free x))
+            , []
             )
 checkifyPattern (Var (Meta _)) _ =
   error "Metavariables should not be the subject of pattern type checking."
 checkifyPattern (In (ConPat c ps)) (NormalTerm t) =
   do (ec,ConSig plics (BindingTelescope ascs bsc)) <- typeInSignature c
-     (ps',elms') <-
+     (ps',elms',cs) <-
        checkifyPatterns
          (zip plics ascs)
          bsc
@@ -824,17 +825,21 @@ checkifyPattern (In (ConPat c ps)) (NormalTerm t) =
      let ms' = [ (plic,m') | (plic, ElaboratedTerm m') <- elms' ]
      return ( conPatH ec ps'
             , ElaboratedTerm (conH ec ms')
+            , cs
             )
 checkifyPattern (In (AssertionPat m)) t =
   do ElaboratedTerm m' <- checkify m t
+     mv <- nextElab nextMeta
      return ( In (AssertionPat m')
-            , ElaboratedTerm m'
+            , ElaboratedTerm (Var $ Meta mv)
+            , [(Var $ Meta mv, m')]
             )
 checkifyPattern (In MakeMeta) _ =
   do meta <- nextElab nextMeta
      let x = Var (Meta meta)
      return ( In (AssertionPat x)
             , ElaboratedTerm x
+            , []
             )
 
 
@@ -873,6 +878,7 @@ checkifyPatterns :: [(Plicity,Scope TermF)]
                  -> Term
                  -> TypeChecker ( [(Plicity,Pattern)]
                                 , [(Plicity,ElaboratedTerm)]
+                                , [(Term,Term)]
                                 )
 checkifyPatterns ascs0 bsc ps0 t =
   do argsToCheck <- accArgsToCheck [] ascs0 ps0
@@ -886,33 +892,36 @@ checkifyPatterns ascs0 bsc ps0 t =
               return (eqs,ret')
          ret' -> return ([],ret')
      unifyHelper (NormalTerm ret') (NormalTerm t)
-     psms' <- forM argsToCheck $ \(plic,p0,mToElabInto,a) ->
+     (ps',ms',cs) <- unzip3 <$> forM argsToCheck (\(plic,p0,mToElabInto,a) ->
                 case p0 of
                   Nothing ->
                     do subMToElabInto <- substitute mToElabInto
                        em' <- evaluate subMToElabInto
                        return ( (plic, In (AssertionPat (normTerm em')))
                               , (plic, ElaboratedTerm (normTerm em'))
+                              , []
                               )
                   Just p ->
                     do subMToElabInto <- substitute mToElabInto
                        eMToElabInto <- evaluate subMToElabInto
                        suba <- substitute a
                        ea <- evaluate suba
-                       (p',ElaboratedTerm m') <- checkifyPattern p ea
+                       (p',ElaboratedTerm m',cs) <- checkifyPattern p ea
                        subm' <- substitute m'
                        em' <- evaluate subm'
                        unifyHelper eMToElabInto em'
                        return ( (plic, p')
                               , (plic, ElaboratedTerm (normTerm em'))
+                              , cs
                               )
+                                          )
      forM_ eqs $ \(l,r) ->
        do subl <- substitute l
           el <- evaluate subl
           subr <- substitute r
           er <- evaluate subr
           unifyHelper el er
-     return $ unzip psms'
+     return (ps',ms',concat cs)
   where
     accArgsToCheck :: [(Plicity,Maybe Pattern,Term,Term)]
                    -> [(Plicity,Scope TermF)]
@@ -984,21 +993,34 @@ checkifyPatternsCaseMotive :: [Pattern]
                            -> CaseMotive
                            -> TypeChecker ([Pattern], ElaboratedTerm)
 checkifyPatternsCaseMotive ps0 (CaseMotive (BindingTelescope ascs bsc)) =
-  do (ps',ms') <- go [] ps0 ascs
+  do (ps',ms',cs) <- go [] ps0 ascs
+     forM_ cs (\(l,r) -> do
+                  subl <- substitute l
+                  el <- evaluate subl
+                  subr <- substitute r
+                  er <- evaluate subr
+                  s <- getElab substitution
+                  unifyHelper el er
+                  s' <- getElab substitution
+                  when (length s /= length s') $
+                    throwError $ "Solving the constraint "
+                    ++ pretty (normTerm el) ++ " == "
+                    ++ pretty (normTerm er) ++ " produced new metavar resolution"
+              )
      return (ps', ElaboratedTerm (instantiate bsc ms'))
   where
     go :: [Term]
        -> [Pattern]
        -> [Scope TermF]
-       -> TypeChecker ([Pattern],[Term])
+       -> TypeChecker ([Pattern],[Term],[(Term,Term)])
     go _ [] [] =
-      return ([],[])
+      return ([],[],[])
     go acc (p:ps) (sc:scs) =
       do subt <- substitute (instantiate sc acc)
          et <- evaluate subt
-         (p',ElaboratedTerm m') <- checkifyPattern p et
-         (ps',ms') <- go (acc ++ [m']) ps scs
-         return (p':ps', m':ms')
+         (p',ElaboratedTerm m',cs) <- checkifyPattern p et
+         (ps',ms',cs') <- go (acc ++ [m']) ps scs
+         return (p':ps', m':ms', cs ++ cs')
     go _ _ _ =
       error $ "The auxiliary function 'go' in 'checkPatternsCaseMotive'"
            ++ " should always have equal number of args for its patterns and"
diff --git a/src/Require/Unification/TypeChecking.hs b/src/Require/Unification/TypeChecking.hs
index 9f9ab1a..b4eff03 100644
--- a/src/Require/Unification/TypeChecking.hs
+++ b/src/Require/Unification/TypeChecking.hs
@@ -995,7 +995,7 @@ checkifyCaseMotive (CaseMotive tele) =
 
 checkifyPattern :: Pattern
                 -> NormalTerm
-                -> TypeChecker (Pattern,ElaboratedTerm)
+                -> TypeChecker (Pattern,ElaboratedTerm,[(Term,Term)])
 checkifyPattern (Var (Bound _ _)) _ =
   error "A bound variable should not be the subject of pattern type checking."
 checkifyPattern (Var (Free x)) t =
@@ -1003,12 +1003,13 @@ checkifyPattern (Var (Free x)) t =
      unifyHelper t (NormalTerm t')  -- @t'@ is guaranteed to be normal
      return ( Var (Free x)
             , ElaboratedTerm (Var (Free x))
+            , []
             )
 checkifyPattern (Var (Meta _)) _ =
   error "Metavariables should not be the subject of pattern type checking."
 checkifyPattern (In (ConPat c ps)) (NormalTerm t) =
   do (ec,ConSig plics (BindingTelescope ascs bsc)) <- typeInSignature c
-     (ps',elms') <-
+     (ps',elms',cs) <-
        checkifyPatterns
          (zip plics ascs)
          bsc
@@ -1017,17 +1018,21 @@ checkifyPattern (In (ConPat c ps)) (NormalTerm t) =
      let ms' = [ (plic,m') | (plic, ElaboratedTerm m') <- elms' ]
      return ( conPatH ec ps'
             , ElaboratedTerm (conH ec ms')
+            , cs
             )
 checkifyPattern (In (AssertionPat m)) t =
   do ElaboratedTerm m' <- checkify m t
+     mv <- nextElab nextMeta
      return ( In (AssertionPat m')
-            , ElaboratedTerm m'
+            , ElaboratedTerm (Var $ Meta mv)
+            , [(Var $ Meta mv, m')]
             )
 checkifyPattern (In MakeMeta) _ =
   do meta <- nextElab nextMeta
      let x = Var (Meta meta)
      return ( In (AssertionPat x)
             , ElaboratedTerm x
+            , []
             )
 
 
@@ -1066,6 +1071,7 @@ checkifyPatterns :: [(Plicity,Scope TermF)]
                  -> Term
                  -> TypeChecker ( [(Plicity,Pattern)]
                                 , [(Plicity,ElaboratedTerm)]
+                                , [(Term,Term)]
                                 )
 checkifyPatterns ascs0 bsc ps0 t =
   do argsToCheck <- accArgsToCheck [] ascs0 ps0
@@ -1079,33 +1085,36 @@ checkifyPatterns ascs0 bsc ps0 t =
               return (eqs,ret')
          ret' -> return ([],ret')
      unifyHelper (NormalTerm ret') (NormalTerm t)
-     psms' <- forM argsToCheck $ \(plic,p0,mToElabInto,a) ->
+     (ps',ms',cs) <- unzip3 <$> forM argsToCheck (\(plic,p0,mToElabInto,a) ->
                 case p0 of
                   Nothing ->
                     do subMToElabInto <- substitute mToElabInto
                        em' <- evaluate subMToElabInto
                        return ( (plic, In (AssertionPat (normTerm em')))
                               , (plic, ElaboratedTerm (normTerm em'))
+                              , []
                               )
                   Just p ->
                     do subMToElabInto <- substitute mToElabInto
                        eMToElabInto <- evaluate subMToElabInto
                        suba <- substitute a
                        ea <- evaluate suba
-                       (p',ElaboratedTerm m') <- checkifyPattern p ea
+                       (p',ElaboratedTerm m',cs) <- checkifyPattern p ea
                        subm' <- substitute m'
                        em' <- evaluate subm'
                        unifyHelper eMToElabInto em'
                        return ( (plic, p')
                               , (plic, ElaboratedTerm (normTerm em'))
+                              , cs
                               )
+                                                )
      forM_ eqs $ \(l,r) ->
        do subl <- substitute l
           el <- evaluate subl
           subr <- substitute r
           er <- evaluate subr
           unifyHelper el er
-     return $ unzip psms'
+     return (ps',ms',concat cs)
   where
     accArgsToCheck :: [(Plicity,Maybe Pattern,Term,Term)]
                    -> [(Plicity,Scope TermF)]
@@ -1177,21 +1186,34 @@ checkifyPatternsCaseMotive :: [Pattern]
                            -> CaseMotive
                            -> TypeChecker ([Pattern], ElaboratedTerm)
 checkifyPatternsCaseMotive ps0 (CaseMotive (BindingTelescope ascs bsc)) =
-  do (ps',ms') <- go [] ps0 ascs
+  do (ps',ms',cs) <- go [] ps0 ascs
+     forM_ cs (\(l,r) -> do
+                  subl <- substitute l
+                  el <- evaluate subl
+                  subr <- substitute r
+                  er <- evaluate subr
+                  s <- getElab substitution
+                  unifyHelper el er
+                  s' <- getElab substitution
+                  when (length s /= length s') $
+                    throwError $ "Solving the constraint "
+                    ++ pretty (normTerm el) ++ " == "
+                    ++ pretty (normTerm er) ++ " produced new metavar resolution"
+              )
      return (ps', ElaboratedTerm (instantiate bsc ms'))
   where
     go :: [Term]
        -> [Pattern]
        -> [Scope TermF]
-       -> TypeChecker ([Pattern],[Term])
+       -> TypeChecker ([Pattern],[Term],[(Term,Term)])
     go _ [] [] =
-      return ([],[])
+      return ([],[],[])
     go acc (p:ps) (sc:scs) =
       do subt <- substitute (instantiate sc acc)
          et <- evaluate subt
-         (p',ElaboratedTerm m') <- checkifyPattern p et
-         (ps',ms') <- go (acc ++ [m']) ps scs
-         return (p':ps', m':ms')
+         (p',ElaboratedTerm m',cs) <- checkifyPattern p et
+         (ps',ms',cs') <- go (acc ++ [m']) ps scs
+         return (p':ps', m':ms', cs ++ cs')
     go _ _ _ =
       error $ "The auxiliary function 'go' in 'checkPatternsCaseMotive'"
            ++ " should always have equal number of args for its patterns and"

From 290c9863c021fc0d4782bb7d9f9225db0cb3f2e1 Mon Sep 17 00:00:00 2001
From: Ilya Yanok <ilya.yanok@gmail.com>
Date: Fri, 2 Jun 2017 19:48:24 +0200
Subject: [PATCH 6/6] unification: change the way unification works

This patch does the following:
 1. Now we have two types of meta variables: Exist and Constraint, the
 first to be used to find implicit arguments and stuff like that, while
 the second to be used for solving assertion pattern constraints. They
 need to be handled differently during the unification process: for
 example, it's absolutely legal (and desirable) to instantiate ?meta to
 'x' while unifying 'f x' with 'f ?meta' if ?meta is existential (stands
 for implicit argument and stuff like that), but it would lead to
 undesirable results (like proving injectivity for arbitrary function)
 if ?meta comes from the checking of an assertion pattern.

 2. Equation constructor now gets an extra Bool argument. It essentially
 signals if this equation is good for both constraints and existentials
 or only for existentials.
 3. equate method also gets an extra Bool argument representing if
 current context is ok to solve constraints or only to pick
 existentials. There are really only two reasonable two to handle this
 argument in the equate implementation:
   - pass it to the subsequent Equations if this language construct is
     injective
   - ignore it and set subsequent Equations flag to False if the
     language construct is not guaranteed to be injective (like function
     application or record projections)

 3. Fix all the variant to compile with the new code. Function
 applications, case, record projections and all
 quote/continuations/require stuff are made only for existentials (the
 latter triple is here mostly because I'm not sure about them and it's
 always safe to be conservative).

This fixes the problem with proving arbitrary functions injectivity
everywhere except the Dependent.Monadic variant.
---
 src/Continuations/Unification/TypeChecking.hs | 42 +++++-----
 src/Continuations/Unification/Unification.hs  | 78 ++++++++---------
 src/Dependent/Monadic/TypeChecking.hs         |  4 +-
 src/Dependent/Unification/TypeChecking.hs     |  8 +-
 src/Dependent/Unification/Unification.hs      | 42 +++++-----
 .../Unification/TypeChecking.hs               | 42 +++++-----
 .../Unification/Unification.hs                | 42 +++++-----
 src/Modular/Unification/TypeChecking.hs       | 42 +++++-----
 src/Modular/Unification/Unification.hs        | 42 +++++-----
 src/OpenDefs/Unification/TypeChecking.hs      | 42 +++++-----
 src/OpenDefs/Unification/Unification.hs       | 54 ++++++------
 src/Poly/Unification/TypeChecking.hs          | 16 ++--
 src/Poly/Unification/Unification.hs           | 18 ++--
 src/Quasiquote/Unification/TypeChecking.hs    | 42 +++++-----
 src/Quasiquote/Unification/Unification.hs     | 66 +++++++--------
 src/Record/Unification/TypeChecking.hs        | 42 +++++-----
 src/Record/Unification/Unification.hs         | 54 ++++++------
 src/Require/Unification/TypeChecking.hs       | 42 +++++-----
 src/Require/Unification/Unification.hs        | 84 +++++++++----------
 src/Simple/Monadic/TypeChecking.hs            |  4 +-
 src/Simple/Unification/TypeChecking.hs        |  8 +-
 src/Simple/Unification/Unification.hs         | 12 +--
 src/Utils/ABT.hs                              | 16 ++--
 src/Utils/Unifier.hs                          | 42 ++++++----
 24 files changed, 447 insertions(+), 437 deletions(-)

diff --git a/src/Continuations/Unification/TypeChecking.hs b/src/Continuations/Unification/TypeChecking.hs
index 6ef08e4..ec0a333 100644
--- a/src/Continuations/Unification/TypeChecking.hs
+++ b/src/Continuations/Unification/TypeChecking.hs
@@ -344,7 +344,7 @@ inferify (Var (Free x)) =
      return (ElaboratedTerm (Var (Free x)), t)
 inferify (Var (Bound _ _)) =
   error "Bound type variables should not be the subject of type checking."
-inferify (Var (Meta x)) =
+inferify (Var (Meta _ x)) =
   throwError $ "The metavariable " ++ show x
             ++ " appears in checkable code, when it should not."
 inferify (In (Defined x)) =
@@ -550,8 +550,8 @@ inferifyApplication f (In (Fun Expl _ _)) Impl m =
     ++ pretty (appH Impl f m)
 inferifyApplication f (In (Fun Impl _ sc)) Expl m =
   do meta <- nextElab nextMeta
-     let f' = appH Impl f (Var (Meta meta))
-         t' = instantiate sc [Var (Meta meta)]
+     let f' = appH Impl f (Var (Meta Exist meta))
+         t' = instantiate sc [Var (Meta Exist meta)]
      inferifyApplication  f' t' Expl m
 inferifyApplication f _ _ _ =
   throwError $ "Cannot apply non-function: " ++ pretty f
@@ -608,7 +608,7 @@ inferifyConArgs ascs0 bsc0 ms0 = go [] ascs0 bsc0 ms0
          go (acc ++ [(Impl,m')]) ascs bsc ms
     go acc ((Impl,_):ascs) bsc ms =
       do meta <- nextElab nextMeta
-         go (acc ++ [(Impl,Var (Meta meta))]) ascs bsc ms
+         go (acc ++ [(Impl,Var (Meta Exist meta))]) ascs bsc ms
     go _ _ _ _ =
       throwError "Cannot match signature."
 
@@ -886,7 +886,7 @@ checkifyConArgs ascs0 bsc ms0 t =
       return acc
     accArgsToCheck acc ((Expl,asc):ascs) ((Expl,m):ms) =
       do meta <- nextElab nextMeta
-         let x = Var (Meta meta)
+         let x = Var (Meta Exist meta)
              xs = [ x' | (_,_,x',_) <- acc ]
              newSuspension = (Expl, Just m, x, instantiate asc xs)
          accArgsToCheck
@@ -895,7 +895,7 @@ checkifyConArgs ascs0 bsc ms0 t =
            ms
     accArgsToCheck acc ((Impl,asc):ascs) ((Impl,m):ms) =
       do meta <- nextElab nextMeta
-         let x = Var (Meta meta)
+         let x = Var (Meta Exist meta)
              xs = [ x' | (_,_,x',_) <- acc ]
              newSuspension = (Impl, Just m, x, instantiate asc xs)
          accArgsToCheck
@@ -904,7 +904,7 @@ checkifyConArgs ascs0 bsc ms0 t =
            ms
     accArgsToCheck acc ((Impl,asc):ascs) ms =
       do meta <- nextElab nextMeta
-         let x = Var (Meta meta)
+         let x = Var (Meta Exist meta)
              xs = [ x' | (_,_,x',_) <- acc ]
              newSuspension = (Impl, Nothing, x, instantiate asc xs)
          accArgsToCheck
@@ -917,12 +917,12 @@ checkifyConArgs ascs0 bsc ms0 t =
     swapMetas :: [(Plicity,Term)]
               -> TypeChecker ([(Term,Term)], [(Plicity,Term)])
     swapMetas [] = return ([],[])
-    swapMetas ((plic, Var (Meta meta)):ms) =
+    swapMetas ((plic, Var (Meta Exist meta)):ms) =
       do (eqs,ms') <- swapMetas ms
-         return (eqs, (plic,Var (Meta meta)):ms')
+         return (eqs, (plic,Var (Meta Exist meta)):ms')
     swapMetas ((plic,m):ms) =
       do meta <- nextElab nextMeta
-         let x = Var (Meta meta)
+         let x = Var (Meta Exist meta)
          (eqs,ms') <- swapMetas ms
          return ((x,m):eqs, (plic,x):ms')
      
@@ -988,7 +988,7 @@ checkifyPattern (Var (Free x)) t =
             , ElaboratedTerm (Var (Free x))
             , []
             )
-checkifyPattern (Var (Meta _)) _ =
+checkifyPattern (Var (Meta _ _)) _ =
   error "Metavariables should not be the subject of pattern type checking."
 checkifyPattern (In (ConPat c ps)) (NormalTerm t) =
   do (ec,ConSig plics (BindingTelescope ascs bsc)) <- typeInSignature c
@@ -1007,12 +1007,12 @@ checkifyPattern (In (AssertionPat m)) t =
   do ElaboratedTerm m' <- checkify m t
      mv <- nextElab nextMeta
      return ( In (AssertionPat m')
-            , ElaboratedTerm (Var $ Meta mv)
-            , [(Var $ Meta mv, m')]
+            , ElaboratedTerm (Var $ Meta Constraint mv)
+            , [(Var $ Meta Constraint mv, m')]
             )
 checkifyPattern (In MakeMeta) _ =
   do meta <- nextElab nextMeta
-     let x = Var (Meta meta)
+     let x = Var (Meta Exist meta)
      return ( In (AssertionPat x)
             , ElaboratedTerm x
             , []
@@ -1107,7 +1107,7 @@ checkifyPatterns ascs0 bsc ps0 t =
       return acc
     accArgsToCheck acc ((Expl,asc):ascs) ((Expl,p):ps) =
       do meta <- nextElab nextMeta
-         let x = Var (Meta meta)
+         let x = Var (Meta Exist meta)
              xs = [ x' | (_,_,x',_) <- acc ]
              newSuspension = (Expl, Just p, x, instantiate asc xs)
          accArgsToCheck
@@ -1116,7 +1116,7 @@ checkifyPatterns ascs0 bsc ps0 t =
            ps
     accArgsToCheck acc ((Impl,asc):ascs) ((Impl,p):ps) =
       do meta <- nextElab nextMeta
-         let x = Var (Meta meta)
+         let x = Var (Meta Exist meta)
              xs = [ x' | (_,_,x',_) <- acc ]
              newSuspension = (Impl, Just p, x, instantiate asc xs)
          accArgsToCheck
@@ -1125,7 +1125,7 @@ checkifyPatterns ascs0 bsc ps0 t =
            ps
     accArgsToCheck acc ((Impl,asc):ascs) ps =
       do meta <- nextElab nextMeta
-         let x = Var (Meta meta)
+         let x = Var (Meta Exist meta)
              xs = [ x' | (_,_,x',_) <- acc ]
              newSuspension = (Impl, Nothing, x, instantiate asc xs)
          accArgsToCheck
@@ -1138,12 +1138,12 @@ checkifyPatterns ascs0 bsc ps0 t =
     swapMetas :: [(Plicity,Term)]
               -> TypeChecker ([(Term,Term)], [(Plicity,Term)])
     swapMetas [] = return ([],[])
-    swapMetas ((plic, Var (Meta meta)):ms) =
+    swapMetas ((plic, Var (Meta Exist meta)):ms) =
       do (eqs,ms') <- swapMetas ms
-         return (eqs, (plic,Var (Meta meta)):ms')
+         return (eqs, (plic,Var (Meta Exist meta)):ms')
     swapMetas ((plic,m):ms) =
       do meta <- nextElab nextMeta
-         let x = Var (Meta meta)
+         let x = Var (Meta Exist meta)
          (eqs,ms') <- swapMetas ms
          return ((x,m):eqs, (plic,x):ms')
 
@@ -1230,7 +1230,7 @@ checkifyClause (Clause pscs sc) mot@(CaseMotive (BindingTelescope ascs _)) =
      l <- getElab quoteLevel
      ctx' <- forM ns $ \n ->
                do m <- nextElab nextMeta
-                  return (n, QLJ (Var (Meta m)) l)
+                  return (n, QLJ (Var (Meta Exist m)) l)
      extendElab context ctx' $
        do (ps',ElaboratedTerm ret) <-
             checkifyPatternsCaseMotive
diff --git a/src/Continuations/Unification/Unification.hs b/src/Continuations/Unification/Unification.hs
index a08ffbc..42e77b3 100644
--- a/src/Continuations/Unification/Unification.hs
+++ b/src/Continuations/Unification/Unification.hs
@@ -35,44 +35,44 @@ import Control.Monad.Except
 -- | Equating terms by trivial structural equations.
 
 instance MonadUnify TermF Elaborator where
-  equate (Defined n1) (Defined n2) =
+  equate _ (Defined n1) (Defined n2) =
     if n1 == n2
        then return []
        else throwError $ "Mismatching names "
                          ++ showName n1 ++ " and " ++ showName n2
-  equate (Ann m1 t1) (Ann m2 t2) =
-    return [ Equation (instantiate0 m1) (instantiate0 m2)
-           , Equation (instantiate0 t1) (instantiate0 t2)
+  equate f (Ann m1 t1) (Ann m2 t2) =
+    return [ Equation f (instantiate0 m1) (instantiate0 m2)
+           , Equation f (instantiate0 t1) (instantiate0 t2)
            ]
-  equate Type Type =
+  equate _ Type Type =
     return []
-  equate (Fun plic1 a1 sc1) (Fun plic2 a2 sc2) =
+  equate f (Fun plic1 a1 sc1) (Fun plic2 a2 sc2) =
     do unless (plic1 == plic2)
          $ throwError $ "Mismatching plicities when unifying "
              ++ pretty (In (Fun plic1 a1 sc1)) ++ " with "
              ++ pretty (In (Fun plic2 a2 sc2))
        ns <- freshRelTo (names sc1) context
        let xs = map (Var . Free) ns
-       return [ Equation (instantiate0 a1) (instantiate0 a2)
-              , Equation (instantiate sc1 xs) (instantiate sc2 xs)
+       return [ Equation f (instantiate0 a1) (instantiate0 a2)
+              , Equation f (instantiate sc1 xs) (instantiate sc2 xs)
               ]
-  equate (Lam plic1 sc1) (Lam plic2 sc2) =
+  equate f (Lam plic1 sc1) (Lam plic2 sc2) =
     do unless (plic1 == plic2)
          $ throwError $ "Mismatching plicities when unifying "
              ++ pretty (In (Lam plic1 sc1)) ++ " with "
              ++ pretty (In (Lam plic2 sc2))
        ns <- freshRelTo (names sc1) context
        let xs = map (Var . Free) ns
-       return [ Equation (instantiate sc1 xs) (instantiate sc2 xs) ]
-  equate (App plic1 f1 a1) (App plic2 f2 a2) =
+       return [ Equation f (instantiate sc1 xs) (instantiate sc2 xs) ]
+  equate _ (App plic1 f1 a1) (App plic2 f2 a2) =
     do unless (plic1 == plic2)
          $ throwError $ "Mismatching plicities when unifying "
              ++ pretty (In (App plic1 f1 a1)) ++ " with "
              ++ pretty (In (App plic2 f2 a2))
-       return [ Equation (instantiate0 f1) (instantiate0 f2)
-              , Equation (instantiate0 a1) (instantiate0 a2)
+       return [ Equation False (instantiate0 f1) (instantiate0 f2)
+              , Equation False (instantiate0 a1) (instantiate0 a2)
               ]
-  equate (Con c1 as1) (Con c2 as2) =
+  equate f (Con c1 as1) (Con c2 as2) =
     do unless (c1 == c2)
          $ throwError $ "Mismatching constructors "
                      ++ showName c1 ++ " and " ++ showName c2
@@ -87,10 +87,10 @@ instance MonadUnify TermF Elaborator where
              ++ pretty (In (Con c1 as1)) ++ " with "
              ++ pretty (In (Con c2 as2))
        return $ zipWith
-                  Equation
+                  (Equation f)
                   (map instantiate0 as1')
                   (map instantiate0 as2')
-  equate (Case as1 mot1 cs1) (Case as2 mot2 cs2) =
+  equate _ (Case as1 mot1 cs1) (Case as2 mot2 cs2) =
     do unless (length as1 == length as2)
          $ throwError $ "Mismatching number of case arguments in "
                      ++ pretty (In (Case as1 mot1 cs1)) ++ " and "
@@ -100,13 +100,13 @@ instance MonadUnify TermF Elaborator where
                      ++ pretty (In (Case as1 mot1 cs1)) ++ " and "
                      ++ pretty (In (Case as2 mot2 cs2))
        let argEqs = zipWith
-                      Equation
+                      (Equation False)
                         (map instantiate0 as1)
                         (map instantiate0 as2)
        motEqs <- equateCaseMotive mot1 mot2
        clauseEqs <- fmap concat $ zipWithM equateClause cs1 cs2
        return $ argEqs ++ motEqs ++ clauseEqs
-  equate (RecordType fields1 tele1) (RecordType fields2 tele2) =
+  equate f (RecordType fields1 tele1) (RecordType fields2 tele2) =
     do unless (fields1 == fields2)
          $ throwError $ "Record types have different field names: "
              ++ pretty (In (RecordType fields1 tele1))
@@ -121,8 +121,8 @@ instance MonadUnify TermF Elaborator where
              ++ pretty (In (RecordType fields1 tele1))
              ++ " and "
              ++ pretty (In (RecordType fields2 tele2))
-       return $ zipWith Equation as1 as2
-  equate (RecordCon fields1) (RecordCon fields2) =
+       return $ zipWith (Equation f) as1 as2
+  equate f (RecordCon fields1) (RecordCon fields2) =
     do unless (length fields1 == length fields2)
          $ throwError $ "Records have different number of fields: "
              ++ pretty (In (RecordCon fields1))
@@ -136,38 +136,38 @@ instance MonadUnify TermF Elaborator where
              ++ " and "
              ++ pretty (In (RecordCon fields2))
        return $ zipWith
-                  Equation
+                  (Equation f)
                   (map instantiate0 ms1)
                   (map instantiate0 ms2)
-  equate (RecordProj r1 x1) (RecordProj r2 x2) =
+  equate _ (RecordProj r1 x1) (RecordProj r2 x2) =
     do unless (x1 == x2)
          $ throwError $ "Record projections have different names: "
              ++ pretty (In (RecordProj r1 x1))
              ++ " and "
              ++ pretty (In (RecordProj r2 x2))
-       return [Equation (instantiate0 r1) (instantiate0 r2)]
-  equate (QuotedType res1 a1) (QuotedType res2 a2) =
+       return [Equation False (instantiate0 r1) (instantiate0 r2)]
+  equate _ (QuotedType res1 a1) (QuotedType res2 a2) =
     do unless (res1 == res2)
          $ throwError $ "Quoted types have different reset locations: "
              ++ pretty (In (QuotedType res1 a1))
              ++ " and "
              ++ pretty (In (QuotedType res2 a2))
-       return [Equation (instantiate0 a1) (instantiate0 a2)]
-  equate (Quote m1) (Quote m2) =
-    return [Equation (instantiate0 m1) (instantiate0 m2)]
-  equate (Unquote m1) (Unquote m2) =
-    return [Equation (instantiate0 m1) (instantiate0 m2)]
-  equate (Continue m1) (Continue m2) =
-    return [Equation (instantiate0 m1) (instantiate0 m2)]
-  equate (Shift res1 m1) (Shift res2 m2) =
+       return [Equation False (instantiate0 a1) (instantiate0 a2)]
+  equate _ (Quote m1) (Quote m2) =
+    return [Equation False (instantiate0 m1) (instantiate0 m2)]
+  equate _ (Unquote m1) (Unquote m2) =
+    return [Equation False (instantiate0 m1) (instantiate0 m2)]
+  equate _ (Continue m1) (Continue m2) =
+    return [Equation False (instantiate0 m1) (instantiate0 m2)]
+  equate _ (Shift res1 m1) (Shift res2 m2) =
     do unless (res1 == res2)
          $ throwError "Shifts have different reset locations."
-       return [Equation (instantiate0 m1) (instantiate0 m2)]
-  equate (Reset res1 m1) (Reset res2 m2) =
+       return [Equation False (instantiate0 m1) (instantiate0 m2)]
+  equate _ (Reset res1 m1) (Reset res2 m2) =
     do unless (res1 == res2)
          $ throwError "Resets have different reset locations."
-       return [Equation (instantiate0 m1) (instantiate0 m2)]
-  equate l r =
+       return [Equation False (instantiate0 m1) (instantiate0 m2)]
+  equate _ l r =
     throwError $ "Cannot unify " ++ pretty (In l) ++ " with " ++ pretty (In r)
 
 
@@ -185,7 +185,7 @@ equateCaseMotive mot1@(CaseMotive tele1) mot2@(CaseMotive tele2) =
      unless (length as1 == length as2)
        $ throwError $ "Motives not equal: " ++ pretty mot1 ++ " and "
                    ++ pretty mot2
-     return $ zipWith Equation as1 as2 ++ [ Equation b1 b2 ]
+     return $ zipWith (Equation False) as1 as2 ++ [ Equation False b1 b2 ]
      
 
 
@@ -210,5 +210,5 @@ equateClause (Clause pscs1 sc1) (Clause pscs2 sc2) =
        Nothing ->
          throwError "Patterns are not equal."
        Just pEqss ->
-         return $ [ Equation a1 a2 | (a1,a2) <- concat pEqss ]
-               ++ [ Equation b1 b2 ]
\ No newline at end of file
+         return $ [ Equation False a1 a2 | (a1,a2) <- concat pEqss ]
+               ++ [ Equation False b1 b2 ]
diff --git a/src/Dependent/Monadic/TypeChecking.hs b/src/Dependent/Monadic/TypeChecking.hs
index f9ec010..ab6781e 100644
--- a/src/Dependent/Monadic/TypeChecking.hs
+++ b/src/Dependent/Monadic/TypeChecking.hs
@@ -140,7 +140,7 @@ infer (Var (Bound _ _)) =
   error "A bound variable should never be the subject of type inference."
 infer (Var (Free x)) =
   typeInContext x
-infer (Var (Meta _)) =
+infer (Var (Meta _ _)) =
   error "Meta variables should not exist in this type checker."
 infer (In (Defined x)) =
   typeInDefinitions x
@@ -309,7 +309,7 @@ checkPattern (Var (Free x)) (NormalTerm t) =
          , Var (Free x)
          , []
          )
-checkPattern (Var (Meta _)) _ =
+checkPattern (Var (Meta _ _)) _ =
   error "Metavariables should not occur in this type checker."
 checkPattern (In (ConPat _ _)) (NormalTerm (In Type)) =
   throwError "Cannot pattern match on a type."
diff --git a/src/Dependent/Unification/TypeChecking.hs b/src/Dependent/Unification/TypeChecking.hs
index eeb02f4..20da8cf 100644
--- a/src/Dependent/Unification/TypeChecking.hs
+++ b/src/Dependent/Unification/TypeChecking.hs
@@ -163,7 +163,7 @@ inferify (Var (Free x)) =
      return  t
 inferify (Var (Bound _ _)) =
   error "Bound type variables should not be the subject of type checking."
-inferify (Var (Meta x)) =
+inferify (Var (Meta _ x)) =
   throwError $ "The metavariable " ++ show x
             ++ " appears in checkable code, when it should not."
 inferify (In (Defined x)) =
@@ -326,7 +326,7 @@ checkifyPattern (Var (Free x)) t =
   do t' <- typeInContext x
      unifyHelper t (NormalTerm t')  -- @t'@ is guaranteed to be normal
      return (Var (Free x), [])
-checkifyPattern (Var (Meta _)) _ =
+checkifyPattern (Var (Meta _ _)) _ =
   error "Metavariables should not be the subject of pattern type checking."
 checkifyPattern (In (ConPat c ps)) t =
   do consig@(ConSig (BindingTelescope ascs _)) <- typeInSignature c
@@ -344,7 +344,7 @@ checkifyPattern (In (ConPat c ps)) t =
 checkifyPattern (In (AssertionPat m)) t =
   do checkify m t
      mv <- nextElab nextMeta
-     return (Var $ Meta mv, [(Var $ Meta mv, m)])
+     return (Var $ Meta Constraint mv, [(Var $ Meta Constraint mv, m)])
 
 
 
@@ -465,7 +465,7 @@ checkifyClause (Clause pscs sc) mot@(CaseMotive (BindingTelescope ascs _)) =
          xs2 = map (Var . Free) ns
      ctx' <- forM ns $ \n ->
                do m <- nextElab nextMeta
-                  return (n, Var (Meta m))
+                  return (n, Var (Meta Exist m))
      extendElab context ctx' $
        do ret <- checkifyPatternsCaseMotive
                    (map (\psc -> patternInstantiate psc xs1 xs2)
diff --git a/src/Dependent/Unification/Unification.hs b/src/Dependent/Unification/Unification.hs
index e647a4a..147607d 100644
--- a/src/Dependent/Unification/Unification.hs
+++ b/src/Dependent/Unification/Unification.hs
@@ -34,31 +34,31 @@ import Control.Monad.Except
 -- | Equating terms by trivial structural equations.
 
 instance MonadUnify TermF Elaborator where
-  equate (Defined n1) (Defined n2) =
+  equate _ (Defined n1) (Defined n2) =
     if n1 == n2
        then return []
        else throwError $ "Mismatching names " ++ n1 ++ " and " ++ n2
-  equate (Ann m1 t1) (Ann m2 t2) =
-    return [ Equation (instantiate0 m1) (instantiate0 m2)
-           , Equation (instantiate0 t1) (instantiate0 t2)
+  equate f (Ann m1 t1) (Ann m2 t2) =
+    return [ Equation f (instantiate0 m1) (instantiate0 m2)
+           , Equation f (instantiate0 t1) (instantiate0 t2)
            ]
-  equate Type Type =
+  equate _ Type Type =
     return []
-  equate (Fun a1 sc1) (Fun a2 sc2) =
+  equate f (Fun a1 sc1) (Fun a2 sc2) =
     do ns <- freshRelTo (names sc1) context
        let xs = map (Var . Free) ns
-       return [ Equation (instantiate0 a1) (instantiate0 a2)
-              , Equation (instantiate sc1 xs) (instantiate sc2 xs)
+       return [ Equation f (instantiate0 a1) (instantiate0 a2)
+              , Equation f (instantiate sc1 xs) (instantiate sc2 xs)
               ]
-  equate (Lam sc1) (Lam sc2) =
+  equate f (Lam sc1) (Lam sc2) =
     do ns <- freshRelTo (names sc1) context
        let xs = map (Var . Free) ns
-       return [ Equation (instantiate sc1 xs) (instantiate sc2 xs) ]
-  equate (App f1 a1) (App f2 a2) =
-    return [ Equation (instantiate0 f1) (instantiate0 f2)
-           , Equation (instantiate0 a1) (instantiate0 a2)
+       return [ Equation f (instantiate sc1 xs) (instantiate sc2 xs) ]
+  equate _ (App f1 a1) (App f2 a2) =
+    return [ Equation False (instantiate0 f1) (instantiate0 f2)
+           , Equation False (instantiate0 a1) (instantiate0 a2)
            ]
-  equate (Con c1 as1) (Con c2 as2) =
+  equate f (Con c1 as1) (Con c2 as2) =
     do unless (c1 == c2)
          $ throwError $ "Mismatching constructors "
                      ++ c1 ++ " and " ++ c2
@@ -67,10 +67,10 @@ instance MonadUnify TermF Elaborator where
                          ++ pretty (In (Con c1 as1)) ++ " and "
                          ++ pretty (In (Con c2 as1))
        return $ zipWith
-                  Equation
+                  (Equation f)
                   (map instantiate0 as1)
                   (map instantiate0 as2)
-  equate (Case as1 mot1 cs1) (Case as2 mot2 cs2) =
+  equate _ (Case as1 mot1 cs1) (Case as2 mot2 cs2) =
     do unless (length as1 == length as2)
          $ throwError $ "Mismatching number of case arguments in "
                      ++ pretty (In (Case as1 mot1 cs1)) ++ " and "
@@ -80,13 +80,13 @@ instance MonadUnify TermF Elaborator where
                      ++ pretty (In (Case as1 mot1 cs1)) ++ " and "
                      ++ pretty (In (Case as2 mot2 cs2))
        let argEqs = zipWith
-                      Equation
+                      (Equation False)
                         (map instantiate0 as1)
                         (map instantiate0 as2)
        motEqs <- equateCaseMotive mot1 mot2
        clauseEqs <- fmap concat $ zipWithM equateClause cs1 cs2
        return $ argEqs ++ motEqs ++ clauseEqs
-  equate l r =
+  equate _ l r =
     throwError $ "Cannot unify " ++ pretty (In l) ++ " with " ++ pretty (In r)
 
 
@@ -104,7 +104,7 @@ equateCaseMotive mot1@(CaseMotive tele1) mot2@(CaseMotive tele2) =
      unless (length as1 == length as2)
        $ throwError $ "Motives not equal: " ++ pretty mot1 ++ " and "
                    ++ pretty mot2
-     return $ zipWith Equation as1 as2 ++ [ Equation b1 b2 ]
+     return $ zipWith (Equation False) as1 as2 ++ [ Equation False b1 b2 ]
      
 
 
@@ -129,5 +129,5 @@ equateClause (Clause pscs1 sc1) (Clause pscs2 sc2) =
        Nothing ->
          throwError "Patterns are not equal."
        Just pEqss ->
-         return $ [ Equation a1 a2 | (a1,a2) <- concat pEqss ]
-               ++ [ Equation b1 b2 ]
\ No newline at end of file
+         return $ [ Equation False a1 a2 | (a1,a2) <- concat pEqss ]
+               ++ [ Equation False b1 b2 ]
diff --git a/src/DependentImplicit/Unification/TypeChecking.hs b/src/DependentImplicit/Unification/TypeChecking.hs
index 301d0a3..65e5300 100644
--- a/src/DependentImplicit/Unification/TypeChecking.hs
+++ b/src/DependentImplicit/Unification/TypeChecking.hs
@@ -194,7 +194,7 @@ inferify (Var (Free x)) =
      return (ElaboratedTerm (Var (Free x)), t)
 inferify (Var (Bound _ _)) =
   error "Bound type variables should not be the subject of type checking."
-inferify (Var (Meta x)) =
+inferify (Var (Meta _ x)) =
   throwError $ "The metavariable " ++ show x
             ++ " appears in checkable code, when it should not."
 inferify (In (Defined x)) =
@@ -305,8 +305,8 @@ inferifyApplication f (In (Fun Expl _ _)) Impl m =
     ++ pretty (appH Impl f m)
 inferifyApplication f (In (Fun Impl _ sc)) Expl m =
   do meta <- nextElab nextMeta
-     let f' = appH Impl f (Var (Meta meta))
-         t' = instantiate sc [Var (Meta meta)]
+     let f' = appH Impl f (Var (Meta Exist meta))
+         t' = instantiate sc [Var (Meta Exist meta)]
      inferifyApplication  f' t' Expl m
 inferifyApplication f _ _ _ =
   throwError $ "Cannot apply non-function: " ++ pretty f
@@ -363,7 +363,7 @@ inferifyConArgs ascs0 bsc0 ms0 = go [] ascs0 bsc0 ms0
          go (acc ++ [(Impl,m')]) ascs bsc ms
     go acc ((Impl,_):ascs) bsc ms =
       do meta <- nextElab nextMeta
-         go (acc ++ [(Impl,Var (Meta meta))]) ascs bsc ms
+         go (acc ++ [(Impl,Var (Meta Exist meta))]) ascs bsc ms
     go _ _ _ _ =
       throwError "Cannot match signature."
 
@@ -576,7 +576,7 @@ checkifyConArgs ascs0 bsc ms0 t =
       return acc
     accArgsToCheck acc ((Expl,asc):ascs) ((Expl,m):ms) =
       do meta <- nextElab nextMeta
-         let x = Var (Meta meta)
+         let x = Var (Meta Exist meta)
              xs = [ x' | (_,_,x',_) <- acc ]
              newSuspension = (Expl, Just m, x, instantiate asc xs)
          accArgsToCheck
@@ -585,7 +585,7 @@ checkifyConArgs ascs0 bsc ms0 t =
            ms
     accArgsToCheck acc ((Impl,asc):ascs) ((Impl,m):ms) =
       do meta <- nextElab nextMeta
-         let x = Var (Meta meta)
+         let x = Var (Meta Exist meta)
              xs = [ x' | (_,_,x',_) <- acc ]
              newSuspension = (Impl, Just m, x, instantiate asc xs)
          accArgsToCheck
@@ -594,7 +594,7 @@ checkifyConArgs ascs0 bsc ms0 t =
            ms
     accArgsToCheck acc ((Impl,asc):ascs) ms =
       do meta <- nextElab nextMeta
-         let x = Var (Meta meta)
+         let x = Var (Meta Exist meta)
              xs = [ x' | (_,_,x',_) <- acc ]
              newSuspension = (Impl, Nothing, x, instantiate asc xs)
          accArgsToCheck
@@ -607,12 +607,12 @@ checkifyConArgs ascs0 bsc ms0 t =
     swapMetas :: [(Plicity,Term)]
               -> TypeChecker ([(Term,Term)], [(Plicity,Term)])
     swapMetas [] = return ([],[])
-    swapMetas ((plic, Var (Meta meta)):ms) =
+    swapMetas ((plic, Var (Meta Exist meta)):ms) =
       do (eqs,ms') <- swapMetas ms
-         return (eqs, (plic,Var (Meta meta)):ms')
+         return (eqs, (plic,Var (Meta Exist meta)):ms')
     swapMetas ((plic,m):ms) =
       do meta <- nextElab nextMeta
-         let x = Var (Meta meta)
+         let x = Var (Meta Exist meta)
          (eqs,ms') <- swapMetas ms
          return ((x,m):eqs, (plic,x):ms')
      
@@ -678,7 +678,7 @@ checkifyPattern (Var (Free x)) t =
             , ElaboratedTerm (Var (Free x))
             , []
             )
-checkifyPattern (Var (Meta _)) _ =
+checkifyPattern (Var (Meta _ _)) _ =
   error "Metavariables should not be the subject of pattern type checking."
 checkifyPattern (In (ConPat _ _)) (NormalTerm (In Type)) =
   throwError "Cannot pattern match on a type."
@@ -699,12 +699,12 @@ checkifyPattern (In (AssertionPat m)) t =
   do ElaboratedTerm m' <- checkify m t
      mv <- nextElab nextMeta
      return ( In (AssertionPat m')
-            , ElaboratedTerm (Var $ Meta mv)
-            , [(Var $ Meta mv, m')]
+            , ElaboratedTerm (Var $ Meta Constraint mv)
+            , [(Var $ Meta Constraint mv, m')]
             )
 checkifyPattern (In MakeMeta) _ =
   do meta <- nextElab nextMeta
-     let x = Var (Meta meta)
+     let x = Var (Meta Exist meta)
      return ( In (AssertionPat x)
             , ElaboratedTerm x
             , []
@@ -799,7 +799,7 @@ checkifyPatterns ascs0 bsc ps0 t =
       return acc
     accArgsToCheck acc ((Expl,asc):ascs) ((Expl,p):ps) =
       do meta <- nextElab nextMeta
-         let x = Var (Meta meta)
+         let x = Var (Meta Exist meta)
              xs = [ x' | (_,_,x',_) <- acc ]
              newSuspension = (Expl, Just p, x, instantiate asc xs)
          accArgsToCheck
@@ -808,7 +808,7 @@ checkifyPatterns ascs0 bsc ps0 t =
            ps
     accArgsToCheck acc ((Impl,asc):ascs) ((Impl,p):ps) =
       do meta <- nextElab nextMeta
-         let x = Var (Meta meta)
+         let x = Var (Meta Exist meta)
              xs = [ x' | (_,_,x',_) <- acc ]
              newSuspension = (Impl, Just p, x, instantiate asc xs)
          accArgsToCheck
@@ -817,7 +817,7 @@ checkifyPatterns ascs0 bsc ps0 t =
            ps
     accArgsToCheck acc ((Impl,asc):ascs) ps =
       do meta <- nextElab nextMeta
-         let x = Var (Meta meta)
+         let x = Var (Meta Exist meta)
              xs = [ x' | (_,_,x',_) <- acc ]
              newSuspension = (Impl, Nothing, x, instantiate asc xs)
          accArgsToCheck
@@ -830,12 +830,12 @@ checkifyPatterns ascs0 bsc ps0 t =
     swapMetas :: [(Plicity,Term)]
               -> TypeChecker ([(Term,Term)], [(Plicity,Term)])
     swapMetas [] = return ([],[])
-    swapMetas ((plic, Var (Meta meta)):ms) =
+    swapMetas ((plic, Var (Meta Exist meta)):ms) =
       do (eqs,ms') <- swapMetas ms
-         return (eqs, (plic,Var (Meta meta)):ms')
+         return (eqs, (plic,Var (Meta Exist meta)):ms')
     swapMetas ((plic,m):ms) =
       do meta <- nextElab nextMeta
-         let x = Var (Meta meta)
+         let x = Var (Meta Exist meta)
          (eqs,ms') <- swapMetas ms
          return ((x,m):eqs, (plic,x):ms')
 
@@ -921,7 +921,7 @@ checkifyClause (Clause pscs sc) mot@(CaseMotive (BindingTelescope ascs _)) =
          xs2 = map (Var . Free) ns
      ctx' <- forM ns $ \n ->
                do m <- nextElab nextMeta
-                  return (n, Var (Meta m))
+                  return (n, Var (Meta Exist m))
      extendElab context ctx' $
        do (ps',ElaboratedTerm ret) <-
             checkifyPatternsCaseMotive
diff --git a/src/DependentImplicit/Unification/Unification.hs b/src/DependentImplicit/Unification/Unification.hs
index 0d1255f..6e15dc2 100644
--- a/src/DependentImplicit/Unification/Unification.hs
+++ b/src/DependentImplicit/Unification/Unification.hs
@@ -34,43 +34,43 @@ import Control.Monad.Except
 -- | Equating terms by trivial structural equations.
 
 instance MonadUnify TermF Elaborator where
-  equate (Defined n1) (Defined n2) =
+  equate _ (Defined n1) (Defined n2) =
     if n1 == n2
        then return []
        else throwError $ "Mismatching names " ++ n1 ++ " and " ++ n2
-  equate (Ann m1 t1) (Ann m2 t2) =
-    return [ Equation (instantiate0 m1) (instantiate0 m2)
-           , Equation (instantiate0 t1) (instantiate0 t2)
+  equate f (Ann m1 t1) (Ann m2 t2) =
+    return [ Equation f (instantiate0 m1) (instantiate0 m2)
+           , Equation f (instantiate0 t1) (instantiate0 t2)
            ]
-  equate Type Type =
+  equate _ Type Type =
     return []
-  equate (Fun plic1 a1 sc1) (Fun plic2 a2 sc2) =
+  equate f (Fun plic1 a1 sc1) (Fun plic2 a2 sc2) =
     do unless (plic1 == plic2)
          $ throwError $ "Mismatching plicities when unifying "
              ++ pretty (In (Fun plic1 a1 sc1)) ++ " with "
              ++ pretty (In (Fun plic2 a2 sc2))
        ns <- freshRelTo (names sc1) context
        let xs = map (Var . Free) ns
-       return [ Equation (instantiate0 a1) (instantiate0 a2)
-              , Equation (instantiate sc1 xs) (instantiate sc2 xs)
+       return [ Equation f (instantiate0 a1) (instantiate0 a2)
+              , Equation f (instantiate sc1 xs) (instantiate sc2 xs)
               ]
-  equate (Lam plic1 sc1) (Lam plic2 sc2) =
+  equate f (Lam plic1 sc1) (Lam plic2 sc2) =
     do unless (plic1 == plic2)
          $ throwError $ "Mismatching plicities when unifying "
              ++ pretty (In (Lam plic1 sc1)) ++ " with "
              ++ pretty (In (Lam plic2 sc2))
        ns <- freshRelTo (names sc1) context
        let xs = map (Var . Free) ns
-       return [ Equation (instantiate sc1 xs) (instantiate sc2 xs) ]
-  equate (App plic1 f1 a1) (App plic2 f2 a2) =
+       return [ Equation f (instantiate sc1 xs) (instantiate sc2 xs) ]
+  equate _ (App plic1 f1 a1) (App plic2 f2 a2) =
     do unless (plic1 == plic2)
          $ throwError $ "Mismatching plicities when unifying "
              ++ pretty (In (App plic1 f1 a1)) ++ " with "
              ++ pretty (In (App plic2 f2 a2))
-       return [ Equation (instantiate0 f1) (instantiate0 f2)
-              , Equation (instantiate0 a1) (instantiate0 a2)
+       return [ Equation False (instantiate0 f1) (instantiate0 f2)
+              , Equation False (instantiate0 a1) (instantiate0 a2)
               ]
-  equate (Con c1 as1) (Con c2 as2) =
+  equate f (Con c1 as1) (Con c2 as2) =
     do unless (c1 == c2)
          $ throwError $ "Mismatching constructors "
                      ++ c1 ++ " and " ++ c2
@@ -85,10 +85,10 @@ instance MonadUnify TermF Elaborator where
              ++ pretty (In (Con c1 as1)) ++ " with "
              ++ pretty (In (Con c2 as2))
        return $ zipWith
-                  Equation
+                  (Equation f)
                   (map instantiate0 as1')
                   (map instantiate0 as2')
-  equate (Case as1 mot1 cs1) (Case as2 mot2 cs2) =
+  equate _ (Case as1 mot1 cs1) (Case as2 mot2 cs2) =
     do unless (length as1 == length as2)
          $ throwError $ "Mismatching number of case arguments in "
                      ++ pretty (In (Case as1 mot1 cs1)) ++ " and "
@@ -98,13 +98,13 @@ instance MonadUnify TermF Elaborator where
                      ++ pretty (In (Case as1 mot1 cs1)) ++ " and "
                      ++ pretty (In (Case as2 mot2 cs2))
        let argEqs = zipWith
-                      Equation
+                      (Equation False)
                         (map instantiate0 as1)
                         (map instantiate0 as2)
        motEqs <- equateCaseMotive mot1 mot2
        clauseEqs <- fmap concat $ zipWithM equateClause cs1 cs2
        return $ argEqs ++ motEqs ++ clauseEqs
-  equate l r =
+  equate _ l r =
     throwError $ "Cannot unify " ++ pretty (In l) ++ " with " ++ pretty (In r)
 
 
@@ -122,7 +122,7 @@ equateCaseMotive mot1@(CaseMotive tele1) mot2@(CaseMotive tele2) =
      unless (length as1 == length as2)
        $ throwError $ "Motives not equal: " ++ pretty mot1 ++ " and "
                    ++ pretty mot2
-     return $ zipWith Equation as1 as2 ++ [ Equation b1 b2 ]
+     return $ zipWith (Equation False) as1 as2 ++ [ Equation False b1 b2 ]
      
 
 
@@ -147,5 +147,5 @@ equateClause (Clause pscs1 sc1) (Clause pscs2 sc2) =
        Nothing ->
          throwError "Patterns are not equal."
        Just pEqss ->
-         return $ [ Equation a1 a2 | (a1,a2) <- concat pEqss ]
-               ++ [ Equation b1 b2 ]
\ No newline at end of file
+         return $ [ Equation False a1 a2 | (a1,a2) <- concat pEqss ]
+               ++ [ Equation False b1 b2 ]
diff --git a/src/Modular/Unification/TypeChecking.hs b/src/Modular/Unification/TypeChecking.hs
index 168571a..6b4854d 100644
--- a/src/Modular/Unification/TypeChecking.hs
+++ b/src/Modular/Unification/TypeChecking.hs
@@ -232,7 +232,7 @@ inferify (Var (Free x)) =
      return (ElaboratedTerm (Var (Free x)), t)
 inferify (Var (Bound _ _)) =
   error "Bound type variables should not be the subject of type checking."
-inferify (Var (Meta x)) =
+inferify (Var (Meta _ x)) =
   throwError $ "The metavariable " ++ show x
             ++ " appears in checkable code, when it should not."
 inferify (In (Defined x)) =
@@ -343,8 +343,8 @@ inferifyApplication f (In (Fun Expl _ _)) Impl m =
     ++ pretty (appH Impl f m)
 inferifyApplication f (In (Fun Impl _ sc)) Expl m =
   do meta <- nextElab nextMeta
-     let f' = appH Impl f (Var (Meta meta))
-         t' = instantiate sc [Var (Meta meta)]
+     let f' = appH Impl f (Var (Meta Exist meta))
+         t' = instantiate sc [Var (Meta Exist meta)]
      inferifyApplication  f' t' Expl m
 inferifyApplication f _ _ _ =
   throwError $ "Cannot apply non-function: " ++ pretty f
@@ -401,7 +401,7 @@ inferifyConArgs ascs0 bsc0 ms0 = go [] ascs0 bsc0 ms0
          go (acc ++ [(Impl,m')]) ascs bsc ms
     go acc ((Impl,_):ascs) bsc ms =
       do meta <- nextElab nextMeta
-         go (acc ++ [(Impl,Var (Meta meta))]) ascs bsc ms
+         go (acc ++ [(Impl,Var (Meta Exist meta))]) ascs bsc ms
     go _ _ _ _ =
       throwError "Cannot match signature."
 
@@ -614,7 +614,7 @@ checkifyConArgs ascs0 bsc ms0 t =
       return acc
     accArgsToCheck acc ((Expl,asc):ascs) ((Expl,m):ms) =
       do meta <- nextElab nextMeta
-         let x = Var (Meta meta)
+         let x = Var (Meta Exist meta)
              xs = [ x' | (_,_,x',_) <- acc ]
              newSuspension = (Expl, Just m, x, instantiate asc xs)
          accArgsToCheck
@@ -623,7 +623,7 @@ checkifyConArgs ascs0 bsc ms0 t =
            ms
     accArgsToCheck acc ((Impl,asc):ascs) ((Impl,m):ms) =
       do meta <- nextElab nextMeta
-         let x = Var (Meta meta)
+         let x = Var (Meta Exist meta)
              xs = [ x' | (_,_,x',_) <- acc ]
              newSuspension = (Impl, Just m, x, instantiate asc xs)
          accArgsToCheck
@@ -632,7 +632,7 @@ checkifyConArgs ascs0 bsc ms0 t =
            ms
     accArgsToCheck acc ((Impl,asc):ascs) ms =
       do meta <- nextElab nextMeta
-         let x = Var (Meta meta)
+         let x = Var (Meta Exist meta)
              xs = [ x' | (_,_,x',_) <- acc ]
              newSuspension = (Impl, Nothing, x, instantiate asc xs)
          accArgsToCheck
@@ -645,12 +645,12 @@ checkifyConArgs ascs0 bsc ms0 t =
     swapMetas :: [(Plicity,Term)]
               -> TypeChecker ([(Term,Term)], [(Plicity,Term)])
     swapMetas [] = return ([],[])
-    swapMetas ((plic, Var (Meta meta)):ms) =
+    swapMetas ((plic, Var (Meta Exist meta)):ms) =
       do (eqs,ms') <- swapMetas ms
-         return (eqs, (plic,Var (Meta meta)):ms')
+         return (eqs, (plic,Var (Meta Exist meta)):ms')
     swapMetas ((plic,m):ms) =
       do meta <- nextElab nextMeta
-         let x = Var (Meta meta)
+         let x = Var (Meta Exist meta)
          (eqs,ms') <- swapMetas ms
          return ((x,m):eqs, (plic,x):ms')
      
@@ -716,7 +716,7 @@ checkifyPattern (Var (Free x)) t =
             , ElaboratedTerm (Var (Free x))
             , []
             )
-checkifyPattern (Var (Meta _)) _ =
+checkifyPattern (Var (Meta _ _)) _ =
   error "Metavariables should not be the subject of pattern type checking."
 checkifyPattern (In (ConPat c ps)) (NormalTerm t) =
   do (ec,ConSig plics (BindingTelescope ascs bsc)) <- typeInSignature c
@@ -735,12 +735,12 @@ checkifyPattern (In (AssertionPat m)) t =
   do ElaboratedTerm m' <- checkify m t
      mv <- nextElab nextMeta
      return ( In (AssertionPat m')
-            , ElaboratedTerm (Var $ Meta mv)
-            , [(Var $ Meta mv, m')]
+            , ElaboratedTerm (Var $ Meta Constraint mv)
+            , [(Var $ Meta Constraint mv, m')]
             )
 checkifyPattern (In MakeMeta) _ =
   do meta <- nextElab nextMeta
-     let x = Var (Meta meta)
+     let x = Var (Meta Exist meta)
      return ( In (AssertionPat x)
             , ElaboratedTerm x
             , []
@@ -835,7 +835,7 @@ checkifyPatterns ascs0 bsc ps0 t =
       return acc
     accArgsToCheck acc ((Expl,asc):ascs) ((Expl,p):ps) =
       do meta <- nextElab nextMeta
-         let x = Var (Meta meta)
+         let x = Var (Meta Exist meta)
              xs = [ x' | (_,_,x',_) <- acc ]
              newSuspension = (Expl, Just p, x, instantiate asc xs)
          accArgsToCheck
@@ -844,7 +844,7 @@ checkifyPatterns ascs0 bsc ps0 t =
            ps
     accArgsToCheck acc ((Impl,asc):ascs) ((Impl,p):ps) =
       do meta <- nextElab nextMeta
-         let x = Var (Meta meta)
+         let x = Var (Meta Exist meta)
              xs = [ x' | (_,_,x',_) <- acc ]
              newSuspension = (Impl, Just p, x, instantiate asc xs)
          accArgsToCheck
@@ -853,7 +853,7 @@ checkifyPatterns ascs0 bsc ps0 t =
            ps
     accArgsToCheck acc ((Impl,asc):ascs) ps =
       do meta <- nextElab nextMeta
-         let x = Var (Meta meta)
+         let x = Var (Meta Exist meta)
              xs = [ x' | (_,_,x',_) <- acc ]
              newSuspension = (Impl, Nothing, x, instantiate asc xs)
          accArgsToCheck
@@ -866,12 +866,12 @@ checkifyPatterns ascs0 bsc ps0 t =
     swapMetas :: [(Plicity,Term)]
               -> TypeChecker ([(Term,Term)], [(Plicity,Term)])
     swapMetas [] = return ([],[])
-    swapMetas ((plic, Var (Meta meta)):ms) =
+    swapMetas ((plic, Var (Meta Exist meta)):ms) =
       do (eqs,ms') <- swapMetas ms
-         return (eqs, (plic,Var (Meta meta)):ms')
+         return (eqs, (plic,Var (Meta Exist meta)):ms')
     swapMetas ((plic,m):ms) =
       do meta <- nextElab nextMeta
-         let x = Var (Meta meta)
+         let x = Var (Meta Exist meta)
          (eqs,ms') <- swapMetas ms
          return ((x,m):eqs, (plic,x):ms')
 
@@ -957,7 +957,7 @@ checkifyClause (Clause pscs sc) mot@(CaseMotive (BindingTelescope ascs _)) =
          xs2 = map (Var . Free) ns
      ctx' <- forM ns $ \n ->
                do m <- nextElab nextMeta
-                  return (n, Var (Meta m))
+                  return (n, Var (Meta Exist m))
      extendElab context ctx' $
        do (ps',ElaboratedTerm ret) <-
             checkifyPatternsCaseMotive
diff --git a/src/Modular/Unification/Unification.hs b/src/Modular/Unification/Unification.hs
index 2847aa8..e675235 100644
--- a/src/Modular/Unification/Unification.hs
+++ b/src/Modular/Unification/Unification.hs
@@ -35,44 +35,44 @@ import Control.Monad.Except
 -- | Equating terms by trivial structural equations.
 
 instance MonadUnify TermF Elaborator where
-  equate (Defined n1) (Defined n2) =
+  equate _ (Defined n1) (Defined n2) =
     if n1 == n2
        then return []
        else throwError $ "Mismatching names "
                          ++ showName n1 ++ " and " ++ showName n2
-  equate (Ann m1 t1) (Ann m2 t2) =
-    return [ Equation (instantiate0 m1) (instantiate0 m2)
-           , Equation (instantiate0 t1) (instantiate0 t2)
+  equate f (Ann m1 t1) (Ann m2 t2) =
+    return [ Equation f (instantiate0 m1) (instantiate0 m2)
+           , Equation f (instantiate0 t1) (instantiate0 t2)
            ]
-  equate Type Type =
+  equate _ Type Type =
     return []
-  equate (Fun plic1 a1 sc1) (Fun plic2 a2 sc2) =
+  equate f (Fun plic1 a1 sc1) (Fun plic2 a2 sc2) =
     do unless (plic1 == plic2)
          $ throwError $ "Mismatching plicities when unifying "
              ++ pretty (In (Fun plic1 a1 sc1)) ++ " with "
              ++ pretty (In (Fun plic2 a2 sc2))
        ns <- freshRelTo (names sc1) context
        let xs = map (Var . Free) ns
-       return [ Equation (instantiate0 a1) (instantiate0 a2)
-              , Equation (instantiate sc1 xs) (instantiate sc2 xs)
+       return [ Equation f (instantiate0 a1) (instantiate0 a2)
+              , Equation f (instantiate sc1 xs) (instantiate sc2 xs)
               ]
-  equate (Lam plic1 sc1) (Lam plic2 sc2) =
+  equate f (Lam plic1 sc1) (Lam plic2 sc2) =
     do unless (plic1 == plic2)
          $ throwError $ "Mismatching plicities when unifying "
              ++ pretty (In (Lam plic1 sc1)) ++ " with "
              ++ pretty (In (Lam plic2 sc2))
        ns <- freshRelTo (names sc1) context
        let xs = map (Var . Free) ns
-       return [ Equation (instantiate sc1 xs) (instantiate sc2 xs) ]
-  equate (App plic1 f1 a1) (App plic2 f2 a2) =
+       return [ Equation f (instantiate sc1 xs) (instantiate sc2 xs) ]
+  equate _ (App plic1 f1 a1) (App plic2 f2 a2) =
     do unless (plic1 == plic2)
          $ throwError $ "Mismatching plicities when unifying "
              ++ pretty (In (App plic1 f1 a1)) ++ " with "
              ++ pretty (In (App plic2 f2 a2))
-       return [ Equation (instantiate0 f1) (instantiate0 f2)
-              , Equation (instantiate0 a1) (instantiate0 a2)
+       return [ Equation False (instantiate0 f1) (instantiate0 f2)
+              , Equation False (instantiate0 a1) (instantiate0 a2)
               ]
-  equate (Con c1 as1) (Con c2 as2) =
+  equate f (Con c1 as1) (Con c2 as2) =
     do unless (c1 == c2)
          $ throwError $ "Mismatching constructors "
                      ++ showName c1 ++ " and " ++ showName c2
@@ -87,10 +87,10 @@ instance MonadUnify TermF Elaborator where
              ++ pretty (In (Con c1 as1)) ++ " with "
              ++ pretty (In (Con c2 as2))
        return $ zipWith
-                  Equation
+                  (Equation f)
                   (map instantiate0 as1')
                   (map instantiate0 as2')
-  equate (Case as1 mot1 cs1) (Case as2 mot2 cs2) =
+  equate _ (Case as1 mot1 cs1) (Case as2 mot2 cs2) =
     do unless (length as1 == length as2)
          $ throwError $ "Mismatching number of case arguments in "
                      ++ pretty (In (Case as1 mot1 cs1)) ++ " and "
@@ -100,13 +100,13 @@ instance MonadUnify TermF Elaborator where
                      ++ pretty (In (Case as1 mot1 cs1)) ++ " and "
                      ++ pretty (In (Case as2 mot2 cs2))
        let argEqs = zipWith
-                      Equation
+                      (Equation False)
                         (map instantiate0 as1)
                         (map instantiate0 as2)
        motEqs <- equateCaseMotive mot1 mot2
        clauseEqs <- fmap concat $ zipWithM equateClause cs1 cs2
        return $ argEqs ++ motEqs ++ clauseEqs
-  equate l r =
+  equate _ l r =
     throwError $ "Cannot unify " ++ pretty (In l) ++ " with " ++ pretty (In r)
 
 
@@ -124,7 +124,7 @@ equateCaseMotive mot1@(CaseMotive tele1) mot2@(CaseMotive tele2) =
      unless (length as1 == length as2)
        $ throwError $ "Motives not equal: " ++ pretty mot1 ++ " and "
                    ++ pretty mot2
-     return $ zipWith Equation as1 as2 ++ [ Equation b1 b2 ]
+     return $ zipWith (Equation False) as1 as2 ++ [ Equation False b1 b2 ]
      
 
 
@@ -149,5 +149,5 @@ equateClause (Clause pscs1 sc1) (Clause pscs2 sc2) =
        Nothing ->
          throwError "Patterns are not equal."
        Just pEqss ->
-         return $ [ Equation a1 a2 | (a1,a2) <- concat pEqss ]
-               ++ [ Equation b1 b2 ]
\ No newline at end of file
+         return $ [ Equation False a1 a2 | (a1,a2) <- concat pEqss ]
+               ++ [ Equation False b1 b2 ]
diff --git a/src/OpenDefs/Unification/TypeChecking.hs b/src/OpenDefs/Unification/TypeChecking.hs
index 3080b75..41ca240 100644
--- a/src/OpenDefs/Unification/TypeChecking.hs
+++ b/src/OpenDefs/Unification/TypeChecking.hs
@@ -245,7 +245,7 @@ inferify (Var (Free x)) =
      return (ElaboratedTerm (Var (Free x)), t)
 inferify (Var (Bound _ _)) =
   error "Bound type variables should not be the subject of type checking."
-inferify (Var (Meta x)) =
+inferify (Var (Meta _ x)) =
   throwError $ "The metavariable " ++ show x
             ++ " appears in checkable code, when it should not."
 inferify (In (Defined x)) =
@@ -392,8 +392,8 @@ inferifyApplication f (In (Fun Expl _ _)) Impl m =
     ++ pretty (appH Impl f m)
 inferifyApplication f (In (Fun Impl _ sc)) Expl m =
   do meta <- nextElab nextMeta
-     let f' = appH Impl f (Var (Meta meta))
-         t' = instantiate sc [Var (Meta meta)]
+     let f' = appH Impl f (Var (Meta Exist meta))
+         t' = instantiate sc [Var (Meta Exist meta)]
      inferifyApplication  f' t' Expl m
 inferifyApplication f _ _ _ =
   throwError $ "Cannot apply non-function: " ++ pretty f
@@ -450,7 +450,7 @@ inferifyConArgs ascs0 bsc0 ms0 = go [] ascs0 bsc0 ms0
          go (acc ++ [(Impl,m')]) ascs bsc ms
     go acc ((Impl,_):ascs) bsc ms =
       do meta <- nextElab nextMeta
-         go (acc ++ [(Impl,Var (Meta meta))]) ascs bsc ms
+         go (acc ++ [(Impl,Var (Meta Exist meta))]) ascs bsc ms
     go _ _ _ _ =
       throwError "Cannot match signature."
 
@@ -710,7 +710,7 @@ checkifyConArgs ascs0 bsc ms0 t =
       return acc
     accArgsToCheck acc ((Expl,asc):ascs) ((Expl,m):ms) =
       do meta <- nextElab nextMeta
-         let x = Var (Meta meta)
+         let x = Var (Meta Exist meta)
              xs = [ x' | (_,_,x',_) <- acc ]
              newSuspension = (Expl, Just m, x, instantiate asc xs)
          accArgsToCheck
@@ -719,7 +719,7 @@ checkifyConArgs ascs0 bsc ms0 t =
            ms
     accArgsToCheck acc ((Impl,asc):ascs) ((Impl,m):ms) =
       do meta <- nextElab nextMeta
-         let x = Var (Meta meta)
+         let x = Var (Meta Exist meta)
              xs = [ x' | (_,_,x',_) <- acc ]
              newSuspension = (Impl, Just m, x, instantiate asc xs)
          accArgsToCheck
@@ -728,7 +728,7 @@ checkifyConArgs ascs0 bsc ms0 t =
            ms
     accArgsToCheck acc ((Impl,asc):ascs) ms =
       do meta <- nextElab nextMeta
-         let x = Var (Meta meta)
+         let x = Var (Meta Exist meta)
              xs = [ x' | (_,_,x',_) <- acc ]
              newSuspension = (Impl, Nothing, x, instantiate asc xs)
          accArgsToCheck
@@ -741,12 +741,12 @@ checkifyConArgs ascs0 bsc ms0 t =
     swapMetas :: [(Plicity,Term)]
               -> TypeChecker ([(Term,Term)], [(Plicity,Term)])
     swapMetas [] = return ([],[])
-    swapMetas ((plic, Var (Meta meta)):ms) =
+    swapMetas ((plic, Var (Meta Exist meta)):ms) =
       do (eqs,ms') <- swapMetas ms
-         return (eqs, (plic,Var (Meta meta)):ms')
+         return (eqs, (plic,Var (Meta Exist meta)):ms')
     swapMetas ((plic,m):ms) =
       do meta <- nextElab nextMeta
-         let x = Var (Meta meta)
+         let x = Var (Meta Exist meta)
          (eqs,ms') <- swapMetas ms
          return ((x,m):eqs, (plic,x):ms')
      
@@ -812,7 +812,7 @@ checkifyPattern (Var (Free x)) t =
             , ElaboratedTerm (Var (Free x))
             , []
             )
-checkifyPattern (Var (Meta _)) _ =
+checkifyPattern (Var (Meta _ _)) _ =
   error "Metavariables should not be the subject of pattern type checking."
 checkifyPattern (In (ConPat c ps)) (NormalTerm t) =
   do (ec,ConSig plics (BindingTelescope ascs bsc)) <- typeInSignature c
@@ -831,12 +831,12 @@ checkifyPattern (In (AssertionPat m)) t =
   do ElaboratedTerm m' <- checkify m t
      mv <- nextElab nextMeta
      return ( In (AssertionPat m')
-            , ElaboratedTerm (Var $ Meta mv)
-            , [(Var $ Meta mv, m')]
+            , ElaboratedTerm (Var $ Meta Constraint mv)
+            , [(Var $ Meta Constraint mv, m')]
             )
 checkifyPattern (In MakeMeta) _ =
   do meta <- nextElab nextMeta
-     let x = Var (Meta meta)
+     let x = Var (Meta Exist meta)
      return ( In (AssertionPat x)
             , ElaboratedTerm x
             , []
@@ -931,7 +931,7 @@ checkifyPatterns ascs0 bsc ps0 t =
       return acc
     accArgsToCheck acc ((Expl,asc):ascs) ((Expl,p):ps) =
       do meta <- nextElab nextMeta
-         let x = Var (Meta meta)
+         let x = Var (Meta Exist meta)
              xs = [ x' | (_,_,x',_) <- acc ]
              newSuspension = (Expl, Just p, x, instantiate asc xs)
          accArgsToCheck
@@ -940,7 +940,7 @@ checkifyPatterns ascs0 bsc ps0 t =
            ps
     accArgsToCheck acc ((Impl,asc):ascs) ((Impl,p):ps) =
       do meta <- nextElab nextMeta
-         let x = Var (Meta meta)
+         let x = Var (Meta Exist meta)
              xs = [ x' | (_,_,x',_) <- acc ]
              newSuspension = (Impl, Just p, x, instantiate asc xs)
          accArgsToCheck
@@ -949,7 +949,7 @@ checkifyPatterns ascs0 bsc ps0 t =
            ps
     accArgsToCheck acc ((Impl,asc):ascs) ps =
       do meta <- nextElab nextMeta
-         let x = Var (Meta meta)
+         let x = Var (Meta Exist meta)
              xs = [ x' | (_,_,x',_) <- acc ]
              newSuspension = (Impl, Nothing, x, instantiate asc xs)
          accArgsToCheck
@@ -962,12 +962,12 @@ checkifyPatterns ascs0 bsc ps0 t =
     swapMetas :: [(Plicity,Term)]
               -> TypeChecker ([(Term,Term)], [(Plicity,Term)])
     swapMetas [] = return ([],[])
-    swapMetas ((plic, Var (Meta meta)):ms) =
+    swapMetas ((plic, Var (Meta Exist meta)):ms) =
       do (eqs,ms') <- swapMetas ms
-         return (eqs, (plic,Var (Meta meta)):ms')
+         return (eqs, (plic,Var (Meta Exist meta)):ms')
     swapMetas ((plic,m):ms) =
       do meta <- nextElab nextMeta
-         let x = Var (Meta meta)
+         let x = Var (Meta Exist meta)
          (eqs,ms') <- swapMetas ms
          return ((x,m):eqs, (plic,x):ms')
 
@@ -1053,7 +1053,7 @@ checkifyClause (Clause pscs sc) mot@(CaseMotive (BindingTelescope ascs _)) =
          xs2 = map (Var . Free) ns
      ctx' <- forM ns $ \n ->
                do m <- nextElab nextMeta
-                  return (n, Var (Meta m))
+                  return (n, Var (Meta Exist m))
      extendElab context ctx' $
        do (ps',ElaboratedTerm ret) <-
             checkifyPatternsCaseMotive
diff --git a/src/OpenDefs/Unification/Unification.hs b/src/OpenDefs/Unification/Unification.hs
index b7869ee..c6b905f 100644
--- a/src/OpenDefs/Unification/Unification.hs
+++ b/src/OpenDefs/Unification/Unification.hs
@@ -35,44 +35,44 @@ import Control.Monad.Except
 -- | Equating terms by trivial structural equations.
 
 instance MonadUnify TermF Elaborator where
-  equate (Defined n1) (Defined n2) =
+  equate _ (Defined n1) (Defined n2) =
     if n1 == n2
        then return []
        else throwError $ "Mismatching names "
                          ++ showName n1 ++ " and " ++ showName n2
-  equate (Ann m1 t1) (Ann m2 t2) =
-    return [ Equation (instantiate0 m1) (instantiate0 m2)
-           , Equation (instantiate0 t1) (instantiate0 t2)
+  equate f (Ann m1 t1) (Ann m2 t2) =
+    return [ Equation f (instantiate0 m1) (instantiate0 m2)
+           , Equation f (instantiate0 t1) (instantiate0 t2)
            ]
-  equate Type Type =
+  equate _ Type Type =
     return []
-  equate (Fun plic1 a1 sc1) (Fun plic2 a2 sc2) =
+  equate f (Fun plic1 a1 sc1) (Fun plic2 a2 sc2) =
     do unless (plic1 == plic2)
          $ throwError $ "Mismatching plicities when unifying "
              ++ pretty (In (Fun plic1 a1 sc1)) ++ " with "
              ++ pretty (In (Fun plic2 a2 sc2))
        ns <- freshRelTo (names sc1) context
        let xs = map (Var . Free) ns
-       return [ Equation (instantiate0 a1) (instantiate0 a2)
-              , Equation (instantiate sc1 xs) (instantiate sc2 xs)
+       return [ Equation f (instantiate0 a1) (instantiate0 a2)
+              , Equation f (instantiate sc1 xs) (instantiate sc2 xs)
               ]
-  equate (Lam plic1 sc1) (Lam plic2 sc2) =
+  equate f (Lam plic1 sc1) (Lam plic2 sc2) =
     do unless (plic1 == plic2)
          $ throwError $ "Mismatching plicities when unifying "
              ++ pretty (In (Lam plic1 sc1)) ++ " with "
              ++ pretty (In (Lam plic2 sc2))
        ns <- freshRelTo (names sc1) context
        let xs = map (Var . Free) ns
-       return [ Equation (instantiate sc1 xs) (instantiate sc2 xs) ]
-  equate (App plic1 f1 a1) (App plic2 f2 a2) =
+       return [ Equation f (instantiate sc1 xs) (instantiate sc2 xs) ]
+  equate _ (App plic1 f1 a1) (App plic2 f2 a2) =
     do unless (plic1 == plic2)
          $ throwError $ "Mismatching plicities when unifying "
              ++ pretty (In (App plic1 f1 a1)) ++ " with "
              ++ pretty (In (App plic2 f2 a2))
-       return [ Equation (instantiate0 f1) (instantiate0 f2)
-              , Equation (instantiate0 a1) (instantiate0 a2)
+       return [ Equation False (instantiate0 f1) (instantiate0 f2)
+              , Equation False (instantiate0 a1) (instantiate0 a2)
               ]
-  equate (Con c1 as1) (Con c2 as2) =
+  equate f (Con c1 as1) (Con c2 as2) =
     do unless (c1 == c2)
          $ throwError $ "Mismatching constructors "
                      ++ showName c1 ++ " and " ++ showName c2
@@ -87,10 +87,10 @@ instance MonadUnify TermF Elaborator where
              ++ pretty (In (Con c1 as1)) ++ " with "
              ++ pretty (In (Con c2 as2))
        return $ zipWith
-                  Equation
+                  (Equation f)
                   (map instantiate0 as1')
                   (map instantiate0 as2')
-  equate (Case as1 mot1 cs1) (Case as2 mot2 cs2) =
+  equate _ (Case as1 mot1 cs1) (Case as2 mot2 cs2) =
     do unless (length as1 == length as2)
          $ throwError $ "Mismatching number of case arguments in "
                      ++ pretty (In (Case as1 mot1 cs1)) ++ " and "
@@ -100,13 +100,13 @@ instance MonadUnify TermF Elaborator where
                      ++ pretty (In (Case as1 mot1 cs1)) ++ " and "
                      ++ pretty (In (Case as2 mot2 cs2))
        let argEqs = zipWith
-                      Equation
+                      (Equation False)
                         (map instantiate0 as1)
                         (map instantiate0 as2)
        motEqs <- equateCaseMotive mot1 mot2
        clauseEqs <- fmap concat $ zipWithM equateClause cs1 cs2
        return $ argEqs ++ motEqs ++ clauseEqs
-  equate (RecordType fields1 tele1) (RecordType fields2 tele2) =
+  equate f (RecordType fields1 tele1) (RecordType fields2 tele2) =
     do unless (fields1 == fields2)
          $ throwError $ "Record types have different field names: "
              ++ pretty (In (RecordType fields1 tele1))
@@ -121,8 +121,8 @@ instance MonadUnify TermF Elaborator where
              ++ pretty (In (RecordType fields1 tele1))
              ++ " and "
              ++ pretty (In (RecordType fields2 tele2))
-       return $ zipWith Equation as1 as2
-  equate (RecordCon fields1) (RecordCon fields2) =
+       return $ zipWith (Equation f) as1 as2
+  equate f (RecordCon fields1) (RecordCon fields2) =
     do unless (length fields1 == length fields2)
          $ throwError $ "Records have different number of fields: "
              ++ pretty (In (RecordCon fields1))
@@ -136,17 +136,17 @@ instance MonadUnify TermF Elaborator where
              ++ " and "
              ++ pretty (In (RecordCon fields2))
        return $ zipWith
-                  Equation
+                  (Equation f)
                   (map instantiate0 ms1)
                   (map instantiate0 ms2)
-  equate (RecordProj r1 x1) (RecordProj r2 x2) =
+  equate _ (RecordProj r1 x1) (RecordProj r2 x2) =
     do unless (x1 == x2)
          $ throwError $ "Record projections have different names: "
              ++ pretty (In (RecordProj r1 x1))
              ++ " and "
              ++ pretty (In (RecordProj r2 x2))
-       return [Equation (instantiate0 r1) (instantiate0 r2)]
-  equate l r =
+       return [Equation False (instantiate0 r1) (instantiate0 r2)]
+  equate _ l r =
     throwError $ "Cannot unify " ++ pretty (In l) ++ " with " ++ pretty (In r)
 
 
@@ -164,7 +164,7 @@ equateCaseMotive mot1@(CaseMotive tele1) mot2@(CaseMotive tele2) =
      unless (length as1 == length as2)
        $ throwError $ "Motives not equal: " ++ pretty mot1 ++ " and "
                    ++ pretty mot2
-     return $ zipWith Equation as1 as2 ++ [ Equation b1 b2 ]
+     return $ zipWith (Equation False) as1 as2 ++ [ Equation False b1 b2 ]
      
 
 
@@ -189,5 +189,5 @@ equateClause (Clause pscs1 sc1) (Clause pscs2 sc2) =
        Nothing ->
          throwError "Patterns are not equal."
        Just pEqss ->
-         return $ [ Equation a1 a2 | (a1,a2) <- concat pEqss ]
-               ++ [ Equation b1 b2 ]
\ No newline at end of file
+         return $ [ Equation False a1 a2 | (a1,a2) <- concat pEqss ]
+               ++ [ Equation False b1 b2 ]
diff --git a/src/Poly/Unification/TypeChecking.hs b/src/Poly/Unification/TypeChecking.hs
index b5af9f0..e28c02b 100644
--- a/src/Poly/Unification/TypeChecking.hs
+++ b/src/Poly/Unification/TypeChecking.hs
@@ -119,7 +119,7 @@ isType (Var (Free x)) =
   tyVarExists x
 isType (Var (Bound _ _)) =
   error "Bound type variables should not be the subject of type checking."
-isType (Var (Meta _)) =
+isType (Var (Meta _ _)) =
   error "Metavariables should not be the subject of type checking."
 isType (In (TyCon c as)) =
   do TyConSig ar <- tyconExists c
@@ -150,7 +150,7 @@ instantiateParams argscs retsc =
   do metas <- replicateM
                (length (names retsc))
                (nextElab nextMeta)
-     let ms = map (Var . Meta) metas
+     let ms = map (Var . Meta Exist) metas
      return ( map (\sc -> instantiate sc ms) argscs
             , instantiate retsc ms
             )
@@ -169,7 +169,7 @@ instantiateParams argscs retsc =
 instantiateQuantifiers :: Type -> TypeChecker Type
 instantiateQuantifiers (In (Forall sc)) =
   do meta <- nextElab nextMeta
-     let m = Var (Meta meta)
+     let m = Var (Meta Exist meta)
      instantiateQuantifiers (instantiate sc [m])
 instantiateQuantifiers t = return t
 
@@ -215,7 +215,7 @@ inferify (Var (Bound _ _)) =
   error "A bound variable should never be the subject of type inference."
 inferify (Var (Free n)) =
   typeInContext n
-inferify (Var (Meta _)) =
+inferify (Var (Meta _ _)) =
   error "Metavariables should not be the subject of type inference."
 inferify (In (Defined x)) =
   typeInDefinitions x
@@ -227,7 +227,7 @@ inferify (In (Ann m t)) =
 inferify (In (Lam sc)) =
   do [n] <- freshRelTo (names sc) context
      meta <- nextElab nextMeta
-     let arg = Var (Meta meta)
+     let arg = Var (Meta Exist meta)
      ret <- extendElab context [(n, arg)]
               $ inferify (instantiate sc [Var (Free n)])
      subs <- getElab substitution
@@ -287,7 +287,7 @@ inferifyClause patTys (Clause pscs sc) =
          xs2 = map (Var . Free) ns
      ctx' <- forM ns $ \n -> do
                m <- nextElab nextMeta
-               return (n,Var (Meta m))
+               return (n,Var (Meta Exist m))
      extendElab context ctx' $ do
        zipWithM_ checkifyPattern
                  (map (\psc -> instantiate psc xs1) pscs)
@@ -403,7 +403,7 @@ subtype t (In (Forall sc')) =
      subtype t (instantiate sc' [Var (Free n)])
 subtype (In (Forall sc)) t' =
   do meta <- nextElab nextMeta
-     let x2 = Var (Meta meta)
+     let x2 = Var (Meta Exist meta)
      subtype (instantiate sc [x2]) t'
 subtype (In (Fun arg ret)) (In (Fun arg' ret')) =
   do subtype (instantiate0 arg') (instantiate0 arg)
@@ -432,7 +432,7 @@ subtype t t' =
 checkifyPattern :: Pattern -> Type -> TypeChecker ()
 checkifyPattern (Var (Bound _ _)) _ =
   error "A bound variable should not be the subject of pattern type checking."
-checkifyPattern (Var (Meta _)) _ =
+checkifyPattern (Var (Meta _ _)) _ =
   error "Metavariables should not be the subject of type checking."
 checkifyPattern (Var (Free n)) t =
   do t' <- typeInContext n
diff --git a/src/Poly/Unification/Unification.hs b/src/Poly/Unification/Unification.hs
index 5c784a8..53a4b65 100644
--- a/src/Poly/Unification/Unification.hs
+++ b/src/Poly/Unification/Unification.hs
@@ -33,7 +33,7 @@ import Control.Monad.Except
 -- | Equating terms by trivial structural equations.
 
 instance MonadUnify TypeF Elaborator where
-  equate (TyCon tycon1 as1) (TyCon tycon2 as2) =
+  equate f (TyCon tycon1 as1) (TyCon tycon2 as2) =
     do unless (tycon1 == tycon2)
          $ throwError $ "Mismatching type constructors "
                      ++ tycon1 ++ " and " ++ tycon2
@@ -42,16 +42,16 @@ instance MonadUnify TypeF Elaborator where
                          ++ pretty (In (TyCon tycon1 as1)) ++ " and "
                          ++ pretty (In (TyCon tycon2 as1))
        return $ zipWith
-                  Equation
+                  (Equation f)
                   (map instantiate0 as1)
                   (map instantiate0 as2)
-  equate (Fun a1 b1) (Fun a2 b2) =
-    return [ Equation (instantiate0 a1) (instantiate0 a2)
-           , Equation (instantiate0 b1) (instantiate0 b2)
+  equate f (Fun a1 b1) (Fun a2 b2) =
+    return [ Equation f (instantiate0 a1) (instantiate0 a2)
+           , Equation f (instantiate0 b1) (instantiate0 b2)
            ]
-  equate (Forall sc1) (Forall sc2) =
+  equate f (Forall sc1) (Forall sc2) =
     do ns <- freshRelTo (names sc1) context
        let xs = map (Var . Free) ns
-       return [ Equation (instantiate sc1 xs) (instantiate sc2 xs) ]
-  equate l r =
-    throwError $ "Cannot unify " ++ pretty (In l) ++ " with " ++ pretty (In r)
\ No newline at end of file
+       return [ Equation f (instantiate sc1 xs) (instantiate sc2 xs) ]
+  equate _ l r =
+    throwError $ "Cannot unify " ++ pretty (In l) ++ " with " ++ pretty (In r)
diff --git a/src/Quasiquote/Unification/TypeChecking.hs b/src/Quasiquote/Unification/TypeChecking.hs
index da876ce..41970f5 100644
--- a/src/Quasiquote/Unification/TypeChecking.hs
+++ b/src/Quasiquote/Unification/TypeChecking.hs
@@ -284,7 +284,7 @@ inferify (Var (Free x)) =
      return (ElaboratedTerm (Var (Free x)), t)
 inferify (Var (Bound _ _)) =
   error "Bound type variables should not be the subject of type checking."
-inferify (Var (Meta x)) =
+inferify (Var (Meta _ x)) =
   throwError $ "The metavariable " ++ show x
             ++ " appears in checkable code, when it should not."
 inferify (In (Defined x)) =
@@ -446,8 +446,8 @@ inferifyApplication f (In (Fun Expl _ _)) Impl m =
     ++ pretty (appH Impl f m)
 inferifyApplication f (In (Fun Impl _ sc)) Expl m =
   do meta <- nextElab nextMeta
-     let f' = appH Impl f (Var (Meta meta))
-         t' = instantiate sc [Var (Meta meta)]
+     let f' = appH Impl f (Var (Meta Exist meta))
+         t' = instantiate sc [Var (Meta Exist meta)]
      inferifyApplication  f' t' Expl m
 inferifyApplication f _ _ _ =
   throwError $ "Cannot apply non-function: " ++ pretty f
@@ -504,7 +504,7 @@ inferifyConArgs ascs0 bsc0 ms0 = go [] ascs0 bsc0 ms0
          go (acc ++ [(Impl,m')]) ascs bsc ms
     go acc ((Impl,_):ascs) bsc ms =
       do meta <- nextElab nextMeta
-         go (acc ++ [(Impl,Var (Meta meta))]) ascs bsc ms
+         go (acc ++ [(Impl,Var (Meta Exist meta))]) ascs bsc ms
     go _ _ _ _ =
       throwError "Cannot match signature."
 
@@ -780,7 +780,7 @@ checkifyConArgs ascs0 bsc ms0 t =
       return acc
     accArgsToCheck acc ((Expl,asc):ascs) ((Expl,m):ms) =
       do meta <- nextElab nextMeta
-         let x = Var (Meta meta)
+         let x = Var (Meta Exist meta)
              xs = [ x' | (_,_,x',_) <- acc ]
              newSuspension = (Expl, Just m, x, instantiate asc xs)
          accArgsToCheck
@@ -789,7 +789,7 @@ checkifyConArgs ascs0 bsc ms0 t =
            ms
     accArgsToCheck acc ((Impl,asc):ascs) ((Impl,m):ms) =
       do meta <- nextElab nextMeta
-         let x = Var (Meta meta)
+         let x = Var (Meta Exist meta)
              xs = [ x' | (_,_,x',_) <- acc ]
              newSuspension = (Impl, Just m, x, instantiate asc xs)
          accArgsToCheck
@@ -798,7 +798,7 @@ checkifyConArgs ascs0 bsc ms0 t =
            ms
     accArgsToCheck acc ((Impl,asc):ascs) ms =
       do meta <- nextElab nextMeta
-         let x = Var (Meta meta)
+         let x = Var (Meta Exist meta)
              xs = [ x' | (_,_,x',_) <- acc ]
              newSuspension = (Impl, Nothing, x, instantiate asc xs)
          accArgsToCheck
@@ -811,12 +811,12 @@ checkifyConArgs ascs0 bsc ms0 t =
     swapMetas :: [(Plicity,Term)]
               -> TypeChecker ([(Term,Term)], [(Plicity,Term)])
     swapMetas [] = return ([],[])
-    swapMetas ((plic, Var (Meta meta)):ms) =
+    swapMetas ((plic, Var (Meta Exist meta)):ms) =
       do (eqs,ms') <- swapMetas ms
-         return (eqs, (plic,Var (Meta meta)):ms')
+         return (eqs, (plic,Var (Meta Exist meta)):ms')
     swapMetas ((plic,m):ms) =
       do meta <- nextElab nextMeta
-         let x = Var (Meta meta)
+         let x = Var (Meta Exist meta)
          (eqs,ms') <- swapMetas ms
          return ((x,m):eqs, (plic,x):ms')
      
@@ -882,7 +882,7 @@ checkifyPattern (Var (Free x)) t =
             , ElaboratedTerm (Var (Free x))
             , []
             )
-checkifyPattern (Var (Meta _)) _ =
+checkifyPattern (Var (Meta _ _)) _ =
   error "Metavariables should not be the subject of pattern type checking."
 checkifyPattern (In (ConPat c ps)) (NormalTerm t) =
   do (ec,ConSig plics (BindingTelescope ascs bsc)) <- typeInSignature c
@@ -901,12 +901,12 @@ checkifyPattern (In (AssertionPat m)) t =
   do ElaboratedTerm m' <- checkify m t
      mv <- nextElab nextMeta
      return ( In (AssertionPat m')
-            , ElaboratedTerm (Var $ Meta mv)
-            , [(Var $ Meta mv, m')]
+            , ElaboratedTerm (Var $ Meta Constraint mv)
+            , [(Var $ Meta Constraint mv, m')]
             )
 checkifyPattern (In MakeMeta) _ =
   do meta <- nextElab nextMeta
-     let x = Var (Meta meta)
+     let x = Var (Meta Exist meta)
      return ( In (AssertionPat x)
             , ElaboratedTerm x
             , []
@@ -1001,7 +1001,7 @@ checkifyPatterns ascs0 bsc ps0 t =
       return acc
     accArgsToCheck acc ((Expl,asc):ascs) ((Expl,p):ps) =
       do meta <- nextElab nextMeta
-         let x = Var (Meta meta)
+         let x = Var (Meta Exist meta)
              xs = [ x' | (_,_,x',_) <- acc ]
              newSuspension = (Expl, Just p, x, instantiate asc xs)
          accArgsToCheck
@@ -1010,7 +1010,7 @@ checkifyPatterns ascs0 bsc ps0 t =
            ps
     accArgsToCheck acc ((Impl,asc):ascs) ((Impl,p):ps) =
       do meta <- nextElab nextMeta
-         let x = Var (Meta meta)
+         let x = Var (Meta Exist meta)
              xs = [ x' | (_,_,x',_) <- acc ]
              newSuspension = (Impl, Just p, x, instantiate asc xs)
          accArgsToCheck
@@ -1019,7 +1019,7 @@ checkifyPatterns ascs0 bsc ps0 t =
            ps
     accArgsToCheck acc ((Impl,asc):ascs) ps =
       do meta <- nextElab nextMeta
-         let x = Var (Meta meta)
+         let x = Var (Meta Exist meta)
              xs = [ x' | (_,_,x',_) <- acc ]
              newSuspension = (Impl, Nothing, x, instantiate asc xs)
          accArgsToCheck
@@ -1032,12 +1032,12 @@ checkifyPatterns ascs0 bsc ps0 t =
     swapMetas :: [(Plicity,Term)]
               -> TypeChecker ([(Term,Term)], [(Plicity,Term)])
     swapMetas [] = return ([],[])
-    swapMetas ((plic, Var (Meta meta)):ms) =
+    swapMetas ((plic, Var (Meta Exist meta)):ms) =
       do (eqs,ms') <- swapMetas ms
-         return (eqs, (plic,Var (Meta meta)):ms')
+         return (eqs, (plic,Var (Meta Exist meta)):ms')
     swapMetas ((plic,m):ms) =
       do meta <- nextElab nextMeta
-         let x = Var (Meta meta)
+         let x = Var (Meta Exist meta)
          (eqs,ms') <- swapMetas ms
          return ((x,m):eqs, (plic,x):ms')
 
@@ -1124,7 +1124,7 @@ checkifyClause (Clause pscs sc) mot@(CaseMotive (BindingTelescope ascs _)) =
      l <- getElab quoteLevel
      ctx' <- forM ns $ \n ->
                do m <- nextElab nextMeta
-                  return (n, QLJ (Var (Meta m)) l)
+                  return (n, QLJ (Var (Meta Exist m)) l)
      extendElab context ctx' $
        do (ps',ElaboratedTerm ret) <-
             checkifyPatternsCaseMotive
diff --git a/src/Quasiquote/Unification/Unification.hs b/src/Quasiquote/Unification/Unification.hs
index 7216215..2bb222f 100644
--- a/src/Quasiquote/Unification/Unification.hs
+++ b/src/Quasiquote/Unification/Unification.hs
@@ -35,44 +35,44 @@ import Control.Monad.Except
 -- | Equating terms by trivial structural equations.
 
 instance MonadUnify TermF Elaborator where
-  equate (Defined n1) (Defined n2) =
+  equate _ (Defined n1) (Defined n2) =
     if n1 == n2
        then return []
        else throwError $ "Mismatching names "
                          ++ showName n1 ++ " and " ++ showName n2
-  equate (Ann m1 t1) (Ann m2 t2) =
-    return [ Equation (instantiate0 m1) (instantiate0 m2)
-           , Equation (instantiate0 t1) (instantiate0 t2)
+  equate f (Ann m1 t1) (Ann m2 t2) =
+    return [ Equation f (instantiate0 m1) (instantiate0 m2)
+           , Equation f (instantiate0 t1) (instantiate0 t2)
            ]
-  equate Type Type =
+  equate _ Type Type =
     return []
-  equate (Fun plic1 a1 sc1) (Fun plic2 a2 sc2) =
+  equate f (Fun plic1 a1 sc1) (Fun plic2 a2 sc2) =
     do unless (plic1 == plic2)
          $ throwError $ "Mismatching plicities when unifying "
              ++ pretty (In (Fun plic1 a1 sc1)) ++ " with "
              ++ pretty (In (Fun plic2 a2 sc2))
        ns <- freshRelTo (names sc1) context
        let xs = map (Var . Free) ns
-       return [ Equation (instantiate0 a1) (instantiate0 a2)
-              , Equation (instantiate sc1 xs) (instantiate sc2 xs)
+       return [ Equation f (instantiate0 a1) (instantiate0 a2)
+              , Equation f (instantiate sc1 xs) (instantiate sc2 xs)
               ]
-  equate (Lam plic1 sc1) (Lam plic2 sc2) =
+  equate f (Lam plic1 sc1) (Lam plic2 sc2) =
     do unless (plic1 == plic2)
          $ throwError $ "Mismatching plicities when unifying "
              ++ pretty (In (Lam plic1 sc1)) ++ " with "
              ++ pretty (In (Lam plic2 sc2))
        ns <- freshRelTo (names sc1) context
        let xs = map (Var . Free) ns
-       return [ Equation (instantiate sc1 xs) (instantiate sc2 xs) ]
-  equate (App plic1 f1 a1) (App plic2 f2 a2) =
+       return [ Equation f (instantiate sc1 xs) (instantiate sc2 xs) ]
+  equate _ (App plic1 f1 a1) (App plic2 f2 a2) =
     do unless (plic1 == plic2)
          $ throwError $ "Mismatching plicities when unifying "
              ++ pretty (In (App plic1 f1 a1)) ++ " with "
              ++ pretty (In (App plic2 f2 a2))
-       return [ Equation (instantiate0 f1) (instantiate0 f2)
-              , Equation (instantiate0 a1) (instantiate0 a2)
+       return [ Equation False (instantiate0 f1) (instantiate0 f2)
+              , Equation False (instantiate0 a1) (instantiate0 a2)
               ]
-  equate (Con c1 as1) (Con c2 as2) =
+  equate f (Con c1 as1) (Con c2 as2) =
     do unless (c1 == c2)
          $ throwError $ "Mismatching constructors "
                      ++ showName c1 ++ " and " ++ showName c2
@@ -87,10 +87,10 @@ instance MonadUnify TermF Elaborator where
              ++ pretty (In (Con c1 as1)) ++ " with "
              ++ pretty (In (Con c2 as2))
        return $ zipWith
-                  Equation
+                  (Equation f)
                   (map instantiate0 as1')
                   (map instantiate0 as2')
-  equate (Case as1 mot1 cs1) (Case as2 mot2 cs2) =
+  equate _ (Case as1 mot1 cs1) (Case as2 mot2 cs2) =
     do unless (length as1 == length as2)
          $ throwError $ "Mismatching number of case arguments in "
                      ++ pretty (In (Case as1 mot1 cs1)) ++ " and "
@@ -100,13 +100,13 @@ instance MonadUnify TermF Elaborator where
                      ++ pretty (In (Case as1 mot1 cs1)) ++ " and "
                      ++ pretty (In (Case as2 mot2 cs2))
        let argEqs = zipWith
-                      Equation
+                      (Equation False)
                         (map instantiate0 as1)
                         (map instantiate0 as2)
        motEqs <- equateCaseMotive mot1 mot2
        clauseEqs <- fmap concat $ zipWithM equateClause cs1 cs2
        return $ argEqs ++ motEqs ++ clauseEqs
-  equate (RecordType fields1 tele1) (RecordType fields2 tele2) =
+  equate f (RecordType fields1 tele1) (RecordType fields2 tele2) =
     do unless (fields1 == fields2)
          $ throwError $ "Record types have different field names: "
              ++ pretty (In (RecordType fields1 tele1))
@@ -121,8 +121,8 @@ instance MonadUnify TermF Elaborator where
              ++ pretty (In (RecordType fields1 tele1))
              ++ " and "
              ++ pretty (In (RecordType fields2 tele2))
-       return $ zipWith Equation as1 as2
-  equate (RecordCon fields1) (RecordCon fields2) =
+       return $ zipWith (Equation f) as1 as2
+  equate f (RecordCon fields1) (RecordCon fields2) =
     do unless (length fields1 == length fields2)
          $ throwError $ "Records have different number of fields: "
              ++ pretty (In (RecordCon fields1))
@@ -136,23 +136,23 @@ instance MonadUnify TermF Elaborator where
              ++ " and "
              ++ pretty (In (RecordCon fields2))
        return $ zipWith
-                  Equation
+                  (Equation f)
                   (map instantiate0 ms1)
                   (map instantiate0 ms2)
-  equate (RecordProj r1 x1) (RecordProj r2 x2) =
+  equate _ (RecordProj r1 x1) (RecordProj r2 x2) =
     do unless (x1 == x2)
          $ throwError $ "Record projections have different names: "
              ++ pretty (In (RecordProj r1 x1))
              ++ " and "
              ++ pretty (In (RecordProj r2 x2))
-       return [Equation (instantiate0 r1) (instantiate0 r2)]
-  equate (QuotedType a1) (QuotedType a2) =
-    return [Equation (instantiate0 a1) (instantiate0 a2)]
-  equate (Quote m1) (Quote m2) =
-    return [Equation (instantiate0 m1) (instantiate0 m2)]
-  equate (Unquote m1) (Unquote m2) =
-    return [Equation (instantiate0 m1) (instantiate0 m2)]
-  equate l r =
+       return [Equation False (instantiate0 r1) (instantiate0 r2)]
+  equate _ (QuotedType a1) (QuotedType a2) =
+    return [Equation False (instantiate0 a1) (instantiate0 a2)]
+  equate _ (Quote m1) (Quote m2) =
+    return [Equation False (instantiate0 m1) (instantiate0 m2)]
+  equate _ (Unquote m1) (Unquote m2) =
+    return [Equation False (instantiate0 m1) (instantiate0 m2)]
+  equate _ l r =
     throwError $ "Cannot unify " ++ pretty (In l) ++ " with " ++ pretty (In r)
 
 
@@ -170,7 +170,7 @@ equateCaseMotive mot1@(CaseMotive tele1) mot2@(CaseMotive tele2) =
      unless (length as1 == length as2)
        $ throwError $ "Motives not equal: " ++ pretty mot1 ++ " and "
                    ++ pretty mot2
-     return $ zipWith Equation as1 as2 ++ [ Equation b1 b2 ]
+     return $ zipWith (Equation False) as1 as2 ++ [ Equation False b1 b2 ]
      
 
 
@@ -195,5 +195,5 @@ equateClause (Clause pscs1 sc1) (Clause pscs2 sc2) =
        Nothing ->
          throwError "Patterns are not equal."
        Just pEqss ->
-         return $ [ Equation a1 a2 | (a1,a2) <- concat pEqss ]
-               ++ [ Equation b1 b2 ]
\ No newline at end of file
+         return $ [ Equation False a1 a2 | (a1,a2) <- concat pEqss ]
+               ++ [ Equation False b1 b2 ]
diff --git a/src/Record/Unification/TypeChecking.hs b/src/Record/Unification/TypeChecking.hs
index 38b6d4f..ce649b2 100644
--- a/src/Record/Unification/TypeChecking.hs
+++ b/src/Record/Unification/TypeChecking.hs
@@ -245,7 +245,7 @@ inferify (Var (Free x)) =
      return (ElaboratedTerm (Var (Free x)), t)
 inferify (Var (Bound _ _)) =
   error "Bound type variables should not be the subject of type checking."
-inferify (Var (Meta x)) =
+inferify (Var (Meta _ x)) =
   throwError $ "The metavariable " ++ show x
             ++ " appears in checkable code, when it should not."
 inferify (In (Defined x)) =
@@ -392,8 +392,8 @@ inferifyApplication f (In (Fun Expl _ _)) Impl m =
     ++ pretty (appH Impl f m)
 inferifyApplication f (In (Fun Impl _ sc)) Expl m =
   do meta <- nextElab nextMeta
-     let f' = appH Impl f (Var (Meta meta))
-         t' = instantiate sc [Var (Meta meta)]
+     let f' = appH Impl f (Var (Meta Exist meta))
+         t' = instantiate sc [Var (Meta Exist meta)]
      inferifyApplication  f' t' Expl m
 inferifyApplication f _ _ _ =
   throwError $ "Cannot apply non-function: " ++ pretty f
@@ -450,7 +450,7 @@ inferifyConArgs ascs0 bsc0 ms0 = go [] ascs0 bsc0 ms0
          go (acc ++ [(Impl,m')]) ascs bsc ms
     go acc ((Impl,_):ascs) bsc ms =
       do meta <- nextElab nextMeta
-         go (acc ++ [(Impl,Var (Meta meta))]) ascs bsc ms
+         go (acc ++ [(Impl,Var (Meta Exist meta))]) ascs bsc ms
     go _ _ _ _ =
       throwError "Cannot match signature."
 
@@ -710,7 +710,7 @@ checkifyConArgs ascs0 bsc ms0 t =
       return acc
     accArgsToCheck acc ((Expl,asc):ascs) ((Expl,m):ms) =
       do meta <- nextElab nextMeta
-         let x = Var (Meta meta)
+         let x = Var (Meta Exist meta)
              xs = [ x' | (_,_,x',_) <- acc ]
              newSuspension = (Expl, Just m, x, instantiate asc xs)
          accArgsToCheck
@@ -719,7 +719,7 @@ checkifyConArgs ascs0 bsc ms0 t =
            ms
     accArgsToCheck acc ((Impl,asc):ascs) ((Impl,m):ms) =
       do meta <- nextElab nextMeta
-         let x = Var (Meta meta)
+         let x = Var (Meta Exist meta)
              xs = [ x' | (_,_,x',_) <- acc ]
              newSuspension = (Impl, Just m, x, instantiate asc xs)
          accArgsToCheck
@@ -728,7 +728,7 @@ checkifyConArgs ascs0 bsc ms0 t =
            ms
     accArgsToCheck acc ((Impl,asc):ascs) ms =
       do meta <- nextElab nextMeta
-         let x = Var (Meta meta)
+         let x = Var (Meta Exist meta)
              xs = [ x' | (_,_,x',_) <- acc ]
              newSuspension = (Impl, Nothing, x, instantiate asc xs)
          accArgsToCheck
@@ -741,12 +741,12 @@ checkifyConArgs ascs0 bsc ms0 t =
     swapMetas :: [(Plicity,Term)]
               -> TypeChecker ([(Term,Term)], [(Plicity,Term)])
     swapMetas [] = return ([],[])
-    swapMetas ((plic, Var (Meta meta)):ms) =
+    swapMetas ((plic, Var (Meta Exist meta)):ms) =
       do (eqs,ms') <- swapMetas ms
-         return (eqs, (plic,Var (Meta meta)):ms')
+         return (eqs, (plic,Var (Meta Exist meta)):ms')
     swapMetas ((plic,m):ms) =
       do meta <- nextElab nextMeta
-         let x = Var (Meta meta)
+         let x = Var (Meta Exist meta)
          (eqs,ms') <- swapMetas ms
          return ((x,m):eqs, (plic,x):ms')
      
@@ -812,7 +812,7 @@ checkifyPattern (Var (Free x)) t =
             , ElaboratedTerm (Var (Free x))
             , []
             )
-checkifyPattern (Var (Meta _)) _ =
+checkifyPattern (Var (Meta _ _)) _ =
   error "Metavariables should not be the subject of pattern type checking."
 checkifyPattern (In (ConPat c ps)) (NormalTerm t) =
   do (ec,ConSig plics (BindingTelescope ascs bsc)) <- typeInSignature c
@@ -831,12 +831,12 @@ checkifyPattern (In (AssertionPat m)) t =
   do ElaboratedTerm m' <- checkify m t
      mv <- nextElab nextMeta
      return ( In (AssertionPat m')
-            , ElaboratedTerm (Var $ Meta mv)
-            , [(Var $ Meta mv, m')]
+            , ElaboratedTerm (Var $ Meta Constraint mv)
+            , [(Var $ Meta Constraint mv, m')]
             )
 checkifyPattern (In MakeMeta) _ =
   do meta <- nextElab nextMeta
-     let x = Var (Meta meta)
+     let x = Var (Meta Exist meta)
      return ( In (AssertionPat x)
             , ElaboratedTerm x
             , []
@@ -931,7 +931,7 @@ checkifyPatterns ascs0 bsc ps0 t =
       return acc
     accArgsToCheck acc ((Expl,asc):ascs) ((Expl,p):ps) =
       do meta <- nextElab nextMeta
-         let x = Var (Meta meta)
+         let x = Var (Meta Exist meta)
              xs = [ x' | (_,_,x',_) <- acc ]
              newSuspension = (Expl, Just p, x, instantiate asc xs)
          accArgsToCheck
@@ -940,7 +940,7 @@ checkifyPatterns ascs0 bsc ps0 t =
            ps
     accArgsToCheck acc ((Impl,asc):ascs) ((Impl,p):ps) =
       do meta <- nextElab nextMeta
-         let x = Var (Meta meta)
+         let x = Var (Meta Exist meta)
              xs = [ x' | (_,_,x',_) <- acc ]
              newSuspension = (Impl, Just p, x, instantiate asc xs)
          accArgsToCheck
@@ -949,7 +949,7 @@ checkifyPatterns ascs0 bsc ps0 t =
            ps
     accArgsToCheck acc ((Impl,asc):ascs) ps =
       do meta <- nextElab nextMeta
-         let x = Var (Meta meta)
+         let x = Var (Meta Exist meta)
              xs = [ x' | (_,_,x',_) <- acc ]
              newSuspension = (Impl, Nothing, x, instantiate asc xs)
          accArgsToCheck
@@ -962,12 +962,12 @@ checkifyPatterns ascs0 bsc ps0 t =
     swapMetas :: [(Plicity,Term)]
               -> TypeChecker ([(Term,Term)], [(Plicity,Term)])
     swapMetas [] = return ([],[])
-    swapMetas ((plic, Var (Meta meta)):ms) =
+    swapMetas ((plic, Var (Meta Exist meta)):ms) =
       do (eqs,ms') <- swapMetas ms
-         return (eqs, (plic,Var (Meta meta)):ms')
+         return (eqs, (plic,Var (Meta Exist meta)):ms')
     swapMetas ((plic,m):ms) =
       do meta <- nextElab nextMeta
-         let x = Var (Meta meta)
+         let x = Var (Meta Exist meta)
          (eqs,ms') <- swapMetas ms
          return ((x,m):eqs, (plic,x):ms')
 
@@ -1053,7 +1053,7 @@ checkifyClause (Clause pscs sc) mot@(CaseMotive (BindingTelescope ascs _)) =
          xs2 = map (Var . Free) ns
      ctx' <- forM ns $ \n ->
                do m <- nextElab nextMeta
-                  return (n, Var (Meta m))
+                  return (n, Var (Meta Exist m))
      extendElab context ctx' $
        do (ps',ElaboratedTerm ret) <-
             checkifyPatternsCaseMotive
diff --git a/src/Record/Unification/Unification.hs b/src/Record/Unification/Unification.hs
index 1ce54eb..5b84fd0 100644
--- a/src/Record/Unification/Unification.hs
+++ b/src/Record/Unification/Unification.hs
@@ -35,44 +35,44 @@ import Control.Monad.Except
 -- | Equating terms by trivial structural equations.
 
 instance MonadUnify TermF Elaborator where
-  equate (Defined n1) (Defined n2) =
+  equate _ (Defined n1) (Defined n2) =
     if n1 == n2
        then return []
        else throwError $ "Mismatching names "
                          ++ showName n1 ++ " and " ++ showName n2
-  equate (Ann m1 t1) (Ann m2 t2) =
-    return [ Equation (instantiate0 m1) (instantiate0 m2)
-           , Equation (instantiate0 t1) (instantiate0 t2)
+  equate f (Ann m1 t1) (Ann m2 t2) =
+    return [ Equation f (instantiate0 m1) (instantiate0 m2)
+           , Equation f (instantiate0 t1) (instantiate0 t2)
            ]
-  equate Type Type =
+  equate _ Type Type =
     return []
-  equate (Fun plic1 a1 sc1) (Fun plic2 a2 sc2) =
+  equate f (Fun plic1 a1 sc1) (Fun plic2 a2 sc2) =
     do unless (plic1 == plic2)
          $ throwError $ "Mismatching plicities when unifying "
              ++ pretty (In (Fun plic1 a1 sc1)) ++ " with "
              ++ pretty (In (Fun plic2 a2 sc2))
        ns <- freshRelTo (names sc1) context
        let xs = map (Var . Free) ns
-       return [ Equation (instantiate0 a1) (instantiate0 a2)
-              , Equation (instantiate sc1 xs) (instantiate sc2 xs)
+       return [ Equation f (instantiate0 a1) (instantiate0 a2)
+              , Equation f (instantiate sc1 xs) (instantiate sc2 xs)
               ]
-  equate (Lam plic1 sc1) (Lam plic2 sc2) =
+  equate f (Lam plic1 sc1) (Lam plic2 sc2) =
     do unless (plic1 == plic2)
          $ throwError $ "Mismatching plicities when unifying "
              ++ pretty (In (Lam plic1 sc1)) ++ " with "
              ++ pretty (In (Lam plic2 sc2))
        ns <- freshRelTo (names sc1) context
        let xs = map (Var . Free) ns
-       return [ Equation (instantiate sc1 xs) (instantiate sc2 xs) ]
-  equate (App plic1 f1 a1) (App plic2 f2 a2) =
+       return [ Equation f (instantiate sc1 xs) (instantiate sc2 xs) ]
+  equate _ (App plic1 f1 a1) (App plic2 f2 a2) =
     do unless (plic1 == plic2)
          $ throwError $ "Mismatching plicities when unifying "
              ++ pretty (In (App plic1 f1 a1)) ++ " with "
              ++ pretty (In (App plic2 f2 a2))
-       return [ Equation (instantiate0 f1) (instantiate0 f2)
-              , Equation (instantiate0 a1) (instantiate0 a2)
+       return [ Equation False (instantiate0 f1) (instantiate0 f2)
+              , Equation False (instantiate0 a1) (instantiate0 a2)
               ]
-  equate (Con c1 as1) (Con c2 as2) =
+  equate f (Con c1 as1) (Con c2 as2) =
     do unless (c1 == c2)
          $ throwError $ "Mismatching constructors "
                      ++ showName c1 ++ " and " ++ showName c2
@@ -87,10 +87,10 @@ instance MonadUnify TermF Elaborator where
              ++ pretty (In (Con c1 as1)) ++ " with "
              ++ pretty (In (Con c2 as2))
        return $ zipWith
-                  Equation
+                  (Equation f)
                   (map instantiate0 as1')
                   (map instantiate0 as2')
-  equate (Case as1 mot1 cs1) (Case as2 mot2 cs2) =
+  equate _ (Case as1 mot1 cs1) (Case as2 mot2 cs2) =
     do unless (length as1 == length as2)
          $ throwError $ "Mismatching number of case arguments in "
                      ++ pretty (In (Case as1 mot1 cs1)) ++ " and "
@@ -100,13 +100,13 @@ instance MonadUnify TermF Elaborator where
                      ++ pretty (In (Case as1 mot1 cs1)) ++ " and "
                      ++ pretty (In (Case as2 mot2 cs2))
        let argEqs = zipWith
-                      Equation
+                      (Equation False)
                         (map instantiate0 as1)
                         (map instantiate0 as2)
        motEqs <- equateCaseMotive mot1 mot2
        clauseEqs <- fmap concat $ zipWithM equateClause cs1 cs2
        return $ argEqs ++ motEqs ++ clauseEqs
-  equate (RecordType fields1 tele1) (RecordType fields2 tele2) =
+  equate f (RecordType fields1 tele1) (RecordType fields2 tele2) =
     do unless (fields1 == fields2)
          $ throwError $ "Record types have different field names: "
              ++ pretty (In (RecordType fields1 tele1))
@@ -121,8 +121,8 @@ instance MonadUnify TermF Elaborator where
              ++ pretty (In (RecordType fields1 tele1))
              ++ " and "
              ++ pretty (In (RecordType fields2 tele2))
-       return $ zipWith Equation as1 as2
-  equate (RecordCon fields1) (RecordCon fields2) =
+       return $ zipWith (Equation f) as1 as2
+  equate f (RecordCon fields1) (RecordCon fields2) =
     do unless (length fields1 == length fields2)
          $ throwError $ "Records have different number of fields: "
              ++ pretty (In (RecordCon fields1))
@@ -136,17 +136,17 @@ instance MonadUnify TermF Elaborator where
              ++ " and "
              ++ pretty (In (RecordCon fields2))
        return $ zipWith
-                  Equation
+                  (Equation f)
                   (map instantiate0 ms1)
                   (map instantiate0 ms2)
-  equate (RecordProj r1 x1) (RecordProj r2 x2) =
+  equate _ (RecordProj r1 x1) (RecordProj r2 x2) =
     do unless (x1 == x2)
          $ throwError $ "Record projections have different names: "
              ++ pretty (In (RecordProj r1 x1))
              ++ " and "
              ++ pretty (In (RecordProj r2 x2))
-       return [Equation (instantiate0 r1) (instantiate0 r2)]
-  equate l r =
+       return [Equation False (instantiate0 r1) (instantiate0 r2)]
+  equate _ l r =
     throwError $ "Cannot unify " ++ pretty (In l) ++ " with " ++ pretty (In r)
 
 
@@ -164,7 +164,7 @@ equateCaseMotive mot1@(CaseMotive tele1) mot2@(CaseMotive tele2) =
      unless (length as1 == length as2)
        $ throwError $ "Motives not equal: " ++ pretty mot1 ++ " and "
                    ++ pretty mot2
-     return $ zipWith Equation as1 as2 ++ [ Equation b1 b2 ]
+     return $ zipWith (Equation False) as1 as2 ++ [ Equation False b1 b2 ]
      
 
 
@@ -189,5 +189,5 @@ equateClause (Clause pscs1 sc1) (Clause pscs2 sc2) =
        Nothing ->
          throwError "Patterns are not equal."
        Just pEqss ->
-         return $ [ Equation a1 a2 | (a1,a2) <- concat pEqss ]
-               ++ [ Equation b1 b2 ]
\ No newline at end of file
+         return $ [ Equation False a1 a2 | (a1,a2) <- concat pEqss ]
+               ++ [ Equation False b1 b2 ]
diff --git a/src/Require/Unification/TypeChecking.hs b/src/Require/Unification/TypeChecking.hs
index b4eff03..384270b 100644
--- a/src/Require/Unification/TypeChecking.hs
+++ b/src/Require/Unification/TypeChecking.hs
@@ -344,7 +344,7 @@ inferify (Var (Free x)) =
      return (ElaboratedTerm (Var (Free x)), t)
 inferify (Var (Bound _ _)) =
   error "Bound type variables should not be the subject of type checking."
-inferify (Var (Meta x)) =
+inferify (Var (Meta _ x)) =
   throwError $ "The metavariable " ++ show x
             ++ " appears in checkable code, when it should not."
 inferify (In (Defined x)) =
@@ -552,8 +552,8 @@ inferifyApplication f (In (Fun Expl _ _)) Impl m =
     ++ pretty (appH Impl f m)
 inferifyApplication f (In (Fun Impl _ sc)) Expl m =
   do meta <- nextElab nextMeta
-     let f' = appH Impl f (Var (Meta meta))
-         t' = instantiate sc [Var (Meta meta)]
+     let f' = appH Impl f (Var (Meta Exist meta))
+         t' = instantiate sc [Var (Meta Exist meta)]
      inferifyApplication  f' t' Expl m
 inferifyApplication f _ _ _ =
   throwError $ "Cannot apply non-function: " ++ pretty f
@@ -610,7 +610,7 @@ inferifyConArgs ascs0 bsc0 ms0 = go [] ascs0 bsc0 ms0
          go (acc ++ [(Impl,m')]) ascs bsc ms
     go acc ((Impl,_):ascs) bsc ms =
       do meta <- nextElab nextMeta
-         go (acc ++ [(Impl,Var (Meta meta))]) ascs bsc ms
+         go (acc ++ [(Impl,Var (Meta Exist meta))]) ascs bsc ms
     go _ _ _ _ =
       throwError "Cannot match signature."
 
@@ -903,7 +903,7 @@ checkifyConArgs ascs0 bsc ms0 t =
       return acc
     accArgsToCheck acc ((Expl,asc):ascs) ((Expl,m):ms) =
       do meta <- nextElab nextMeta
-         let x = Var (Meta meta)
+         let x = Var (Meta Exist meta)
              xs = [ x' | (_,_,x',_) <- acc ]
              newSuspension = (Expl, Just m, x, instantiate asc xs)
          accArgsToCheck
@@ -912,7 +912,7 @@ checkifyConArgs ascs0 bsc ms0 t =
            ms
     accArgsToCheck acc ((Impl,asc):ascs) ((Impl,m):ms) =
       do meta <- nextElab nextMeta
-         let x = Var (Meta meta)
+         let x = Var (Meta Exist meta)
              xs = [ x' | (_,_,x',_) <- acc ]
              newSuspension = (Impl, Just m, x, instantiate asc xs)
          accArgsToCheck
@@ -921,7 +921,7 @@ checkifyConArgs ascs0 bsc ms0 t =
            ms
     accArgsToCheck acc ((Impl,asc):ascs) ms =
       do meta <- nextElab nextMeta
-         let x = Var (Meta meta)
+         let x = Var (Meta Exist meta)
              xs = [ x' | (_,_,x',_) <- acc ]
              newSuspension = (Impl, Nothing, x, instantiate asc xs)
          accArgsToCheck
@@ -934,12 +934,12 @@ checkifyConArgs ascs0 bsc ms0 t =
     swapMetas :: [(Plicity,Term)]
               -> TypeChecker ([(Term,Term)], [(Plicity,Term)])
     swapMetas [] = return ([],[])
-    swapMetas ((plic, Var (Meta meta)):ms) =
+    swapMetas ((plic, Var (Meta Exist meta)):ms) =
       do (eqs,ms') <- swapMetas ms
-         return (eqs, (plic,Var (Meta meta)):ms')
+         return (eqs, (plic,Var (Meta Exist meta)):ms')
     swapMetas ((plic,m):ms) =
       do meta <- nextElab nextMeta
-         let x = Var (Meta meta)
+         let x = Var (Meta Exist meta)
          (eqs,ms') <- swapMetas ms
          return ((x,m):eqs, (plic,x):ms')
      
@@ -1005,7 +1005,7 @@ checkifyPattern (Var (Free x)) t =
             , ElaboratedTerm (Var (Free x))
             , []
             )
-checkifyPattern (Var (Meta _)) _ =
+checkifyPattern (Var (Meta _ _)) _ =
   error "Metavariables should not be the subject of pattern type checking."
 checkifyPattern (In (ConPat c ps)) (NormalTerm t) =
   do (ec,ConSig plics (BindingTelescope ascs bsc)) <- typeInSignature c
@@ -1024,12 +1024,12 @@ checkifyPattern (In (AssertionPat m)) t =
   do ElaboratedTerm m' <- checkify m t
      mv <- nextElab nextMeta
      return ( In (AssertionPat m')
-            , ElaboratedTerm (Var $ Meta mv)
-            , [(Var $ Meta mv, m')]
+            , ElaboratedTerm (Var $ Meta Constraint mv)
+            , [(Var $ Meta Constraint mv, m')]
             )
 checkifyPattern (In MakeMeta) _ =
   do meta <- nextElab nextMeta
-     let x = Var (Meta meta)
+     let x = Var (Meta Exist meta)
      return ( In (AssertionPat x)
             , ElaboratedTerm x
             , []
@@ -1124,7 +1124,7 @@ checkifyPatterns ascs0 bsc ps0 t =
       return acc
     accArgsToCheck acc ((Expl,asc):ascs) ((Expl,p):ps) =
       do meta <- nextElab nextMeta
-         let x = Var (Meta meta)
+         let x = Var (Meta Exist meta)
              xs = [ x' | (_,_,x',_) <- acc ]
              newSuspension = (Expl, Just p, x, instantiate asc xs)
          accArgsToCheck
@@ -1133,7 +1133,7 @@ checkifyPatterns ascs0 bsc ps0 t =
            ps
     accArgsToCheck acc ((Impl,asc):ascs) ((Impl,p):ps) =
       do meta <- nextElab nextMeta
-         let x = Var (Meta meta)
+         let x = Var (Meta Exist meta)
              xs = [ x' | (_,_,x',_) <- acc ]
              newSuspension = (Impl, Just p, x, instantiate asc xs)
          accArgsToCheck
@@ -1142,7 +1142,7 @@ checkifyPatterns ascs0 bsc ps0 t =
            ps
     accArgsToCheck acc ((Impl,asc):ascs) ps =
       do meta <- nextElab nextMeta
-         let x = Var (Meta meta)
+         let x = Var (Meta Exist meta)
              xs = [ x' | (_,_,x',_) <- acc ]
              newSuspension = (Impl, Nothing, x, instantiate asc xs)
          accArgsToCheck
@@ -1155,12 +1155,12 @@ checkifyPatterns ascs0 bsc ps0 t =
     swapMetas :: [(Plicity,Term)]
               -> TypeChecker ([(Term,Term)], [(Plicity,Term)])
     swapMetas [] = return ([],[])
-    swapMetas ((plic, Var (Meta meta)):ms) =
+    swapMetas ((plic, Var (Meta Exist meta)):ms) =
       do (eqs,ms') <- swapMetas ms
-         return (eqs, (plic,Var (Meta meta)):ms')
+         return (eqs, (plic,Var (Meta Exist meta)):ms')
     swapMetas ((plic,m):ms) =
       do meta <- nextElab nextMeta
-         let x = Var (Meta meta)
+         let x = Var (Meta Exist meta)
          (eqs,ms') <- swapMetas ms
          return ((x,m):eqs, (plic,x):ms')
 
@@ -1247,7 +1247,7 @@ checkifyClause (Clause pscs sc) mot@(CaseMotive (BindingTelescope ascs _)) =
      l <- getElab quoteLevel
      ctx' <- forM ns $ \n ->
                do m <- nextElab nextMeta
-                  return (n, QLJ (Var (Meta m)) l)
+                  return (n, QLJ (Var (Meta Exist m)) l)
      extendElab context ctx' $
        do (ps',ElaboratedTerm ret) <-
             checkifyPatternsCaseMotive
diff --git a/src/Require/Unification/Unification.hs b/src/Require/Unification/Unification.hs
index 9654fbb..c58c835 100644
--- a/src/Require/Unification/Unification.hs
+++ b/src/Require/Unification/Unification.hs
@@ -35,44 +35,44 @@ import Control.Monad.Except
 -- | Equating terms by trivial structural equations.
 
 instance MonadUnify TermF Elaborator where
-  equate (Defined n1) (Defined n2) =
+  equate _ (Defined n1) (Defined n2) =
     if n1 == n2
        then return []
        else throwError $ "Mismatching names "
                          ++ showName n1 ++ " and " ++ showName n2
-  equate (Ann m1 t1) (Ann m2 t2) =
-    return [ Equation (instantiate0 m1) (instantiate0 m2)
-           , Equation (instantiate0 t1) (instantiate0 t2)
+  equate f (Ann m1 t1) (Ann m2 t2) =
+    return [ Equation f (instantiate0 m1) (instantiate0 m2)
+           , Equation f (instantiate0 t1) (instantiate0 t2)
            ]
-  equate Type Type =
+  equate _ Type Type =
     return []
-  equate (Fun plic1 a1 sc1) (Fun plic2 a2 sc2) =
+  equate f (Fun plic1 a1 sc1) (Fun plic2 a2 sc2) =
     do unless (plic1 == plic2)
          $ throwError $ "Mismatching plicities when unifying "
              ++ pretty (In (Fun plic1 a1 sc1)) ++ " with "
              ++ pretty (In (Fun plic2 a2 sc2))
        ns <- freshRelTo (names sc1) context
        let xs = map (Var . Free) ns
-       return [ Equation (instantiate0 a1) (instantiate0 a2)
-              , Equation (instantiate sc1 xs) (instantiate sc2 xs)
+       return [ Equation f (instantiate0 a1) (instantiate0 a2)
+              , Equation f (instantiate sc1 xs) (instantiate sc2 xs)
               ]
-  equate (Lam plic1 sc1) (Lam plic2 sc2) =
+  equate f (Lam plic1 sc1) (Lam plic2 sc2) =
     do unless (plic1 == plic2)
          $ throwError $ "Mismatching plicities when unifying "
              ++ pretty (In (Lam plic1 sc1)) ++ " with "
              ++ pretty (In (Lam plic2 sc2))
        ns <- freshRelTo (names sc1) context
        let xs = map (Var . Free) ns
-       return [ Equation (instantiate sc1 xs) (instantiate sc2 xs) ]
-  equate (App plic1 f1 a1) (App plic2 f2 a2) =
+       return [ Equation f (instantiate sc1 xs) (instantiate sc2 xs) ]
+  equate _ (App plic1 f1 a1) (App plic2 f2 a2) =
     do unless (plic1 == plic2)
          $ throwError $ "Mismatching plicities when unifying "
              ++ pretty (In (App plic1 f1 a1)) ++ " with "
              ++ pretty (In (App plic2 f2 a2))
-       return [ Equation (instantiate0 f1) (instantiate0 f2)
-              , Equation (instantiate0 a1) (instantiate0 a2)
+       return [ Equation False (instantiate0 f1) (instantiate0 f2)
+              , Equation False (instantiate0 a1) (instantiate0 a2)
               ]
-  equate (Con c1 as1) (Con c2 as2) =
+  equate f (Con c1 as1) (Con c2 as2) =
     do unless (c1 == c2)
          $ throwError $ "Mismatching constructors "
                      ++ showName c1 ++ " and " ++ showName c2
@@ -87,10 +87,10 @@ instance MonadUnify TermF Elaborator where
              ++ pretty (In (Con c1 as1)) ++ " with "
              ++ pretty (In (Con c2 as2))
        return $ zipWith
-                  Equation
+                  (Equation f)
                   (map instantiate0 as1')
                   (map instantiate0 as2')
-  equate (Case as1 mot1 cs1) (Case as2 mot2 cs2) =
+  equate _ (Case as1 mot1 cs1) (Case as2 mot2 cs2) =
     do unless (length as1 == length as2)
          $ throwError $ "Mismatching number of case arguments in "
                      ++ pretty (In (Case as1 mot1 cs1)) ++ " and "
@@ -100,13 +100,13 @@ instance MonadUnify TermF Elaborator where
                      ++ pretty (In (Case as1 mot1 cs1)) ++ " and "
                      ++ pretty (In (Case as2 mot2 cs2))
        let argEqs = zipWith
-                      Equation
+                      (Equation False)
                         (map instantiate0 as1)
                         (map instantiate0 as2)
        motEqs <- equateCaseMotive mot1 mot2
        clauseEqs <- fmap concat $ zipWithM equateClause cs1 cs2
        return $ argEqs ++ motEqs ++ clauseEqs
-  equate (RecordType fields1 tele1) (RecordType fields2 tele2) =
+  equate f (RecordType fields1 tele1) (RecordType fields2 tele2) =
     do unless (fields1 == fields2)
          $ throwError $ "Record types have different field names: "
              ++ pretty (In (RecordType fields1 tele1))
@@ -121,8 +121,8 @@ instance MonadUnify TermF Elaborator where
              ++ pretty (In (RecordType fields1 tele1))
              ++ " and "
              ++ pretty (In (RecordType fields2 tele2))
-       return $ zipWith Equation as1 as2
-  equate (RecordCon fields1) (RecordCon fields2) =
+       return $ zipWith (Equation f) as1 as2
+  equate f (RecordCon fields1) (RecordCon fields2) =
     do unless (length fields1 == length fields2)
          $ throwError $ "Records have different number of fields: "
              ++ pretty (In (RecordCon fields1))
@@ -136,44 +136,44 @@ instance MonadUnify TermF Elaborator where
              ++ " and "
              ++ pretty (In (RecordCon fields2))
        return $ zipWith
-                  Equation
+                  (Equation f)
                   (map instantiate0 ms1)
                   (map instantiate0 ms2)
-  equate (RecordProj r1 x1) (RecordProj r2 x2) =
+  equate _ (RecordProj r1 x1) (RecordProj r2 x2) =
     do unless (x1 == x2)
          $ throwError $ "Record projections have different names: "
              ++ pretty (In (RecordProj r1 x1))
              ++ " and "
              ++ pretty (In (RecordProj r2 x2))
-       return [Equation (instantiate0 r1) (instantiate0 r2)]
-  equate (QuotedType res1 a1) (QuotedType res2 a2) =
+       return [Equation False (instantiate0 r1) (instantiate0 r2)]
+  equate _ (QuotedType res1 a1) (QuotedType res2 a2) =
     do unless (res1 == res2)
          $ throwError $ "Quoted types have different reset locations: "
              ++ pretty (In (QuotedType res1 a1))
              ++ " and "
              ++ pretty (In (QuotedType res2 a2))
-       return [Equation (instantiate0 a1) (instantiate0 a2)]
-  equate (Quote m1) (Quote m2) =
-    return [Equation (instantiate0 m1) (instantiate0 m2)]
-  equate (Unquote m1) (Unquote m2) =
-    return [Equation (instantiate0 m1) (instantiate0 m2)]
-  equate (Continue m1) (Continue m2) =
-    return [Equation (instantiate0 m1) (instantiate0 m2)]
-  equate (Shift res1 m1) (Shift res2 m2) =
+       return [Equation False (instantiate0 a1) (instantiate0 a2)]
+  equate _ (Quote m1) (Quote m2) =
+    return [Equation False (instantiate0 m1) (instantiate0 m2)]
+  equate _ (Unquote m1) (Unquote m2) =
+    return [Equation False (instantiate0 m1) (instantiate0 m2)]
+  equate _ (Continue m1) (Continue m2) =
+    return [Equation False (instantiate0 m1) (instantiate0 m2)]
+  equate _ (Shift res1 m1) (Shift res2 m2) =
     do unless (res1 == res2)
          $ throwError "Shifts have different reset locations."
-       return [Equation (instantiate0 m1) (instantiate0 m2)]
-  equate (Reset res1 m1) (Reset res2 m2) =
+       return [Equation False (instantiate0 m1) (instantiate0 m2)]
+  equate _ (Reset res1 m1) (Reset res2 m2) =
     do unless (res1 == res2)
          $ throwError "Resets have different reset locations."
-       return [Equation (instantiate0 m1) (instantiate0 m2)]
-  equate (Require a1 sc1) (Require a2 sc2) =
+       return [Equation False (instantiate0 m1) (instantiate0 m2)]
+  equate _ (Require a1 sc1) (Require a2 sc2) =
     do ns <- freshRelTo (names sc1) context
        let xs = map (Var . Free) ns
-       return [ Equation (instantiate0 a1) (instantiate0 a2)
-              , Equation (instantiate sc1 xs) (instantiate sc2 xs)
+       return [ Equation False (instantiate0 a1) (instantiate0 a2)
+              , Equation False (instantiate sc1 xs) (instantiate sc2 xs)
               ]
-  equate l r =
+  equate _ l r =
     throwError $ "Cannot unify " ++ pretty (In l) ++ " with " ++ pretty (In r)
 
 
@@ -191,7 +191,7 @@ equateCaseMotive mot1@(CaseMotive tele1) mot2@(CaseMotive tele2) =
      unless (length as1 == length as2)
        $ throwError $ "Motives not equal: " ++ pretty mot1 ++ " and "
                    ++ pretty mot2
-     return $ zipWith Equation as1 as2 ++ [ Equation b1 b2 ]
+     return $ zipWith (Equation False) as1 as2 ++ [ Equation False b1 b2 ]
      
 
 
@@ -216,5 +216,5 @@ equateClause (Clause pscs1 sc1) (Clause pscs2 sc2) =
        Nothing ->
          throwError "Patterns are not equal."
        Just pEqss ->
-         return $ [ Equation a1 a2 | (a1,a2) <- concat pEqss ]
-               ++ [ Equation b1 b2 ]
\ No newline at end of file
+         return $ [ Equation False a1 a2 | (a1,a2) <- concat pEqss ]
+               ++ [ Equation False b1 b2 ]
diff --git a/src/Simple/Monadic/TypeChecking.hs b/src/Simple/Monadic/TypeChecking.hs
index b5faa34..a0d7f18 100644
--- a/src/Simple/Monadic/TypeChecking.hs
+++ b/src/Simple/Monadic/TypeChecking.hs
@@ -140,7 +140,7 @@ infer (Var (Bound _ _)) =
   error "A bound variable should never be the subject of type inference."
 infer (Var (Free x)) =
   typeInContext x
-infer (Var (Meta _)) =
+infer (Var (Meta _ _)) =
   error "Metavariables should not occur in this type checker."
 infer (In (Defined n)) =
   typeInDefinitions n
@@ -275,7 +275,7 @@ checkPattern (Var (Bound _ _)) _ =
   error "A bound variable should never be the subject of type checking."
 checkPattern (Var (Free x)) t =
   return [(x,t)]
-checkPattern (Var (Meta _)) _ =
+checkPattern (Var (Meta _ _)) _ =
   error "Metavariables should not occur in this type checker."
 checkPattern (In (ConPat c ps)) t =
   do ConSig args ret <- typeInSignature c
diff --git a/src/Simple/Unification/TypeChecking.hs b/src/Simple/Unification/TypeChecking.hs
index 96b552f..03ea8d1 100644
--- a/src/Simple/Unification/TypeChecking.hs
+++ b/src/Simple/Unification/TypeChecking.hs
@@ -142,7 +142,7 @@ inferify (Var (Bound _ _)) =
   error "A bound variable should never be the subject of type inference."
 inferify (Var (Free x)) =
   typeInContext x
-inferify (Var (Meta _)) =
+inferify (Var (Meta _ _)) =
   error "Metavariables should not occur in this type checker."
 inferify (In (Defined x)) =
   typeInDefinitions x
@@ -152,7 +152,7 @@ inferify (In (Ann m t)) =
 inferify (In (Lam sc)) =
   do [n] <- freshRelTo (names sc) context
      meta <- nextElab nextMeta
-     let arg = Var (Meta meta)
+     let arg = Var (Meta Exist meta)
      ret <- extendElab context [(n, arg)]
               $ inferify (instantiate sc [Var (Free n)])
      subs <- getElab substitution
@@ -203,7 +203,7 @@ inferifyClause patTys (Clause pscs sc) =
          xs2 = map (Var . Free) ns
      ctx' <- forM ns $ \n -> do
                m <- nextElab nextMeta
-               return (n,Var (Meta m))
+               return (n,Var (Meta Exist m))
      extendElab context ctx' $ do
        zipWithM_ checkifyPattern
                  (map (\psc -> instantiate psc xs1) pscs)
@@ -306,7 +306,7 @@ checkifyPattern (Var (Free n)) t =
      unify substitution context t t'
 checkifyPattern (Var (Bound _ _)) _ =
   error "A bound variable should not be the subject of pattern type checking."
-checkifyPattern (Var (Meta _)) _ =
+checkifyPattern (Var (Meta _ _)) _ =
   error "A metavariable should not be the subject of pattern type checking."
 checkifyPattern (In (ConPat c ps)) t =
   do ConSig args ret <- typeInSignature c
diff --git a/src/Simple/Unification/Unification.hs b/src/Simple/Unification/Unification.hs
index 5509d75..46a2bb8 100644
--- a/src/Simple/Unification/Unification.hs
+++ b/src/Simple/Unification/Unification.hs
@@ -31,14 +31,14 @@ import Control.Monad.Except
 -- | Equating terms by trivial structural equations.
 
 instance MonadUnify TypeF Elaborator where
-  equate (TyCon tycon1) (TyCon tycon2) =
+  equate _ (TyCon tycon1) (TyCon tycon2) =
     do unless (tycon1 == tycon2)
          $ throwError $ "Mismatching type constructors "
                      ++ tycon1 ++ " and " ++ tycon2
        return []
-  equate (Fun a1 b1) (Fun a2 b2) =
-    return [ Equation (instantiate0 a1) (instantiate0 a2)
-           , Equation (instantiate0 b1) (instantiate0 b2)
+  equate f (Fun a1 b1) (Fun a2 b2) =
+    return [ Equation f (instantiate0 a1) (instantiate0 a2)
+           , Equation f (instantiate0 b1) (instantiate0 b2)
            ]
-  equate l r =
-    throwError $ "Cannot unify " ++ pretty (In l) ++ " with " ++ pretty (In r)
\ No newline at end of file
+  equate _ l r =
+    throwError $ "Cannot unify " ++ pretty (In l) ++ " with " ++ pretty (In r)
diff --git a/src/Utils/ABT.hs b/src/Utils/ABT.hs
index da2064c..633c634 100644
--- a/src/Utils/ABT.hs
+++ b/src/Utils/ABT.hs
@@ -87,10 +87,12 @@ deriving instance Show (f (Scope f)) => Show (ABT f)
 -- binder that binds the index. All both have string values that represent the
 -- stored display name of the variable, for pretty printing.
 
+data MetaType = Exist | Constraint deriving (Show,Eq,Ord)
+
 data Variable
   = Free FreeVar
   | Bound String BoundVar
-  | Meta MetaVar
+  | Meta MetaType MetaVar
   deriving (Show)
 
 
@@ -99,7 +101,7 @@ data Variable
 name :: Variable -> String
 name (Free (FreeVar n)) = n
 name (Bound n _)        = n
-name (Meta i)           = "?" ++ show i
+name (Meta _ i)           = "?" ++ show i
 
 
 -- | Equality of variables is by the parts which identify them, so names for
@@ -108,7 +110,7 @@ name (Meta i)           = "?" ++ show i
 instance Eq Variable where
   Free x    == Free y    = x == y
   Bound _ i == Bound _ j = i == j
-  Meta m    == Meta n    = m == n
+  Meta _ m  == Meta _ n  = m == n
   _         == _         = False
 
 
@@ -659,9 +661,9 @@ freeToDefinedScope d (Scope ns _ b) =
 
 substMetas :: (Functor f, Foldable f) => [(MetaVar, ABT f)] -> ABT f -> ABT f
 substMetas [] x = x
-substMetas subs (Var (Meta m)) =
+substMetas subs (Var (Meta mt m)) =
   case lookup m subs of
-    Nothing -> Var (Meta m)
+    Nothing -> Var (Meta mt m)
     Just x -> x
 substMetas _ (Var v) =
   Var v
@@ -682,7 +684,7 @@ occurs :: (Functor f, Foldable f) => MetaVar -> ABT f -> Bool
 occurs m x = fold ocAlgV ocAlgRec ocAlgSc x
   where
     ocAlgV :: Variable -> Bool
-    ocAlgV (Meta m') = m == m'
+    ocAlgV (Meta _ m') = m == m'
     ocAlgV _ = False
     
     ocAlgRec :: Foldable f => f Bool -> Bool
@@ -697,7 +699,7 @@ occurs m x = fold ocAlgV ocAlgRec ocAlgSc x
 metaVars :: (Functor f, Foldable f) => ABT f -> [MetaVar]
 metaVars = fold mvAlgV mvAlgRec mvAlgSc
   where
-    mvAlgV (Meta n) = [n]
+    mvAlgV (Meta _ n) = [n]
     mvAlgV _        = []
     
     mvAlgRec :: Foldable f => f [MetaVar] -> [MetaVar]
diff --git a/src/Utils/Unifier.hs b/src/Utils/Unifier.hs
index 9e70ab2..4f0f6d1 100644
--- a/src/Utils/Unifier.hs
+++ b/src/Utils/Unifier.hs
@@ -144,15 +144,15 @@ updateSubstitutionJ subsl ctxl subs =
 
 -- | Equations are just pairs of values.
 
-data Equation a = Equation a a
+data Equation a = Equation Bool a a
 
 
 -- | Equations can be substituted into, as will be necessary during solving.
 
 substMetasEquation :: (Functor f, Foldable f)
                    => Substitution f -> Equation (ABT f) -> Equation (ABT f)
-substMetasEquation subs (Equation l r) =
-  Equation (substMetas subs l) (substMetas subs r)
+substMetasEquation subs (Equation f l r) =
+  Equation f (substMetas subs l) (substMetas subs r)
 
 
 
@@ -162,7 +162,8 @@ substMetasEquation subs (Equation l r) =
 -- ABTs. This involves producing a new set of equations from the input.
 
 class Monad m => MonadUnify f m where
-  equate :: f (Scope f)
+  equate :: Bool
+         -> f (Scope f)
          -> f (Scope f)
          -> m [Equation (ABT f)]
 
@@ -186,15 +187,20 @@ solve eqs0 = go eqs0 []
     
     go [] subs = return subs
     
-    go (Equation (Var (Meta x)) (Var (Meta y)):eqs) subs
+    go (Equation f (Var (Meta mxt x)) (Var (Meta myt y)):eqs) subs
       | x == y = go eqs subs
-      | otherwise = go eqs' subs'
+      | otherwise = case (f,mxt,myt) of
+          (False,Constraint,Constraint) -> throwError $ "Cannot unify " ++ show x ++ " with " ++ show y
+          _ -> go eqs' subs'
       where
-        newSubs = [(x, Var (Meta y))]
+        (x',y') = if mxt <= myt then (x,y) else (y,x)
+        newSubs = [(x', Var (Meta (max mxt myt) y'))]
         eqs' = map (substMetasEquation newSubs) eqs
         subs' = substMetasSubs newSubs (newSubs ++ subs)
-    
-    go (Equation v1@(Var (Meta x)) r:eqs) subs =
+
+    go (Equation False v1@(Var (Meta Constraint _)) r:_) _ =
+      throwError $ "Cannot unify " ++ pretty v1 ++ " with " ++ pretty r
+    go (Equation _ v1@(Var (Meta _ x)) r:eqs) subs =
       do unless (not (occurs x r))
            $ throwError $ "Cannot unify because " ++ pretty v1
                        ++ " occurs in " ++ pretty r
@@ -203,8 +209,10 @@ solve eqs0 = go eqs0 []
         newSubs = [(x,r)]
         eqs' = map (substMetasEquation newSubs) eqs
         subs' = substMetasSubs newSubs (newSubs ++ subs)
-    
-    go (Equation l v2@(Var (Meta y)):eqs) subs =
+
+    go (Equation False l v2@(Var (Meta Constraint _)):_) _ =
+      throwError $ "Cannot unify " ++ pretty l ++ " with " ++ pretty v2
+    go (Equation _ l v2@(Var (Meta _ y)):eqs) subs =
       do unless (not (occurs y l))
            $ throwError $ "Cannot unify because " ++ pretty v2
                        ++ " occurs in " ++ pretty l
@@ -214,16 +222,16 @@ solve eqs0 = go eqs0 []
         eqs' = map (substMetasEquation newSubs) eqs
         subs' = substMetasSubs newSubs (newSubs ++ subs)
     
-    go (Equation v1@(Var x) v2@(Var y):eqs) subs
+    go (Equation _ v1@(Var x) v2@(Var y):eqs) subs
       | x == y = go eqs subs
       | otherwise = throwError $ "Cannot unify variables " ++ pretty v1
                               ++ " and " ++ pretty v2
     
-    go (Equation (In l) (In r):eqs) subs =
-      do newEqs <- equate l r
+    go (Equation f (In l) (In r):eqs) subs =
+      do newEqs <- equate f l r
          go (newEqs ++ eqs) subs
     
-    go (Equation l r:_) _ =
+    go (Equation _ l r:_) _ =
       throwError $ "Cannot unify " ++ pretty l ++ " and " ++ pretty r
 
 
@@ -243,7 +251,7 @@ unify :: ( Eq a, Functor f, Foldable f, Pretty (ABT f)
 unify subsl ctxl l r =
   do newSubs <-
        catchError
-         (solve [Equation l r])
+         (solve [Equation True l r])
          (\e -> throwError $
                   "Could not unify "++ pretty l ++ " with " ++ pretty r
                     ++ ". " ++ e)
@@ -267,7 +275,7 @@ unifyJ :: ( Eq a, Functor f, Foldable f, Pretty (ABT f)
 unifyJ subsl ctxl l r =
   do newSubs <-
        catchError
-         (solve [Equation l r])
+         (solve [Equation True l r])
          (\e -> throwError $
                   "Could not unify "++ pretty l ++ " with " ++ pretty r
                     ++ ". " ++ e)