diff --git a/idris.cabal b/idris.cabal
--- a/idris.cabal
+++ b/idris.cabal
@@ -1,5 +1,5 @@
 Name:           idris
-Version:        0.9.17
+Version:        0.9.17.1
 License:        BSD3
 License-file:   LICENSE
 Author:         Edwin Brady
@@ -301,6 +301,9 @@
                        test/reg060/run
                        test/reg060/*.idr
                        test/reg060/expected
+                       test/reg061/run
+                       test/reg061/*.idr
+                       test/reg061/expected
 
                        test/basic001/run
                        test/basic001/*.idr
@@ -513,9 +516,22 @@
                        test/proof004/run
                        test/proof004/*.idr
                        test/proof004/expected
+                       test/proof005/run
+                       test/proof005/*.idr
+                       test/proof005/expected
+                       test/proof006/run
+                       test/proof006/*.idr
+                       test/proof006/expected
+                       test/proof007/run
+                       test/proof007/*.idr
+                       test/proof007/expected
                        test/proof008/run
                        test/proof008/*.idr
                        test/proof008/expected
+                       test/proof009/run
+                       test/proof009/*.idr
+                       test/proof009/expected
+                       test/proof009/input
 
                        test/quasiquote001/run
                        test/quasiquote001/*.idr
diff --git a/libs/contrib/Data/Graph.idr b/libs/contrib/Data/Graph.idr
new file mode 100644
--- /dev/null
+++ b/libs/contrib/Data/Graph.idr
@@ -0,0 +1,8 @@
+module Data.Graph
+
+import Data.Vect
+
+data Edge e = MkEdge e e
+
+data Graph : Nat −> Nat −> Type −> Type −> Type where
+  MkGraph : Vect m v −> Vect n (Edge k) −> Graph m n v k
diff --git a/libs/contrib/Data/Polyhedra.idr b/libs/contrib/Data/Polyhedra.idr
new file mode 100644
--- /dev/null
+++ b/libs/contrib/Data/Polyhedra.idr
@@ -0,0 +1,9 @@
+module Data.Polyhedra
+
+import Data.Vect
+import Data.Graph
+
+data Face f = MkFace (Vect n f)
+
+data Polyhedron : Nat -> Nat -> Nat -> Type -> Type where
+  MkPolyhedron : Vect k v -> Vect m (Edge v) -> Vect n (Face v) -> Polyhedron k m n v
diff --git a/libs/effects/Effect/File.idr b/libs/effects/Effect/File.idr
--- a/libs/effects/Effect/File.idr
+++ b/libs/effects/Effect/File.idr
@@ -117,9 +117,10 @@
 ||| @ m The file mode.
 open : (fname : String)
        -> (m : Mode)
-       -> { [FILE_IO ()] ==> [FILE_IO (if result
-                                          then OpenFile m
-                                          else ())] } Eff Bool
+       -> { [FILE_IO ()] ==> {result}
+            [FILE_IO (if result
+                        then OpenFile m
+                        else ())] } Eff Bool
 open f m = call $ Open f m
 
 
diff --git a/src/Idris/AbsSyntax.hs b/src/Idris/AbsSyntax.hs
--- a/src/Idris/AbsSyntax.hs
+++ b/src/Idris/AbsSyntax.hs
@@ -543,10 +543,13 @@
 addConstraints fc (v, cs)
     = do i <- getIState
          let ctxt = tt_ctxt i
-         let ctxt' = ctxt { uconstraints = nub cs ++ uconstraints ctxt,
-                            next_tvar = v }
-         let ics = zip cs (repeat fc) ++ idris_constraints i
+         let ctxt' = ctxt { next_tvar = v }
+         let ics = insertAll (zip cs (repeat fc)) (idris_constraints i)
          putIState $ i { tt_ctxt = ctxt', idris_constraints = ics }
+  where
+    insertAll [] c = c
+    insertAll ((c, fc) : cs) ics 
+       = insertAll cs $ S.insert (ConstraintFC c fc) ics
 
 addDeferred = addDeferred' Ref
 addDeferredTyCon = addDeferred' (TCon 0 0)
diff --git a/src/Idris/AbsSyntaxTree.hs b/src/Idris/AbsSyntaxTree.hs
--- a/src/Idris/AbsSyntaxTree.hs
+++ b/src/Idris/AbsSyntaxTree.hs
@@ -157,7 +157,7 @@
 -- | The global state used in the Idris monad
 data IState = IState {
     tt_ctxt :: Context, -- ^ All the currently defined names and their terms
-    idris_constraints :: [(UConstraint, FC)],
+    idris_constraints :: S.Set ConstraintFC,
       -- ^ A list of universe constraints and their corresponding source locations
     idris_infixes :: [FixDecl], -- ^ Currently defined infix operators
     idris_implicits :: Ctxt [PArg],
@@ -309,7 +309,7 @@
 
 -- | The initial state for the compiler
 idrisInit :: IState
-idrisInit = IState initContext [] []
+idrisInit = IState initContext S.empty []
                    emptyContext emptyContext emptyContext emptyContext
                    emptyContext emptyContext emptyContext emptyContext
                    emptyContext emptyContext emptyContext emptyContext
diff --git a/src/Idris/Core/Binary.hs b/src/Idris/Core/Binary.hs
--- a/src/Idris/Core/Binary.hs
+++ b/src/Idris/Core/Binary.hs
@@ -546,7 +546,22 @@
                            return (TCon (x1x2 `div` 65536) (x1x2 `mod` 65536))
                    _ -> error "Corrupted binary data for NameType"
 
+-- record concrete levels only, for now
+instance Binary UExp where
+    put x = case x of
+                 UVar t -> do putWord8 0
+                              put ((-1) :: Int) -- TMP HACK!
+                 UVal t -> do putWord8 1 
+                              put t
 
+    get = do i <- getWord8
+             case i of
+                 0 -> do x1 <- get
+                         return (UVar x1)
+                 1 -> do x1 <- get
+                         return (UVal x1)
+                 _ -> error "Corrupted binary data for UExp"
+
 instance {- (Binary n) => -} Binary (TT Name) where
         put x
           = {-# SCC "putTT" #-}
@@ -600,7 +615,7 @@
                            x2 <- getWord8
                            return (Proj x1 ((fromEnum x2)-1))
                    6 -> return Erased
-                   7 -> do x1 <- get
+                   7 -> do x1 <- get 
                            return (TType x1)
                    8 -> return Impossible
                    9 -> do x1 <- get
diff --git a/src/Idris/Core/Constraints.hs b/src/Idris/Core/Constraints.hs
--- a/src/Idris/Core/Constraints.hs
+++ b/src/Idris/Core/Constraints.hs
@@ -1,71 +1,223 @@
 -- | Check universe constraints.
-module Idris.Core.Constraints(ucheck) where
+module Idris.Core.Constraints ( ucheck ) where
 
-import Idris.Core.TT
-import Idris.Core.Typecheck
+import Idris.Core.TT ( TC(..), UExp(..), UConstraint(..), FC(..), 
+                       ConstraintFC(..), Err'(..) )
 
 import Control.Applicative
-import Control.Arrow
-import Control.Monad.RWS
-import Control.Monad.State
-import qualified Data.Set as S
-import Data.List
-import Data.Maybe
+import Control.Monad.State.Strict
+import Data.List ( partition )
 import qualified Data.Map.Strict as M
+import qualified Data.Set as S
 
-import Debug.Trace
 
 -- | Check that a list of universe constraints can be satisfied.
-ucheck :: [(UConstraint, FC)] -> TC ()
-ucheck cs = acyclic rels (map fst (M.toList rels))
-  where lhs (ULT l _) = l
-        lhs (ULE l _) = l
-        cs' = S.toList (S.fromList cs)
-        rels = mkRels cs' M.empty
+ucheck :: S.Set ConstraintFC -> TC ()
+ucheck = void . solve 10 . S.filter (not . ignore)
+    where
+        -- TODO: remove the first ignore clause once Idris.Core.Binary:598 is dealt with
+        ignore (ConstraintFC c _) | any (== Var (-1)) (varsIn c) = True
+        ignore (ConstraintFC (ULE a b) _) = a == b
+        ignore _ = False
 
-type Relations = M.Map UExp [(UConstraint, FC)]
+newtype Var = Var Int
+    deriving (Eq, Ord, Show)
 
-mkRels :: [(UConstraint, FC)] -> Relations -> Relations
-mkRels [] acc = acc
-mkRels ((c, f) : cs) acc
-    | not (ignore c)
-       = case M.lookup (lhs c) acc of
-              Nothing -> mkRels cs (M.insert (lhs c) [(c,f)] acc)
-              Just rs -> mkRels cs (M.insert (lhs c) ((c,f):rs) acc)
-    | otherwise = mkRels cs acc
-  where lhs (ULT l _) = l
-        lhs (ULE l _) = l
-        ignore (ULE l r) = l == r
-        ignore _ = False
+data Domain = Domain Int Int
+    deriving (Eq, Ord, Show)
 
+data SolverState =
+    SolverState
+        { queue       :: Queue
+        , domainStore :: M.Map Var ( Domain
+                                   , S.Set ConstraintFC        -- constraints that effected this variable
+                                   )
+        , cons_lhs    :: M.Map Var (S.Set ConstraintFC)
+        , cons_rhs    :: M.Map Var (S.Set ConstraintFC)
+        }
 
-acyclic :: Relations -> [UExp] -> TC ()
-acyclic r cvs = checkCycle (fileFC "root") r [] 0 cvs
-  where
-    checkCycle :: FC -> Relations -> [(UExp, FC)] -> Int -> [UExp] -> TC ()
-    checkCycle fc r path inc [] = return ()
-    checkCycle fc r path inc (c : cs)
-        = do check fc r path inc c
-             -- Remove c from r since we know there's no cycles now
-             let r' = M.insert c [] r
-             checkCycle fc r' path inc cs
+data Queue = Queue [ConstraintFC] (S.Set UConstraint)
 
-    check fc r path inc (UVar x) | x < 0 = return ()
-    check fc r path inc cv
-        | inc > 0 && cv `elem` map fst path
-            = Error $ At fc UniverseError
-                -- FIXME: Make informative
-                -- e.g. (Msg ("Cycle: " ++ show cv ++ ", " ++ show path))
-                -- Issue #1725 on the issue tracker.
-                -- https://github.com/idris-lang/Idris-dev/issues/1725
-        -- if we reach a cycle but we're at the same universe level, it's
-        -- fine, because they must all be equal, so stop.
-        | inc == 0 && cv `elem` map fst path
-            = return ()
-        | otherwise
-             = case M.lookup cv r of
-                    Nothing -> return ()
-                    Just cs -> mapM_ (next r ((cv, fc):path) inc) cs
 
-    next r path inc (ULT l x, fc) = check fc r path (inc + 1) x
-    next r path inc (ULE l x, fc) = check fc r path inc x
+solve :: Int -> S.Set ConstraintFC -> TC (M.Map Var Int)
+solve maxUniverseLevel ucs =
+    evalStateT (propagate >> extractSolution) initSolverState
+
+    where
+        inpConstraints = S.toAscList ucs
+
+        -- | initial solver state.
+        --   the queue contains all constraints, the domain store contains the initial domains.
+        initSolverState :: SolverState
+        initSolverState =
+            let
+                (initUnaryQueue, initQueue) = partition (\ c -> length (varsIn (uconstraint c)) == 1) inpConstraints
+            in
+                SolverState
+                    { queue = Queue (initUnaryQueue ++ initQueue) (S.fromList (map uconstraint (initUnaryQueue ++ initQueue)))
+                    , domainStore = M.fromList
+                        [ (v, (Domain 0 maxUniverseLevel, S.empty))
+                        | v <- ordNub [ v
+                                      | ConstraintFC c _ <- inpConstraints
+                                      , v <- varsIn c
+                                      ]
+                        ]
+                    , cons_lhs = constraintsLHS
+                    , cons_rhs = constraintsRHS
+                    }
+
+        lhs (ULT (UVar x) _) = Just (Var x)
+        lhs (ULE (UVar x) _) = Just (Var x)
+        lhs _ = Nothing
+
+        rhs (ULT _ (UVar x)) = Just (Var x)
+        rhs (ULE _ (UVar x)) = Just (Var x)
+        rhs _ = Nothing
+
+        -- | a map from variables to the list of constraints the variable occurs in. (in the LHS of a constraint)
+        constraintsLHS :: M.Map Var (S.Set ConstraintFC)
+        constraintsLHS = M.fromListWith S.union
+            [ (v, S.singleton (ConstraintFC c fc))
+            | (ConstraintFC c fc) <- inpConstraints
+            , let vars = varsIn c
+            , length vars > 1               -- do not register unary constraints
+            , v <- vars
+            , lhs c == Just v
+            ]
+
+        -- | a map from variables to the list of constraints the variable occurs in. (in the RHS of a constraint)
+        constraintsRHS :: M.Map Var (S.Set ConstraintFC)
+        constraintsRHS = M.fromListWith S.union
+            [ (v, S.singleton (ConstraintFC c fc))
+            | (ConstraintFC c fc) <- inpConstraints
+            , let vars = varsIn c
+            , length vars > 1               -- do not register unary constraints
+            , v <- vars
+            , rhs c == Just v
+            ]
+
+        -- | this is where the actual work is done.
+        --   dequeue the first constraint,
+        --   filter domains,
+        --   update domains (possibly resulting in a domain wipe out),
+        --   until the queue is empty.
+        propagate :: StateT SolverState TC ()
+        propagate = do
+            mcons <- nextConstraint
+            case mcons of
+                Nothing -> return ()
+                Just (ConstraintFC cons fc) -> do
+                    case cons of
+                        ULE a b -> do
+                            Domain lowerA upperA <- domainOf a
+                            Domain lowerB upperB <- domainOf b
+                            when (upperB < upperA) $ updateUpperBoundOf (ConstraintFC cons fc) a upperB
+                            when (lowerA > lowerB) $ updateLowerBoundOf (ConstraintFC cons fc) b lowerA
+                        ULT a b -> do
+                            Domain lowerA upperA <- domainOf a
+                            Domain lowerB upperB <- domainOf b
+                            let upperB_pred = pred upperB
+                            let lowerA_succ = succ lowerA
+                            when (upperB_pred < upperA) $ updateUpperBoundOf (ConstraintFC cons fc) a upperB_pred
+                            when (lowerA_succ > lowerB) $ updateLowerBoundOf (ConstraintFC cons fc) b lowerA_succ
+                    propagate
+
+        -- | extract a solution from the state.
+        extractSolution :: (MonadState SolverState m, Functor m) => m (M.Map Var Int)
+        extractSolution = M.map (extractValue . fst) <$> gets domainStore
+
+        extractValue :: Domain -> Int
+        extractValue (Domain x _) = x
+
+        -- | dequeue the first constraint.
+        nextConstraint :: MonadState SolverState m => m (Maybe ConstraintFC)
+        nextConstraint = do
+            Queue list set <- gets queue
+            case list of
+                [] -> return Nothing
+                (q:qs) -> do
+                    modify $ \ st -> st { queue = Queue qs (S.delete (uconstraint q) set) }
+                    return (Just q)
+
+        -- | look up the domain of a variable from the state.
+        --   for convenience, this function also accepts UVal's and returns a singleton domain for them.
+        domainOf :: MonadState SolverState m => UExp -> m Domain
+        domainOf (UVar var) = gets (fst . (M.! Var var) . domainStore)
+        domainOf (UVal val) = return (Domain val val)
+
+        updateUpperBoundOf :: ConstraintFC -> UExp -> Int -> StateT SolverState TC ()
+        updateUpperBoundOf suspect (UVar var) upper = do
+            doms <- gets domainStore
+            let (oldDom@(Domain lower _), suspects) = doms M.! Var var
+            let newDom = Domain lower upper
+            when (wipeOut newDom) $ lift $ Error $ At (ufc suspect) $ Msg $ unlines
+                $ "Universe inconsistency."
+                : ("Working on: " ++ show (UVar var))
+                : ("Old domain: " ++ show oldDom)
+                : ("New domain: " ++ show newDom)
+                : "Involved constraints: "
+                : map (("\t"++) . show) (suspect : S.toList suspects)
+            modify $ \ st -> st { domainStore = M.insert (Var var) (newDom, S.insert suspect suspects) doms }
+            addToQueueRHS (uconstraint suspect) (Var var)
+        updateUpperBoundOf _ UVal{} _ = return ()
+
+        updateLowerBoundOf :: ConstraintFC -> UExp -> Int -> StateT SolverState TC ()
+        updateLowerBoundOf suspect (UVar var) lower = do
+            doms <- gets domainStore
+            let (oldDom@(Domain _ upper), suspects) = doms M.! Var var
+            let newDom = Domain lower upper
+            when (wipeOut newDom) $ lift $ Error $ At (ufc suspect) $ Msg $ unlines
+                $ "Universe inconsistency."
+                : ("Working on: " ++ show (UVar var))
+                : ("Old domain: " ++ show oldDom)
+                : ("New domain: " ++ show newDom)
+                : "Involved constraints: "
+                : map (("\t"++) . show) (suspect : S.toList suspects)
+            modify $ \ st -> st { domainStore = M.insert (Var var) (newDom, S.insert suspect suspects) doms }
+            addToQueueLHS (uconstraint suspect) (Var var)
+        updateLowerBoundOf _ UVal{} _ = return ()
+
+        -- | add all constraints (with the given var on the lhs) to the queue
+        addToQueueLHS :: MonadState SolverState m => UConstraint -> Var -> m ()
+        addToQueueLHS thisCons var = do
+            clhs <- gets cons_lhs
+            case M.lookup var clhs of
+                Nothing -> return ()
+                Just cs -> do
+                    Queue list set <- gets queue
+                    let set' = S.insert thisCons set
+                    let newCons = [ c | c <- S.toList cs, uconstraint c `S.notMember` set' ]
+                    if null newCons
+                        then return ()
+                        else modify $ \ st -> st { queue = Queue (list ++ newCons)
+                                                                 (S.union set (S.fromList (map uconstraint newCons))) }
+
+        -- | add all constraints (with the given var on the rhs) to the queue
+        addToQueueRHS :: MonadState SolverState m => UConstraint -> Var -> m ()
+        addToQueueRHS thisCons var = do
+            crhs <- gets cons_rhs
+            case M.lookup var crhs of
+                Nothing -> return ()
+                Just cs -> do
+                    Queue list set <- gets queue
+                    let set' = S.insert thisCons set
+                    let newCons = [ c | c <- S.toList cs, uconstraint c `S.notMember` set' ]
+                    if null newCons
+                        then return ()
+                        else modify $ \ st -> st { queue = Queue (list ++ newCons)
+                                                                 (insertAll (map uconstraint newCons) set) }
+
+        insertAll [] s = s
+        insertAll (x : xs) s = insertAll xs (S.insert x s)
+
+        -- | check if a domain is wiped out.
+        wipeOut :: Domain -> Bool
+        wipeOut (Domain l u) = l > u
+
+ordNub :: Ord a => [a] -> [a]
+ordNub = S.toList . S.fromList
+
+-- | variables in a constraint
+varsIn :: UConstraint -> [Var]
+varsIn (ULT a b) = [ Var v | UVar v <- [a,b] ]
+varsIn (ULE a b) = [ Var v | UVar v <- [a,b] ]
diff --git a/src/Idris/Core/Evaluate.hs b/src/Idris/Core/Evaluate.hs
--- a/src/Idris/Core/Evaluate.hs
+++ b/src/Idris/Core/Evaluate.hs
@@ -5,7 +5,7 @@
                 rt_simplify, simplify, specialise, hnf, convEq, convEq',
                 Def(..), CaseInfo(..), CaseDefs(..),
                 Accessibility(..), Totality(..), PReason(..), MetaInformation(..),
-                Context, initContext, ctxtAlist, uconstraints, next_tvar,
+                Context, initContext, ctxtAlist, next_tvar,
                 addToCtxt, setAccess, setTotal, setMetaInformation, addCtxtDef, addTyDecl,
                 addDatatype, addCasedef, simplifyCasedef, addOperator,
                 lookupNames, lookupTyName, lookupTyNameExact, lookupTy, lookupTyExact,
@@ -786,16 +786,15 @@
 -- | Contexts used for global definitions and for proof state. They contain
 -- universe constraints and existing definitions.
 data Context = MkContext {
-                  uconstraints    :: [UConstraint],
                   next_tvar       :: Int,
                   definitions     :: Ctxt (Def, Accessibility, Totality, MetaInformation)
                 } deriving Show
 
 -- | The initial empty context
-initContext = MkContext [] 0 emptyContext
+initContext = MkContext 0 emptyContext
 
 mapDefCtxt :: (Def -> Def) -> Context -> Context
-mapDefCtxt f (MkContext c t defs) = MkContext c t (mapCtxt f' defs)
+mapDefCtxt f (MkContext t defs) = MkContext t (mapCtxt f' defs)
    where f' (d, a, t, m) = f' (f d, a, t, m)
 
 -- | Get the definitions from a context
diff --git a/src/Idris/Core/TT.hs b/src/Idris/Core/TT.hs
--- a/src/Idris/Core/TT.hs
+++ b/src/Idris/Core/TT.hs
@@ -782,14 +782,6 @@
 instance Sized UExp where
   size _ = 1
 
--- We assume that universe levels have been checked, so anything external
--- can just have the same universe variable and we won't get any new
--- cycles.
-
-instance Binary UExp where
-    put x = return ()
-    get = return (UVar (-1))
-
 instance Show UExp where
     show (UVar x) | x < 26 = [toEnum (x + fromEnum 'a')]
                   | otherwise = toEnum ((x `mod` 26) + fromEnum 'a') : show (x `div` 26)
@@ -801,6 +793,16 @@
                  | ULE UExp UExp -- ^ Less than or equal to
   deriving (Eq, Ord)
 
+data ConstraintFC = ConstraintFC { uconstraint :: UConstraint,
+                                   ufc :: FC }
+  deriving Show
+
+instance Eq ConstraintFC where
+    x == y = uconstraint x == uconstraint y  
+
+instance Ord ConstraintFC where
+    compare x y = compare (uconstraint x) (uconstraint y)
+
 instance Show UConstraint where
     show (ULT x y) = show x ++ " < " ++ show y
     show (ULE x y) = show x ++ " <= " ++ show y
@@ -1191,6 +1193,8 @@
           Just $ RBind n' b' sc'
   where safeForgetEnvB env (Let t v) = liftM2 Let (safeForgetEnv env t) 
                                                   (safeForgetEnv env v)
+        safeForgetEnvB env (Guess t v) = liftM2 Guess (safeForgetEnv env t) 
+                                                      (safeForgetEnv env v)
         safeForgetEnvB env b = do ty' <- safeForgetEnv env (binderTy b)
                                   Just $ fmap (\_ -> ty') b 
 safeForgetEnv env (App f a) = liftM2 RApp (safeForgetEnv env f) (safeForgetEnv env a)
diff --git a/src/Idris/Core/Typecheck.hs b/src/Idris/Core/Typecheck.hs
--- a/src/Idris/Core/Typecheck.hs
+++ b/src/Idris/Core/Typecheck.hs
@@ -86,15 +86,38 @@
       | (P nt n' ty : _) <- lookupP_all (not holes) n ctxt 
            = return (P nt n' ty, ty)
       | otherwise = do lift $ tfail $ NoSuchVariable n
+  chk u env ap@(RApp f RType) | not holes
+    -- special case to reduce constraintss
+      = do (fv, fty) <- chk u env f
+           let fty' = case uniqueBinders (map fst env) (finalise fty) of
+                        ty@(Bind x (Pi i s k) t) -> ty
+                        _ -> uniqueBinders (map fst env)
+                                 $ case hnf ctxt env fty of
+                                     ty@(Bind x (Pi i s k) t) -> ty
+                                     _ -> normalise ctxt env fty
+           case fty' of
+             Bind x (Pi i (TType v') k) t ->
+               do (v, cs) <- get
+                  put (v+1, ULT (UVar v) v' : cs)
+                  let apty = simplify initContext env
+                                 (Bind x (Let (TType v') (TType (UVar v))) t)
+                  return (App fv (TType (UVar v)), apty)
+             Bind x (Pi i s k) t ->
+                 do (av, aty) <- chk u env RType 
+                    convertsC ctxt env aty s
+                    let apty = simplify initContext env
+                                        (Bind x (Let aty av) t)
+                    return (App fv av, apty)
+             t -> lift $ tfail $ NonFunctionType fv fty
   chk u env ap@(RApp f a)
       = do (fv, fty) <- chk u env f
-           (av, aty) <- chk u env a
            let fty' = case uniqueBinders (map fst env) (finalise fty) of
                         ty@(Bind x (Pi i s k) t) -> ty
                         _ -> uniqueBinders (map fst env)
                                  $ case hnf ctxt env fty of
                                      ty@(Bind x (Pi i s k) t) -> ty
                                      _ -> normalise ctxt env fty
+           (av, aty) <- chk u env a
            case fty' of
              Bind x (Pi i s k) t ->
                  do convertsC ctxt env aty s
@@ -135,17 +158,22 @@
           constType TheWorld = Constant WorldType
           constType Forgot  = Erased
           constType _       = TType (UVal 0)
-  chk u env (RForce t) = do (_, ty) <- chk u env t
-                            return (Erased, ty)
+  chk u env (RForce t) 
+      = do (_, ty) <- chk u env t
+           return (Erased, ty)
   chk u env (RBind n (Pi i s k) t)
       = do (sv, st) <- chk u env s
-           (kv, kt) <- chk u env k
-           (tv, tt) <- chk st ((n, Pi i sv kv) : env) t
            (v, cs) <- get
+           (kv, kt) <- chk u env k -- no need to validate these constraints, they are independent
+           put (v+1, cs)
+           let maxu = UVar v
+           (tv, tt) <- chk st ((n, Pi i sv kv) : env) t
            case (normalise ctxt env st, normalise ctxt env tt) of
                 (TType su, TType tu) -> do
-                    when (not holes) $ put (v+1, ULE su (UVar v):ULE tu (UVar v):cs)
-                    let k' = st `smaller` kv `smaller` TType (UVar v) `smaller` u
+                    when (not holes) $ do (v, cs) <- get
+                                          put (v, ULE su maxu : 
+                                                  ULE tu maxu : cs)
+                    let k' = TType (UVar v) `smaller` st `smaller` kv `smaller` u
                     return (Bind n (Pi i (uniqueBinders (map fst env) sv) k')
                               (pToV n tv), k')
                 (un, un') ->
diff --git a/src/Idris/Elab/Data.hs b/src/Idris/Elab/Data.hs
--- a/src/Idris/Elab/Data.hs
+++ b/src/Idris/Elab/Data.hs
@@ -64,7 +64,7 @@
     = do let codata = Codata `elem` opts
          iLOG (show fc)
          undef <- isUndefined fc n
-         (cty, _, t, inacc) <- buildType info syn fc [] n t_in
+         (cty, ckind, t, inacc) <- buildType info syn fc [] n t_in
          -- if n is defined already, make sure it is just a type declaration
          -- with the same type we've just elaborated, and no constructors
          -- yet
@@ -76,7 +76,7 @@
          let unique = case getRetTy cty of
                            UType UniqueType -> True
                            _ -> False
-         cons <- mapM (elabCon cnameinfo syn n codata (getRetTy cty)) dcons
+         cons <- mapM (elabCon cnameinfo syn n codata (getRetTy cty) ckind) dcons
          ttag <- getName
          i <- getIState
          let as = map (const (Left (Msg ""))) (getArgTys cty)
@@ -210,16 +210,18 @@
                      }
 
 elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->
-           Type -> -- for kind checking
+           Type -> -- for unique kind checking
+           Type -> -- data type's kind
            (Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, PTerm, FC, [Name]) ->
            Idris (Name, Type)
-elabCon info syn tn codata expkind (doc, argDocs, n, t_in, fc, forcenames)
+elabCon info syn tn codata expkind dkind (doc, argDocs, n, t_in, fc, forcenames)
     = do checkUndefined fc n
          logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ show t_in
          (cty, ckind, t, inacc) <- buildType info syn fc [Constructor] n (if codata then mkLazy t_in else t_in)
          ctxt <- getContext
          let cty' = normalise ctxt [] cty
          checkUniqueKind ckind expkind
+         addDataConstraint ckind dkind
 
          -- Check that the constructor type is, in fact, a part of the family being defined
          tyIs n cty'
@@ -279,6 +281,13 @@
         = tclift $ tfail (At fc (UniqueKindError UniqueType n))
     checkUniqueKind (UType AllTypes) _ = return ()
     checkUniqueKind _ _ = return ()
+
+    -- Constructor's kind must be <= expected kind
+    addDataConstraint (TType con) (TType exp) 
+       = do ctxt <- getContext
+            let v = next_tvar ctxt
+            addConstraints fc (v, [ULT con exp])
+    addDataConstraint _ _ = return ()
 
 type EliminatorState = StateT (Map.Map String Int) Idris
 
diff --git a/src/Idris/ElabTerm.hs b/src/Idris/ElabTerm.hs
--- a/src/Idris/ElabTerm.hs
+++ b/src/Idris/ElabTerm.hs
@@ -1734,7 +1734,8 @@
         bname _ = Nothing
     runT (Intro xs) = mapM_ (\x -> do attack; intro (Just x)) xs
     runT Intros = do g <- goal
-                     attack; intro (bname g)
+                     attack; 
+                     intro (bname g)
                      try' (runT Intros)
                           (return ()) True
       where
diff --git a/src/Idris/IBC.hs b/src/Idris/IBC.hs
--- a/src/Idris/IBC.hs
+++ b/src/Idris/IBC.hs
@@ -37,7 +37,7 @@
 import Util.Zlib (decompressEither)
 
 ibcVersion :: Word8
-ibcVersion = 100
+ibcVersion = 101
 
 data IBCFile = IBCFile { ver :: Word8,
                          sourcefile :: FilePath,
diff --git a/src/Idris/Parser.hs b/src/Idris/Parser.hs
--- a/src/Idris/Parser.hs
+++ b/src/Idris/Parser.hs
@@ -59,6 +59,7 @@
 import Data.Monoid
 import Data.Char
 import Data.Ord
+import Data.Generics.Uniplate.Data (descendM)
 import qualified Data.Map as M
 import qualified Data.HashSet as HS
 import qualified Data.Text as T
@@ -276,7 +277,7 @@
          when (length ns /= length (nub ns))
             $ unexpected "repeated variable in syntax rule"
          lchar '='
-         tm <- typeExpr (allowImp syn)
+         tm <- typeExpr (allowImp syn) >>= uniquifyBinders [n | Binding n <- syms]
          terminator
          return (Rule (mkSimple syms) tm sty)
   where
@@ -297,7 +298,51 @@
        where ts = dropWhile isSpace . dropWhileEnd isSpace $ s
     mkSimple' (e : es) = e : mkSimple' es
     mkSimple' [] = []
+    
+    -- Prevent syntax variable capture by making all binders under syntax unique
+    -- (the ol' Common Lisp GENSYM approach)
+    uniquifyBinders :: [Name] -> PTerm -> IdrisParser PTerm
+    uniquifyBinders userNames = fixBind []
+      where
+        fixBind :: [(Name, Name)] -> PTerm -> IdrisParser PTerm
+        fixBind rens (PRef fc n) | Just n' <- lookup n rens =
+          return $ PRef fc n'
+        fixBind rens (PPatvar fc n) | Just n' <- lookup n rens =
+          return $ PPatvar fc n'
+        fixBind rens (PLam fc n ty body)
+          | n `elem` userNames = liftM2 (PLam fc n) (fixBind rens ty) (fixBind rens body)
+          | otherwise =
+            do ty' <- fixBind rens ty
+               n' <- gensym n
+               body' <- fixBind ((n,n'):rens) body
+               return $ PLam fc n' ty' body'
+        fixBind rens (PPi plic n argTy body)
+          | n `elem` userNames = liftM2 (PPi plic n) (fixBind rens argTy) (fixBind rens body)
+          | otherwise =
+            do ty' <- fixBind rens argTy
+               n' <- gensym n
+               body' <- fixBind ((n,n'):rens) body
+               return $ (PPi plic n' ty' body')
+        fixBind rens (PLet fc n ty val body)
+          | n `elem` userNames = liftM3 (PLet fc n)
+                                        (fixBind rens ty)
+                                        (fixBind rens val)
+                                        (fixBind rens body)
+          | otherwise =
+            do ty' <- fixBind rens ty
+               val' <- fixBind rens val
+               n' <- gensym n
+               body' <- fixBind ((n,n'):rens) body
+               return $ (PLet fc n' ty' val' body')
+        fixBind rens (PMatchApp fc n) | Just n' <- lookup n rens =
+          return $ PMatchApp fc n'
+        fixBind rens x = descendM (fixBind rens) x
 
+        gensym :: Name -> IdrisParser Name
+        gensym n = do ist <- get
+                      let idx = idris_name ist
+                      put ist { idris_name = idx + 1 }
+                      return $ sMN idx (show n)
 
 {- | Parses a syntax symbol (either binding variable, keyword or expression)
 
diff --git a/src/Idris/REPL.hs b/src/Idris/REPL.hs
--- a/src/Idris/REPL.hs
+++ b/src/Idris/REPL.hs
@@ -87,6 +87,7 @@
 import Data.Maybe
 import Data.List hiding (group)
 import Data.Char
+import qualified Data.Set as S
 import Data.Version
 import Data.Word (Word)
 import Data.Either (partitionEithers)
@@ -945,9 +946,10 @@
 process fn Universes
                      = do i <- getIState
                           let cs = idris_constraints i
+                          let cslist = S.toAscList cs 
 --                        iputStrLn $ showSep "\n" (map show cs)
-                          iputStrLn $ show (map fst cs)
-                          let n = length cs
+                          iputStrLn $ show (map uconstraint cslist)
+                          let n = length cslist
                           iputStrLn $ "(" ++ show n ++ " constraints)"
                           case ucheck cs of
                             Error e -> iPrintError $ pshow i e
diff --git a/test/error001/expected b/test/error001/expected
--- a/test/error001/expected
+++ b/test/error001/expected
@@ -1,1 +1,9 @@
-test002.idr:5:6:Universe inconsistency
+test002.idr:1:6:Universe inconsistency.
+Working on: z
+Old domain: Domain 6 6
+New domain: Domain 6 5
+Involved constraints: 
+	ConstraintFC {uconstraint = z <= a1, ufc = test002.idr:1:6}
+	ConstraintFC {uconstraint = y < z, ufc = test002.idr:1:6}
+	ConstraintFC {uconstraint = z <= a1, ufc = test002.idr:1:6}
+
diff --git a/test/proof005/DefaultArgSubstitutionSuccess.idr b/test/proof005/DefaultArgSubstitutionSuccess.idr
new file mode 100644
--- /dev/null
+++ b/test/proof005/DefaultArgSubstitutionSuccess.idr
@@ -0,0 +1,44 @@
+module DefaultArgSubstitutionSuccess
+
+DecProofType : {a:Type} -> Dec a -> Type
+DecProofType {a} (Yes _)  = a
+DecProofType {a} (No _)   = a -> Void
+
+decProof : {a:Type} -> (dec : Dec a) -> DecProofType dec
+decProof (Yes x)  = x
+decProof (No x)   = x
+
+DecType : {a:Type} -> Dec a -> Type
+DecType {a} _ = a
+
+
+argsAreSame : (n:Nat) -> (m:Nat)
+              -> { default (decProof (decEq m n)) same : (m=n) } -> ()
+argsAreSame _ _ = ()
+
+
+argsAreDiff : (n:Nat) -> (m:Nat)
+              -> { default (decProof (decEq m n)) same : (m=n) -> Void } -> ()
+argsAreDiff _ _ = ()
+
+
+data SameNats : Type where
+  same : (n:Nat) -> (m:Nat) ->
+         { default (decProof (decEq m n)) same : (m=n) } -> SameNats
+
+data DiffNats : Type where
+  diff : (n:Nat) -> (m:Nat) ->
+         { default (decProof (decEq m n)) same : (m=n) -> Void } -> DiffNats
+
+
+zArgsAreSame : ()
+zArgsAreSame = argsAreSame Z Z
+
+zszArgsAreDiff : ()
+zszArgsAreDiff = argsAreDiff Z (S Z)
+
+sameNatZs : SameNats
+sameNatZs = same Z Z
+
+diffNatsZSZ : DiffNats
+diffNatsZSZ = diff Z (S Z)
diff --git a/test/proof005/expected b/test/proof005/expected
new file mode 100644
--- /dev/null
+++ b/test/proof005/expected
diff --git a/test/proof005/run b/test/proof005/run
new file mode 100644
--- /dev/null
+++ b/test/proof005/run
@@ -0,0 +1,3 @@
+#!/usr/bin/env bash
+idris --check $@ DefaultArgSubstitutionSuccess.idr
+rm -f *.ibc
diff --git a/test/proof006/DefaultArgSubstitutionSyntax.idr b/test/proof006/DefaultArgSubstitutionSyntax.idr
new file mode 100644
--- /dev/null
+++ b/test/proof006/DefaultArgSubstitutionSyntax.idr
@@ -0,0 +1,49 @@
+module DefaultArgSubstitutionSyntax
+
+DecProofType : {a:Type} -> Dec a -> Type
+DecProofType {a} (Yes _)  = a
+DecProofType {a} (No _)   = a -> Void
+
+decProof : {a:Type} -> (dec : Dec a) -> DecProofType dec
+decProof (Yes x)  = x
+decProof (No x)   = x
+
+DecType : {a:Type} -> Dec a -> Type
+DecType {a} _ = a
+
+
+syntax "{{" [prfname] ":" "accept" [dec] "}}" "->" [ret] 
+  = { default (decProof dec) prfname : DecType dec } -> ret
+
+syntax "{{" [prfname] ":" "reject" [dec] "}}" "->" [ret] 
+  = { default (decProof dec) prfname : DecType dec -> Void } -> ret
+
+
+argsAreSame : (n:Nat) -> (m:Nat)
+              -> {{ same : accept (decEq n m) }} -> ()
+argsAreSame _ _ = ()
+
+
+argsAreDiff : (n:Nat) -> (m:Nat)
+              -> {{ diff : reject (decEq m n) }} -> ()
+argsAreDiff _ _ = ()
+
+
+data SameNats : Type where
+  same : (n:Nat) -> (m:Nat) -> {{ same : accept (decEq m n) }} -> SameNats
+
+data DiffNats : Type where
+  diff : (n:Nat) -> (m:Nat) -> {{ diff : reject (decEq m n) }} -> DiffNats
+
+
+zArgsAreSame : ()
+zArgsAreSame = argsAreSame Z Z
+
+zszArgsAreDiff : ()
+zszArgsAreDiff = argsAreDiff Z (S Z)
+
+sameNatZs : SameNats
+sameNatZs = same Z Z
+
+diffNatsZSZ : DiffNats
+diffNatsZSZ = diff Z (S Z)
diff --git a/test/proof006/expected b/test/proof006/expected
new file mode 100644
--- /dev/null
+++ b/test/proof006/expected
diff --git a/test/proof006/run b/test/proof006/run
new file mode 100644
--- /dev/null
+++ b/test/proof006/run
@@ -0,0 +1,3 @@
+#!/usr/bin/env bash
+idris --check $@ DefaultArgSubstitutionSyntax.idr
+rm -f *.ibc
diff --git a/test/proof007/DefaultArgUnknownName.idr b/test/proof007/DefaultArgUnknownName.idr
new file mode 100644
--- /dev/null
+++ b/test/proof007/DefaultArgUnknownName.idr
@@ -0,0 +1,10 @@
+module DefaultArgUnknownName
+
+-- FIXME: What is the expected behaviour here? Should the type declaration
+-- not compile?
+funWithBadDefArg : { default sadgjhsag arg : () } -> ()
+funWithBadDefArg = ()
+
+test : ()
+test = funWithBadDefArg
+
diff --git a/test/proof007/expected b/test/proof007/expected
new file mode 100644
--- /dev/null
+++ b/test/proof007/expected
@@ -0,0 +1,4 @@
+DefaultArgUnknownName.idr:9:6:
+When elaborating right hand side of test:
+When elaborating argument arg to function DefaultArgUnknownName.funWithBadDefArg:
+        No such variable sadgjhsag
diff --git a/test/proof007/run b/test/proof007/run
new file mode 100644
--- /dev/null
+++ b/test/proof007/run
@@ -0,0 +1,3 @@
+#!/usr/bin/env bash
+idris --consolewidth 80 --check $@ DefaultArgUnknownName.idr
+rm -f *.ibc
diff --git a/test/proof009/expected b/test/proof009/expected
new file mode 100644
--- /dev/null
+++ b/test/proof009/expected
@@ -0,0 +1,26 @@
+Type checking ./proof009.idr
+
+
+----------                 Goal:                  ----------
+{hole0} : Int -> Int -> Int
+-Main.arhs> ----------              Other goals:              ----------
+{hole0}
+----------              Assumptions:              ----------
+ x : Int
+----------                 Goal:                  ----------
+{hole1} : Int -> Int
+-Main.arhs> ----------              Other goals:              ----------
+{hole1},{hole0}
+----------              Assumptions:              ----------
+ x : Int
+ y : Int
+----------                 Goal:                  ----------
+{hole2} : Int
+-Main.arhs> arhs: No more goals.
+-Main.arhs> Proof completed!
+Main.arhs = proof
+  intro x
+  intros
+  trivial
+
+
diff --git a/test/proof009/input b/test/proof009/input
new file mode 100644
--- /dev/null
+++ b/test/proof009/input
@@ -0,0 +1,6 @@
+:p arhs
+intro x
+intros
+trivial
+qed
+:q
diff --git a/test/proof009/proof009.idr b/test/proof009/proof009.idr
new file mode 100644
--- /dev/null
+++ b/test/proof009/proof009.idr
@@ -0,0 +1,9 @@
+afn : Int -> Int -> Int
+afn x y = ?arhs
+
+-- plus_comm_rhs_1 : y = plus y 0
+-- 
+-- plus_comm : (x, y : Nat) -> plus x y = plus y x
+-- plus_comm Z y = plus_comm_rhs_1
+-- plus_comm (S k) y = ?plus_comm_rhs_2
+
diff --git a/test/proof009/run b/test/proof009/run
new file mode 100644
--- /dev/null
+++ b/test/proof009/run
@@ -0,0 +1,3 @@
+#!/usr/bin/env bash
+idris $@ --quiet proof009.idr < input
+rm -f *.ibc
diff --git a/test/quasiquote001/expected b/test/quasiquote001/expected
--- a/test/quasiquote001/expected
+++ b/test/quasiquote001/expected
@@ -1,5 +1,5 @@
 (App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 8 0) (UN Unit) (TType (UVar -1)))) (P (DCon 0 0) (UN MkUnit) (P (TCon 0 0) (UN Unit) Erased))) (App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 8 0) (UN Unit) (TType (UVar -1)))) (P (DCon 0 0) (UN MkUnit) (P (TCon 0 0) (UN Unit) Erased))) (App (P (DCon 0 1) (NS (UN Nil) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 0)))) (P (TCon 8 0) (UN Unit) (TType (UVar -1))))))
 --------------
-(App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 32))) (TType (UVar 34))) (App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 36))) (App (App (App (App (P (DCon 0 4) (NS (UN MkPair) ["Builtins"]) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (NS (UN Pair) ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 30))) (TType (UVar 32))) (P (TCon 8 0) (NS (UN Nat) ["Nat", "Prelude"]) (TType (UVar -1)))) (P (TCon 8 0) (NS (UN Nat) ["Nat", "Prelude"]) (TType (UVar -1))))) (App (P (DCon 0 1) (NS (UN Nil) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 0)))) (TType (UVar 38)))))
+(App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 24))) (TType (UVar 25))) (App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 26))) (App (App (App (App (P (DCon 0 4) (NS (UN MkPair) ["Builtins"]) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (NS (UN Pair) ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 22))) (TType (UVar 23))) (P (TCon 8 0) (NS (UN Nat) ["Nat", "Prelude"]) (TType (UVar -1)))) (P (TCon 8 0) (NS (UN Nat) ["Nat", "Prelude"]) (TType (UVar -1))))) (App (P (DCon 0 1) (NS (UN Nil) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 0)))) (TType (UVar 27)))))
 --------------
-(App (App (App (App (P (DCon 0 4) (NS (UN MkPair) ["Builtins"]) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (NS (UN Pair) ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 30))) (TType (UVar 32))) (App (App (App (App (P (DCon 0 4) (NS (UN MkPair) ["Builtins"]) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (NS (UN Pair) ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 30))) (TType (UVar 32))) (TType (UVar 32))) (TType (UVar 32)))) (App (App (App (App (P (DCon 0 4) (NS (UN MkPair) ["Builtins"]) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (NS (UN Pair) ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 30))) (TType (UVar 32))) (TType (UVar 32))) (TType (UVar 32))))
+(App (App (App (App (P (DCon 0 4) (NS (UN MkPair) ["Builtins"]) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (NS (UN Pair) ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 22))) (TType (UVar 23))) (App (App (App (App (P (DCon 0 4) (NS (UN MkPair) ["Builtins"]) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (NS (UN Pair) ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 22))) (TType (UVar 23))) (TType (UVar 24))) (TType (UVar 24)))) (App (App (App (App (P (DCon 0 4) (NS (UN MkPair) ["Builtins"]) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (NS (UN Pair) ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 22))) (TType (UVar 23))) (TType (UVar 24))) (TType (UVar 24))))
diff --git a/test/reg061/Capture.idr b/test/reg061/Capture.idr
new file mode 100644
--- /dev/null
+++ b/test/reg061/Capture.idr
@@ -0,0 +1,9 @@
+module Capture
+
+-- Test for variable capture in syntax
+
+syntax delay  [x] = \z => case z of { () => x }
+syntax delay' [z] = delay z
+
+capture : a -> () -> a
+capture x = delay' x
diff --git a/test/reg061/expected b/test/reg061/expected
new file mode 100644
--- /dev/null
+++ b/test/reg061/expected
diff --git a/test/reg061/run b/test/reg061/run
new file mode 100644
--- /dev/null
+++ b/test/reg061/run
@@ -0,0 +1,3 @@
+#!/usr/bin/env bash
+idris $@ Capture.idr --check
+rm -f *.ibc