diff --git a/Agda.cabal b/Agda.cabal
--- a/Agda.cabal
+++ b/Agda.cabal
@@ -1,5 +1,5 @@
 name:            Agda
-version:         2.4.0
+version:         2.4.0.1
 cabal-version:   >= 1.8
 build-type:      Custom
 license:         OtherLicense
@@ -49,13 +49,14 @@
                     lib/prim/Agda/Primitive.agda
 
 source-repository head
-  type:     darcs
-  location: http://code.haskell.org/Agda/
+  type:     git
+  location: https://github.com/agda/agda.git
 
 source-repository this
-  type:     darcs
-  location: http://code.haskell.org/Agda/
-  tag:      2.4.0
+  type:     git
+  location: https://github.com/agda/agda.git
+  branch:   maint-2.4.0
+  tag:      2.4.0.1
 
 flag epic
   default: False
@@ -410,7 +411,7 @@
 executable agda
   hs-source-dirs: src/main
   main-is:        Main.hs
-  build-depends:  Agda == 2.4.0,
+  build-depends:  Agda == 2.4.0.1,
                   -- Nothing is used from the following package, except
                   -- for the prelude.
                   base >= 3 && < 6
diff --git a/CHANGELOG b/CHANGELOG
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -1,4 +1,16 @@
 ------------------------------------------------------------------------
+-- Release notes for Agda 2 version 2.4.0.1
+------------------------------------------------------------------------
+
+Important changes since 2.4.0:
+
+* The option --compile-no-main has been renamed to --no-main.
+
+* COMPILED_DATA pragmas can now be given for records.
+
+* Various bug fixes.
+
+------------------------------------------------------------------------
 -- Release notes for Agda 2 version 2.4.0
 ------------------------------------------------------------------------
 
@@ -105,7 +117,23 @@
 Language
 ========
 
-TODO: Document quoteContext.
+* Experimental feature: quoteContext
+  
+  There is a new keyword 'quoteContext' that gives users access to the
+  list of names in the current local context. For instance:
+
+    open import Data.Nat
+    open import Data.List
+    open import Reflection
+
+    foo : ℕ → ℕ → ℕ
+    foo 0 m = 0
+    foo (suc n) m = quoteContext xs in ?
+
+  In the remaining goal, the list xs will consist of two names, n and
+  m, corresponding to the two local variables. At the moment it is not
+  possible to access let bound variables -- this feature may be added
+  in the future.
 
 * Experimental feature: Varying arity.
   Function clauses may now have different arity, e.g.,
