diff --git a/Agda.cabal b/Agda.cabal
--- a/Agda.cabal
+++ b/Agda.cabal
@@ -1,5 +1,5 @@
 name:            Agda
-version:         2.5.1
+version:         2.5.1.1
 cabal-version:   >= 1.8
 build-type:      Custom
 license:         OtherLicense
@@ -35,6 +35,7 @@
 tested-with:        GHC == 7.6.3
                     GHC == 7.8.4
                     GHC == 7.10.3
+                    GHC == 8.0.1
 extra-source-files: src/full/undefined.h
                     README.md
                     CHANGELOG
@@ -76,8 +77,8 @@
 
 source-repository this
   type:     git
-  location: https://github.com/agda/agda/tree/2.5.1
-  tag:      2.5.1
+  location: https://github.com/agda/agda/tree/v2.5.1.1
+  tag:      v2.5.1.1
 
 flag cpphs
   default:     True
@@ -99,12 +100,13 @@
     ghc-options: -pgmP cpphs -optP --cpp
 
   if flag(uhc)
-    build-depends:    shuffle >= 0.1.3.3
-                    , uhc-light >= 1.1.9.2 && < 1.2
-                    , uhc-util >= 0.1.6.3 && < 0.1.6.6
-                    , uulib >= 0.9.20
-    -- we use the CPP processor to conditionally import the UHC Light modules. If UHC Light is not
-    -- present, we instead create dummy definitions, see module Agda.Compiler.UHC.Bridge.
+    build-depends:  shuffle >= 0.1.3.3
+                  , uhc-light >= 1.1.9.2 && < 1.2
+                  , uhc-util >= 0.1.6.3 && < 0.1.6.7
+                  , uulib >= 0.9.20
+    -- we use the CPP processor to conditionally import the UHC Light
+    -- modules. If UHC Light is not present, we instead create dummy
+    -- definitions, see module Agda.Compiler.UHC.Bridge.
     cpp-options:    -DUHC_BACKEND
 
   if os(windows)
@@ -534,7 +536,7 @@
   hs-source-dirs: src/main
   main-is:        Main.hs
   build-depends:
-    Agda == 2.5.1
+    Agda == 2.5.1.1
     -- Nothing is used from the following package, except for the
     -- prelude.
     , base >= 4.6.0.1 && < 6
@@ -572,3 +574,4 @@
     , mtl >= 2.1.1 && <= 2.1.3.1 || >= 2.2.1 && < 2.3
     , filepath >= 1.3.0.1 && < 1.5
   ghc-options:  -rtsopts
+
diff --git a/CHANGELOG b/CHANGELOG
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -1,4 +1,60 @@
 ------------------------------------------------------------------------
+-- Release notes for Agda version 2.5.1.1
+------------------------------------------------------------------------
+
+Important changes since 2.5.1:
+
+Installation and infrastructure
+===============================
+
+* Added support for GHC 8.0.1.
+
+Bug fixes
+=========
+
+* Fixed a serious performance problem with instance search
+
+  Issues #1952 and #1998. Also related: #1955 and #2025
+
+* Interactively splitting variable with C-c C-c no longer introduces
+  new trailing patterns.  This fixes issue #1950.
+
+    data Ty : Set where
+      _⇒_ : Ty → Ty → Ty
+
+    ⟦_⟧ : Ty → Set
+    ⟦ A ⇒ B ⟧ = ⟦ A ⟧ → ⟦ B ⟧
+
+    data Term : Ty → Set where
+      K : (A B : Ty) → Term (A ⇒ (B ⇒ A))
+
+    test : (A : Ty) (a : Term A) → ⟦ A ⟧
+    test A a = {!a!}
+
+  Before change, case splitting on `a` would give
+
+    test .(A ⇒ (B ⇒ A)) (K A B) x x₁ = ?
+
+  Now, it yields
+
+    test .(A ⇒ (B ⇒ A)) (K A B) = ?
+
+* Other issues fixed ( see https://github.com/agda/agda/issues ):
+  - #1322 (Missing error for attempted higher order instance)
+  - #1951 (mixfix binders not working in 'syntax')
+  - #1967 (too eager insteance search error)
+  - #1974 (lost constraint dependencies)
+  - #1982 (internal error in unifier)
+  - #2034 (function type instance goals)
+
+Compiler backends
+=================
+
+* UHC compiler backend
+
+  Added support for UHC 1.1.9.4.
+
+------------------------------------------------------------------------
 -- Release notes for Agda version 2.5.1
 ------------------------------------------------------------------------
 
diff --git a/dist/build/Agda/Syntax/Parser/Lexer.hs b/dist/build/Agda/Syntax/Parser/Lexer.hs
--- a/dist/build/Agda/Syntax/Parser/Lexer.hs
+++ b/dist/build/Agda/Syntax/Parser/Lexer.hs
@@ -267,27 +267,6 @@
 {-# LINE 1 "templates/GenericTemplate.hs" #-}
 {-# LINE 1 "<built-in>" #-}
 {-# LINE 1 "<command-line>" #-}
-{-# LINE 9 "<command-line>" #-}
-{-# LINE 1 "/usr/local/stow/ghc-8.0-upstream/lib/ghc-8.0.0.20160316/include/ghcversion.h" #-}
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-{-# LINE 9 "<command-line>" #-}
 {-# LINE 1 "templates/GenericTemplate.hs" #-}
 -- -----------------------------------------------------------------------------
 -- ALEX TEMPLATE
diff --git a/dist/build/Agda/Syntax/Parser/Parser.hs b/dist/build/Agda/Syntax/Parser/Parser.hs
--- a/dist/build/Agda/Syntax/Parser/Parser.hs
+++ b/dist/build/Agda/Syntax/Parser/Parser.hs
@@ -6324,27 +6324,6 @@
 {-# LINE 1 "templates/GenericTemplate.hs" #-}
 {-# LINE 1 "<built-in>" #-}
 {-# LINE 1 "<command-line>" #-}
-{-# LINE 11 "<command-line>" #-}
-{-# LINE 1 "/usr/local/stow/ghc-8.0-upstream/lib/ghc-8.0.0.20160316/include/ghcversion.h" #-}
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-{-# LINE 11 "<command-line>" #-}
 {-# LINE 1 "templates/GenericTemplate.hs" #-}
 -- Id: GenericTemplate.hs,v 1.26 2005/01/14 14:47:22 simonmar Exp 
 
diff --git a/src/data/emacs-mode/agda2-mode.el b/src/data/emacs-mode/agda2-mode.el
--- a/src/data/emacs-mode/agda2-mode.el
+++ b/src/data/emacs-mode/agda2-mode.el
@@ -10,7 +10,7 @@
 
 ;;; Code:
 
-(defvar agda2-version "2.5.1"
+(defvar agda2-version "2.5.1.1"
   "The version of the Agda mode.
 Note that the same version of the Agda executable must be used.")
 
diff --git a/src/full/Agda/Interaction/BasicOps.hs b/src/full/Agda/Interaction/BasicOps.hs
--- a/src/full/Agda/Interaction/BasicOps.hs
+++ b/src/full/Agda/Interaction/BasicOps.hs
@@ -295,7 +295,7 @@
       FindInScopeOF _ _ _        -> __IMPOSSIBLE__
 
 instance Reify ProblemConstraint (Closure (OutputForm Expr Expr)) where
-  reify (PConstr pid cl) = enterClosure cl $ \c -> buildClosure =<< (OutputForm (getRange c) pid <$> reify c)
+  reify (PConstr pids cl) = enterClosure cl $ \c -> buildClosure =<< (OutputForm (getRange c) (last pids) <$> reify c)
 
 instance Reify Constraint (OutputConstraint Expr Expr) where
     reify (ValueCmp cmp t u v)   = CmpInType cmp <$> reify t <*> reify u <*> reify v
diff --git a/src/full/Agda/Interaction/Imports.hs b/src/full/Agda/Interaction/Imports.hs
--- a/src/full/Agda/Interaction/Imports.hs
+++ b/src/full/Agda/Interaction/Imports.hs
@@ -726,6 +726,11 @@
     -- Andreas, Makoto, 2014-10-18 AIM XX: repeating the experiment
     -- with discarding also the nameBindingSite in QName:
     -- Saves 10% on serialization time (and file size)!
+    --
+    -- NOTE: We no longer discard all nameBindingSites (but the commit
+    -- that introduced this change seems to have made Agda a bit
+    -- faster and interface file sizes a bit smaller, at least for the
+    -- standard library).
     builtin <- use stLocalBuiltins
     ms      <- getImports
     mhs     <- mapM (\ m -> (m,) <$> moduleHash m) $ Set.toList ms
@@ -736,7 +741,8 @@
     -- Non-closed display forms are not applicable outside the module anyway,
     -- and should be dead-code eliminated (#1928).
     display <- HMap.filter (not . null) . HMap.map (filter isClosed) <$> use stImportsDisplayForms
-    (display, sig) <- second killRange <$> (eliminateDeadCode display =<< getSignature)
+    -- TODO: Kill some ranges?
+    (display, sig) <- eliminateDeadCode display =<< getSignature
     -- Andreas, 2015-02-09 kill ranges in pattern synonyms before
     -- serialization to avoid error locations pointing to external files
     -- when expanding a pattern synoym.
diff --git a/src/full/Agda/Syntax/Common.hs b/src/full/Agda/Syntax/Common.hs
--- a/src/full/Agda/Syntax/Common.hs
+++ b/src/full/Agda/Syntax/Common.hs
@@ -18,6 +18,7 @@
 import qualified Data.ByteString.Char8 as ByteString
 import Data.Foldable
 import Data.Hashable
+import qualified Data.Strict.Maybe as Strict
 import Data.Monoid
 import Data.Traversable
 import Data.Typeable (Typeable)
@@ -768,32 +769,49 @@
 
 newtype Constr a = Constr a
 
-data Placeholder
+------------------------------------------------------------------------
+-- * Placeholders (used to parse sections)
+------------------------------------------------------------------------
+
+-- | The position of a name part or underscore in a name.
+
+data PositionInName
   = Beginning
-    -- ^ @_foo@.
+    -- ^ The following underscore is at the beginning of the name:
+    -- @_foo@.
   | Middle
-    -- ^ @foo_bar@.
+    -- ^ The following underscore is in the middle of the name:
+    -- @foo_bar@.
   | End
-    -- ^ @foo_@.
+    -- ^ The following underscore is at the end of the name: @foo_@.
   deriving (Show, Eq, Ord)
 
 -- | Placeholders are used to represent the underscores in a section.
+
 data MaybePlaceholder e
-  = Placeholder !Placeholder
-  | NoPlaceholder e
+  = Placeholder !PositionInName
+  | NoPlaceholder !(Strict.Maybe PositionInName) e
+    -- ^ The second argument is used only (but not always) for name
+    -- parts other than underscores.
   deriving (Typeable, Eq, Ord, Functor, Foldable, Traversable, Show)
 
+-- | An abbreviation: @noPlaceholder = 'NoPlaceholder'
+-- 'Strict.Nothing'@.
+
+noPlaceholder :: e -> MaybePlaceholder e
+noPlaceholder = NoPlaceholder Strict.Nothing
+
 instance HasRange a => HasRange (MaybePlaceholder a) where
-  getRange Placeholder{}     = noRange
-  getRange (NoPlaceholder e) = getRange e
+  getRange Placeholder{}       = noRange
+  getRange (NoPlaceholder _ e) = getRange e
 
 instance KillRange a => KillRange (MaybePlaceholder a) where
-  killRange p@Placeholder{}   = p
-  killRange (NoPlaceholder e) = killRange1 NoPlaceholder e
+  killRange p@Placeholder{}     = p
+  killRange (NoPlaceholder p e) = killRange1 (NoPlaceholder p) e
 
 instance NFData a => NFData (MaybePlaceholder a) where
-  rnf (Placeholder _)   = ()
-  rnf (NoPlaceholder a) = rnf a
+  rnf (Placeholder _)     = ()
+  rnf (NoPlaceholder _ a) = rnf a
 
 ---------------------------------------------------------------------------
 -- * Interaction meta variables
diff --git a/src/full/Agda/Syntax/Concrete/Operators.hs b/src/full/Agda/Syntax/Concrete/Operators.hs
--- a/src/full/Agda/Syntax/Concrete/Operators.hs
+++ b/src/full/Agda/Syntax/Concrete/Operators.hs
@@ -452,9 +452,9 @@
             nonAssoc = case filter (isInfix NonAssoc) ops of
               []  -> Nothing
               ops -> Just $ do
-                x <- NoPlaceholder <$> higher
+                x <- noPlaceholder <$> higher
                 f <- choice In ops
-                y <- NoPlaceholder <$> higher
+                y <- noPlaceholder <$> higher
                 return (f x y)
 
             or p1 []   p2 []   = Nothing
@@ -466,7 +466,7 @@
             preRight =
               or (choice Pre)
                  (filter isPrefix ops)
-                 (\ops -> flip ($) <$> (NoPlaceholder <$> higher)
+                 (\ops -> flip ($) <$> (noPlaceholder <$> higher)
                                    <*> choice In ops)
                  (filter (isInfix RightAssoc) ops)
 
@@ -474,14 +474,14 @@
             preRights = do
               preRight <- preRight
               return $ Data.Function.fix $ \preRights ->
-                preRight <*> (NoPlaceholder <$> (preRights <|> higher))
+                preRight <*> (noPlaceholder <$> (preRights <|> higher))
 
             postLeft :: Maybe (Parser e (MaybePlaceholder e -> e))
             postLeft =
               or (choice Post)
                  (filter isPostfix ops)
                  (\ops -> flip <$> choice In ops
-                               <*> (NoPlaceholder <$> higher))
+                               <*> (noPlaceholder <$> higher))
                  (filter (isInfix LeftAssoc) ops)
 
             postLefts :: Maybe (Parser e e)
@@ -489,7 +489,7 @@
               postLeft <- postLeft
               return $ Data.Function.fix $ \postLefts ->
                 memoise (PostLeftsK key) $
-                  flip ($) <$> (NoPlaceholder <$> (postLefts <|> higher))
+                  flip ($) <$> (noPlaceholder <$> (postLefts <|> higher))
                            <*> postLeft
 
 ---------------------------------------------------------------------------
diff --git a/src/full/Agda/Syntax/Concrete/Operators/Parser.hs b/src/full/Agda/Syntax/Concrete/Operators/Parser.hs
--- a/src/full/Agda/Syntax/Concrete/Operators/Parser.hs
+++ b/src/full/Agda/Syntax/Concrete/Operators/Parser.hs
@@ -12,6 +12,7 @@
 import Data.Either
 import Data.Hashable
 import Data.Maybe
+import qualified Data.Strict.Maybe as Strict
 import Data.Set (Set)
 
 import GHC.Generics (Generic)
@@ -42,26 +43,26 @@
 type Parser tok a =
   MemoisedCPS.Parser MemoKey tok (MaybePlaceholder tok) a
 
-placeholder :: Placeholder -> Parser e (MaybePlaceholder e)
+placeholder :: PositionInName -> Parser e (MaybePlaceholder e)
 placeholder p = sat $ \t ->
   case t of
     Placeholder p' | p' == p -> True
     _                        -> False
 
 maybePlaceholder ::
-  Maybe Placeholder -> Parser e e -> Parser e (MaybePlaceholder e)
+  Maybe PositionInName -> Parser e e -> Parser e (MaybePlaceholder e)
 maybePlaceholder mp p = case mp of
   Nothing -> p'
   Just h  -> placeholder h <|> p'
   where
-  p' = NoPlaceholder <$> p
+  p' = noPlaceholder <$> p
 
 notPlaceholder :: Parser e e
 notPlaceholder = do
   tok <- token
   case tok of
-    Placeholder _   -> empty
-    NoPlaceholder e -> return e
+    Placeholder _     -> empty
+    NoPlaceholder _ e -> return e
 
 sat' :: (e -> Bool) -> Parser e e
 sat' p = do
@@ -116,7 +117,7 @@
         IdentP x         -> LocalV x
         AppP e1 e2       -> AppV e1 e2
         OpAppP r d ns es -> OpAppV d ns ((map . fmap . fmap)
-                                           (NoPlaceholder . Ordinary) es)
+                                           (noPlaceholder . Ordinary) es)
         HiddenP _ e      -> HiddenArgV e
         InstanceP _ e    -> InstanceArgV e
         ParenP _ e       -> ParenV e
@@ -128,8 +129,8 @@
         OpAppV d ns es -> let ess :: [NamedArg Pattern]
                               ess = (map . fmap . fmap)
                                       (\x -> case x of
-                                          Placeholder{}   -> __IMPOSSIBLE__
-                                          NoPlaceholder x -> fromOrdinary __IMPOSSIBLE__ x)
+                                          Placeholder{}     -> __IMPOSSIBLE__
+                                          NoPlaceholder _ x -> fromOrdinary __IMPOSSIBLE__ x)
                                       es
                           in OpAppP (fuseRange d ess) d ns ess
         HiddenArgV e   -> HiddenP (getRange e) e
@@ -143,8 +144,13 @@
 data ParseSections = ParseSections | DoNotParseSections
   deriving (Eq, Show)
 
+-- | Runs a parser. If sections should be parsed, then identifiers
+-- with at least two name parts are split up into multiple tokens,
+-- using 'PositionInName' to record the tokens' original positions
+-- within their respective identifiers.
+
 parse :: IsExpr e => (ParseSections, Parser e a) -> [e] -> [a]
-parse (DoNotParseSections, p) es = Parser.parse p (map NoPlaceholder es)
+parse (DoNotParseSections, p) es = Parser.parse p (map noPlaceholder es)
 parse (ParseSections,      p) es = Parser.parse p
                                      (concat $ map splitExpr es)
   where
@@ -153,11 +159,11 @@
     LocalV n -> splitName n
     _        -> noSplit
     where
-    noSplit = [NoPlaceholder e]
+    noSplit = [noPlaceholder e]
 
     splitName n = case last ns of
-      NoName{}  -> noSplit
-      Name r ps -> splitParts r (init ns) Beginning ps
+      Name r ps@(_ : _ : _) -> splitParts r (init ns) Beginning ps
+      _                     -> noSplit
       where
       ns = qnameParts n
 
@@ -168,14 +174,17 @@
       -- Note also that the module qualifier, if any, is only applied
       -- to the first name part.
 
-      splitParts _ _ _ []          = []
+      splitParts _ _ _ []          = __IMPOSSIBLE__
       splitParts _ _ _ (Hole : []) = [Placeholder End]
+      splitParts r m _ (Id s : []) = [part r m End s]
       splitParts r m w (Hole : ps) = Placeholder w : splitParts r m  Middle ps
-      splitParts r m _ (Id s : ps) = part          : splitParts r [] Middle ps
-        where
-        part = NoPlaceholder $ unExprView $ LocalV $
-                 foldr Qual (QName (Name r [Id s])) m
+      splitParts r m w (Id s : ps) = part r m w s  : splitParts r [] Middle ps
 
+      part r m w s =
+        NoPlaceholder (Strict.Just w)
+                      (unExprView $ LocalV $
+                         foldr Qual (QName (Name r [Id s])) m)
+
 ---------------------------------------------------------------------------
 -- * Parser combinators
 ---------------------------------------------------------------------------
@@ -196,6 +205,51 @@
             LocalV y | str == show y -> Just (getRange y)
             _                        -> Nothing
 
+-- | Parses a split-up, unqualified name consisting of at least two
+-- name parts.
+--
+-- The parser does not check that underscores and other name parts
+-- alternate. The range of the resulting name is the range of the
+-- first name part that is not an underscore.
+
+atLeastTwoParts :: IsExpr e => Parser e Name
+atLeastTwoParts = do
+  (r, ps) <- parts Beginning
+  case r of
+    Nothing -> __IMPOSSIBLE__
+    Just r  -> return (Name r ps)
+  where
+  parts pos = do
+    tok          <- token
+    (pos', r, p) <- case tok of
+      Placeholder pos'                   -> return (pos', Nothing, Hole)
+      NoPlaceholder (Strict.Just pos') e -> case exprView e of
+        LocalV (QName (Name r [Id s])) -> return (pos', Just r, Id s)
+        _                              -> empty
+      _ -> empty
+    if pos == Middle && pos' == End then
+      return (r, [p])
+     else if pos' == pos then do
+      (r', ps) <- parts Middle
+      return (maybe r' Just r, p : ps)
+     else
+      empty
+
+-- | Either a wildcard (@_@), or an unqualified name (possibly
+-- containing multiple name parts).
+
+wildOrUnqualifiedName :: IsExpr e => Parser e (Maybe Name)
+wildOrUnqualifiedName =
+  (Nothing <$ partP [] "_")
+    <|>
+  (do e <- notPlaceholder
+      case exprView e of
+        LocalV (QName n) -> return (Just n)
+        WildV _          -> return Nothing
+        _                -> empty)
+    <|>
+  Just <$> atLeastTwoParts
+
 -- | Used to define the return type of 'opP'.
 
 type family OperatorType (k :: NotationKind) (e :: *) :: *
@@ -288,13 +342,10 @@
     (r, es) <- worker ms xs
     return (r, Right (mkBinding h $ Name noRange [Hole]) : es)
   worker ms (BindHole h : xs) = do
-    e <- notPlaceholder
-    case exprView e of
-      LocalV (QName name) -> ret name
-      WildV e             -> ret (Name noRange [Hole])
-      _                   -> empty
-        -- Old error message: "Expected variable name in binding
-        -- position".
+    e <- wildOrUnqualifiedName
+    case e of
+      Just name -> ret name
+      Nothing   -> ret (Name noRange [Hole])
     where
     ret x = do
       (r, es) <- worker ms xs
@@ -311,10 +362,10 @@
     NamedArg (MaybePlaceholder (OpApp e))
   findExprFor normalHoles binders n =
     case [ h | h@(_, m) <- normalHoles, namedArg m == n ] of
-      [(Placeholder p,   arg)] -> set (Placeholder p) arg
-      [(NoPlaceholder e, arg)] -> case [b | (b, m) <- binders, m == n] of
-        [] -> set (NoPlaceholder (Ordinary e)) arg -- no variable to bind
-        bs -> set (NoPlaceholder (SyntaxBindingLambda (fuseRange bs e) bs e)) arg
+      [(Placeholder p,     arg)] -> set (Placeholder p) arg
+      [(NoPlaceholder _ e, arg)] -> case [b | (b, m) <- binders, m == n] of
+        [] -> set (noPlaceholder (Ordinary e)) arg -- no variable to bind
+        bs -> set (noPlaceholder (SyntaxBindingLambda (fuseRange bs e) bs e)) arg
       _ -> __IMPOSSIBLE__
 
   noPlaceholders :: [NamedArg (MaybePlaceholder (OpApp e))] -> Int
diff --git a/src/full/Agda/Syntax/Concrete/Pretty.hs b/src/full/Agda/Syntax/Concrete/Pretty.hs
--- a/src/full/Agda/Syntax/Concrete/Pretty.hs
+++ b/src/full/Agda/Syntax/Concrete/Pretty.hs
@@ -12,6 +12,7 @@
 
 import Data.Functor
 import Data.Maybe
+import qualified Data.Strict.Maybe as Strict
 
 import Agda.Syntax.Common
 import Agda.Syntax.Concrete
@@ -105,8 +106,8 @@
   pretty (SyntaxBindingLambda r bs e) = pretty (Lam r bs e)
 
 instance Pretty a => Pretty (MaybePlaceholder a) where
-  pretty Placeholder{}     = text "_"
-  pretty (NoPlaceholder e) = pretty e
+  pretty Placeholder{}       = text "_"
+  pretty (NoPlaceholder _ e) = pretty e
 
 instance Pretty Expr where
     pretty e =
@@ -511,7 +512,7 @@
             IdentP x        -> pretty x
             AppP p1 p2      -> sep [ pretty p1, nest 2 $ pretty p2 ]
             RawAppP _ ps    -> fsep $ map pretty ps
-            OpAppP _ q _ ps -> fsep $ prettyOpApp q (fmap (fmap (fmap NoPlaceholder)) ps)
+            OpAppP _ q _ ps -> fsep $ prettyOpApp q (fmap (fmap (fmap (NoPlaceholder Strict.Nothing))) ps)
             HiddenP _ p     -> braces' $ pretty p
             InstanceP _ p   -> dbraces $ pretty p
             ParenP _ p      -> parens $ pretty p
@@ -545,7 +546,7 @@
 
     -- Section underscores should be printed without surrounding
     -- whitespace. This function takes care of that.
-    merge :: [Doc] -> [(Doc, Maybe Placeholder)] -> [Doc]
+    merge :: [Doc] -> [(Doc, Maybe PositionInName)] -> [Doc]
     merge before []                            = reverse before
     merge before ((d, Nothing) : after)        = merge (d : before) after
     merge before ((d, Just Beginning) : after) = mergeRight before d after
diff --git a/src/full/Agda/Syntax/Translation/AbstractToConcrete.hs b/src/full/Agda/Syntax/Translation/AbstractToConcrete.hs
--- a/src/full/Agda/Syntax/Translation/AbstractToConcrete.hs
+++ b/src/full/Agda/Syntax/Translation/AbstractToConcrete.hs
@@ -914,7 +914,7 @@
 cOpApp :: Range -> C.QName -> A.Name -> [C.Expr] -> C.Expr
 cOpApp r x n es =
   C.OpApp r x (Set.singleton n)
-          (map (defaultNamedArg . NoPlaceholder . Ordinary) es)
+          (map (defaultNamedArg . noPlaceholder . Ordinary) es)
 
 tryToRecoverOpApp :: A.Expr -> AbsToCon C.Expr -> AbsToCon C.Expr
 tryToRecoverOpApp e def = caseMaybeM (recoverOpApp bracket cOpApp view e) def return
diff --git a/src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs b/src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs
--- a/src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs
+++ b/src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs
@@ -2049,9 +2049,9 @@
       ScopeM ([A.LamBinding], [NamedArg (Either A.Expr (OpApp e))])
     replacePlaceholders []       = return ([], [])
     replacePlaceholders (a : as) = case namedArg a of
-      NoPlaceholder x -> mapSnd (set (Right x) a :) <$>
-                           replacePlaceholders as
-      Placeholder p   -> do
+      NoPlaceholder _ x -> mapSnd (set (Right x) a :) <$>
+                             replacePlaceholders as
+      Placeholder _     -> do
         x <- freshName noRange "section"
         let i = argInfo a
         (ls, ns) <- replacePlaceholders as
diff --git a/src/full/Agda/Syntax/Translation/InternalToAbstract.hs b/src/full/Agda/Syntax/Translation/InternalToAbstract.hs
--- a/src/full/Agda/Syntax/Translation/InternalToAbstract.hs
+++ b/src/full/Agda/Syntax/Translation/InternalToAbstract.hs
@@ -46,6 +46,7 @@
 import Agda.Syntax.Concrete (FieldAssignment'(..), exprFieldA)
 import Agda.Syntax.Info as Info
 import Agda.Syntax.Abstract as A
+import Agda.Syntax.Abstract.Pretty
 import Agda.Syntax.Internal as I
 import Agda.Syntax.Internal.Pattern as I
 import Agda.Syntax.Scope.Base (isNameInScope, inverseScopeLookupName)
@@ -69,6 +70,7 @@
 import Agda.Utils.Maybe
 import Agda.Utils.Monad
 import Agda.Utils.Permutation
+import Agda.Utils.Pretty
 import Agda.Utils.Size
 import Agda.Utils.Tuple
 
@@ -198,16 +200,25 @@
     -- Ulf, can you add an explanation?
     md <- liftTCM $ -- addContext (replicate (length ps) "x") $
       displayForm f vs
-    reportSLn "reify.display" 20 $
+    reportSLn "reify.display" 60 $
       "display form of " ++ show f ++ " " ++ show ps ++ " " ++ show wps ++ ":\n  " ++ show md
     case md of
-      Just d  | okDisplayForm d ->
+      Just d  | okDisplayForm d -> do
         -- In the display term @d@, @var i@ should be a placeholder
         -- for the @i@th pattern of @ps@.
         -- Andreas, 2014-06-11:
         -- Are we sure that @d@ did not use @var i@ otherwise?
-        reifyDisplayFormP =<< displayLHS (map namedArg ps) wps d
-      _ -> return lhs
+        lhs' <- displayLHS (map namedArg ps) wps d
+        reportSDoc "reify.display" 70 $ do
+          doc <- prettyA lhs'
+          return $ vcat
+            [ text "rewritten lhs to"
+            , text "  lhs' = " <+> doc
+            ]
+        reifyDisplayFormP lhs'
+      _ -> do
+        reportSLn "reify.display" 70 $ "display form absent or not valid as lhs"
+        return lhs
   where
     -- Andreas, 2015-05-03: Ulf, please comment on what
     -- is the idea behind okDisplayForm.
@@ -215,13 +226,15 @@
     -- can serve as a valid left-hand side. That means checking that it is a
     -- defined name applied to valid lhs eliminators (projections or
     -- applications to constructor patterns).
-    okDisplayForm (DWithApp d ds [])   = okDisplayForm d && all okDisplayTerm ds
+    okDisplayForm (DWithApp d ds args) =
+      okDisplayForm d && all okDisplayTerm ds  && all okToDrop args
+      -- Andreas, 2016-05-03, issue #1950.
+      -- We might drop trailing hidden trivial (=variable) patterns.
     okDisplayForm (DTerm (I.Def f vs)) = all okElim vs
     okDisplayForm (DDef f es)          = all okDElim es
     okDisplayForm DDot{}               = False
     okDisplayForm DCon{}               = False
     okDisplayForm DTerm{}              = False
-    okDisplayForm DWithApp{}           = False
 
     okDisplayTerm (DTerm v) = okTerm v
     okDisplayTerm DDot{}    = True
@@ -231,6 +244,12 @@
 
     okDElim (I.Apply v) = okDisplayTerm $ unArg v
     okDElim I.Proj{}    = True
+
+    okToDrop arg = notVisible arg && case ignoreSharing $ unArg arg of
+      I.Var _ []   -> True
+      I.DontCare{} -> True  -- no matching on irrelevant things.  __IMPOSSIBLE__ anyway?
+      I.Level{}    -> True  -- no matching on levels. __IMPOSSIBLE__ anyway?
+      _ -> False
 
     okArg = okTerm . unArg
 
diff --git a/src/full/Agda/TypeChecking/Constraints.hs b/src/full/Agda/TypeChecking/Constraints.hs
--- a/src/full/Agda/TypeChecking/Constraints.hs
+++ b/src/full/Agda/TypeChecking/Constraints.hs
@@ -25,6 +25,7 @@
 import Agda.Utils.Maybe
 import Agda.Utils.Monad
 import Agda.Utils.Pretty (prettyShow)
+import Agda.Utils.Lens
 
 #include "undefined.h"
 import Agda.Utils.Impossible
@@ -205,4 +206,13 @@
   CheckArgs eh r args t0 t1 k    -> checkArguments' eh r args t0 t1 k
   CheckLambda args body target   -> checkPostponedLambda args body target
   UnquoteTactic tac hole t       -> unquoteTactic tac hole t $ return hole
+
+debugConstraints :: TCM ()
+debugConstraints = verboseS "tc.constr" 50 $ do
+  awake    <- use stAwakeConstraints
+  sleeping <- use stSleepingConstraints
+  reportSDoc "" 0 $ vcat
+    [ text "Current constraints"
+    , nest 2 $ vcat [ text "awake " <+> vcat (map prettyTCM awake)
+                    , text "asleep" <+> vcat (map prettyTCM sleeping) ] ]
 
diff --git a/src/full/Agda/TypeChecking/Constraints.hs-boot b/src/full/Agda/TypeChecking/Constraints.hs-boot
--- a/src/full/Agda/TypeChecking/Constraints.hs-boot
+++ b/src/full/Agda/TypeChecking/Constraints.hs-boot
@@ -9,3 +9,4 @@
 noConstraints          :: TCM a -> TCM a
 ifNoConstraints_       :: TCM () -> TCM a -> (ProblemId -> TCM a) -> TCM a
 guardConstraint        :: Constraint -> TCM () -> TCM ()
+debugConstraints       :: TCM ()
diff --git a/src/full/Agda/TypeChecking/Coverage.hs b/src/full/Agda/TypeChecking/Coverage.hs
--- a/src/full/Agda/TypeChecking/Coverage.hs
+++ b/src/full/Agda/TypeChecking/Coverage.hs
@@ -551,7 +551,10 @@
 
 -- | Entry point from @Interaction.MakeCase@.
 splitClauseWithAbsurd :: SplitClause -> Nat -> TCM (Either SplitError (Either SplitClause Covering))
-splitClauseWithAbsurd c x = split' Inductive c (BlockingVar x Nothing)
+splitClauseWithAbsurd c x = split' Inductive False c (BlockingVar x Nothing)
+  -- Andreas, 2016-05-03, issue 1950:
+  -- Do not introduce trailing pattern vars after split,
+  -- because this does not work for with-clauses.
 
 -- | Entry point from @TypeChecking.Empty@ and @Interaction.BasicOps@.
 --   @splitLast CoInductive@ is used in the @refine@ tactics.
@@ -578,7 +581,7 @@
       -> SplitClause
       -> BlockingVar
       -> TCM (Either SplitError Covering)
-split ind sc x = fmap blendInAbsurdClause <$> split' ind sc x
+split ind sc x = fmap blendInAbsurdClause <$> split' ind True sc x
   where
     n = lookupPatternVar sc $ blockingVarNo x
     blendInAbsurdClause :: Either SplitClause Covering -> Covering
@@ -613,10 +616,13 @@
 split' :: Induction
           -- ^ Coinductive constructors are allowed if this argument is
           -- 'CoInductive'.
+       -> Bool
+          -- ^ If 'True', introduce new trailing variable patterns via
+          --   'fixTarget'.
        -> SplitClause
        -> BlockingVar
        -> TCM (Either SplitError (Either SplitClause Covering))
-split' ind sc@(SClause tel ps _ target) (BlockingVar x mcons) = liftTCM $ runExceptionT $ do
+split' ind fixtarget sc@(SClause tel ps _ target) (BlockingVar x mcons) = liftTCM $ runExceptionT $ do
 
   debugInit tel x ps
 
@@ -636,6 +642,7 @@
     forM cons $ \ con ->
       fmap (con,) <$> do
         msc <- computeNeighbourhood delta1 n delta2 d pars ixs x ps con
+        if not fixtarget then return msc else do
         Trav.forM msc $ \ sc -> lift $ snd <$> fixTarget sc{ scTarget = target }
 
   case ns of
diff --git a/src/full/Agda/TypeChecking/Errors.hs b/src/full/Agda/TypeChecking/Errors.hs
--- a/src/full/Agda/TypeChecking/Errors.hs
+++ b/src/full/Agda/TypeChecking/Errors.hs
@@ -839,12 +839,12 @@
         unambiguous e = pretty e
 
         isOrdinary :: MaybePlaceholder (C.OpApp e) -> Bool
-        isOrdinary (NoPlaceholder (C.Ordinary _)) = True
-        isOrdinary _                              = False
+        isOrdinary (NoPlaceholder _ (C.Ordinary _)) = True
+        isOrdinary _                                = False
 
         fromOrdinary :: MaybePlaceholder (C.OpApp e) -> e
-        fromOrdinary (NoPlaceholder (C.Ordinary e)) = e
-        fromOrdinary _                              = __IMPOSSIBLE__
+        fromOrdinary (NoPlaceholder _ (C.Ordinary e)) = e
+        fromOrdinary _                                = __IMPOSSIBLE__
 
         isPlaceholder :: MaybePlaceholder a -> Bool
         isPlaceholder Placeholder{}   = True
diff --git a/src/full/Agda/TypeChecking/Implicit.hs b/src/full/Agda/TypeChecking/Implicit.hs
--- a/src/full/Agda/TypeChecking/Implicit.hs
+++ b/src/full/Agda/TypeChecking/Implicit.hs
@@ -16,7 +16,6 @@
 import Agda.TypeChecking.Monad
 import Agda.TypeChecking.Reduce
 import Agda.TypeChecking.Substitute
-import {-# SOURCE #-} Agda.TypeChecking.InstanceArguments
 import Agda.TypeChecking.Pretty
 
 import Agda.Utils.Tuple
@@ -53,9 +52,10 @@
           mapFst (narg :) <$> implicitNamedArgs (n-1) expand (absApp b v)
       _ -> return ([], t0')
   where
+    newMeta :: Hiding -> String -> Type -> TCM Term
     newMeta Hidden   = newNamedValueMeta RunMetaOccursCheck
-    newMeta Instance = initializeIFSMeta
-    newMeta NotHidden = initializeIFSMeta
+    newMeta Instance = newIFSMeta
+    newMeta NotHidden = newIFSMeta
 
 ---------------------------------------------------------------------------
 
diff --git a/src/full/Agda/TypeChecking/InstanceArguments.hs b/src/full/Agda/TypeChecking/InstanceArguments.hs
--- a/src/full/Agda/TypeChecking/InstanceArguments.hs
+++ b/src/full/Agda/TypeChecking/InstanceArguments.hs
@@ -111,14 +111,6 @@
         handle (TypeError _ (Closure {clValue = InternalError _})) = return Nothing
         handle err                                                 = throwError err
 
--- | @initializeIFSMeta s t@ generates an instance meta of type @t@
---   with suggested name @s@, possibly with leading lambdas.
-initializeIFSMeta :: String -> Type -> TCM Term
-initializeIFSMeta s t = do
-  t <- reduce t  -- see Issue 1321
-  cands <- initialIFSCandidates t
-  newIFSMeta s t cands
-
 -- | @findInScope m (v,a)s@ tries to instantiate on of the types @a@s
 --   of the candidate terms @v@s to the type @t@ of the metavariable @m@.
 --   If successful, meta @m@ is solved with the instantiation of @v@.
@@ -169,6 +161,7 @@
       reportSDoc "tc.instance" 70 $ nest 2 $ vcat
         [ sep [ prettyTCM v <+> text ":", nest 2 $ prettyTCM t ] | Candidate v t _ <- cands ]
       t <- normalise =<< getMetaTypeInContext m
+      insidePi t $ \ t -> do
       reportSDoc "tc.instance" 15 $ text "findInScope 3: t =" <+> prettyTCM t
       reportSLn "tc.instance" 70 $ "findInScope 3: t: " ++ show t
 
@@ -177,6 +170,7 @@
       ifJustM (areThereNonRigidMetaArguments (unEl t)) (\ m -> return (Just (cands, Just m))) $ do
 
         mcands <- checkCandidates m t cands
+        debugConstraints
         case mcands of
 
           Just [] -> do
@@ -192,6 +186,10 @@
               , text "for type" <+> prettyTCM t
               ]
 
+            -- If we actually solved the constraints we should wake up any held
+            -- instance constraints, to make sure we don't forget about them.
+            wakeConstraints (return . const True)
+            solveAwakeConstraints' False
             return Nothing  -- We’re done
 
           _ -> do
@@ -201,6 +199,22 @@
               prettyTCM (List.map candidateTerm cs)
             return (Just (cs, Nothing))
 
+-- | Precondition: type is spine reduced and ends in a Def or a Var.
+insidePi :: Type -> (Type -> TCM a) -> TCM a
+insidePi t ret =
+  case ignoreSharing $ unEl t of
+    Pi a b     -> addContext (absName b, a) $ insidePi (unAbs b) ret
+    Def{}      -> ret t
+    Var{}      -> ret t
+    Sort{}     -> __IMPOSSIBLE__
+    Con{}      -> __IMPOSSIBLE__
+    Lam{}      -> __IMPOSSIBLE__
+    Lit{}      -> __IMPOSSIBLE__
+    Level{}    -> __IMPOSSIBLE__
+    MetaV{}    -> __IMPOSSIBLE__
+    Shared{}   -> __IMPOSSIBLE__
+    DontCare{} -> __IMPOSSIBLE__
+
 -- | A meta _M is rigidly constrained if there is a constraint _M us == D vs,
 -- for inert D. Such metas can safely be instantiated by recursive instance
 -- search, since the constraint limits the solution space.
@@ -309,18 +323,21 @@
 --   If the resulting list contains exactly one element, then the state is the
 --   same as the one obtained after running the corresponding computation. In
 --   all the other cases, the state is reseted.
-filterResetingState :: MetaId -> [Candidate] -> (Candidate -> TCM Bool) -> TCM [Candidate]
+filterResetingState :: MetaId -> [Candidate] -> (Candidate -> TCM YesNoMaybe) -> TCM [Candidate]
 filterResetingState m cands f = disableDestructiveUpdate $ do
   ctxArgs  <- getContextArgs
   let ctxElims = map Apply ctxArgs
       tryC c = do
         ok <- f c
         v  <- instantiateFull (MetaV m ctxElims)
-        a  <- instantiateFull =<< (`piApply` ctxArgs) <$> getMetaType m
+        a  <- instantiateFull =<< (`piApplyM` ctxArgs) =<< getMetaType m
         return (ok, v, a)
   result <- mapM (\c -> do bs <- localTCStateSaving (tryC c); return (c, bs)) cands
-  let result' = [ (c, v, a, s) | (c, ((True, v, a), s)) <- result ]
-  result <- dropSameCandidates m result'
+  let result' = [ (c, v, a, s) | (c, ((r, v, a), s)) <- result, r /= No ]
+      noMaybes = null [ Maybe | (_, ((Maybe, _, _), _)) <- result ]
+            -- It's not safe to compare maybes for equality because they might
+            -- not have instantiated at all.
+  result <- if noMaybes then dropSameCandidates m result' else return result'
   case result of
     [(c, _, _, s)] -> [c] <$ put s
     _              -> return [ c | (c, _, _, _) <- result ]
@@ -355,12 +372,16 @@
                              {- else -} (\ _ -> return False)
                              `catchError` (\ _ -> return False)
 
+data YesNoMaybe = Yes | No | Maybe
+  deriving (Show, Eq)
+
 -- | Given a meta @m@ of type @t@ and a list of candidates @cands@,
 -- @checkCandidates m t cands@ returns a refined list of valid candidates.
 checkCandidates :: MetaId -> Type -> [Candidate] -> TCM (Maybe [Candidate])
 checkCandidates m t cands = disableDestructiveUpdate $
   verboseBracket "tc.instance.candidates" 20 ("checkCandidates " ++ prettyShow m) $
-  ifM (anyMetaTypes cands) (return Nothing) $ Just <$> do
+  ifM (anyMetaTypes cands) (return Nothing) $
+  holdConstraints (\ _ -> isIFSConstraint . clValue . theConstraint) $ Just <$> do
     reportSDoc "tc.instance.candidates" 20 $ nest 2 $ text "target:" <+> prettyTCM t
     reportSDoc "tc.instance.candidates" 20 $ nest 2 $ vcat
       [ text "candidates"
@@ -379,14 +400,15 @@
         MetaV{} -> return True
         _       -> anyMetaTypes cands
 
-    checkCandidateForMeta :: MetaId -> Type -> Candidate -> TCM Bool
+    checkCandidateForMeta :: MetaId -> Type -> Candidate -> TCM YesNoMaybe
     checkCandidateForMeta m t (Candidate term t' eti) = do
       -- Andreas, 2015-02-07: New metas should be created with range of the
       -- current instance meta, thus, we set the range.
       mv <- lookupMeta m
       setCurrentRange mv $ do
-        verboseBracket "tc.instance" 20 ("checkCandidateForMeta " ++ prettyShow m) $ do
-          liftTCM $ flip catchError handle $ do
+        debugConstraints
+        verboseBracket "tc.instance" 20 ("checkCandidateForMeta " ++ prettyShow m) $
+          liftTCM $ runCandidateCheck $ do
             reportSLn "tc.instance" 70 $ "  t: " ++ show t ++ "\n  t':" ++ show t' ++ "\n  term: " ++ show term ++ "."
             reportSDoc "tc.instance" 20 $ vcat
               [ text "checkCandidateForMeta"
@@ -415,24 +437,37 @@
             -- unsolvable by the assignment, but don't do this for FindInScope's
             -- to prevent loops. We currently also ignore UnBlock constraints
             -- to be on the safe side.
+            debugConstraints
             solveAwakeConstraints' True
+
             verboseS "tc.instance" 15 $ do
               sol <- instantiateFull (MetaV m ctxElims)
-              reportSDoc "tc.instance" 15 $
-                sep [ text "instance search: found solution for" <+> prettyTCM m <> text ":"
-                    , nest 2 $ prettyTCM sol ]
-            return True
+              case sol of
+                MetaV m' _ | m == m' ->
+                  reportSDoc "tc.instance" 15 $
+                    sep [ text "instance search: maybe solution for" <+> prettyTCM m <> text ":"
+                        , nest 2 $ prettyTCM v ]
+                _ ->
+                  reportSDoc "tc.instance" 15 $
+                    sep [ text "instance search: found solution for" <+> prettyTCM m <> text ":"
+                        , nest 2 $ prettyTCM sol ]
         where
-          handle :: TCErr -> TCM Bool
+          runCandidateCheck check =
+            flip catchError handle $
+            ifNoConstraints_ check
+              (return Yes)
+              (\ _ -> Maybe <$ reportSLn "tc.instance" 50 "assignment inconclusive")
+
+          handle :: TCErr -> TCM YesNoMaybe
           handle err = do
             reportSDoc "tc.instance" 50 $
               text "assignment failed:" <+> prettyTCM err
-            return False
+            return No
 
-    isIFSConstraint :: Constraint -> Bool
-    isIFSConstraint FindInScope{} = True
-    isIFSConstraint UnBlock{}     = True -- otherwise test/fail/Issue723 loops
-    isIFSConstraint _             = False
+isIFSConstraint :: Constraint -> Bool
+isIFSConstraint FindInScope{} = True
+isIFSConstraint UnBlock{}     = True -- otherwise test/fail/Issue723 loops
+isIFSConstraint _             = False
 
 -- | To preserve the invariant that a constructor is not applied to its
 --   parameter arguments, we explicitly check whether function term
diff --git a/src/full/Agda/TypeChecking/InstanceArguments.hs-boot b/src/full/Agda/TypeChecking/InstanceArguments.hs-boot
deleted file mode 100644
--- a/src/full/Agda/TypeChecking/InstanceArguments.hs-boot
+++ /dev/null
@@ -1,7 +0,0 @@
-
-module Agda.TypeChecking.InstanceArguments where
-
-import Agda.TypeChecking.Monad.Base (TCM)
-import Agda.Syntax.Internal (Type, Term)
-
-initializeIFSMeta :: String -> Type -> TCM Term
diff --git a/src/full/Agda/TypeChecking/MetaVars.hs b/src/full/Agda/TypeChecking/MetaVars.hs
--- a/src/full/Agda/TypeChecking/MetaVars.hs
+++ b/src/full/Agda/TypeChecking/MetaVars.hs
@@ -177,20 +177,19 @@
 -- newTypeMeta_  = newTypeMeta Inf
 
 -- | @newIFSMeta s t cands@ creates a new "implicit from scope" metavariable
---   of type the output type of @t@ with name suggestion @s@ and initial
---   solution candidates @cands@. If @t@ is a function type, then insert enough
+--   of type the output type of @t@ with name suggestion @s@.
+--   If @t@ is a function type, then insert enough
 --   lambdas in front of it.
-newIFSMeta :: MetaNameSuggestion -> Type -> Maybe [Candidate] -> TCM Term
-newIFSMeta s t cands = do
+newIFSMeta :: MetaNameSuggestion -> Type -> TCM Term
+newIFSMeta s t = do
   TelV tel t' <- telView t
   addCtxTel tel $ do
     vs  <- getContextArgs
     ctx <- getContextTelescope
-    teleLam tel <$> newIFSMetaCtx s (telePi_ ctx t') vs (raise (size tel) cands)
+    teleLam tel <$> newIFSMetaCtx s (telePi_ ctx t') vs
 
--- | Create a new value meta with specific dependencies.
-newIFSMetaCtx :: MetaNameSuggestion -> Type -> Args -> Maybe [Candidate] -> TCM Term
-newIFSMetaCtx s t vs cands = do
+newIFSMetaCtx :: MetaNameSuggestion -> Type -> Args -> TCM Term
+newIFSMetaCtx s t vs = do
   reportSDoc "tc.meta.new" 50 $ fsep
     [ text "new ifs meta:"
     , nest 2 $ prettyTCM vs <+> text "|-"
@@ -203,11 +202,11 @@
   reportSDoc "tc.meta.new" 50 $ fsep
     [ nest 2 $ pretty x <+> text ":" <+> prettyTCM t
     ]
-  addConstraint $ FindInScope x Nothing cands
+  addConstraint $ FindInScope x Nothing Nothing
   etaExpandMetaSafe x
   return $ MetaV x $ map Apply vs
 
-
+-- | Create a new value meta with specific dependencies.
 newNamedValueMeta :: RunMetaOccursCheck -> MetaNameSuggestion -> Type -> TCM Term
 newNamedValueMeta b s t = do
   v <- newValueMeta b t
diff --git a/src/full/Agda/TypeChecking/MetaVars.hs-boot b/src/full/Agda/TypeChecking/MetaVars.hs-boot
--- a/src/full/Agda/TypeChecking/MetaVars.hs-boot
+++ b/src/full/Agda/TypeChecking/MetaVars.hs-boot
@@ -12,7 +12,7 @@
 etaExpandMetaSafe :: MetaId -> TCM ()
 assignV           :: CompareDirection -> MetaId -> Args -> Term -> TCM ()
 assign            :: CompareDirection -> MetaId -> Args -> Term -> TCM ()
-newIFSMeta        :: String -> Type -> Maybe [Candidate] -> TCM Term
+newIFSMeta        :: String -> Type -> TCM Term
 newValueMeta      :: RunMetaOccursCheck -> Type -> TCM Term
 newNamedValueMeta :: RunMetaOccursCheck -> String -> Type -> TCM Term
 newTelMeta        :: Telescope -> TCM Args
diff --git a/src/full/Agda/TypeChecking/Monad/Base.hs b/src/full/Agda/TypeChecking/Monad/Base.hs
--- a/src/full/Agda/TypeChecking/Monad/Base.hs
+++ b/src/full/Agda/TypeChecking/Monad/Base.hs
@@ -713,8 +713,8 @@
 type Constraints = [ProblemConstraint]
 
 data ProblemConstraint = PConstr
-  { constraintProblem :: ProblemId
-  , theConstraint     :: Closure Constraint
+  { constraintProblems :: [ProblemId]
+  , theConstraint      :: Closure Constraint
   }
   deriving (Typeable, Show)
 
diff --git a/src/full/Agda/TypeChecking/Monad/Constraints.hs b/src/full/Agda/TypeChecking/Monad/Constraints.hs
--- a/src/full/Agda/TypeChecking/Monad/Constraints.hs
+++ b/src/full/Agda/TypeChecking/Monad/Constraints.hs
@@ -16,6 +16,7 @@
 import Agda.Utils.Lens
 import Agda.Utils.List
 import Agda.Utils.Monad
+import Agda.Utils.Except
 
 #include "undefined.h"
 import Agda.Utils.Impossible
@@ -30,21 +31,26 @@
   current <- currentProblem
   reportSLn "tc.constr.steal" 50 $ "problem " ++ show current ++ " is stealing problem " ++ show pid ++ "'s constraints!"
   -- Rename @pid@ to @current@ in all constraints.
-  let rename pc@(PConstr pid' c) | pid' == pid = PConstr current c
-                                 | otherwise   = pc
+  let rename pc@(PConstr pids c) | elem pid pids = PConstr (current : pids) c
+                                 | otherwise     = pc
   -- We should never steal from an active problem.
   whenM (elem pid <$> asks envActiveProblems) __IMPOSSIBLE__
   modifyAwakeConstraints    $ List.map rename
   modifySleepingConstraints $ List.map rename
 
 solvingProblem :: ProblemId -> TCM a -> TCM a
-solvingProblem pid m = verboseBracket "tc.constr.solve" 50 ("working on problem " ++ show pid) $ do
-  x <- local (\e -> e { envActiveProblems = pid : envActiveProblems e }) m
-  ifNotM (isProblemSolved pid)
-    (reportSLn "tc.constr.solve" 50 $ "problem " ++ show pid ++ " was not solved.")
-    $ {- else -} do
-      reportSLn "tc.constr.solve" 50 $ "problem " ++ show pid ++ " was solved!"
-      wakeConstraints (return . blockedOn pid . clValue . theConstraint)
+solvingProblem pid = solvingProblems [pid]
+
+solvingProblems :: [ProblemId] -> TCM a -> TCM a
+solvingProblems pids m = verboseBracket "tc.constr.solve" 50 ("working on problems " ++ show pids) $ do
+  x <- local (\e -> e { envActiveProblems = pids ++ envActiveProblems e }) m
+  sequence_
+    [ ifNotM (isProblemSolved pid)
+        (reportSLn "tc.constr.solve" 50 $ "problem " ++ show pid ++ " was not solved.")
+      $ {- else -} do
+        reportSLn "tc.constr.solve" 50 $ "problem " ++ show pid ++ " was solved!"
+        wakeConstraints (return . blockedOn pid . clValue . theConstraint)
+    | pid <- pids ]
   return x
   where
     blockedOn pid (Guarded _ pid') = pid == pid'
@@ -53,10 +59,10 @@
 isProblemSolved :: ProblemId -> TCM Bool
 isProblemSolved pid =
   and2M (notElem pid <$> asks envActiveProblems)
-        (all ((/= pid) . constraintProblem) <$> getAllConstraints)
+        (all (notElem pid . constraintProblems) <$> getAllConstraints)
 
 getConstraintsForProblem :: ProblemId -> TCM Constraints
-getConstraintsForProblem pid = List.filter ((== pid) . constraintProblem) <$> getAllConstraints
+getConstraintsForProblem pid = List.filter (elem pid . constraintProblems) <$> getAllConstraints
 
 -- | Get the awake constraints
 getAwakeConstraints :: TCM Constraints
@@ -67,8 +73,8 @@
   c <- use stSleepingConstraints
   (wakeup, sleepin) <- partitionM wake c
   reportSLn "tc.constr.wake" 50 $
-    "waking up         " ++ show (List.map constraintProblem wakeup) ++ "\n" ++
-    "  still sleeping: " ++ show (List.map constraintProblem sleepin)
+    "waking up         " ++ show (List.map constraintProblems wakeup) ++ "\n" ++
+    "  still sleeping: " ++ show (List.map constraintProblems sleepin)
   modifySleepingConstraints $ const sleepin
   modifyAwakeConstraints (++ wakeup)
 
@@ -92,6 +98,23 @@
   modifySleepingConstraints $ (++ awakeOnes)
   modifyAwakeConstraints    $ const []
 
+data ConstraintStatus = AwakeConstraint | SleepingConstraint
+  deriving (Eq, Show)
+
+-- | Suspend constraints matching the predicate during the execution of the
+--   second argument. Caution: held sleeping constraints will not be woken up
+--   by events that would normally trigger a wakeup call.
+holdConstraints :: (ConstraintStatus -> ProblemConstraint -> Bool) -> TCM a -> TCM a
+holdConstraints p m = do
+  (holdAwake, stillAwake)   <- partition (p AwakeConstraint)    <$> use stAwakeConstraints
+  (holdAsleep, stillAsleep) <- partition (p SleepingConstraint) <$> use stSleepingConstraints
+  stAwakeConstraints    .= stillAwake
+  stSleepingConstraints .= stillAsleep
+  let restore = do
+        stAwakeConstraints    %= (holdAwake ++)
+        stSleepingConstraints %= (holdAsleep ++)
+  catchError (m <* restore) (\ err -> restore *> throwError err)
+
 takeAwakeConstraint :: TCM (Maybe ProblemConstraint)
 takeAwakeConstraint = do
   cs <- getAwakeConstraints
@@ -105,15 +128,15 @@
 getAllConstraints = gets $ \s -> s^.stAwakeConstraints ++ s^.stSleepingConstraints
 
 withConstraint :: (Constraint -> TCM a) -> ProblemConstraint -> TCM a
-withConstraint f (PConstr pid c) = do
+withConstraint f (PConstr pids c) = do
   -- We should preserve the problem stack and the isSolvingConstraint flag
-  (pids, isSolving) <- asks $ envActiveProblems &&& envSolvingConstraints
+  (pids', isSolving) <- asks $ envActiveProblems &&& envSolvingConstraints
   enterClosure c $ \c ->
-    local (\e -> e { envActiveProblems = pids, envSolvingConstraints = isSolving }) $
-    solvingProblem pid (f c)
+    local (\e -> e { envActiveProblems = pids', envSolvingConstraints = isSolving }) $
+    solvingProblems pids (f c)
 
 buildProblemConstraint :: ProblemId -> Constraint -> TCM ProblemConstraint
-buildProblemConstraint pid c = PConstr pid <$> buildClosure c
+buildProblemConstraint pid c = PConstr [pid] <$> buildClosure c
 
 buildConstraint :: Constraint -> TCM ProblemConstraint
 buildConstraint c = flip buildProblemConstraint c =<< currentProblem
diff --git a/src/full/Agda/TypeChecking/Pretty.hs b/src/full/Agda/TypeChecking/Pretty.hs
--- a/src/full/Agda/TypeChecking/Pretty.hs
+++ b/src/full/Agda/TypeChecking/Pretty.hs
@@ -221,7 +221,7 @@
   prettyTCM UnusedArg  = empty
 
 instance PrettyTCM ProblemConstraint where
-  prettyTCM (PConstr pid c) = brackets (prettyTCM pid) <+> prettyTCM c
+  prettyTCM (PConstr pid c) = prettyList (map prettyTCM pid) <+> prettyTCM c
 
 instance PrettyTCM Constraint where
     prettyTCM c = case c of
diff --git a/src/full/Agda/TypeChecking/Rules/LHS/Unify.hs b/src/full/Agda/TypeChecking/Rules/LHS/Unify.hs
--- a/src/full/Agda/TypeChecking/Rules/LHS/Unify.hs
+++ b/src/full/Agda/TypeChecking/Rules/LHS/Unify.hs
@@ -602,10 +602,10 @@
             reportSDoc "tc.lhs.unify" 80 $ text "Type of constructor: " <+> prettyTCM ctype
             withMetaInfo' mv $ do
               let perm = mvPermutation mv
-              tel <- permuteTel perm <$> getContextTelescope
+              tel <- permuteTel perm <$> (instantiateFull =<< getContextTelescope)
               reportSDoc "tc.lhs.unify" 100 $ text "Context tel (for new metas): " <+> prettyTCM tel
               -- important: create the meta in the same environment as the original meta
-              newArgsMetaCtx ctype tel (mvPermutation mv) us
+              newArgsMetaCtx ctype tel perm us
           reportSDoc "tc.lhs.unify" 80 $ text "Generated meta args: " <+> prettyTCM margs
           noConstraints $ assignV DirEq m us (Con c margs)
           return $ Just margs
diff --git a/src/full/Agda/TypeChecking/Serialise/Instances/Common.hs b/src/full/Agda/TypeChecking/Serialise/Instances/Common.hs
--- a/src/full/Agda/TypeChecking/Serialise/Instances/Common.hs
+++ b/src/full/Agda/TypeChecking/Serialise/Instances/Common.hs
@@ -1,6 +1,8 @@
 {-# LANGUAGE CPP                       #-}
+{-# LANGUAGE DeriveDataTypeable        #-}
 {-# LANGUAGE ExistentialQuantification #-}
 {-# LANGUAGE FlexibleInstances         #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE ScopedTypeVariables       #-}
 
 #if __GLASGOW_HASKELL__ >= 710
@@ -13,7 +15,7 @@
 
 {-# OPTIONS_GHC -fno-warn-orphans #-}
 
-module Agda.TypeChecking.Serialise.Instances.Common where
+module Agda.TypeChecking.Serialise.Instances.Common () where
 
 import Control.Applicative
 import Control.Monad.Reader
@@ -33,6 +35,7 @@
 import qualified Data.Set as Set
 import Data.Sequence (Seq)
 import qualified Data.Sequence as Seq
+import Data.Typeable (Typeable)
 import Data.Void
 
 import Agda.Syntax.Common
@@ -224,10 +227,25 @@
     valu [p, q] = valu2 P.Interval p q
     valu _      = malformed
 
+-- | Ranges are always deserialised as 'noRange'.
+
 instance EmbPrj Range where
-  icod_ r = icode (P.rangeFile r, P.rangeIntervals r)
-  value r = uncurry P.intervalsToRange `fmap` value r
+  icod_ _ = icode0'
+  value _ = return noRange
 
+-- | Ranges that should be serialised properly.
+
+newtype SerialisedRange = SerialisedRange { underlyingRange :: Range }
+  deriving (Typeable)
+
+instance EmbPrj SerialisedRange where
+  icod_ (SerialisedRange r) =
+    icode2' (P.rangeFile r) (P.rangeIntervals r)
+
+  value = vcase valu where
+    valu [a, b] = SerialisedRange <$> valu2 P.intervalsToRange a b
+    valu _      = malformed
+
 instance EmbPrj C.Name where
   icod_ (C.NoName a b) = icode2 0 a b
   icod_ (C.Name r xs)  = icode2' r xs
@@ -322,10 +340,12 @@
   value n           = A.MName `fmap` value n
 
 instance EmbPrj A.Name where
-  icod_ (A.Name a b c d) = icodeMemo nameD nameC a $ icode4' a b c d
+  icod_ (A.Name a b c d) = icodeMemo nameD nameC a $
+    icode4' a b (SerialisedRange c) d
 
   value = vcase valu where
-    valu [a, b, c, d] = valu4 A.Name a b c d
+    valu [a, b, c, d] = valu4 (\a b c -> A.Name a b (underlyingRange c))
+                              a b c d
     valu _            = malformed
 
 instance EmbPrj a => EmbPrj (C.FieldAssignment' a) where