diff --git a/src/data/emacs-mode/agda2-highlight.el b/src/data/emacs-mode/agda2-highlight.el
--- a/src/data/emacs-mode/agda2-highlight.el
+++ b/src/data/emacs-mode/agda2-highlight.el
@@ -85,51 +85,54 @@
         (cond
          ((equal group 'conor)
           '((agda2-highlight-keyword-face
-             :underline t)
-            (agda2-highlight-string-face)
-            (agda2-highlight-number-face)
-            (agda2-highlight-symbol-face)
+             :bold t)
+            (agda2-highlight-string-face
+             :foreground "firebrick3")
+            (agda2-highlight-number-face
+             :foreground "firebrick3")
+            (agda2-highlight-symbol-face
+             :foreground "grey25")
             (agda2-highlight-primitive-type-face
-             :foreground "blue")
+             :foreground "medium blue")
             (agda2-highlight-bound-variable-face
              :foreground "purple")
             (agda2-highlight-inductive-constructor-face
-             :foreground "dark red")
+             :foreground "firebrick3")
             (agda2-highlight-coinductive-constructor-face
-             :foreground "dark red")
+             :foreground "firebrick3")
             (agda2-highlight-datatype-face
-             :foreground "blue")
+             :foreground "medium blue")
             (agda2-highlight-field-face
-             :foreground "dark red")
+             :foreground "deeppink")
             (agda2-highlight-function-face
-             :foreground "dark green")
+             :foreground "darkgreen")
             (agda2-highlight-module-face
-             :foreground "dark green")
+             :foreground "medium blue")
             (agda2-highlight-postulate-face
-             :foreground "dark green")
+             :foreground "darkgreen")
             (agda2-highlight-primitive-face
-             :foreground "dark green")
+             :foreground "darkgreen")
             (agda2-highlight-record-face
-             :foreground "blue")
+             :foreground "medium blue")
             (agda2-highlight-dotted-face)
             (agda2-highlight-error-face
-             :foreground "black"
-             :background "sandy brown")
+             :foreground "red"
+             :underline)
             (agda2-highlight-unsolved-meta-face
              :foreground "black"
-             :background "gold")
+             :background "yellow")
             (agda2-highlight-unsolved-constraint-face
              :foreground "black"
-             :background "gold")
+             :background "yellow")
             (agda2-highlight-termination-problem-face
              :foreground "black"
-             :background "red")
+             :background "light salmon")
             (agda2-highlight-incomplete-pattern-face
              :foreground "black"
              :background "purple")
             (agda2-highlight-typechecks-face
              :foreground "black"
-             :background "light steel blue")))
+             :background "light blue")))
 	 ((equal group 'default-faces)
           (list (cons 'agda2-highlight-keyword-face
 		      (agda2-highlight-face-attributes
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.4.0"
+(defvar agda2-version "2.4.0.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/Compiler/HaskellTypes.hs b/src/full/Agda/Compiler/HaskellTypes.hs
--- a/src/full/Agda/Compiler/HaskellTypes.hs
+++ b/src/full/Agda/Compiler/HaskellTypes.hs
@@ -122,9 +122,10 @@
           hsApp <$> getHsType d <*> fromArgs args
         Pi a b ->
           if isBinderUsed b  -- Andreas, 2012-04-03.  Q: could we rely on Abs/NoAbs instead of again checking freeness of variable?
-          then underAbstraction a b $ \b ->
-            hsForall <$> getHsVar 0 <*>
-              (hsFun <$> fromType (unDom a) <*> fromType b)
+          then do
+            hsA <- fromType (unDom a)
+            underAbstraction a b $ \b ->
+              hsForall <$> getHsVar 0 <*> (hsFun hsA <$> fromType b)
           else hsFun <$> fromType (unDom a) <*> fromType (absApp b __IMPOSSIBLE__)
         Con c args -> hsApp <$> getHsType (conName c) <*> fromArgs args
         Lam{}      -> err
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
@@ -188,12 +188,12 @@
 data Rewrite =  AsIs | Instantiated | HeadNormal | Simplified | Normalised
     deriving (Read)
 
---rewrite :: Rewrite -> Term -> TCM Term
-rewrite AsIs	     t = return t
-rewrite Instantiated t = return t   -- reify does instantiation
-rewrite HeadNormal   t = {- etaContract =<< -} reduce t
-rewrite Simplified   t = {- etaContract =<< -} simplify t
-rewrite Normalised   t = {- etaContract =<< -} normalise t
+--normalForm :: Rewrite -> Term -> TCM Term
+normalForm AsIs	     t = return t
+normalForm Instantiated t = return t   -- reify does instantiation
+normalForm HeadNormal   t = {- etaContract =<< -} reduce t
+normalForm Simplified   t = {- etaContract =<< -} simplify t
+normalForm Normalised   t = {- etaContract =<< -} normalise t
 
 
 data OutputForm a b = OutputForm Range ProblemId (OutputConstraint a b)
@@ -428,7 +428,7 @@
    where
     rewriteJudg mv (HasType i t) = do
       ms <- getMetaNameSuggestion i
-      t <- rewrite norm t
+      t <- normalForm norm t
       vs <- getContextArgs
       let x = NamedMeta ms i
       reportSDoc "interactive.meta" 10 $ TP.vcat
@@ -482,7 +482,7 @@
       TelV atel _ <- telView a
       let arity = size atel
       a        <- local (\e -> e { envPrintDomainFreePi = True }) $ do
-        reify =<< cleanupType arity args =<< rewrite norm =<< withFunctionType tel vs as EmptyTel a
+        reify =<< cleanupType arity args =<< normalForm norm =<< withFunctionType tel vs as EmptyTel a
       return (OfType' h a)
   where
     cleanupType arity args t = do
@@ -578,7 +578,7 @@
                                xs
 
         out i (Dom _ (x, t)) = escapeContext i $ do
-          t' <- reify =<< rewrite norm t
+          t' <- reify =<< normalForm norm t
           return $ OfType x t'
 
 
@@ -588,7 +588,7 @@
 typeInCurrent :: Rewrite -> Expr -> TCM Expr
 typeInCurrent norm e =
     do 	(_,t) <- wakeIrrelevantVars $ inferExpr e
-        v <- rewrite norm t
+        v <- normalForm norm t
         reify v
 
 
diff --git a/src/full/Agda/Interaction/FindFile.hs b/src/full/Agda/Interaction/FindFile.hs
--- a/src/full/Agda/Interaction/FindFile.hs
+++ b/src/full/Agda/Interaction/FindFile.hs
@@ -13,8 +13,6 @@
   , findInterfaceFile
   , checkModuleName
   , moduleName', moduleName
-  , ModuleToSource
-  , SourceToModule, sourceToModule
   , tests
   ) where
 
@@ -30,6 +28,8 @@
 import Agda.Syntax.Concrete
 import Agda.Syntax.Parser
 import Agda.TypeChecking.Monad.Base
+import Agda.TypeChecking.Monad.Benchmark (billTo)
+import qualified Agda.TypeChecking.Monad.Benchmark as Bench
 import {-# SOURCE #-} Agda.TypeChecking.Monad.Options (getIncludeDirs)
 import Agda.Utils.FileName
 
@@ -153,7 +153,7 @@
 --   Use wisely!
 
 moduleName' :: AbsolutePath -> TCM TopLevelModuleName
-moduleName' file = liftIO $ do
+moduleName' file = billTo [Bench.ModuleName] $ liftIO $ do
   name <- topLevelModuleName <$> parseFile' moduleParser file
   case name of
     TopLevelModuleName ["_"] -> return $ TopLevelModuleName [defaultName]
@@ -172,23 +172,3 @@
   m <- moduleName' file
   checkModuleName m file
   return m
-
--- | Maps top-level module names to the corresponding source file
--- names.
-
-type ModuleToSource = Map TopLevelModuleName AbsolutePath
-
--- | Maps source file names to the corresponding top-level module
--- names.
-
-type SourceToModule = Map AbsolutePath TopLevelModuleName
-
--- | Creates a 'SourceToModule' map based on 'stModuleToSource'.
-
-sourceToModule :: TCM SourceToModule
-sourceToModule =
-  Map.fromList
-     .  map (\(m, f) -> (f, m))
-     .  Map.toList
-     .  stModuleToSource
-    <$> get
diff --git a/src/full/Agda/Interaction/Highlighting/Emacs.hs b/src/full/Agda/Interaction/Highlighting/Emacs.hs
--- a/src/full/Agda/Interaction/Highlighting/Emacs.hs
+++ b/src/full/Agda/Interaction/Highlighting/Emacs.hs
@@ -13,7 +13,7 @@
 import Agda.Interaction.EmacsCommand
 import Agda.Syntax.Common
 import Agda.TypeChecking.Monad
-  (TCM, envHighlightingMethod, HighlightingMethod(..))
+  (TCM, envHighlightingMethod, HighlightingMethod(..), ModuleToSource)
 import Agda.Utils.FileName
 import qualified Agda.Utils.IO.UTF8 as UTF8
 import Agda.Utils.String
diff --git a/src/full/Agda/Interaction/InteractionTop.hs b/src/full/Agda/Interaction/InteractionTop.hs
--- a/src/full/Agda/Interaction/InteractionTop.hs
+++ b/src/full/Agda/Interaction/InteractionTop.hs
@@ -21,6 +21,7 @@
 import Data.Function
 import Data.List as List
 import Data.Maybe
+import Data.Map (Map)
 import qualified Data.Map as Map
 import Data.Monoid
 import Data.Traversable (Traversable)
@@ -94,6 +95,10 @@
     -- the file when it was last loaded.
   , optionsOnReload :: CommandLineOptions
     -- ^ Reset the options on each reload to these.
+  , oldInteractionScopes :: Map InteractionId ScopeInfo
+    -- ^ We remember (the scope of) old interaction points to make it
+    --   possible to parse and compute highlighting information for the
+    --   expression that it got replaced by.
   }
 
 -- | Initial auxiliary interaction state
@@ -103,6 +108,7 @@
   { theInteractionPoints = []
   , theCurrentFile       = Nothing
   , optionsOnReload      = defaultOptions
+  , oldInteractionScopes = Map.empty
   }
 
 
@@ -149,6 +155,23 @@
   s { theInteractionPoints = f (theInteractionPoints s) }
 
 
+-- | Operations for manipulating 'oldInteractionScopes'.
+
+insertOldInteractionScope :: InteractionId -> ScopeInfo -> CommandM ()
+insertOldInteractionScope ii scope =
+  modify $ \s -> s { oldInteractionScopes = Map.insert ii scope $ oldInteractionScopes s }
+
+removeOldInteractionScope :: InteractionId -> CommandM ()
+removeOldInteractionScope ii =
+  modify $ \s -> s { oldInteractionScopes = Map.delete ii $ oldInteractionScopes s }
+
+getOldInteractionScope :: InteractionId -> CommandM ScopeInfo
+getOldInteractionScope ii = do
+  ms <- gets $ Map.lookup ii . oldInteractionScopes
+  case ms of
+    Nothing    -> fail $ "not an old interaction point: " ++ show ii
+    Just scope -> return scope
+
 -- | Run an 'IOTCM' value, catch the exceptions, emit output
 --
 --   If an error happens the state of 'CommandM' does not change,
@@ -554,10 +577,10 @@
                 return Nothing
     mapM_ putResponse resp
 
-interpret (Cmd_highlight ii rng s) = withCurrentFile $
+interpret (Cmd_highlight ii rng s) = withCurrentFile $ do
+  scope <- getOldInteractionScope ii
+  removeOldInteractionScope ii
   lift (do
-    scope <- getOldInteractionScope ii
-    removeOldInteractionPoint ii
     e     <- concreteToAbstract scope =<< B.parseExpr rng s
     printHighlightingInfo =<< generateTokenInfoFromString rng s
     highlightExpr e)
@@ -788,6 +811,8 @@
     mis' <- getInteractionPoints
     reportSLn "interaction.give" 30 $ "interaction points after = " ++ show mis'
     return (ae, mis' \\ mis)
+  -- favonia: backup the old scope for highlighting
+  when (giveRefine == Give) $ insertOldInteractionScope ii scope
   -- sort the new interaction points and put them into the state
   -- in replacement of the old interaction point
   iis       <- lift $ sortInteractionPoints iis
diff --git a/src/full/Agda/Interaction/Options.hs b/src/full/Agda/Interaction/Options.hs
--- a/src/full/Agda/Interaction/Options.hs
+++ b/src/full/Agda/Interaction/Options.hs
@@ -216,11 +216,13 @@
 
 checkOpts :: Flag CommandLineOptions
 checkOpts opts
-  | not (atMostOne [optAllowUnsolved . p, \x -> optCompile x || optCompileNoMain x]) = Left
+  | not (atMostOne [optAllowUnsolved . p, \x -> optCompile x]) = Left
       "Unsolved meta variables are not allowed when compiling.\n"
+  | optCompileNoMain opts && not (optCompile opts) = Left
+      "--no-main only allowed in combination with --compile.\n"
   | not (atMostOne [optGHCiInteraction, isJust . optInputFile]) =
       Left "Choose at most one: input file or --interaction.\n"
-  | not (atMostOne $ interactive ++ [\x -> optCompile x || optCompileNoMain x, optEpicCompile, optJSCompile]) =
+  | not (atMostOne $ interactive ++ [\x -> optCompile x, optEpicCompile, optJSCompile]) =
       Left "Choose at most one: compilers/--interactive/--interaction.\n"
   | not (atMostOne $ interactive ++ [optGenerateHTML]) =
       Left "Choose at most one: --html/--interactive/--interaction.\n"
@@ -357,8 +359,8 @@
                     "for use with the Emacs mode"
     , Option ['c']  ["compile"] (NoArg compileFlag)
                     "compile program using the MAlonzo backend (experimental)"
-    , Option []  ["compile-no-main"] (NoArg compileFlagNoMain)
-                    "compile module and dependencies using the MAlonzo backend (experimental)"
+    , Option []     ["no-main"] (NoArg compileFlagNoMain)
+                    "when compiling using the MAlonzo backend (experimental), do not treat the requested module as the main module of a program"
     , Option []     ["epic"] (NoArg compileEpicFlag) "compile program using the Epic backend"
     , Option []     ["js"] (NoArg compileJSFlag) "compile program using the JS backend"
     , Option []     ["compile-dir"] (ReqArg compileDirFlag "DIR")
diff --git a/src/full/Agda/Interaction/Response.hs b/src/full/Agda/Interaction/Response.hs
--- a/src/full/Agda/Interaction/Response.hs
+++ b/src/full/Agda/Interaction/Response.hs
@@ -14,7 +14,6 @@
   ) where
 
 import Agda.Interaction.Highlighting.Precise
-import Agda.Interaction.FindFile (ModuleToSource)
 import Agda.TypeChecking.Monad.Base
 import Agda.Syntax.Common   (InteractionId(..))
 import Agda.Syntax.Concrete (Expr)
diff --git a/src/full/Agda/Main.hs b/src/full/Agda/Main.hs
--- a/src/full/Agda/Main.hs
+++ b/src/full/Agda/Main.hs
@@ -109,8 +109,9 @@
           interaction :: TCM (Maybe Interface) -> TCM ()
           interaction | i             = runIM . interactionLoop
                       | ghci          = (failIfInt mimicGHCi =<<)
+                      | compile && compileNoMain
+                                      = (MAlonzo.compilerMain False =<<) . (failIfNoInt =<<)
                       | compile       = (MAlonzo.compilerMain True =<<) . (failIfNoInt =<<)
-                      | compileNoMain = (MAlonzo.compilerMain False =<<) . (failIfNoInt =<<)
                       | epic          = (Epic.compilerMain    =<<) . (failIfNoInt =<<)
                       | js            = (JS.compilerMain      =<<) . (failIfNoInt =<<)
                       | otherwise     = (() <$)
diff --git a/src/full/Agda/Syntax/Abstract/Name.hs b/src/full/Agda/Syntax/Abstract/Name.hs
--- a/src/full/Agda/Syntax/Abstract/Name.hs
+++ b/src/full/Agda/Syntax/Abstract/Name.hs
@@ -298,7 +298,11 @@
 
 instance KillRange Name where
   killRange x = x { nameConcrete = killRange $ nameConcrete x
-                  , nameBindingSite = noRange
+                  -- Andreas, 2014-03-30
+                  -- An experiment: what happens if we preserve
+                  -- the range of the binding site, but kill all
+                  -- other ranges before serialization?
+                  -- , nameBindingSite = noRange
                   }
 
 instance KillRange ModuleName where
diff --git a/src/full/Agda/Syntax/Concrete.hs b/src/full/Agda/Syntax/Concrete.hs
--- a/src/full/Agda/Syntax/Concrete.hs
+++ b/src/full/Agda/Syntax/Concrete.hs
@@ -47,6 +47,7 @@
     )
     where
 
+import Control.DeepSeq
 import Data.Typeable (Typeable)
 import Data.Foldable (Foldable)
 import Data.Traversable (Traversable)
@@ -114,6 +115,7 @@
         | Equal !Range Expr Expr               -- ^ ex: @a = b@, used internally in the parser
     deriving (Typeable)
 
+instance NFData Expr
 
 -- | Concrete patterns. No literals in patterns at the moment.
 data Pattern
@@ -131,6 +133,7 @@
 	| LitP Literal                            -- ^ @0@, @1@, etc.
     deriving (Typeable)
 
+instance NFData Pattern
 
 -- | A lambda binding is either domain free or typed.
 type LamBinding = LamBinding' TypedBindings
@@ -206,6 +209,8 @@
              , lhsPatsRight  :: [NamedArg Pattern]  -- ^ side patterns
              }
   deriving (Typeable)
+
+instance NFData LHSCore
 
 {- TRASH
 lhsCoreToPattern :: LHSCore -> Pattern
diff --git a/src/full/Agda/Syntax/Concrete/Name.hs b/src/full/Agda/Syntax/Concrete/Name.hs
--- a/src/full/Agda/Syntax/Concrete/Name.hs
+++ b/src/full/Agda/Syntax/Concrete/Name.hs
@@ -7,6 +7,7 @@
 -}
 module Agda.Syntax.Concrete.Name where
 
+import Control.DeepSeq
 import Control.Applicative
 
 import Data.List
@@ -36,6 +37,8 @@
   = Name !Range [NamePart]  -- ^ A (mixfix) identifier.
   | NoName !Range NameId    -- ^ @_@.
   deriving (Typeable)
+
+instance NFData Name
 
 -- | Mixfix identifiers are composed of words and holes,
 --   e.g. @_+_@ or @if_then_else_@ or @[_/_]@.
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
@@ -27,6 +27,7 @@
     , patternQNames
     ) where
 
+import Control.DeepSeq
 import Control.Applicative
 import Control.Monad
 
@@ -399,7 +400,7 @@
     patP <- buildParser (getRange p) flat DontUseBoundNames
     let cons = getNames [ConName, PatternSynName] flat
     let flds = getNames [FldName] flat
-    case [ res | p' <- parsePat patP p
+    case [ res | p' <- force $ parsePat patP p
                , res <- validPattern (PatternCheckConfig top cons flds) p' ] of
         [(p,lhs)] -> return lhs
         []        -> typeError $ NoParseForLHS lhsOrPatSyn p
@@ -547,7 +548,7 @@
       buildParser (getRange es) flat UseBoundNames
 
     -- Parse
-    case parse p es of
+    case force $ parse p es of
         [e] -> return e
         []  -> do
           -- When the parser fails and a name is not in scope, it is more
diff --git a/src/full/Agda/Syntax/Internal.hs b/src/full/Agda/Syntax/Internal.hs
--- a/src/full/Agda/Syntax/Internal.hs
+++ b/src/full/Agda/Syntax/Internal.hs
@@ -329,8 +329,8 @@
 properlyMatching VarP{} = False
 properlyMatching DotP{} = False
 properlyMatching LitP{} = True
-properlyMatching (ConP _ mt ps) = List.or $ isNothing mt -- not a record cons
-  : map (properlyMatching . namedArg) ps  -- or one of subpatterns is a proper m
+properlyMatching (ConP _ mt ps) = isNothing mt || -- not a record cons
+  List.any (properlyMatching . namedArg) ps  -- or one of subpatterns is a proper m
 properlyMatching ProjP{} = True
 
 ---------------------------------------------------------------------------
@@ -416,7 +416,8 @@
 
 -- | An unapplied variable.
 var :: Nat -> Term
-var i = Var i []
+var i | i >= 0    = Var i []
+      | otherwise = __IMPOSSIBLE__
 
 -- | Add 'DontCare' is it is not already a @DontCare@.
 dontCare :: Term -> Term
diff --git a/src/full/Agda/Syntax/Scope/Monad.hs b/src/full/Agda/Syntax/Scope/Monad.hs
--- a/src/full/Agda/Syntax/Scope/Monad.hs
+++ b/src/full/Agda/Syntax/Scope/Monad.hs
@@ -170,10 +170,19 @@
 -- * Names
 
 -- | Create a fresh abstract name from a concrete name.
+--
+--   This function is used when we translate a concrete name
+--   in a binder.  The 'Range' of the concrete name is
+--   saved as the 'nameBindingSite' of the abstract name.
 freshAbstractName :: Fixity' -> C.Name -> ScopeM A.Name
 freshAbstractName fx x = do
   i <- fresh
-  return $ A.Name i x (getRange x) fx
+  return $ A.Name
+    { nameId          = i
+    , nameConcrete    = x
+    , nameBindingSite = getRange x
+    , nameFixity      = fx
+    }
 
 -- | @freshAbstractName_ = freshAbstractName defaultFixity@
 freshAbstractName_ :: C.Name -> ScopeM A.Name
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
@@ -146,45 +146,50 @@
     DDot  v -> reify v
     DCon c vs -> apps (A.Con (AmbQ [c])) =<< reifyIArgs vs
     DDef f vs -> apps (A.Def f) =<< reifyIArgs vs
-    DWithApp us vs -> do
-      us <- reify us
-      let wapp [e] = e
-          wapp (e : es) = A.WithApp exprInfo e es
-          wapp [] = __IMPOSSIBLE__
-      reifyApp (wapp us) vs
+    DWithApp u us vs -> do
+      (e, es) <- reify (u, us)
+      reifyApp (if null es then e else A.WithApp exprInfo e es) vs
 
+-- | @reifyDisplayForm f vs fallback@
+--   tries to rewrite @f vs@ with a display form for @f@.
+--   If successful, reifies the resulting display term,
+--   otherwise, does @fallback@.
 reifyDisplayForm :: QName -> I.Args -> TCM A.Expr -> TCM A.Expr
-reifyDisplayForm x vs fallback = do
-  enabled <- displayFormsEnabled
-  if enabled
-    then do
-      md <- liftTCM $ displayForm x vs
-      case md of
-        Nothing -> fallback
-        Just d  -> reify d
-    else fallback
+reifyDisplayForm f vs fallback = do
+  ifNotM displayFormsEnabled fallback $ {- else -} do
+  caseMaybeM (liftTCM $ displayForm f vs) fallback reify
 
-{-
-reifyDisplayFormP :: A.LHS -> TCM A.LHS
-reifyDisplayFormP lhs@(A.LHS i A.LHSProj{} wps) =
-  typeError $ NotImplemented "reifyDisplayForm for copatterns"
-reifyDisplayFormP lhs@(A.LHS i (A.LHSHead x ps) wps) =
--}
+-- | @reifyDisplayFormP@ tries to recursively
+--   rewrite a lhs with a display form.
+--
+--   Note: we are not necessarily in the empty context upon entry!
 reifyDisplayFormP :: A.SpineLHS -> TCM A.SpineLHS
-reifyDisplayFormP lhs@(A.SpineLHS i x ps wps) =
+reifyDisplayFormP lhs@(A.SpineLHS i f ps wps) =
   ifNotM displayFormsEnabled (return lhs) $ {- else -} do
-    let vs = [ setHiding h $ defaultArg $ I.var n
-             | (n, h) <- zip [0..] $ map getHiding ps
+    let vs = [ setHiding h $ defaultArg $ I.var i
+             | (i, h) <- zip [0..] $ map getHiding ps
              ]
-    md <- liftTCM $ displayForm x vs
+    -- Try to rewrite @f 0 1 2 ... |ps|-1@ to a dt.
+    -- Andreas, 2014-06-11  Issue 1177:
+    -- I thought we need to add the placeholders for ps to the context,
+    -- because otherwise displayForm will not raise the display term
+    -- and we will have variable clashes.
+    -- But apparently, it has no influence...
+    -- Ulf, can you add an explanation?
+    md <- liftTCM $ -- addContext (replicate (length ps) "x") $
+      displayForm f vs
     reportSLn "reify.display" 20 $
-      "display form of " ++ show x ++ " " ++ show ps ++ " " ++ show wps ++ ":\n  " ++ show md
+      "display form of " ++ show f ++ " " ++ show ps ++ " " ++ show wps ++ ":\n  " ++ show md
     case md of
       Just d  | okDisplayForm d ->
+        -- 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
   where
-    okDisplayForm (DWithApp (d : ds) []) =
+    okDisplayForm (DWithApp d ds []) =
       okDisplayForm d && all okDisplayTerm ds
     okDisplayForm (DTerm (I.Def f vs)) = all okElim vs
     okDisplayForm (DDef f vs) = all okDArg vs
@@ -210,14 +215,17 @@
     okTerm (I.Def x []) = show x == "_" -- Handling wildcards in display forms
     okTerm _            = True -- False
 
-    flattenWith (DWithApp (d : ds) ds1) = case flattenWith d of
-      (f, vs, ds') -> (f, vs, ds' ++ ds ++ map (DTerm . unArg) ds1)
+    -- Flatten a dt into (parentName, parentArgs, withArgs).
+    flattenWith :: DisplayTerm -> (QName, [I.Arg DisplayTerm], [DisplayTerm])
+    flattenWith (DWithApp d ds1 ds2) = case flattenWith d of
+      (f, vs, ds0) -> (f, vs, ds0 ++ ds1 ++ map (DTerm . unArg) ds2)
     flattenWith (DDef f vs) = (f, vs, [])     -- .^ hacky, but we should only hit this when printing debug info
     flattenWith (DTerm (I.Def f es)) =
       let vs = maybe __IMPOSSIBLE__ id $ mapM isApplyElim es
       in (f, map (fmap DTerm) vs, [])
     flattenWith _ = __IMPOSSIBLE__
 
+    displayLHS :: [A.Pattern] -> [A.Pattern] -> DisplayTerm -> TCM A.SpineLHS
     displayLHS ps wps d = case flattenWith d of
       (f, vs, ds) -> do
         ds <- mapM termToPat ds
@@ -229,8 +237,6 @@
         ci   = ConPatInfo False patNoRange
         argToPat arg = fmap unnamed <$> traverse termToPat arg
 
-        len = genericLength ps
-
         termToPat :: DisplayTerm -> TCM A.Pattern
 
         termToPat (DTerm (I.Var n [])) = return $ ps !! n
@@ -247,13 +253,16 @@
         termToPat (DDot v)             = A.DotP patNoRange <$> termToExpr v
         termToPat v                    = A.DotP patNoRange <$> reify v -- __IMPOSSIBLE__
 
+        len = genericLength ps
+
         argsToExpr = mapM (traverse termToExpr)
 
         -- TODO: restructure this to avoid having to repeat the code for reify
         termToExpr :: Term -> TCM A.Expr
-        termToExpr v =
+        termToExpr v = do
+          reportSLn "reify.display" 60 $ "termToExpr " ++ show v
+          -- After unSpine, a Proj elimination is __IMPOSSIBLE__!
           case unSpine v of
-            I.Var n [] | n < len -> return $ A.patternToExpr $ ps !! n
             I.Con c vs ->
               apps (A.Con (AmbQ [conName c])) =<< argsToExpr vs
             I.Def f es -> do
@@ -261,7 +270,14 @@
               apps (A.Def f) =<< argsToExpr vs
             I.Var n es -> do
               let vs = maybe __IMPOSSIBLE__ id $ mapM isApplyElim es
-              uncurry apps =<< (,) <$> reify (I.var (n - len)) <*> argsToExpr vs
+              -- Andreas, 2014-06-11  Issue 1177
+              -- due to β-normalization in substitution,
+              -- even the pattern variables @n < len@ can be
+              -- applied to some args @vs@.
+              e <- if n < len
+                   then return $ A.patternToExpr $ ps !! n
+                   else reify (I.var (n - len))
+              apps e =<< argsToExpr vs
             _ -> return underscore
 
 instance Reify Literal Expr where
@@ -659,9 +675,10 @@
         stripArgs _ [] = []
         stripArgs fixedPos (a : as) =
           case getHiding a of
-            Hidden | canStrip a as -> stripArgs False as
-            _                      -> stripName fixedPos (stripArg a) :
-                                      stripArgs True as
+            Hidden   | canStrip a as -> stripArgs False as
+            Instance | canStrip a as -> stripArgs False as
+            _                        -> stripName fixedPos (stripArg a) :
+                                        stripArgs True as
 
         stripName True  = fmap (unnamed . namedThing)
         stripName False = id
@@ -673,7 +690,7 @@
           ]
           where p = namedArg a
 
-        isUnnamedHidden x = isHidden x && nameOf (unArg x) == Nothing
+        isUnnamedHidden x = notVisible x && nameOf (unArg x) == Nothing
 
         stripArg a = fmap (fmap stripPat) a
 
diff --git a/src/full/Agda/Termination/Inlining.hs b/src/full/Agda/Termination/Inlining.hs
--- a/src/full/Agda/Termination/Inlining.hs
+++ b/src/full/Agda/Termination/Inlining.hs
@@ -186,7 +186,7 @@
           where n' = n - 1
 
     dispToPats :: DisplayTerm -> TCM ([NamedArg Pattern], Permutation)
-    dispToPats (DWithApp (DDef _ vs : ws) zs) = do
+    dispToPats (DWithApp (DDef _ vs) ws zs) = do
       let us = vs ++ map defaultArg ws ++ map (fmap DTerm) zs
       (ps, (j, ren)) <- (`runStateT` (0, [])) $
                         map (fmap unnamed) <$> mapM (traverse dtermToPat) us
@@ -231,8 +231,7 @@
     (vs, es') = splitApplyElims es
 
 dtermToTerm :: DisplayTerm -> Term
-dtermToTerm (DWithApp [] _)        = __IMPOSSIBLE__
-dtermToTerm (DWithApp (d : ds) vs) = dtermToTerm d `apply` (map (defaultArg . dtermToTerm) ds ++ vs)
+dtermToTerm (DWithApp d ds vs)     = dtermToTerm d `apply` (map (defaultArg . dtermToTerm) ds ++ vs)
 dtermToTerm (DCon c args)          = Con (ConHead c []) $ map (fmap dtermToTerm) args
 dtermToTerm (DDef f args)          = Def f $ map (Apply . fmap dtermToTerm) args
 dtermToTerm (DDot v)               = v
diff --git a/src/full/Agda/Termination/TermCheck.hs b/src/full/Agda/Termination/TermCheck.hs
--- a/src/full/Agda/Termination/TermCheck.hs
+++ b/src/full/Agda/Termination/TermCheck.hs
@@ -54,6 +54,7 @@
 import Agda.TypeChecking.Monad.Builtin
 import Agda.TypeChecking.Substitute
 import Agda.TypeChecking.SizedTypes
+import Agda.TypeChecking.Datatypes
 
 import qualified Agda.TypeChecking.Monad.Base.Benchmark as Benchmark
 import Agda.TypeChecking.Monad.Benchmark (billTo, billPureTo)
@@ -489,6 +490,27 @@
     LitDBP{}  -> return p
     ProjDBP{} -> return p
 
+stripNonDataArgs :: [DeBruijnPat] -> TerM [DeBruijnPat]
+stripNonDataArgs ps = do
+  withoutKEnabled <- liftTCM $ optWithoutK <$> pragmaOptions
+  if withoutKEnabled
+    then do
+      f   <- terGetCurrent
+      def <- liftTCM $ getConstInfo f
+      ty  <- liftTCM $ reduce $ defType def
+      TelV tel _ <- liftTCM $ telView ty
+      let types = map (unEl . snd . unDom) $ telToList tel
+      zipWithM stripIfNotData ps types
+    else return ps
+  where
+    stripIfNotData :: DeBruijnPat -> Term -> TerM DeBruijnPat
+    stripIfNotData p ty = liftTCM $ do
+      isData <- isDataOrRecord ty
+      case isData of
+        Just _  -> return p
+        Nothing -> return unusedVar
+
+
 -- | cf. 'TypeChecking.Coverage.Match.buildMPatterns'
 openClause :: Permutation -> [Pattern] -> ClauseBody -> TerM ([DeBruijnPat], Maybe Term)
 openClause perm ps body = do
@@ -517,9 +539,13 @@
 -- | Extract recursive calls from one clause.
 termClause :: Clause -> TerM Calls
 termClause clause = do
-  name <- terGetCurrent
-  ifM (isJust <$> do isWithFunction name) (return mempty) $ do
-  mapM' termClause' =<< do liftTCM $ inlineWithClauses name clause
+  withoutKEnabled <- liftTCM $ optWithoutK <$> pragmaOptions
+  if withoutKEnabled
+    then termClause' clause
+    else do
+      name <- terGetCurrent
+      ifM (isJust <$> do isWithFunction name) (return mempty) $ do
+      mapM' termClause' =<< do liftTCM $ inlineWithClauses name clause
 
 termClause' :: Clause -> TerM Calls
 termClause' clause = do
@@ -541,6 +567,7 @@
       Nothing -> return CallGraph.empty
       Just v -> do
         dbpats <- mapM stripCoConstructors dbpats
+        dbpats <- stripNonDataArgs dbpats
         terSetPatterns dbpats $ do
         reportBody v
   {-
diff --git a/src/full/Agda/TypeChecking/CheckInternal.hs b/src/full/Agda/TypeChecking/CheckInternal.hs
--- a/src/full/Agda/TypeChecking/CheckInternal.hs
+++ b/src/full/Agda/TypeChecking/CheckInternal.hs
@@ -96,7 +96,9 @@
     , text " : "
     , prettyTCM t
     ]
-  v <- elimView v  -- bring projection-like funs in post-fix form
+  -- Bring projection-like funs in post-fix form,
+  -- even lone ones (True).
+  v <- elimView True v
   case ignoreSharing v of
     Var i es   -> do
       a <- typeOfBV i
diff --git a/src/full/Agda/TypeChecking/Conversion.hs b/src/full/Agda/TypeChecking/Conversion.hs
--- a/src/full/Agda/TypeChecking/Conversion.hs
+++ b/src/full/Agda/TypeChecking/Conversion.hs
@@ -470,8 +470,10 @@
         _ -> do
           -- Andreas, 2013-10-20 put projection-like function
           -- into the spine, to make compareElims work.
-          m <- elimView m
-          n <- elimView n
+          -- 'False' means: leave (Def f []) unchanged even for
+          -- proj-like funs.
+          m <- elimView False m
+          n <- elimView False n
           case (ignoreSharing m, ignoreSharing n) of
 	    (Pi{}, Pi{}) -> equalFun m n
 
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
@@ -332,13 +332,15 @@
   -> OneHolePatterns            -- ^ Patterns with hole at split point.
   -> QName                      -- ^ Constructor to fit into hole.
   -> CoverM (Maybe SplitClause) -- ^ New split clause if successful.
-computeNeighbourhood delta1 n delta2 perm d pars ixs hix hps con = do
+computeNeighbourhood delta1 n delta2 perm d pars ixs hix hps c = do
 
   -- Get the type of the datatype
   dtype <- liftTCM $ (`piApply` pars) . defType <$> getConstInfo d
 
   -- Get the real constructor name
-  con <- liftTCM $ getConForm con
+  con <- liftTCM $ getConForm c
+  con <- return $ con { conName = c }  -- What if we restore the current name?
+                                       -- Andreas, 2013-11-29 changes nothing!
 {-
   con <- conSrcCon . theDef <$> getConstInfo con
   Con con [] <- liftTCM $ ignoreSharing <$> (constructorForm =<< normalise (Con con []))
diff --git a/src/full/Agda/TypeChecking/DisplayForm.hs b/src/full/Agda/TypeChecking/DisplayForm.hs
--- a/src/full/Agda/TypeChecking/DisplayForm.hs
+++ b/src/full/Agda/TypeChecking/DisplayForm.hs
@@ -4,99 +4,137 @@
 
 import Control.Applicative
 import Control.Monad.Error
+import Control.Monad.Trans.Maybe
+
 import Data.Traversable (traverse)
 
 import Agda.Syntax.Common hiding (Arg, Dom, NamedArg, ArgInfo)
 import Agda.Syntax.Internal
+
 import Agda.TypeChecking.Monad
 import Agda.TypeChecking.Substitute
 import Agda.TypeChecking.Level
 
+import Agda.Utils.List
+import Agda.Utils.Maybe
+
 #include "../undefined.h"
 import Agda.Utils.Impossible
 
+-- | Find a matching display form for @q vs@.
+--   In essence this tries to reqwrite @q vs@ with any
+--   display form @q ps --> dt@ and returns the instantiated
+--   @dt@ if successful.  First match wins.
 displayForm :: QName -> Args -> TCM (Maybe DisplayTerm)
-displayForm c vs = do
-    odfs  <- defDisplay <$> getConstInfo c
+displayForm q vs = do
+    -- Get display forms for name q.
+    odfs  <- defDisplay <$> getConstInfo q
+    -- Display debug info about the @Open@s.
     unless (null odfs) $ verboseS "tc.display.top" 100 $ do
       n <- getContextId
-      let fvs = map (\(OpenThing n _) -> n) odfs
-      reportSLn "tc.display.top" 100 $ "displayForm: context = " ++ show n ++ ", dfs = " ++ show fvs
-    dfs	  <- do
-      xs <- mapM tryOpen odfs
-      return [ df | Just df <- xs ]
+      reportSLn "tc.display.top" 100 $
+        "displayForm: context = " ++ show n ++
+        ", dfs = " ++ show (map openThingCtxIds odfs)
+    -- Use only the display forms that can be opened in the current context.
+    dfs	  <- catMaybes <$> mapM tryOpen odfs
     scope <- getScope
+    -- Keep the display forms that match the application @c vs@.
     ms <- do
-      ms <- mapM (flip matchDisplayForm vs) dfs
+      ms <- mapM (runMaybeT . (`matchDisplayForm` vs)) dfs
       return [ m | Just m <- ms, inScope scope m ]
     -- Not safe when printing non-terminating terms.
     -- (nfdfs, us) <- normalise (dfs, vs)
     unless (null odfs) $ reportSLn "tc.display.top" 100 $ unlines
-      [ "name        : " ++ show c
+      [ "name        : " ++ show q
       , "displayForms: " ++ show dfs
       , "arguments   : " ++ show vs
       , "matches     : " ++ show ms
       , "result      : " ++ show (foldr (const . Just) Nothing ms)
       ]
-    return $ foldr (const . Just) Nothing ms
-  `catchError` \_ -> return Nothing
+    -- Return the first display form that matches.
+    return $ mhead ms
+
+--  Andreas, 2014-06-11: The following error swallowing
+--  is potentially harmful, making debugging harder.
+--  I removed it, and it does not cause problems on the test suite.
+--  `catchError` \_ -> return Nothing
+
   where
     inScope _ _ = True  -- TODO: distinguish between with display forms and other display forms
 --     inScope scope d = case hd d of
---       Just h  -> maybe False (const True) $ inverseScopeLookupName h scope
+--       Just h  -> isJust $ inverseScopeLookupName h scope
 --       Nothing -> __IMPOSSIBLE__ -- TODO: currently all display forms have heads
-    hd (DTerm (Def x _))    = Just x
-    hd (DTerm (Con x _))    = Just $ conName x
-    hd (DTerm (Shared p))   = hd (DTerm $ derefPtr p)
-    hd (DWithApp (d : _) _) = hd d
-    hd _		    = Nothing
+    -- 'hd' is only used in the commented-out code for 'inScope' above.
+    -- hd (DTerm (Def x _))    = Just x
+    -- hd (DTerm (Con x _))    = Just $ conName x
+    -- hd (DTerm (Shared p))   = hd (DTerm $ derefPtr p)
+    -- hd (DWithApp d _ _) = hd d
+    -- hd _		    = Nothing
 
-matchDisplayForm :: DisplayForm -> Args -> TCM (Maybe DisplayTerm)
-matchDisplayForm (Display n ps v) vs
-  | length ps > length vs = return Nothing
+-- | Match a 'DisplayForm' @q ps = v@ against @q vs@.
+--   Return the 'DisplayTerm' @v[us]@ if the match was successful,
+--   i.e., @vs / ps = Just us@.
+matchDisplayForm :: DisplayForm -> Args -> MaybeT TCM DisplayTerm
+matchDisplayForm (Display _ ps v) vs
+  | length ps > length vs = mzero
   | otherwise             = do
-      fmap (\ us -> applySubst (parallelS $ reverse us) v `apply` vs1) <$> do
-        match n ps $ raise 1 $ map unArg vs0
+      us <- match ps $ raise 1 $ map unArg vs0
+      return $ applySubst (parallelS $ reverse us) v `apply` vs1
   where
     (vs0, vs1) = splitAt (length ps) vs
 
+-- | Class @Match@ for matching a term @p@ in the role of a pattern
+--   against a term @v@.
+--
+--   The 0th variable in @p@ plays the role
+--   of a place holder (pattern variable).  Each occurrence of
+--   @var 0@ in @p@ stands for a different pattern variable.
+--
+--   The result of matching, if successful, is a list of solutions for the
+--   pattern variables, in left-to-right order.
+--
+--   The 0th variable is in scope in the input @v@, but should not
+--   actually occur!
+--   In the output solution, the @0th@ variable is no longer in scope.
+--   (It has been substituted by __IMPOSSIBLE__ which corresponds to
+--   a raise by -1).
 class Match a where
-  match :: Nat -> a -> a -> TCM (Maybe [Term])
+  match :: a -> a -> MaybeT TCM [Term]
 
 instance Match a => Match [a] where
-  match n xs ys = fmap concat . traverse id <$> zipWithM (match n) xs ys
+  match xs ys = concat <$> zipWithM match xs ys
 
 instance Match a => Match (Arg a) where
-  match n p v = match n (unArg p) (unArg v)
+  match p v = match (unArg p) (unArg v)
 
 instance Match a => Match (Elim' a) where
-  match n p v =
+  match p v =
     case (p, v) of
-      (Proj f, Proj f') | f == f' -> return $ Just []
-      (Apply a, Apply a')         -> match n a a'
-      _                           -> return Nothing
+      (Proj f, Proj f') | f == f' -> return []
+      (Apply a, Apply a')         -> match a a'
+      _                           -> mzero
 
 instance Match Term where
-  match n p v = case (ignoreSharing p, ignoreSharing v) of
-    (Var 0 [], v)                  -> return $ Just [subst __IMPOSSIBLE__ v]
-    (Var i ps, Var j vs) | i == j  -> match n ps vs
-    (Def c ps, Def d vs) | c == d  -> match n ps vs
-    (Con c ps, Con d vs) | c == d  -> match n ps vs
-    (Lit l, Lit l')      | l == l' -> return $ Just []
-    (p, v)               | p == v  -> return $ Just []
-    (p, Level l)                   -> match n p =<< reallyUnLevelView l
-    (Sort ps, Sort pv)             -> match n ps pv
-    (p, Sort (Type v))             -> match n p =<< reallyUnLevelView v
-    _                              -> return Nothing
+  match p v = case (ignoreSharing p, ignoreSharing v) of
+    (Var 0 [], v)                  -> return [subst __IMPOSSIBLE__ v]
+    (Var i ps, Var j vs) | i == j  -> match ps vs
+    (Def c ps, Def d vs) | c == d  -> match ps vs
+    (Con c ps, Con d vs) | c == d  -> match ps vs
+    (Lit l, Lit l')      | l == l' -> return []
+    (p, v)               | p == v  -> return []
+    (p, Level l)                   -> match p =<< reallyUnLevelView l
+    (Sort ps, Sort pv)             -> match ps pv
+    (p, Sort (Type v))             -> match p =<< reallyUnLevelView v
+    _                              -> mzero
 
 instance Match Sort where
-  match n p v = case (p, v) of
-    (Type pl, Type vl) -> match n pl vl
-    _ | p == v -> return $ Just []
-    _          -> return Nothing
+  match p v = case (p, v) of
+    (Type pl, Type vl) -> match pl vl
+    _ | p == v -> return []
+    _          -> mzero
 
 instance Match Level where
-  match n p v = do
+  match p v = do
     p <- reallyUnLevelView p
     v <- reallyUnLevelView v
-    match n p v
+    match p v
diff --git a/src/full/Agda/TypeChecking/Injectivity.hs b/src/full/Agda/TypeChecking/Injectivity.hs
--- a/src/full/Agda/TypeChecking/Injectivity.hs
+++ b/src/full/Agda/TypeChecking/Injectivity.hs
@@ -71,17 +71,17 @@
 
 checkInjectivity :: QName -> [Clause] -> TCM FunctionInverse
 checkInjectivity f cs
-  | pointLess cs = return NotInjective
+  | pointLess cs = do
+      reportSLn "tc.inj.check" 20 $ "Injectivity of " ++ show f ++ " would be pointless."
+      return NotInjective
   where
     -- Is it pointless to use injectivity for this function?
     pointLess []      = True
     pointLess (_:_:_) = False
-    pointLess [cl] = all (noMatch . unArg) $ clausePats cl
-      where noMatch ConP{} = False
-            noMatch LitP{} = False
-            noMatch ProjP{}= False
-            noMatch VarP{} = True
-            noMatch DotP{} = True
+    pointLess [cl] = not $ any (properlyMatching . unArg) $ clausePats cl
+        -- Andreas, 2014-06-12
+        -- If we only have record patterns, it is also pointless.
+        -- We need at least one proper match.
 checkInjectivity f cs = do
   reportSLn "tc.inj.check" 40 $ "Checking injectivity of " ++ show f
   -- Extract the head symbol of the rhs of each clause (skip absurd clauses)
@@ -130,6 +130,12 @@
   uinv <- functionInverse u
   vinv <- functionInverse v
   case (uinv, vinv) of
+    -- Andreas, Francesco, 2014-06-12:
+    -- We know that one of u,v is neutral
+    -- (see calls to useInjectivity in Conversion.hs).
+    -- Otherwise, (e.g. if both were Blocked), the following case would be
+    -- unsound, since it assumes the arguments to be pointwise equal.
+    -- It would deliver non-unique solutions for metas.
     (Inv f fArgs _, Inv g gArgs _)
       | f == g    -> do
         a <- defType <$> getConstInfo f
diff --git a/src/full/Agda/TypeChecking/Level.hs b/src/full/Agda/TypeChecking/Level.hs
--- a/src/full/Agda/TypeChecking/Level.hs
+++ b/src/full/Agda/TypeChecking/Level.hs
@@ -73,8 +73,9 @@
 unLevel (Shared p) = unLevel (derefPtr p)
 unLevel v = return v
 
-reallyUnLevelView :: Level -> TCM Term
-reallyUnLevelView nv =
+{-# SPECIALIZE reallyUnLevelView :: Level -> TCM Term #-}
+reallyUnLevelView :: MonadTCM tcm => Level -> tcm Term
+reallyUnLevelView nv = liftTCM $ do
   case nv of
     Max []              -> primLevelZero
     Max [Plus 0 a]      -> return $ unLevelAtom a
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
@@ -14,6 +14,7 @@
 import Control.Monad.State
 import Control.Monad.Reader
 import Control.Monad.Writer
+import Control.Monad.Trans.Maybe
 import Control.Applicative
 
 import Data.Function
@@ -27,6 +28,7 @@
 import Data.Traversable
 import Data.IORef
 
+import Agda.Syntax.Concrete (TopLevelModuleName)
 import Agda.Syntax.Common hiding (Arg, Dom, NamedArg, ArgInfo)
 import qualified Agda.Syntax.Common as Common
 import qualified Agda.Syntax.Concrete as C
@@ -39,7 +41,7 @@
 import Agda.TypeChecking.CompiledClause
 
 import Agda.Interaction.Exceptions
-import {-# SOURCE #-} Agda.Interaction.FindFile
+-- import {-# SOURCE #-} Agda.Interaction.FindFile
 import Agda.Interaction.Options
 import {-# SOURCE #-} Agda.Interaction.Response
   (InteractionOutputCallback, defaultInteractionOutputCallback, Response)
@@ -76,10 +78,6 @@
          , stTermErrs          :: Seq TerminationError
 	 , stMetaStore	       :: MetaStore
 	 , stInteractionPoints :: InteractionPoints
-         , stOldInteractionPoints :: OldInteractionPoints
-            -- ^ We remember (the scope of) old interaction points to make it
-            --   possible to parse and compute highlighting information for the
-            --   expression that it got replaced by.
 	 , stAwakeConstraints    :: Constraints
 	 , stSleepingConstraints :: Constraints
          , stDirty               :: Bool
@@ -161,7 +159,6 @@
   , stTokens               = mempty
   , stTermErrs             = Seq.empty
   , stInteractionPoints    = Map.empty
-  , stOldInteractionPoints = Map.empty
   , stAwakeConstraints     = []
   , stSleepingConstraints  = []
   , stDirty                = False
@@ -234,6 +231,30 @@
 
 
 ---------------------------------------------------------------------------
+-- ** Managing file names
+---------------------------------------------------------------------------
+
+-- | Maps top-level module names to the corresponding source file
+-- names.
+
+type ModuleToSource = Map TopLevelModuleName AbsolutePath
+
+-- | Maps source file names to the corresponding top-level module
+-- names.
+
+type SourceToModule = Map AbsolutePath TopLevelModuleName
+
+-- | Creates a 'SourceToModule' map based on 'stModuleToSource'.
+
+sourceToModule :: TCM SourceToModule
+sourceToModule =
+  Map.fromList
+     .  List.map (\(m, f) -> (f, m))
+     .  Map.toList
+     .  stModuleToSource
+    <$> get
+
+---------------------------------------------------------------------------
 -- ** Interface
 ---------------------------------------------------------------------------
 
@@ -390,7 +411,7 @@
 ---------------------------------------------------------------------------
 
 -- | A thing tagged with the context it came from.
-data Open a = OpenThing [CtxId] a
+data Open a = OpenThing { openThingCtxIds :: [CtxId], openThing :: a }
     deriving (Typeable, Show, Functor)
 
 ---------------------------------------------------------------------------
@@ -566,8 +587,6 @@
 -- | Data structure managing the interaction points.
 type InteractionPoints = Map InteractionId InteractionPoint
 
-type OldInteractionPoints = Map InteractionId ScopeInfo
-
 ---------------------------------------------------------------------------
 -- ** Signature
 ---------------------------------------------------------------------------
@@ -595,24 +614,51 @@
 emptySignature :: Signature
 emptySignature = Sig Map.empty HMap.empty
 
-data DisplayForm = Display Nat [Term] DisplayTerm
-		-- ^ The three arguments are:
-		--
-		--   * @n@: number of free variables;
-		--
-		--   * Patterns for arguments, one extra free var which
-		--     represents pattern vars. There should @n@ of them.
-		--
-		--   * Display form. @n@ free variables.
+-- | A @DisplayForm@ is in essence a rewrite rule
+--   @
+--      q ts --> dt
+--   @
+--   for a defined symbol (could be a constructor as well) @q@.
+--   The right hand side is a 'DisplayTerm' which is used to
+--   'reify' to a more readable 'Abstract.Syntax'.
+--
+--   The patterns @ts@ are just terms, but @var 0@ is interpreted
+--   as a hole.  Each occurrence of @var 0@ is a new hole (pattern var).
+--   For each *occurrence* of @var0@ the rhs @dt@ has a free variable.
+--   These are instantiated when matching a display form against a
+--   term @q vs@ succeeds.
+data DisplayForm = Display
+  { dfFreeVars :: Nat
+    -- ^ Number @n@ of free variables in 'dfRHS'.
+  , dfPats     :: [Term]
+    -- ^ Left hand side patterns, where @var 0@ stands for a pattern
+    --   variable.  There should be @n@ occurrences of @var0@ in
+    --   'dfPats'.
+  , dfRHS      :: DisplayTerm
+    -- ^ Right hand side, with @n@ free variables.
+  }
   deriving (Typeable, Show)
 
-data DisplayTerm = DWithApp [DisplayTerm] Args
-                 | DCon QName [Arg DisplayTerm]
-                 | DDef QName [Arg DisplayTerm]
-                 | DDot Term
-		 | DTerm Term
+-- | A structured presentation of a 'Term' for reification into
+--   'Abstract.Syntax'.
+data DisplayTerm
+  = DWithApp DisplayTerm [DisplayTerm] Args
+    -- ^ @(f vs | ws) us@.
+    --   The first 'DisplayTerm' is the parent function @f@ with its args @vs@.
+    --   The list of 'DisplayTerm's are the with expressions @ws@.
+    --   The 'Args' are additional arguments @us@
+    --   (possible in case the with-application is of function type).
+  | DCon QName [Arg DisplayTerm]
+    -- ^ @c vs@.
+  | DDef QName [Arg DisplayTerm]
+    -- ^ @d vs@.
+  | DDot Term
+    -- ^ @.v@.
+  | DTerm Term
+    -- ^ @v@.
   deriving (Typeable, Show)
 
+-- | By default, we have no display form.
 defaultDisplayForm :: QName -> [Open DisplayForm]
 defaultDisplayForm c = []
 
@@ -712,6 +758,8 @@
     --   will be created: @t = \ pars r -> r .p@
     --   In case of a projection-like function, just the function symbol
     --   is returned as 'Def':  @t = \ pars -> f@.
+  , projArgInfo   :: I.ArgInfo
+    -- ^ The info of the principal (record) argument.
   } deriving (Typeable, Show)
 
 data Defn = Axiom
@@ -877,8 +925,9 @@
 
 -- | Controlling 'reduce'.
 data AllowedReduction
-  = ProjectionReductions -- ^ (projection and) projection-like functions may be reduced
-  | FunctionReductions   -- ^ functions which are not projections may be reduced
+  = ProjectionReductions -- ^ (Projection and) projection-like functions may be reduced.
+  | FunctionReductions   -- ^ Functions which are not projections may be reduced.
+  | LevelReductions      -- ^ Reduce @'Level'@ terms.
   deriving (Show, Eq, Ord, Enum, Bounded)
 
 type AllowedReductions = [AllowedReduction]
@@ -1244,6 +1293,7 @@
 data ExpandHidden
   = ExpandLast      -- ^ Add implicit arguments in the end until type is no longer hidden 'Pi'.
   | DontExpandLast  -- ^ Do not append implicit arguments.
+  deriving (Eq)
 
 data ExpandInstances
   = ExpandInstanceArguments
@@ -1624,6 +1674,9 @@
 {-# RULES "liftTCM/id" liftTCM = id #-}
 instance MonadIO m => MonadTCM (TCMT m) where
     liftTCM = mapTCMT liftIO
+
+instance MonadTCM tcm => MonadTCM (MaybeT tcm) where
+  liftTCM = lift . liftTCM
 
 instance (Error err, MonadTCM tcm) => MonadTCM (ErrorT err tcm) where
   liftTCM = lift . liftTCM
diff --git a/src/full/Agda/TypeChecking/Monad/Base/Benchmark.hs b/src/full/Agda/TypeChecking/Monad/Base/Benchmark.hs
--- a/src/full/Agda/TypeChecking/Monad/Base/Benchmark.hs
+++ b/src/full/Agda/TypeChecking/Monad/Base/Benchmark.hs
@@ -42,6 +42,8 @@
     -- ^ Subphase for 'Termination'.
   | With
     -- ^ Subphase for 'Termination'.
+  | ModuleName
+    -- ^ Subphase for 'Import'.
   | Sort
     -- ^ Subphase for 'Serialize'.
   | Operators
diff --git a/src/full/Agda/TypeChecking/Monad/Base/KillRange.hs b/src/full/Agda/TypeChecking/Monad/Base/KillRange.hs
--- a/src/full/Agda/TypeChecking/Monad/Base/KillRange.hs
+++ b/src/full/Agda/TypeChecking/Monad/Base/KillRange.hs
@@ -60,7 +60,7 @@
   killRange (ConsHead q) = ConsHead $ killRange q
 
 instance KillRange Projection where
-  killRange (Projection a b c d) = killRange4 Projection a b c d
+  killRange (Projection a b c d e) = killRange4 Projection a b c d e
 
 instance KillRange Occurrence where
   killRange = id
@@ -77,7 +77,7 @@
 instance KillRange DisplayTerm where
   killRange dt =
     case dt of
-      DWithApp dts args -> killRange2 DWithApp dts args
+      DWithApp dt dts args -> killRange3 DWithApp dt dts args
       DCon q dts        -> killRange2 DCon q dts
       DDef q dts        -> killRange2 DDef q dts
       DDot v            -> killRange1 DDot v
diff --git a/src/full/Agda/TypeChecking/Monad/Benchmark.hs b/src/full/Agda/TypeChecking/Monad/Benchmark.hs
--- a/src/full/Agda/TypeChecking/Monad/Benchmark.hs
+++ b/src/full/Agda/TypeChecking/Monad/Benchmark.hs
@@ -16,7 +16,7 @@
 
 import Agda.TypeChecking.Monad.Base.Benchmark
 import Agda.TypeChecking.Monad.Base
-import Agda.TypeChecking.Monad.Options
+import{-# SOURCE #-} Agda.TypeChecking.Monad.Options
 import Agda.TypeChecking.Monad.State
 
 import Agda.Utils.Monad
diff --git a/src/full/Agda/TypeChecking/Monad/Env.hs b/src/full/Agda/TypeChecking/Monad/Env.hs
--- a/src/full/Agda/TypeChecking/Monad/Env.hs
+++ b/src/full/Agda/TypeChecking/Monad/Env.hs
@@ -75,7 +75,10 @@
 onlyReduceProjections = local $ \ e -> e { envAllowedReductions = [ProjectionReductions] }
 
 dontReduceProjections :: TCM a -> TCM a
-dontReduceProjections = local $ \ e -> e { envAllowedReductions = [FunctionReductions] }
+dontReduceProjections = local $ \ e -> e { envAllowedReductions = allReductions \\ [ProjectionReductions] }
+
+dontReduceLevels :: TCM a -> TCM a
+dontReduceLevels = local $ \ e -> e { envAllowedReductions = allReductions \\ [LevelReductions] }
 
 allowAllReductions :: TCM a -> TCM a
 allowAllReductions = local $ \ e -> e { envAllowedReductions = allReductions }
diff --git a/src/full/Agda/TypeChecking/Monad/MetaVars.hs b/src/full/Agda/TypeChecking/Monad/MetaVars.hs
--- a/src/full/Agda/TypeChecking/Monad/MetaVars.hs
+++ b/src/full/Agda/TypeChecking/Monad/MetaVars.hs
@@ -12,7 +12,7 @@
 import qualified Data.Foldable as Fold
 import qualified Data.Traversable as Trav
 
-import Agda.Syntax.Common
+import Agda.Syntax.Common as Common
 import Agda.Syntax.Internal
 import Agda.Syntax.Position
 import Agda.Syntax.Scope.Base
@@ -24,9 +24,10 @@
 import Agda.TypeChecking.Monad.Context
 import Agda.TypeChecking.Substitute
 
-import Agda.Utils.Maybe
 import Agda.Utils.Functor ((<.>))
 import Agda.Utils.Fresh
+import Agda.Utils.Maybe
+import Agda.Utils.Monad
 import Agda.Utils.Permutation
 import Agda.Utils.Tuple
 import Agda.Utils.Size
@@ -86,9 +87,49 @@
       return $ piApply t $ permute (takeP (size vs) p) vs
     IsSort{}                 -> __IMPOSSIBLE__
 
-isInstantiatedMeta :: MetaId -> TCM Bool
-isInstantiatedMeta m = isJust <$> isInstantiatedMeta' m
+-- | Check whether all metas are instantiated.
+--   Precondition: argument is a meta (in some form) or a list of metas.
+class IsInstantiatedMeta a where
+  isInstantiatedMeta :: a -> TCM Bool
 
+instance IsInstantiatedMeta MetaId where
+  isInstantiatedMeta m = isJust <$> isInstantiatedMeta' m
+
+instance IsInstantiatedMeta Term where
+  isInstantiatedMeta = loop where
+   loop v =
+    case ignoreSharing v of
+      MetaV x _  -> isInstantiatedMeta x
+      DontCare v -> loop v
+      Level l    -> isInstantiatedMeta l
+      Lam _ b    -> isInstantiatedMeta b
+      Con _ vs   -> isInstantiatedMeta vs
+      _          -> __IMPOSSIBLE__
+
+instance IsInstantiatedMeta Level where
+  isInstantiatedMeta (Max ls) = isInstantiatedMeta ls
+
+instance IsInstantiatedMeta PlusLevel where
+  isInstantiatedMeta (Plus n l) | n == 0 = isInstantiatedMeta l
+  isInstantiatedMeta _ = __IMPOSSIBLE__
+
+instance IsInstantiatedMeta LevelAtom where
+  isInstantiatedMeta (MetaLevel x es) = isInstantiatedMeta x
+  isInstantiatedMeta _ = __IMPOSSIBLE__
+
+instance IsInstantiatedMeta a => IsInstantiatedMeta [a] where
+  isInstantiatedMeta = andM . map isInstantiatedMeta
+
+instance IsInstantiatedMeta a => IsInstantiatedMeta (Maybe a) where
+  isInstantiatedMeta = isInstantiatedMeta . maybeToList
+
+instance IsInstantiatedMeta a => IsInstantiatedMeta (Common.Arg c a) where
+  isInstantiatedMeta = isInstantiatedMeta . unArg
+
+-- | Does not worry about raising.
+instance IsInstantiatedMeta a => IsInstantiatedMeta (Abs a) where
+  isInstantiatedMeta = isInstantiatedMeta . unAbs
+
 isInstantiatedMeta' :: MetaId -> TCM (Maybe Term)
 isInstantiatedMeta' m = do
   mv <- lookupMeta m
@@ -173,12 +214,7 @@
 removeInteractionPoint ii = do
   scope <- getInteractionScope ii
   modifyInteractionPoints $ Map.delete ii
-  modify $ \s -> s { stOldInteractionPoints = Map.insert ii scope $ stOldInteractionPoints s }
 
-removeOldInteractionPoint :: InteractionId -> TCM ()
-removeOldInteractionPoint ii =
-  modify $ \s -> s { stOldInteractionPoints = Map.delete ii $ stOldInteractionPoints s }
-
 -- | Get a list of interaction ids.
 getInteractionPoints :: TCM [InteractionId]
 getInteractionPoints = Map.keys <$> gets stInteractionPoints
@@ -240,13 +276,6 @@
 getInteractionScope :: InteractionId -> TCM ScopeInfo
 getInteractionScope = getMetaScope <.> lookupMeta <=< lookupInteractionId
 
-getOldInteractionScope :: InteractionId -> TCM ScopeInfo
-getOldInteractionScope ii = do
-  ms <- gets $ Map.lookup ii . stOldInteractionPoints
-  case ms of
-    Nothing    -> fail $ "not an old interaction point: " ++ show ii
-    Just scope -> return scope
-
 withMetaInfo' :: MetaVariable -> TCM a -> TCM a
 withMetaInfo' mv = withMetaInfo (miClosRange $ mvInfo mv)
 
@@ -362,3 +391,4 @@
 
 instance UnFreezeMeta a => UnFreezeMeta (Abs a) where
   unfreezeMeta = Fold.mapM_ unfreezeMeta
+
diff --git a/src/full/Agda/TypeChecking/Monad/Open.hs b/src/full/Agda/TypeChecking/Monad/Open.hs
--- a/src/full/Agda/TypeChecking/Monad/Open.hs
+++ b/src/full/Agda/TypeChecking/Monad/Open.hs
@@ -27,7 +27,6 @@
 makeClosed :: a -> Open a
 makeClosed = OpenThing []
 
-
 -- | Extract the value from an open term. Must be done in an extension of the
 --   context in which the term was created.
 getOpen :: Subst a => Open a -> TCM a
@@ -37,6 +36,9 @@
   unless (ctx `isSuffixOf` ctx') $ fail $ "thing out of context (" ++ show ctx ++ " is not a sub context of " ++ show ctx' ++ ")"
   return $ raise (genericLength ctx' - genericLength ctx) x
 
+-- | Try to use an 'Open' the current context.
+--   Returns 'Nothing' if current context is not an extension of the
+--   context in which the 'Open' was created.
 tryOpen :: Subst a => Open a -> TCM (Maybe a)
 tryOpen o =
   (Just <$> getOpen o)
diff --git a/src/full/Agda/TypeChecking/Monad/Options.hs-boot b/src/full/Agda/TypeChecking/Monad/Options.hs-boot
--- a/src/full/Agda/TypeChecking/Monad/Options.hs-boot
+++ b/src/full/Agda/TypeChecking/Monad/Options.hs-boot
@@ -1,5 +1,9 @@
 module Agda.TypeChecking.Monad.Options where
 
+import Control.Applicative
+import Control.Monad.Trans
+
+import Agda.Interaction.Options
 import Agda.TypeChecking.Monad.Base
 import Agda.Utils.FileName
 import Agda.Utils.Pretty
@@ -8,6 +12,15 @@
 
 type VerboseKey = String
 
+class (Functor m, Applicative m, Monad m) => HasOptions m where
+  -- | Returns the pragma options which are currently in effect.
+  pragmaOptions      :: m PragmaOptions
+  -- | Returns the command line options which are currently in effect.
+  commandLineOptions :: m CommandLineOptions
+
+instance MonadIO m => HasOptions (TCMT m)
+
+hasVerbosity :: HasOptions m => VerboseKey -> Int -> m Bool
 verboseS :: MonadTCM tcm => VerboseKey -> Int -> tcm () -> tcm ()
 reportSLn :: MonadTCM tcm => VerboseKey -> Int -> String -> tcm ()
 reportSDoc :: MonadTCM tcm => VerboseKey -> Int -> TCM Doc -> tcm ()
diff --git a/src/full/Agda/TypeChecking/Monad/State.hs b/src/full/Agda/TypeChecking/Monad/State.hs
--- a/src/full/Agda/TypeChecking/Monad/State.hs
+++ b/src/full/Agda/TypeChecking/Monad/State.hs
@@ -9,7 +9,8 @@
 import Data.Map as Map
 import qualified Data.Set as Set
 
-import {-# SOURCE #-} Agda.Interaction.Response
+-- import {-# SOURCE #-} Agda.Interaction.Response
+import Agda.Interaction.Response
   (InteractionOutputCallback, Response)
 
 import Agda.Syntax.Common
diff --git a/src/full/Agda/TypeChecking/Primitive.hs b/src/full/Agda/TypeChecking/Primitive.hs
--- a/src/full/Agda/TypeChecking/Primitive.hs
+++ b/src/full/Agda/TypeChecking/Primitive.hs
@@ -580,7 +580,8 @@
 
     -- Other stuff
     , "primTrustMe"         |-> primTrustMe
-    , "primQNameEquality"  |-> mkPrimFun2 ((==) :: Rel QName)
+    , "primQNameEquality"   |-> mkPrimFun2 ((==) :: Rel QName)
+    , "primShowQName"       |-> mkPrimFun1 (Str . show :: QName -> Str)
     ]
     where
 	(|->) = (,)
diff --git a/src/full/Agda/TypeChecking/ProjectionLike.hs b/src/full/Agda/TypeChecking/ProjectionLike.hs
--- a/src/full/Agda/TypeChecking/ProjectionLike.hs
+++ b/src/full/Agda/TypeChecking/ProjectionLike.hs
@@ -28,33 +28,54 @@
 
 -- | View for a @Def f (Apply a : es)@ where @isProjection f@.
 --   Used for projection-like @f@s.
-data ProjectionView = ProjectionView
-  { projViewProj  :: QName
-  , projViewSelf  :: I.Arg Term
-  , projViewSpine :: Elims
-  }
+data ProjectionView
+  = ProjectionView
+    { projViewProj  :: QName
+    , projViewSelf  :: I.Arg Term
+    , projViewSpine :: Elims
+    }
+    -- ^ A projection or projection-like function, applied to its
+    --   principal argument
+  | LoneProjectionLike QName I.ArgInfo
+    -- ^ Just a lone projection-like function, missing its principal
+    --   argument (from which we could infer the parameters).
+  | NoProjection Term
+    -- ^ Not a projection or projection-like thing.
 
 -- | Semantics of 'ProjectionView'.
 unProjView :: ProjectionView -> Term
-unProjView (ProjectionView f a es) = Def f (Apply a : es)
+unProjView pv =
+  case pv of
+    ProjectionView f a es   -> Def f (Apply a : es)
+    LoneProjectionLike f ai -> Def f []
+    NoProjection v          -> v
 
 -- | Top-level 'ProjectionView' (no reduction).
-projView :: Term -> TCM (Maybe ProjectionView)
+projView :: Term -> TCM ProjectionView
 projView v = do
+  let fallback = return $ NoProjection v
   case ignoreSharing v of
-    Def f (Apply a : es) -> (ProjectionView f a es <$) <$> isProjection f
-    _                    -> return Nothing
+    Def f es -> caseMaybeM (isProjection f) fallback $ \ isP -> do
+      case es of
+        []           -> return $ LoneProjectionLike f $ projArgInfo isP
+        Apply a : es -> return $ ProjectionView f a es
+        -- Since a projection is a function, it cannot be projected itself.
+        Proj{}  : _  -> __IMPOSSIBLE__
+    _ -> fallback
 
 -- | Reduce away top-level projection like functions.
 --   (Also reduces projections, but they should not be there,
 --   since Internal is in lambda- and projection-beta-normal form.)
 --
 reduceProjectionLike :: Term -> TCM Term
-reduceProjectionLike v =
+reduceProjectionLike v = do
   -- Andreas, 2013-11-01 make sure we do not reduce a constructor
   -- because that could be folded back into a literal by reduce.
-  maybeM (return v) (\ _ -> onlyReduceProjections $ reduce v) $ projView v
+  pv <- projView v
+  case pv of
+    ProjectionView{} -> onlyReduceProjections $ reduce v
                             -- ordinary reduce, only different for Def's
+    _                -> return v
 
 -- | Turn prefix projection-like function application into postfix ones.
 --   This does just one layer, such that the top spine contains
@@ -62,18 +83,27 @@
 --   Used in 'compareElims' in @TypeChecking.Conversion@
 --   and in 'Agda.TypeChecking.CheckInternal'.
 --
+--   If the 'Bool' is 'True', a lone projection like function will be
+--   turned into a lambda-abstraction, expecting the principal argument.
+--   If the 'Bool' is 'False', it will be returned unaltered.
+--
 --   No precondition.
 --   Preserves constructorForm, since it really does only something
---   applications of projection-like functions.
-elimView :: Term -> TCM Term
-elimView v = do
+--   on (applications of) projection-like functions.
+elimView :: Bool -> Term -> TCM Term
+elimView loneProjToLambda v = do
   reportSDoc "tc.conv.elim" 30 $ text "elimView of " <+> prettyTCM v
   reportSLn  "tc.conv.elim" 50 $ "v = " ++ show v
   v <- reduceProjectionLike v
   reportSDoc "tc.conv.elim" 40 $
     text "elimView (projections reduced) of " <+> prettyTCM v
-  caseMaybeM (projView v) (return v) $ \ (ProjectionView f a es) -> do
-        (`applyE` (Proj f : es)) <$> elimView (unArg a)
+  pv <- projView v
+  case pv of
+    NoProjection{}        -> return v
+    LoneProjectionLike f ai
+      | loneProjToLambda  -> return $ Lam ai $ Abs "r" $ Var 0 [Proj f]
+      | otherwise         -> return v
+    ProjectionView f a es -> (`applyE` (Proj f : es)) <$> elimView loneProjToLambda (unArg a)
 
 {- Andreas, 2013-11-01: Use of unLevel no longer necessary, since we do not reduce!
   case ignoreSharing v of
@@ -149,7 +179,7 @@
           reportSLn "tc.proj.like" 60 $ "  rewrote clauses to\n    " ++ show cc
 
           -- Andreas, 2013-10-20 build parameter dropping function
-          let ptel = take n $ telToList $ theTel $ telView' t
+          let (ptel, Dom ai _ : _) = splitAt n $ telToList $ theTel $ telView' t
               -- leading lambdas are to ignore parameter applications
               proj = teleNoAbs ptel $ Def x []
               -- proj = foldr (\ (Dom ai (y, _)) -> Lam ai . NoAbs y) (Def x []) ptel
@@ -159,6 +189,7 @@
                 , projFromType = d
                 , projIndex    = n + 1
                 , projDropPars = proj
+                , projArgInfo  = ai
                 }
           let newDef = def
                        { funProjection     = Just projection
diff --git a/src/full/Agda/TypeChecking/Reduce.hs b/src/full/Agda/TypeChecking/Reduce.hs
--- a/src/full/Agda/TypeChecking/Reduce.hs
+++ b/src/full/Agda/TypeChecking/Reduce.hs
@@ -36,6 +36,9 @@
 
 import Agda.Utils.Monad
 import Agda.Utils.HashMap (HashMap)
+import Agda.Utils.Maybe
+import Agda.Utils.Monad
+import Agda.Utils.Tuple
 
 #include "../undefined.h"
 import Agda.Utils.Impossible
@@ -282,7 +285,10 @@
           v <- unfoldDefinition False reduceB' (Con c []) (conName c) args
           traverse reduceNat v
       Sort s   -> fmap sortTm <$> reduceB' s
-      Level l  -> fmap levelTm <$> reduceB' l
+      Level l  -> ifM (elem LevelReductions <$> asks envAllowedReductions)
+                    {- then -} (fmap levelTm <$> reduceB' l)
+                    {- else -} done
+      -- Level l  -> fmap levelTm <$> reduceB' l
       Pi _ _   -> done
       Lit _    -> done
       Var _ _  -> done
@@ -390,7 +396,7 @@
                   = retSimpl $ notBlocked $ v0 `applyE` es -- not fully applied
       | otherwise = {-# SCC "reducePrimitive" #-} do
           let (es1,es2) = genericSplitAt ar es
-              args1     = maybe __IMPOSSIBLE__ id $ mapM isApplyElim es1
+              args1     = fromMaybe __IMPOSSIBLE__ $ mapM isApplyElim es1
           r <- primFunImplementation pf args1
           case r of
             NoReduction args1' -> do
@@ -1101,7 +1107,7 @@
   instantiateFull' (DDot  v)	   = DDot  <$> instantiateFull' v
   instantiateFull' (DCon c vs)	   = DCon c <$> instantiateFull' vs
   instantiateFull' (DDef c vs)	   = DDef c <$> instantiateFull' vs
-  instantiateFull' (DWithApp vs ws) = uncurry DWithApp <$> instantiateFull' (vs, ws)
+  instantiateFull' (DWithApp v vs ws) = uncurry3 DWithApp <$> instantiateFull' (v, vs, ws)
 
 instance InstantiateFull Defn where
     instantiateFull' d = case d of
diff --git a/src/full/Agda/TypeChecking/Reduce/Monad.hs b/src/full/Agda/TypeChecking/Reduce/Monad.hs
--- a/src/full/Agda/TypeChecking/Reduce/Monad.hs
+++ b/src/full/Agda/TypeChecking/Reduce/Monad.hs
@@ -177,6 +177,3 @@
           init' [] = {-'-} __IMPOSSIBLE__
           init' xs = init xs
 
-instantiateDef :: Definition -> ReduceM Definition
-instantiateDef def = undefined
-
diff --git a/src/full/Agda/TypeChecking/Rules/Builtin/Coinduction.hs b/src/full/Agda/TypeChecking/Rules/Builtin/Coinduction.hs
--- a/src/full/Agda/TypeChecking/Rules/Builtin/Coinduction.hs
+++ b/src/full/Agda/TypeChecking/Rules/Builtin/Coinduction.hs
@@ -139,6 +139,7 @@
           , projFromType = inf
           , projIndex    = 3
           , projDropPars = teleNoAbs (take 2 $ telToList tel) $ Def flat []
+          , projArgInfo  = defaultArgInfo
           }
     addConstant flat $
       flatDefn { defPolarity       = []
diff --git a/src/full/Agda/TypeChecking/Rules/Decl.hs b/src/full/Agda/TypeChecking/Rules/Decl.hs
--- a/src/full/Agda/TypeChecking/Rules/Decl.hs
+++ b/src/full/Agda/TypeChecking/Rules/Decl.hs
@@ -287,7 +287,7 @@
   -- namesDefs <- mapM (\ q -> (q,) <$> getConstInfo q) $ Set.toList names
   -- mapM_ checkInj namesDefs
 
-  forM_ (Set.toList names) $ \ q -> do
+  Fold.forM_ names $ \ q -> do
     def <- getConstInfo q
     case theDef def of
       d@Function{ funClauses = cs, funTerminates = Just True } -> do
@@ -376,20 +376,7 @@
              unless (m == m') $ typeError $ GenericError $
               "COMPILED_DATA directives must appear in the same module " ++
               "as their corresponding datatype definition,"
-          case theDef def of
-            Datatype{dataCons = cs}
-              | length cs /= length hcs -> do
-                  let n_forms_are = case length hcs of
-                        1 -> "1 compiled form is"
-                        n -> show n ++ " compiled forms are"
-                      only | null hcs               = ""
-                           | length hcs < length cs = "only "
-                           | otherwise              = ""
-
-                  err <- fsep $ [prettyTCM x] ++ pwords ("has " ++ show (length cs) ++
-                                " constructors, but " ++ only ++ n_forms_are ++ " given [" ++ unwords hcs ++ "]")
-                  typeError $ GenericError $ show err
-              | otherwise -> do
+          let addCompiledData cs = do
                 addHaskellType x hs
                 let computeHaskellType c = do
                       def <- getConstInfo c
@@ -399,13 +386,33 @@
                             a <- reduce a
                             case unEl a of
                               Pi a (NoAbs _ b) -> underPars (n - 1) b
-                              Pi a b  -> underAbstraction a b $ underPars (n - 1)
+                              Pi a b  -> underAbstraction a b $ \b -> hsForall <$> getHsVar 0 <*> underPars (n - 1) b
                               _       -> __IMPOSSIBLE__
                       ty <- underPars np $ defType def
                       reportSLn "tc.pragma.compile" 10 $ "Haskell type for " ++ show c ++ ": " ++ ty
                       return ty
                 hts <- mapM computeHaskellType cs
                 sequence_ $ zipWith3 addHaskellCode cs hts hcs
+          case theDef def of
+            Datatype{dataCons = cs}
+              | length cs /= length hcs -> do
+                  let n_forms_are = case length hcs of
+                        1 -> "1 compiled form is"
+                        n -> show n ++ " compiled forms are"
+                      only | null hcs               = ""
+                           | length hcs < length cs = "only "
+                           | otherwise              = ""
+
+                  err <- fsep $ [prettyTCM x] ++ pwords ("has " ++ show (length cs) ++
+                                " constructors, but " ++ only ++ n_forms_are ++ " given [" ++ unwords hcs ++ "]")
+                  typeError $ GenericError $ show err
+              | otherwise -> addCompiledData cs
+            Record{recConHead = ch}
+              | length hcs == 1 -> addCompiledData [conName ch]
+              | otherwise -> do
+                  err <- fsep $ [prettyTCM x] ++ pwords ("has 1 constructor, but " ++
+                                show (length hcs) ++ " Haskell constructors are given [" ++ unwords hcs ++ "]")
+                  typeError $ GenericError $ show err
             _ -> typeError $ GenericError "COMPILED_DATA on non datatype"
         A.CompiledPragma x hs -> do
           def <- getConstInfo x
diff --git a/src/full/Agda/TypeChecking/Rules/Def.hs b/src/full/Agda/TypeChecking/Rules/Def.hs
--- a/src/full/Agda/TypeChecking/Rules/Def.hs
+++ b/src/full/Agda/TypeChecking/Rules/Def.hs
@@ -355,21 +355,24 @@
 insertPatterns pats (A.RewriteRHS qs eqs rhs wh) = A.RewriteRHS qs eqs (insertPatterns pats rhs) wh
 insertPatterns pats rhs = rhs
 
+-- | Parameters for creating a @with@-function.
 data WithFunctionProblem
-      = NoWithFunction
-      | WithFunction QName                -- parent function name
-                     QName                -- with function name
-                     Telescope            -- arguments to parent function
-                     Telescope            -- arguments to the with function before the with expressions
-                     Telescope            -- arguments to the with function after the with expressions
-                     [Term]               -- with expressions
-                     [Type]               -- types of the with expressions
-                     Type                 -- type of the right hand side
-                     [I.NamedArg Pattern] -- parent patterns
-                     Permutation          -- permutation resulting from splitting the telescope into needed and unneeded vars
-                     Permutation          -- permutation reordering the variables in the parent pattern
-                     Permutation          -- final permutation (including permutation for the parent clause)
-                     [A.Clause]           -- the given clauses for the with function
+  = NoWithFunction
+  | WithFunction
+    { wfParentName :: QName                -- ^ parent function name
+    , wfName       :: QName                -- ^ with function name
+    , wfParentTel  :: Telescope            -- ^ arguments to parent function
+    , wfBeforeTel  :: Telescope            -- ^ arguments to the with function before the with expressions
+    , wfAfterTel   :: Telescope            -- ^ arguments to the with function after the with expressions
+    , wfExprs      :: [Term]               -- ^ with expressions
+    , wfExprTypes  :: [Type]               -- ^ types of the with expressions
+    , wfRHSType    :: Type                 -- ^ type of the right hand side
+    , wfParentPats :: [I.NamedArg Pattern] -- ^ parent patterns
+    , wfPermSplit  :: Permutation          -- ^ permutation resulting from splitting the telescope into needed and unneeded vars
+    , wfPermParent :: Permutation          -- ^ permutation reordering the variables in the parent pattern
+    , wfPermFinal  :: Permutation          -- ^ final permutation (including permutation for the parent clause)
+    , wfClauses    :: [A.Clause]           -- ^ the given clauses for the with function
+    }
 
 -- | Type check a function clause.
 {-
diff --git a/src/full/Agda/TypeChecking/Rules/Record.hs b/src/full/Agda/TypeChecking/Rules/Record.hs
--- a/src/full/Agda/TypeChecking/Rules/Record.hs
+++ b/src/full/Agda/TypeChecking/Rules/Record.hs
@@ -360,6 +360,7 @@
           -- split the telescope into parameters (ptel) and the type or the record
           -- (rt) which should be  R ptel
           (ptel,[rt]) = splitAt (size tel - 1) $ telToList tel
+          projArgI    = domInfo rt
 	  conp	 = defaultArg
 		 $ ConP con (Just (False, argFromDom $ fmap snd rt))
                    [ Arg info $ unnamed $ VarP "x" | Dom info _ <- telToList ftel ]
@@ -380,7 +381,7 @@
 
       -- Andreas, 2013-10-20
       -- creating the projection construction function
-      let core = Lam defaultArgInfo $ Abs "r" $ bodyMod $ projcall
+      let core = Lam projArgI $ Abs "r" $ bodyMod $ projcall
           -- leading lambdas are to ignore parameter applications
           proj = teleNoAbs ptel core
           -- proj = foldr (\ (Dom ai (x, _)) -> Lam ai . NoAbs x) core ptel
@@ -392,6 +393,7 @@
             -- start counting with 1:
             , projIndex    = size ptel + 1  -- which is @size tel@
             , projDropPars = proj
+            , projArgInfo  = projArgI
             }
 
       reportSDoc "tc.rec.proj" 80 $ sep
diff --git a/src/full/Agda/TypeChecking/Rules/Term.hs b/src/full/Agda/TypeChecking/Rules/Term.hs
--- a/src/full/Agda/TypeChecking/Rules/Term.hs
+++ b/src/full/Agda/TypeChecking/Rules/Term.hs
@@ -687,11 +687,13 @@
               blockTerm t' $ coerce v ty t'
         e0@(A.QuoteContext _ x e) -> do
           ctx <- getContext
-          lets <- envLetBindings <$> ask
           thisModule <- currentModule
+--          Disabled let bindings for now, as there is no way to get your hands on the
+--          associated terms using the current reflection mechanism.
+--          lets <- envLetBindings <$> ask
+--          let letNames = map (quoteName . qualify thisModule) $ Map.keys lets
           let contextNames = map (\(Dom _ (nm,_)) -> quoteName $ qualify thisModule nm) ctx
-          let letNames = map (quoteName . qualify thisModule) $ Map.keys lets
-          let names = contextNames ++ letNames
+          let names = contextNames -- ++ letNames
           nameList <- buildList <*> return names
           ctxType <- el (list primQName)
           (v, ctxType) <- addLetBinding defaultArgInfo x nameList ctxType (inferExpr e)
@@ -1201,7 +1203,7 @@
                   ErrorT (Args, [I.NamedArg A.Expr], Type) TCM (Args, Type)
 
 -- Case: no arguments, do not insert trailing hidden arguments: We are done.
-checkArguments DontExpandLast _ _ [] t0 t1 = return ([], t0)
+checkArguments DontExpandLast DontExpandInstanceArguments _ [] t0 t1 = return ([], t0)
 
 -- Case: no arguments, but need to insert trailing hiddens.
 checkArguments exh    expandIFS r [] t0 t1 =
@@ -1209,8 +1211,9 @@
       t1' <- unEl <$> reduce t1
       implicitArgs (-1) (expand t1') t0
     where
-      expand (Pi (Dom info _) _)   Hidden = getHiding info /= Hidden
-      expand _                     Hidden = True
+      expand (Pi (Dom info _) _)   Hidden = getHiding info /= Hidden &&
+                                            exh == ExpandLast
+      expand _                     Hidden = exh == ExpandLast
       expand (Pi (Dom info _) _) Instance = getHiding info /= Instance &&
                                             expandIFS == ExpandInstanceArguments
       expand _                   Instance = expandIFS == ExpandInstanceArguments
diff --git a/src/full/Agda/TypeChecking/Serialise.hs b/src/full/Agda/TypeChecking/Serialise.hs
--- a/src/full/Agda/TypeChecking/Serialise.hs
+++ b/src/full/Agda/TypeChecking/Serialise.hs
@@ -71,7 +71,7 @@
 
 import Agda.TypeChecking.Monad
 import Agda.TypeChecking.CompiledClause
-import Agda.TypeChecking.Pretty
+-- import Agda.TypeChecking.Pretty
 
 import Agda.Utils.BiMap (BiMap)
 import qualified Agda.Utils.BiMap as BiMap
@@ -89,7 +89,7 @@
 -- 32-bit machines). Word64 does not have these problems.
 
 currentInterfaceVersion :: Word64
-currentInterfaceVersion = 20140603 * 10 + 0
+currentInterfaceVersion = 20140611 * 10 + 0
 
 -- | Constructor tag (maybe omitted) and argument indices.
 
@@ -257,9 +257,12 @@
   case r of
     Right x   -> return (Just x)
     Left  err -> do
-      reportSDoc "import.iface" 5 $
-        text "Error when decoding interface file:" $+$
-        nest 2 (prettyTCM err)
+      reportSLn "import.iface" 5 $ "Error when decoding interface file"
+      -- Andreas, 2014-06-11 deactivated debug printing
+      -- in order to get rid of dependency of Serialize on TCM.Pretty
+      -- reportSDoc "import.iface" 5 $
+      --   text "Error when decoding interface file:"
+      --   $+$ nest 2 (prettyTCM err)
       return Nothing
 
   where
@@ -885,12 +888,12 @@
   icode (DDot     a  ) = icode1 1 a
   icode (DCon     a b) = icode2 2 a b
   icode (DDef     a b) = icode2 3 a b
-  icode (DWithApp a b) = icode2 4 a b
+  icode (DWithApp a b c) = icode3 4 a b c
   value = vcase valu where valu [a]       = valu1 DTerm a
                            valu [1, a]    = valu1 DDot a
                            valu [2, a, b] = valu2 DCon a b
                            valu [3, a, b] = valu2 DDef a b
-                           valu [4, a, b] = valu2 DWithApp a b
+                           valu [4, a, b, c] = valu3 DWithApp a b c
                            valu _         = malformed
 
 instance EmbPrj MutualId where
@@ -903,9 +906,9 @@
                            valu _                             = malformed
 
 instance EmbPrj Projection where
-  icode (Projection a b c d) = icode4' a b c d
-  value = vcase valu where valu [a, b, c, d] = valu4 Projection a b c d
-                           valu _            = malformed
+  icode (Projection a b c d e) = icode5' a b c d e
+  value = vcase valu where valu [a, b, c, d, e] = valu5 Projection a b c d e
+                           valu _               = malformed
 
 instance EmbPrj HaskellExport where
   icode (HsExport a b) = icode2' a b
diff --git a/src/full/Agda/TypeChecking/Substitute.hs b/src/full/Agda/TypeChecking/Substitute.hs
--- a/src/full/Agda/TypeChecking/Substitute.hs
+++ b/src/full/Agda/TypeChecking/Substitute.hs
@@ -24,8 +24,9 @@
 
 import Agda.Utils.List
 import Agda.Utils.Monad
-import Agda.Utils.Size
 import Agda.Utils.Permutation
+import Agda.Utils.Size
+import Agda.Utils.Tuple
 
 #include "../undefined.h"
 import Agda.Utils.Impossible
@@ -268,7 +269,7 @@
   apply (DDot v)           args = DDot  $ apply v args
   apply (DCon c vs)        args = DCon c $ vs ++ map (fmap DTerm) args
   apply (DDef c vs)        args = DDef c $ vs ++ map (fmap DTerm) args
-  apply (DWithApp v args') args = DWithApp v $ args' ++ args
+  apply (DWithApp v ws args') args = DWithApp v ws $ args' ++ args
 
 instance Apply t => Apply [t] where
   apply  ts args = map (`apply` args) ts
@@ -646,7 +647,7 @@
   applySubst rho (DDot v)         = DDot  $ applySubst rho v
   applySubst rho (DCon c vs)      = DCon c $ applySubst rho vs
   applySubst rho (DDef c vs)      = DDef c $ applySubst rho vs
-  applySubst rho (DWithApp vs ws) = uncurry DWithApp $ applySubst rho (vs, ws)
+  applySubst rho (DWithApp v vs ws) = uncurry3 DWithApp $ applySubst rho (v, vs, ws)
 
 instance Subst a => Subst (Tele a) where
   applySubst rho  EmptyTel         = EmptyTel
diff --git a/src/full/Agda/TypeChecking/With.hs b/src/full/Agda/TypeChecking/With.hs
--- a/src/full/Agda/TypeChecking/With.hs
+++ b/src/full/Agda/TypeChecking/With.hs
@@ -292,24 +292,42 @@
 --   For instance, @aux a b c@ as @f (suc a) (suc b) | c@
 --
 --   @n@ is the number of with arguments.
-withDisplayForm :: QName -> QName -> Telescope -> Telescope -> Nat -> [I.NamedArg Pattern] -> Permutation -> Permutation -> TCM DisplayForm
+withDisplayForm
+  :: QName       -- ^ The name of parent function.
+  -> QName       -- ^ The name of the with-function.
+  -> Telescope   -- ^ The arguments of the with function before the with exprs.
+  -> Telescope   -- ^ The arguments of the with function after the with exprs.
+  -> Nat         -- ^ The number of with expressions.
+  -> [I.NamedArg Pattern] -- ^ The parent patterns.
+  -> Permutation -- ^ Permutation to split into needed and unneeded vars.
+  -> Permutation -- ^ Permutation reordering the variables in parent patterns.
+  -> TCM DisplayForm
 withDisplayForm f aux delta1 delta2 n qs perm@(Perm m _) lhsPerm = do
-  topArgs <- raise (n + size delta1 + size delta2) <$> getContextArgs
+
+  -- Compute the arity of the display form.
+  let arity0 = n + size delta1 + size delta2
+  -- The currently free variables have to be added to the front.
+  topArgs <- raise arity0 <$> getContextArgs
+  let top    = genericLength topArgs
+      arity  = arity0 + top
+
+  -- Build the rhs of the display form.
   x <- freshNoName_
   let wild = Def (qualify (mnameFromList []) x) []
+      -- Building the arguments to the with function
+      (ys0, ys1) = splitAt (size delta1) (permute perm $ map Just [m - 1, m - 2..0])
+      ys = reverse $ ys0 ++ genericReplicate n Nothing ++ ys1
 
   let tqs = patsToTerms lhsPerm qs
-      top = genericLength topArgs
       vs = map (fmap DTerm) topArgs ++ applySubst (sub top ys wild) tqs
-      dt = DWithApp (DDef f vs : map DTerm withArgs) []
       withArgs = map var $ genericTake n $ downFrom $ size delta2 + n
---      withArgs = reverse $ map var [size delta2..size delta2 + n - 1]
-      pats = genericReplicate (n + size delta1 + size delta2 + top) (var 0)
-      -- Building the arguments to the with function
-      (ys0, ys1) = splitAt (size delta1) (permute perm $ map Just [m - 1, m - 2..0])
-      ys = reverse $ ys0 ++ genericReplicate n Nothing ++ ys1
+      dt = DWithApp (DDef f vs) (map DTerm withArgs) []
 
-  let display = Display (n + size delta1 + size delta2 + top) pats dt
+  -- Build the lhs of the display form.
+  -- @var 0@ is the pattern variable (hole).
+  let pats = genericReplicate arity (var 0)
+
+  let display = Display arity pats dt
       addFullCtx = addCtxTel delta1
                  . flip (foldr addCtxString_) (map ("w" ++) $ map show [1..n])
                  . addCtxTel delta2
diff --git a/src/full/Agda/Utils/List.hs b/src/full/Agda/Utils/List.hs
--- a/src/full/Agda/Utils/List.hs
+++ b/src/full/Agda/Utils/List.hs
@@ -44,16 +44,12 @@
   loop [a]      = ([], a)
   loop (a : as) = mapFst (a:) $ loop as
 
--- | Lookup function (safe).
-
+-- | Lookup function (partially safe).
 (!!!) :: [a] -> Int -> Maybe a
-[]     !!! _ = Nothing
-(x:xs) !!! 0 = Just x
-(x:xs) !!! n = xs !!! predecessor n
-
-predecessor n
-  | n > 0     = n - 1
-  | otherwise = __IMPOSSIBLE__
+_        !!! n | n < 0 = __IMPOSSIBLE__
+[]       !!! _         = Nothing
+(x : _)  !!! 0         = Just x
+(_ : xs) !!! n         = xs !!! (n - 1)
 
 -- | downFrom n = [n-1,..1,0]
 downFrom :: Integral a => a -> [a]