diff --git a/Agda.cabal b/Agda.cabal
--- a/Agda.cabal
+++ b/Agda.cabal
@@ -1,5 +1,5 @@
 name:            Agda
-version:         2.6.0
+version:         2.6.0.1
 cabal-version:   >= 1.10
 build-type:      Custom
 license:         OtherLicense
@@ -37,7 +37,8 @@
                     GHC == 8.0.2
                     GHC == 8.2.2
                     GHC == 8.4.4
-                    GHC == 8.6.4
+                    GHC == 8.6.5
+
 extra-source-files: CHANGELOG.md
                     README.md
                     doc/user-manual.pdf
@@ -46,7 +47,7 @@
                     stack-8.0.2.yaml
                     stack-8.2.2.yaml
                     stack-8.4.4.yaml
-                    stack-8.6.4.yaml
+                    stack-8.6.5.yaml
 
 data-dir:           src/data
 data-files:         Agda.css
@@ -82,6 +83,7 @@
                     lib/prim/Agda/Builtin/TrustMe.agda
                     lib/prim/Agda/Builtin/Unit.agda
                     lib/prim/Agda/Builtin/Word.agda
+                    lib/prim/Agda/Builtin/Word/Properties.agda
                     lib/prim/Agda/Primitive.agda
                     lib/prim/Agda/Primitive/Cubical.agda
                     MAlonzo/src/MAlonzo/*.hs
@@ -94,7 +96,7 @@
 source-repository this
   type:     git
   location: https://github.com/agda/agda.git
-  tag:      v2.6.0
+  tag:      v2.6.0.1
 
 flag cpphs
   default:     False
@@ -225,7 +227,7 @@
 
   -- ASR (2018-09-14). We add the dependency on the filemanip library
   -- due to Issue #3225.
-  if impl(ghc >= 7.10) && impl(ghc < 8.0)
+  if impl(ghc < 8.0)
     build-depends:   transformers == 0.4.2.0
                    , filemanip >= 0.3.6.2 && < 0.4
 
@@ -576,33 +578,32 @@
   if impl(ghc >= 8.0)
     ghc-options: -Wunrecognised-warning-flags
 
-  if impl(ghc >= 7.10)
-    ghc-options: -fwarn-deprecated-flags
-                 -fwarn-deriving-typeable
-                 -fwarn-dodgy-exports
-                 -fwarn-dodgy-foreign-imports
-                 -fwarn-dodgy-imports
-                 -fwarn-duplicate-exports
-                 -fwarn-empty-enumerations
-                 -fwarn-hi-shadowing
-                 -fwarn-identities
-                 -fwarn-incomplete-patterns
-                 -fwarn-inline-rule-shadowing
-                 -fwarn-missing-fields
-                 -fwarn-missing-methods
-                 -fwarn-missing-signatures
-                 -fwarn-tabs
-                 -fwarn-typed-holes
-                 -fwarn-overflowed-literals
-                 -fwarn-overlapping-patterns
-                 -fwarn-unrecognised-pragmas
-                 -fwarn-unticked-promoted-constructors
-                 -fwarn-unused-do-bind
-                 -fwarn-warnings-deprecations
-                 -fwarn-wrong-do-bind
+  ghc-options: -fwarn-deprecated-flags
+               -fwarn-deriving-typeable
+               -fwarn-dodgy-exports
+               -fwarn-dodgy-foreign-imports
+               -fwarn-dodgy-imports
+               -fwarn-duplicate-exports
+               -fwarn-empty-enumerations
+               -fwarn-hi-shadowing
+               -fwarn-identities
+               -fwarn-incomplete-patterns
+               -fwarn-inline-rule-shadowing
+               -fwarn-missing-fields
+               -fwarn-missing-methods
+               -fwarn-missing-signatures
+               -fwarn-tabs
+               -fwarn-typed-holes
+               -fwarn-overflowed-literals
+               -fwarn-overlapping-patterns
+               -fwarn-unrecognised-pragmas
+               -fwarn-unticked-promoted-constructors
+               -fwarn-unused-do-bind
+               -fwarn-warnings-deprecations
+               -fwarn-wrong-do-bind
 
   -- These options will be removed in GHC 8.0.1.
-  if impl(ghc >= 7.10) && impl(ghc < 8.0)
+  if impl(ghc < 8.0)
     ghc-options: -fwarn-context-quantification
                  -fwarn-duplicate-constraints
                  -fwarn-pointless-pragmas
@@ -663,13 +664,12 @@
                   -- except for the prelude.
                 , base >= 4.8.0.0 && < 6
   default-language: Haskell2010
-  if impl(ghc >= 7)
-    -- If someone installs Agda with the setuid bit set, then the
-    -- presence of +RTS may be a security problem (see GHC bug #3910).
-    -- However, we sometimes recommend people to use +RTS to control
-    -- Agda's memory usage, so we want this functionality enabled by
-    -- default.
-    ghc-options:  -rtsopts
+  -- If someone installs Agda with the setuid bit set, then the
+  -- presence of +RTS may be a security problem (see GHC bug #3910).
+  -- However, we sometimes recommend people to use +RTS to control
+  -- Agda's memory usage, so we want this functionality enabled by
+  -- default.
+  ghc-options:  -rtsopts
 
 executable agda-mode
   hs-source-dirs:   src/agda-mode
diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,26 @@
+Release notes for Agda version 2.6.0.1
+======================================
+
+Installation and infrastructure
+-------------------------------
+
+* Added support for GHC 8.6.5.
+
+List of all closed issues
+-------------------------
+
+For 2.6.0.1, the following issues have been closed
+(see [bug tracker](https://github.com/agda/agda/issues)):
+
+  -  [#3685](https://github.com/agda/agda/issues/3685): Support GHC 8.6.5
+  -  [#3692](https://github.com/agda/agda/issues/3692): Omission of absurd patterns in automatically added absurd clauses causes too optimistic polarity.
+  -  [#3694](https://github.com/agda/agda/issues/3694): Importing Agda.Builtin.Size in one module affects another module
+  -  [#3696](https://github.com/agda/agda/issues/3696): Make `AgdaAny` polykinded?
+  -  [#3697](https://github.com/agda/agda/issues/3697): Panic when checking non-Setω data definitions with --type-in-type
+  -  [#3701](https://github.com/agda/agda/issues/3701): [ re agda/agda-stdlib#710 ] toNat for machine words is injective
+  -  [#3731](https://github.com/agda/agda/issues/3731): GHC backend thinks that a constructor called 'main' is the main program
+  -  [#3742](https://github.com/agda/agda/issues/3742): Strange error message for code that combines mutual and abstract
+
 Release notes for Agda version 2.6.0
 ====================================
 
@@ -5,18 +28,18 @@
 ----------
 
 * Added support for [Cubical
-  Agda](https://agda.readthedocs.io/en/latest/language/cubical.html)
+  Agda](https://agda.readthedocs.io/en/v2.6.0/language/cubical.html)
   which adds new features such as univalence and higher inductive
   types to Agda.
 
 * Added support for ML-style [automatic generalization of
-  variables](https://agda.readthedocs.io/en/latest/language/generalization-of-declared-variables.html).
+  variables](https://agda.readthedocs.io/en/v2.6.0/language/generalization-of-declared-variables.html).
 
 * Added a new sort ``Prop`` of [definitionally proof-irrelevant
-  propositions](https://agda.readthedocs.io/en/latest/language/prop.html).
+  propositions](https://agda.readthedocs.io/en/v2.6.0/language/prop.html).
 
 * The implementation of [instance
-  search](https://agda.readthedocs.io/en/latest/language/instance-arguments.html)
+  search](https://agda.readthedocs.io/en/v2.6.0/language/instance-arguments.html)
   got a major overhaul and no longer supports overlapping instances
   (unless enabled by a flag).
 
@@ -59,7 +82,7 @@
    -- _∘_ : {Γ Δ Θ : Con} → Sub Θ Δ → Sub Γ Θ → Sub Γ Δ
   ```
 
-  See the [user manual](https://agda.readthedocs.io/en/latest/language/generalization-of-declared-variables.html)
+  See the [user manual](https://agda.readthedocs.io/en/v2.6.0/language/generalization-of-declared-variables.html)
   for more details.
 
 * Data type and record definitions separated from their type signatures can no
@@ -145,14 +168,14 @@
   univalence and higher inductive types. Option `--cubical` enables
   the cubical mode, and cubical primitives are defined in the module
   `Agda.Primitive.Cubical`.  See the [user
-  manual](https://agda.readthedocs.io/en/latest/language/cubical.html)
+  manual](https://agda.readthedocs.io/en/v2.6.0/language/cubical.html)
   for more info.
 
 * Agda now supports the new sort ``Prop`` of [definitionally
   proof-irrelevant propositions](https://hal.inria.fr/hal-01859964).
   Option `--prop` enables the `Prop` universe but is off by default.
   Option `--no-prop` disables the `Prop` universe.  See the [user
-  manual](https://agda.readthedocs.io/en/latest/language/prop.html)
+  manual](https://agda.readthedocs.io/en/v2.6.0/language/prop.html)
   for more details.
 
   In the absense of `Prop`, the sort `Set` is the lowest sort, thus,
@@ -299,7 +322,6 @@
 Reflection
 ----------
 
-
 * New TC primitive `noConstraints` [Issue
   [#2351](https://github.com/agda/agda/issues/2351)]:
 
@@ -483,7 +505,7 @@
     {-# COMPILED_JS f e #-}
   ```
 
-  See the [user manual](https://agda.readthedocs.io/en/latest/language/foreign-function-interface.html)
+  See the [user manual](https://agda.readthedocs.io/en/v2.6.0/language/foreign-function-interface.html)
   for how to use the `COMPILE` and `FOREIGN` pragmas that replaced these in Agda 2.5.
 
 ### New warnings
@@ -3194,7 +3216,7 @@
     ```
 
     This change fixes an inconsistency, see [Issue [#2169](https://github.com/agda/agda/issues/2169)].
-    For further detail see the [user manual](http://agda.readthedocs.io/en/latest/language/built-ins.html#floats).
+    For further detail see the [user manual](http://agda.readthedocs.io/en/v2.5.2/language/built-ins.html#floats).
 
   - Floats now have only one `NaN` value. This is necessary
     for proper Float support in the JavaScript backend,
@@ -3850,7 +3872,7 @@
 -------------
 
 * There is now an official Agda User Manual:
-  http://agda.readthedocs.org/en/stable/
+  https://agda.readthedocs.io/
 
 Installation and infrastructure
 -------------------------------
diff --git a/Setup.hs b/Setup.hs
--- a/Setup.hs
+++ b/Setup.hs
@@ -8,7 +8,7 @@
 -- ASR (2019-01-10): The Cabal macro @MIN_VERSION_Cabal@ is avaliable
 -- from Cabal_>_1.24 so this macro is not supported with the
 -- "standard" GHC 7.10.3 which is shipped with Cabal 1.22.5.0.
-#if __GLASGOW_HASKELL__ > 710
+#if __GLASGOW_HASKELL__ >= 800
 #if MIN_VERSION_Cabal(2,3,0)
 import Distribution.System ( buildPlatform )
 #endif
@@ -84,7 +84,7 @@
 -- ASR (2019-01-10): The Cabal macro @MIN_VERSION_Cabal@ is avaliable
 -- from Cabal_>_1.24 so this macro is not supported with the
 -- "standard" GHC 7.10.3 which is shipped with Cabal 1.22.5.0.
-#if __GLASGOW_HASKELL__ > 710
+#if __GLASGOW_HASKELL__ >= 800
 #if MIN_VERSION_Cabal(2,3,0)
 agdaExeExtension = exeExtension buildPlatform
 #else
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
@@ -7659,8 +7659,7 @@
 
 
 {-# LINE 10 "<command-line>" #-}
-{-# LINE 1 "/usr/local/stow/ghc-8.6.5-rc1/lib/ghc-8.6.4.20190406/include/ghcversion.h" #-}
-
+{-# LINE 1 "/usr/local/stow/ghc-8.6.5/lib/ghc-8.6.5/include/ghcversion.h" #-}
 
 
 
@@ -7677,409 +7676,7 @@
 
 
 {-# LINE 10 "<command-line>" #-}
-{-# LINE 1 "/tmp/ghc23210_0/ghc_2.h" #-}
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
+{-# LINE 1 "/tmp/ghc31894_0/ghc_2.h" #-}
 
 
 
diff --git a/doc/user-manual.pdf b/doc/user-manual.pdf
Binary files a/doc/user-manual.pdf and b/doc/user-manual.pdf differ
diff --git a/src/data/MAlonzo/src/MAlonzo/RTE.hs b/src/data/MAlonzo/src/MAlonzo/RTE.hs
--- a/src/data/MAlonzo/src/MAlonzo/RTE.hs
+++ b/src/data/MAlonzo/src/MAlonzo/RTE.hs
@@ -1,8 +1,10 @@
-{-# LANGUAGE CPP #-}
+{-# LANGUAGE CPP       #-}
+{-# LANGUAGE PolyKinds #-}
+
 module MAlonzo.RTE where
 
 import Unsafe.Coerce
-#if __GLASGOW_HASKELL__ >= 802
+#if __GLASGOW_HASKELL__ >= 800
 import qualified GHC.Exts as GHC (Any)
 #else
 import qualified GHC.Prim as GHC (Any)
@@ -147,5 +149,5 @@
 
 -- Support for musical coinduction.
 
-data Inf a            = Sharp { flat :: a }
-type Infinity level a = Inf a
+data Inf                   a = Sharp { flat :: a }
+type Infinity (level :: *) a = Inf a
diff --git a/src/data/emacs-mode/agda2-mode-pkg.el b/src/data/emacs-mode/agda2-mode-pkg.el
--- a/src/data/emacs-mode/agda2-mode-pkg.el
+++ b/src/data/emacs-mode/agda2-mode-pkg.el
@@ -1,2 +1,2 @@
-(define-package "agda2-mode" "2.6.0"
+(define-package "agda2-mode" "2.6.0.1"
   "interactive development for Agda, a dependently typed functional programming language")
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.6.0"
+(defvar agda2-version "2.6.0.1"
   "The version of the Agda mode.
 Note that the same version of the Agda executable must be used.")
 
diff --git a/src/data/lib/prim/Agda/Builtin/Word/Properties.agda b/src/data/lib/prim/Agda/Builtin/Word/Properties.agda
new file mode 100644
--- /dev/null
+++ b/src/data/lib/prim/Agda/Builtin/Word/Properties.agda
@@ -0,0 +1,10 @@
+{-# OPTIONS --without-K --safe --no-sized-types --no-guardedness #-}
+
+module Agda.Builtin.Word.Properties where
+
+open import Agda.Builtin.Word
+open import Agda.Builtin.Equality
+
+primitive
+
+  primWord64ToNatInjective : ∀ a b → primWord64ToNat a ≡ primWord64ToNat b → a ≡ b
diff --git a/src/full/Agda/Compiler/Backend.hs b/src/full/Agda/Compiler/Backend.hs
--- a/src/full/Agda/Compiler/Backend.hs
+++ b/src/full/Agda/Compiler/Backend.hs
@@ -82,7 +82,7 @@
       --   required.
   , postModule       :: env -> menv -> IsMain -> ModuleName -> [def] -> TCM mod
       -- ^ Called after all definitions of a module has been compiled.
-  , compileDef       :: env -> menv -> Definition -> TCM def
+  , compileDef       :: env -> menv -> IsMain -> Definition -> TCM def
       -- ^ Compile a single definition.
   , scopeCheckingSuffices :: Bool
     -- ^ True if the backend works if @--only-scope-checking@ is used.
@@ -201,8 +201,8 @@
     Skip m         -> return m
     Recompile menv -> do
       defs <- map snd . sortDefs <$> curDefs
-      res  <- mapM (compileDef' backend env menv <=< instantiateFull) defs
+      res  <- mapM (compileDef' backend env menv isMain <=< instantiateFull) defs
       postModule backend env menv isMain (iModuleName i) res
 
-compileDef' :: Backend' opts env menv mod def -> env -> menv -> Definition -> TCM def
-compileDef' backend env menv def = setCurrentRange (defName def) $ compileDef backend env menv def
+compileDef' :: Backend' opts env menv mod def -> env -> menv -> IsMain -> Definition -> TCM def
+compileDef' backend env menv isMain def = setCurrentRange (defName def) $ compileDef backend env menv isMain def
diff --git a/src/full/Agda/Compiler/Common.hs b/src/full/Agda/Compiler/Common.hs
--- a/src/full/Agda/Compiler/Common.hs
+++ b/src/full/Agda/Compiler/Common.hs
@@ -44,6 +44,7 @@
 data IsMain = IsMain | NotMain
   deriving (Eq, Show)
 
+-- | Conjunctive semigroup ('NotMain' is absorbing).
 instance Semigroup IsMain where
   NotMain <> _ = NotMain
   _       <> NotMain = NotMain
diff --git a/src/full/Agda/Compiler/JS/Compiler.hs b/src/full/Agda/Compiler/JS/Compiler.hs
--- a/src/full/Agda/Compiler/JS/Compiler.hs
+++ b/src/full/Agda/Compiler/JS/Compiler.hs
@@ -151,8 +151,8 @@
       IsMain  -> Just $ Apply (Lookup Self $ MemberId "main") [Lambda 1 emp]
       NotMain -> Nothing
 
-jsCompileDef :: JSOptions -> JSModuleEnv -> Definition -> TCM (Maybe Export)
-jsCompileDef _ kit def = definition kit (defName def, def)
+jsCompileDef :: JSOptions -> JSModuleEnv -> IsMain -> Definition -> TCM (Maybe Export)
+jsCompileDef _ kit _isMain def = definition kit (defName def, def)
 
 --------------------------------------------------
 -- Naming
diff --git a/src/full/Agda/Compiler/MAlonzo/Compiler.hs b/src/full/Agda/Compiler/MAlonzo/Compiler.hs
--- a/src/full/Agda/Compiler/MAlonzo/Compiler.hs
+++ b/src/full/Agda/Compiler/MAlonzo/Compiler.hs
@@ -181,7 +181,7 @@
     (map fakeDecl (hsImps ++ code) ++ concat defs)
   hasMainFunction <$> curIF
 
-ghcCompileDef :: GHCOptions -> GHCModuleEnv -> Definition -> TCM [HS.Decl]
+ghcCompileDef :: GHCOptions -> GHCModuleEnv -> IsMain -> Definition -> TCM [HS.Decl]
 ghcCompileDef _ = definition
 
 -- Compilation ------------------------------------------------------------
@@ -224,16 +224,16 @@
 -- Main compiling clauses
 --------------------------------------------------
 
-definition :: GHCModuleEnv -> Definition -> TCM [HS.Decl]
+definition :: GHCModuleEnv -> IsMain -> Definition -> TCM [HS.Decl]
 -- ignore irrelevant definitions
 {- Andreas, 2012-10-02: Invariant no longer holds
 definition kit (Defn NonStrict _ _  _ _ _ _ _ _) = __IMPOSSIBLE__
 -}
-definition env Defn{defArgInfo = info, defName = q} | not $ usableModality info = do
+definition _env _isMain Defn{defArgInfo = info, defName = q} | not $ usableModality info = do
   reportSDoc "compile.ghc.definition" 10 $
     "Not compiling" <+> prettyTCM q <> "."
   return []
-definition env Defn{defName = q, defType = ty, theDef = d} = do
+definition env isMain def@Defn{defName = q, defType = ty, theDef = d} = do
   reportSDoc "compile.ghc.definition" 10 $ vcat
     [ "Compiling" <+> prettyTCM q <> ":"
     , nest 2 $ text (show d)
@@ -243,7 +243,7 @@
   mlist  <- getBuiltinName builtinList
   minf   <- getBuiltinName builtinInf
   mflat  <- getBuiltinName builtinFlat
-  checkTypeOfMain q ty $ do
+  checkTypeOfMain isMain q def $ do
     infodecl q <$> case d of
 
       _ | Just HsDefn{} <- pragma, Just q == mflat ->
@@ -314,12 +314,19 @@
       Function{} -> function pragma $ functionViaTreeless q
 
       Datatype{ dataPars = np, dataIxs = ni, dataClause = cl, dataCons = cs }
-        | Just (HsData r ty hsCons) <- pragma -> setCurrentRange r $ do
+        | Just hsdata@(HsData r ty hsCons) <- pragma -> setCurrentRange r $ do
+        reportSDoc "compile.ghc.definition" 40 $ hsep $
+          [ "Compiling data type with COMPILE pragma ...", pretty hsdata ]
         computeErasedConstructorArgs q
         ccscov <- constructorCoverageCode q (np + ni) cs ty hsCons
         cds <- mapM compiledcondecl cs
-        return $ tvaldecl q (dataInduction d) (np + ni) [] (Just __IMPOSSIBLE__) ++
-                 [compiledTypeSynonym q ty np] ++ cds ++ ccscov
+        let result = concat $
+              [ tvaldecl q (dataInduction d) (np + ni) [] (Just __IMPOSSIBLE__)
+              , [ compiledTypeSynonym q ty np ]
+              , cds
+              , ccscov
+              ]
+        return result
       Datatype{ dataPars = np, dataIxs = ni, dataClause = cl,
                 dataCons = cs, dataInduction = ind } -> do
         computeErasedConstructorArgs q
diff --git a/src/full/Agda/Compiler/MAlonzo/Pragmas.hs b/src/full/Agda/Compiler/MAlonzo/Pragmas.hs
--- a/src/full/Agda/Compiler/MAlonzo/Pragmas.hs
+++ b/src/full/Agda/Compiler/MAlonzo/Pragmas.hs
@@ -47,6 +47,16 @@
   getRange (HsData   r _ _) = r
   getRange (HsExport r _)   = r
 
+instance Pretty HaskellPragma where
+  pretty = \case
+    HsDefn   _r hsCode        -> equals <+> text hsCode
+    HsType   _r hsType        -> equals <+> text hsType
+    HsData   _r hsType hsCons -> hsep $
+      [ equals, "data", text hsType
+      , parens $ hsep $ map text $ List.intersperse "|" hsCons
+      ]
+    HsExport _r hsCode        -> "as" <+> text hsCode
+
 -- Syntax for Haskell pragmas:
 --  HsDefn CODE       "= CODE"
 --  HsType TYPE       "= type TYPE"
diff --git a/src/full/Agda/Compiler/MAlonzo/Primitives.hs b/src/full/Agda/Compiler/MAlonzo/Primitives.hs
--- a/src/full/Agda/Compiler/MAlonzo/Primitives.hs
+++ b/src/full/Agda/Compiler/MAlonzo/Primitives.hs
@@ -5,7 +5,7 @@
 import Control.Monad.State
 import Data.Char
 import qualified Data.List as List
-import Data.Map as M
+import qualified Data.Map as Map
 import Data.Maybe
 
 import Agda.Compiler.Common
@@ -26,29 +26,46 @@
 import Agda.Utils.Except
 import Agda.Utils.Lens
 import Agda.Utils.Monad
+import Agda.Utils.Pretty (prettyShow)
 import qualified Agda.Utils.HashMap as HMap
 import qualified Agda.Utils.Haskell.Syntax as HS
 
 #include "undefined.h"
 import Agda.Utils.Impossible
 
-isMainFunction :: QName -> Bool
-isMainFunction q = "main" == show (nameConcrete $ qnameName q)
+-- Andreas, 2019-04-29, issue #3731: exclude certain kinds of names, like constructors.
+-- TODO: Also only consider top-level definition (not buried inside a module).
+isMainFunction :: QName -> Defn -> Bool
+isMainFunction q = \case
+    Axiom{}                             -> perhaps
+    Function{ funProjection = Nothing } -> perhaps
+    Function{ funProjection = Just{}  } -> no
+    AbstractDefn{}                      -> no
+    GeneralizableVar{}                  -> no
+    DataOrRecSig{}                      -> no
+    Datatype{}                          -> no
+    Record{}                            -> no
+    Constructor{}                       -> no
+    Primitive{}                         -> no
+  where
+  perhaps = "main" == prettyShow (nameConcrete $ qnameName q)  -- ignores the qualification!?
+  no      = False
 
 hasMainFunction :: Interface -> IsMain
 hasMainFunction i
-  | List.any isMainFunction names = IsMain
-  | otherwise                     = NotMain
+  | List.any (\ (x, def) -> isMainFunction x $ theDef def) names = IsMain
+  | otherwise = NotMain
   where
-    names = HMap.keys $ iSignature i ^. sigDefinitions
+    names = HMap.toList $ iSignature i ^. sigDefinitions
 
 -- | Check that the main function has type IO a, for some a.
-checkTypeOfMain :: QName -> Type -> TCM [HS.Decl] -> TCM [HS.Decl]
-checkTypeOfMain q ty ret
-  | not (isMainFunction q) = ret
+checkTypeOfMain :: IsMain -> QName -> Definition -> TCM [HS.Decl] -> TCM [HS.Decl]
+checkTypeOfMain NotMain q def ret = ret
+checkTypeOfMain  IsMain q def ret
+  | not (isMainFunction q $ theDef def) = ret
   | otherwise = do
     Def io _ <- primIO
-    ty <- normalise ty
+    ty <- normalise $ defType def
     case unEl ty of
       Def d _ | d == io -> (mainAlias :) <$> ret
       _                 -> do
@@ -115,7 +132,7 @@
 xForPrim :: [(String, TCM [a])] -> TCM [a]
 xForPrim table = do
   qs <- HMap.keys <$> curDefs
-  bs <- toList <$> getsTC stBuiltinThings
+  bs <- Map.toList <$> getsTC stBuiltinThings
   let getName (Builtin (Def q _))    = q
       getName (Builtin (Con q _ _))  = conName q
       getName (Builtin (Lam _ b))    = getName (Builtin $ unAbs b)
@@ -162,6 +179,7 @@
   -- Machine word functions
   , "primWord64ToNat"   |-> return "MAlonzo.RTE.word64ToNat"
   , "primWord64FromNat" |-> return "MAlonzo.RTE.word64FromNat"
+  , "primWord64ToNatInjective" |-> return "erased"
 
   -- Floating point functions
   , "primNatToFloat"        |-> return "(fromIntegral :: Integer -> Double)"
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
@@ -551,8 +551,11 @@
   toConcrete (OfType' e t) = OfType' <$> toConcrete e <*> toConcreteCtx TopCtx t
 
 getConstraints :: TCM [OutputForm C.Expr C.Expr]
-getConstraints = liftTCM $ do
-    cs <- M.getAllConstraints
+getConstraints = getConstraints' $ const True
+
+getConstraints' :: (ProblemConstraint -> Bool) -> TCM [OutputForm C.Expr C.Expr]
+getConstraints' f = liftTCM $ do
+    cs <- filter f <$> M.getAllConstraints
     cs <- forM cs $ \c -> do
             cl <- reify c
             enterClosure cl abstractToConcrete_
diff --git a/src/full/Agda/Interaction/Highlighting/Generate.hs b/src/full/Agda/Interaction/Highlighting/Generate.hs
--- a/src/full/Agda/Interaction/Highlighting/Generate.hs
+++ b/src/full/Agda/Interaction/Highlighting/Generate.hs
@@ -665,8 +665,19 @@
     UselessAbstract{}    -> deadcodeHighlighting $ P.getRange w
     UselessInstance{}    -> deadcodeHighlighting $ P.getRange w
     UselessPrivate{}     -> deadcodeHighlighting $ P.getRange w
-    _ -> mempty -- TODO: explore highlighting opportunities here!
-
+    -- TODO: explore highlighting opportunities here!
+    EmptyPrimitive{} -> mempty
+    InvalidCatchallPragma{} -> mempty
+    InvalidNoPositivityCheckPragma{} -> mempty
+    InvalidNoUniverseCheckPragma{} -> mempty
+    InvalidTerminationCheckPragma{} -> mempty
+    MissingDefinitions{} -> mempty
+    PolarityPragmasButNotPostulates{} -> mempty
+    PragmaNoTerminationCheck{} -> mempty
+    PragmaCompiled{} -> mempty
+    UnknownFixityInMixfixDecl{} -> mempty
+    UnknownNamesInFixityDecl{} -> mempty
+    UnknownNamesInPolarityPragmas{} -> mempty
 
 
 -- | Generate syntax highlighting for termination errors.
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
@@ -42,6 +42,7 @@
 import qualified Agda.TypeChecking.Pretty as TCP
 import Agda.TypeChecking.Rules.Term (checkExpr, isType_)
 import Agda.TypeChecking.Errors
+import Agda.TypeChecking.MetaVars.Mention
 
 import Agda.Syntax.Fixity
 import Agda.Syntax.Position
@@ -1485,12 +1486,18 @@
   lift $ do
     goal <- B.withInteractionId ii $ prettyTypeOfMeta norm ii
     ctx  <- prettyContext norm True ii
-    return $ vcat
+    m    <- lookupInteractionId ii
+    constr <- vcat . map pretty <$> B.getConstraints' (mentionsMeta m)
+    let constrDoc = ifNull constr [] $ \constr ->
+          [ text $ delimiter "Constraints"
+          , constr
+          ]
+    return $ vcat $
       [ "Goal:" <+> goal
       , doc
       , text (replicate 60 '\x2014')
       , ctx
-      ]
+      ] ++ constrDoc
 
 -- | Shows all the top-level names in the given module, along with
 -- their types.
diff --git a/src/full/Agda/Interaction/Options/Lenses.hs b/src/full/Agda/Interaction/Options/Lenses.hs
--- a/src/full/Agda/Interaction/Options/Lenses.hs
+++ b/src/full/Agda/Interaction/Options/Lenses.hs
@@ -167,6 +167,7 @@
   , "Agda" </> "Builtin" </> "String" </> "Properties.agda"
   , "Agda" </> "Builtin" </> "Unit.agda"
   , "Agda" </> "Builtin" </> "Word.agda"
+  , "Agda" </> "Builtin" </> "Word" </> "Properties.agda"
   ])
 
 -- | These builtins may not use postulates under --safe. They are not
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
@@ -489,6 +489,10 @@
 namedDBVarP :: Int -> PatVarName -> Named_ DeBruijnPattern
 namedDBVarP m = (fmap . fmap) (\x -> DBPatVar x m) . namedVarP
 
+-- | Make an absurd pattern with the given de Bruijn index.
+absurdP :: Int -> DeBruijnPattern
+absurdP = VarP PatOAbsurd . DBPatVar absurdPatternName
+
 -- | The @ConPatternInfo@ states whether the constructor belongs to
 --   a record type (@Just@) or data type (@Nothing@).
 --   In the former case, the @PatOrigin@ says whether the record pattern
@@ -859,7 +863,7 @@
 telFromList = telFromList' id
 
 -- | Convert a telescope to its list form.
-telToList :: Telescope -> ListTel
+telToList :: Tele (Dom t) -> [Dom (ArgName,t)]
 telToList EmptyTel                    = []
 telToList (ExtendTel arg (Abs x tel)) = fmap (x,) arg : telToList tel
 telToList (ExtendTel _    NoAbs{}   ) = __IMPOSSIBLE__
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
@@ -12,10 +12,6 @@
 import qualified Data.Set as Set
 import qualified Data.IntSet as IntSet
 
-#if __GLASGOW_HASKELL__ <= 708
-import Data.Traversable ( traverse )
-#endif
-
 import Agda.Syntax.Abstract.Views (isSet)
 import Agda.Syntax.Common
 import Agda.Syntax.Internal
@@ -1459,9 +1455,9 @@
 
         hasMeta ClosedLevel{}               = False
         hasMeta (Plus _ MetaLevel{})        = True
-        hasMeta (Plus _ (BlockedLevel _ v)) = not $ null $ allMetas v
-        hasMeta (Plus _ (NeutralLevel _ v)) = not $ null $ allMetas v
-        hasMeta (Plus _ (UnreducedLevel v)) = not $ null $ allMetas v
+        hasMeta (Plus _ (BlockedLevel _ v)) = isJust $ firstMeta v
+        hasMeta (Plus _ (NeutralLevel _ v)) = isJust $ firstMeta v
+        hasMeta (Plus _ (UnreducedLevel v)) = isJust $ firstMeta v
 
         isThisMeta x (Plus _ (MetaLevel y _)) = x == y
         isThisMeta _ _                      = False
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
@@ -55,7 +55,7 @@
 
 import Agda.TypeChecking.Conversion (tryConversion, equalType, equalTermOnFace)
 import Agda.TypeChecking.Datatypes (getConForm)
-import {-# SOURCE #-} Agda.TypeChecking.Empty ( isEmptyTel, isEmptyType )
+import {-# SOURCE #-} Agda.TypeChecking.Empty ( checkEmptyTel, isEmptyTel, isEmptyType )
 import Agda.TypeChecking.Free
 import Agda.TypeChecking.Irrelevance
 import Agda.TypeChecking.Patterns.Internal (dotPatternsToPatterns)
@@ -225,13 +225,21 @@
 
   -- filter out the missing clauses that are absurd.
   pss <- flip filterM pss $ \(tel,ps) ->
-    ifNotM (isEmptyTel tel) (return True) $ do
+    -- Andreas, 2019-04-13, issue #3692: when adding missing absurd
+    -- clauses, also put the absurd pattern in.
+    caseEitherM (checkEmptyTel noRange tel) (\ _ -> return True) $ \ l -> do
+      -- Now, @l@ is the first type in @tel@ (counting from 0=leftmost)
+      -- which is empty.  Turn it into a de Bruijn index @i@.
+      let i = size tel - 1 - l
+      -- Build a substitution mapping this pattern variable to the absurd pattern.
+      let sub = inplaceS i $ absurdP i
+        -- ifNotM (isEmptyTel tel) (return True) $ do
       -- Jesper, 2018-11-28, Issue #3407: if the clause is absurd,
       -- add the appropriate absurd clause to the definition.
       let cl = Clause { clauseLHSRange    = noRange
                       , clauseFullRange   = noRange
                       , clauseTel         = tel
-                      , namedClausePats   = ps
+                      , namedClausePats   = applySubst sub ps
                       , clauseBody        = Nothing
                       , clauseType        = Nothing
                       , clauseCatchall    = False
@@ -241,6 +249,11 @@
         sep [ "adding missing absurd clause"
             , nest 2 $ prettyTCM $ QNamed f cl
             ]
+      reportSDoc "tc.cover.missing" 80 $ inTopContext $ vcat
+        [ "l   = " <+> pretty l
+        , "i   = " <+> pretty i
+        , "cl  = " <+> pretty (QNamed f cl)
+        ]
       addClauses f [cl]
       return False
 
diff --git a/src/full/Agda/TypeChecking/Empty.hs b/src/full/Agda/TypeChecking/Empty.hs
--- a/src/full/Agda/TypeChecking/Empty.hs
+++ b/src/full/Agda/TypeChecking/Empty.hs
@@ -1,9 +1,5 @@
 
-module Agda.TypeChecking.Empty
-       ( isEmptyType
-       , isEmptyTel
-       , ensureEmptyType
-       ) where
+module Agda.TypeChecking.Empty where
 
 import Control.Monad.Except
 
@@ -94,11 +90,15 @@
     -- If t is a record type, see if any of the field types is empty
     Right (r, pars, def) -> do
       if recEtaEquality def == NoEta then return $ Left Fail else do
-        checkEmptyTel range $ recTel def `apply` pars
+        void <$> do checkEmptyTel range $ recTel def `apply` pars
 
-checkEmptyTel :: Range -> Telescope -> TCM (Either ErrorNonEmpty ())
-checkEmptyTel r EmptyTel            = return $ Left Fail
-checkEmptyTel r (ExtendTel dom tel) = orEitherM
-  [ checkEmptyType r (unDom dom)
-  , underAbstraction dom tel (checkEmptyTel r)
-  ]
+-- | Check whether one of the types in the given telescope is constructor-less
+--   and if yes, return its index in the telescope (0 = leftmost).
+checkEmptyTel :: Range -> Telescope -> TCM (Either ErrorNonEmpty Int)
+checkEmptyTel r = loop 0
+  where
+  loop i EmptyTel            = return $ Left Fail
+  loop i (ExtendTel dom tel) = orEitherM
+    [ (i <$) <$> checkEmptyType r (unDom dom)
+    , underAbstraction dom tel $ loop (succ i)
+    ]
diff --git a/src/full/Agda/TypeChecking/Empty.hs-boot b/src/full/Agda/TypeChecking/Empty.hs-boot
--- a/src/full/Agda/TypeChecking/Empty.hs-boot
+++ b/src/full/Agda/TypeChecking/Empty.hs-boot
@@ -5,7 +5,10 @@
 import Agda.Syntax.Internal (Type, Telescope)
 import Agda.Syntax.Position (Range)
 
+data ErrorNonEmpty
+
 isEmptyType :: Type      -> TCM Bool
 isEmptyTel  :: Telescope -> TCM Bool
 
 ensureEmptyType :: Range -> Type -> TCM ()
+checkEmptyTel   :: Range -> Telescope -> TCM (Either ErrorNonEmpty Int)
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
@@ -452,7 +452,6 @@
   ShouldEndInApplicationOfTheDatatype{}    -> "ShouldEndInApplicationOfTheDatatype"
   SplitError{}                             -> "SplitError"
   ImpossibleConstructor{}                  -> "ImpossibleConstructor"
-  TooFewFields{}                           -> "TooFewFields"
   TooManyFields{}                          -> "TooManyFields"
   TooManyPolarities{}                      -> "TooManyPolarities"
   SplitOnIrrelevant{}                      -> "SplitOnIrrelevant"
@@ -797,13 +796,11 @@
     NotLeqSort s1 s2 -> fsep $
       [prettyTCM s1] ++ pwords "is not less or equal than" ++ [prettyTCM s2]
 
-    TooFewFields r xs -> fsep $
-      pwords "Missing fields" ++ punctuate comma (map pretty xs) ++
-      pwords "in an element of the record" ++ [prettyTCM r]
-
-    TooManyFields r xs -> fsep $
+    TooManyFields r missing xs -> fsep $
       pwords "The record type" ++ [prettyTCM r] ++
-      pwords "does not have the fields" ++ punctuate comma (map pretty xs)
+      pwords "does not have the fields" ++ punctuate comma (map pretty xs) ++
+      if null missing then [] else
+        pwords "but it would have the fields"  ++ punctuate comma (map pretty missing)
 
     DuplicateConstructors xs -> fsep $
       pwords "Duplicate constructors" ++ punctuate comma (map pretty xs) ++
diff --git a/src/full/Agda/TypeChecking/Generalize.hs b/src/full/Agda/TypeChecking/Generalize.hs
--- a/src/full/Agda/TypeChecking/Generalize.hs
+++ b/src/full/Agda/TypeChecking/Generalize.hs
@@ -14,6 +14,7 @@
 import Data.Map (Map)
 import qualified Data.Map as Map
 import Data.List (nub, partition, init, sortBy)
+import Data.Monoid
 import Data.Function (on)
 import Data.Traversable
 
@@ -48,6 +49,7 @@
 import Agda.Utils.Maybe
 import Agda.Utils.Monad
 import Agda.Utils.Size
+import Agda.Utils.Singleton
 import Agda.Utils.Permutation
 import qualified Agda.Utils.Graph.TopSort as Graph
 
@@ -212,7 +214,7 @@
     case mvInstantiation mv of
       InstV _ v -> do
         parentName <- getMetaNameSuggestion x
-        metas <- filterM canGeneralize . allMetas =<< instantiateFull v
+        metas <- filterM canGeneralize . allMetasList =<< instantiateFull v
         let suggestNames i [] = return ()
             suggestNames i (m : ms)  = do
               name <- getMetaNameSuggestion m
@@ -546,7 +548,7 @@
                    _ -> err
           telList = telToList genTel
           names   = map (fst . unDom) telList
-          late    = map (fst . unDom) $ filter (elem x . allMetas) telList
+          late    = map (fst . unDom) $ filter (getAny . allMetas (Any . (== x))) telList
           projs (Proj _ q)
             | elem q genRecFields = Set.fromList [x | Just x <- [getGeneralizedFieldName q]]
           projs _                 = Set.empty
@@ -691,9 +693,10 @@
 -- | Sort metas in dependency order.
 sortMetas :: [MetaId] -> TCM [MetaId]
 sortMetas metas = do
-  metaGraph <- fmap concat $ forM metas $ \ m -> do
-                  deps <- nub . filter (`elem` metas) . allMetas <$> getType m
-                  return [ (m, m') | m' <- deps ]
+  metaGraph <- concat <$> do
+    forM metas $ \ m -> do
+      deps <- allMetas (\ m' -> if m' `elem` metas then singleton m' else mempty) <$> getType m
+      return [ (m, m') | m' <- Set.toList deps ]
 
   caseMaybe (Graph.topSort metas metaGraph)
             (typeError GeneralizeCyclicDependency)
@@ -804,4 +807,3 @@
     r { theDef = (theDef r) { recTel = fullTel } }
   where
     setType q ty = modifyGlobalDefinition q $ \ d -> d { defType = ty }
-
diff --git a/src/full/Agda/TypeChecking/IApplyConfluence.hs b/src/full/Agda/TypeChecking/IApplyConfluence.hs
--- a/src/full/Agda/TypeChecking/IApplyConfluence.hs
+++ b/src/full/Agda/TypeChecking/IApplyConfluence.hs
@@ -30,30 +30,13 @@
 import Agda.TypeChecking.Primitive.Cubical
 import Agda.TypeChecking.Monad
 import Agda.TypeChecking.Monad.Builtin
-
--- import Agda.TypeChecking.Rules.LHS (checkSortOfSplitVar)
--- import Agda.TypeChecking.Rules.LHS.Problem (allFlexVars)
--- import Agda.TypeChecking.Rules.LHS.Unify
-
--- import Agda.TypeChecking.Coverage.Match
--- import Agda.TypeChecking.Coverage.SplitTree
-
 import Agda.TypeChecking.Conversion (tryConversion, equalType, equalTermOnFace)
--- import Agda.TypeChecking.Datatypes (getConForm)
--- import {-# SOURCE #-} Agda.TypeChecking.Empty (isEmptyTel)
--- import Agda.TypeChecking.Free
--- import Agda.TypeChecking.Irrelevance
--- import Agda.TypeChecking.Patterns.Internal (dotPatternsToPatterns)
 import Agda.TypeChecking.Pretty
 import Agda.TypeChecking.Substitute
 import Agda.TypeChecking.Reduce
 import Agda.TypeChecking.Records
 import Agda.TypeChecking.Telescope
 import Agda.TypeChecking.Telescope.Path
--- import Agda.TypeChecking.MetaVars
--- import Agda.TypeChecking.Warnings
-
--- import Agda.Interaction.Options
 
 import Agda.Utils.Either
 import Agda.Utils.Except
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
@@ -20,6 +20,7 @@
 import qualified Data.Set as Set
 import qualified Data.List as List
 import Data.Function (on)
+import Data.Monoid hiding ((<>))
 
 import Agda.Interaction.Options (optOverlappingInstances)
 
@@ -342,7 +343,7 @@
 dropSameCandidates m cands0 = verboseBracket "tc.instance" 30 "dropSameCandidates" $ do
   metas <- getMetaVariableSet
   -- Does `it` have any metas in the initial meta variable store?
-  let freshMetas = any ((`IntSet.notMember` metas) . metaId) . allMetas
+  let freshMetas = getAny . allMetas (Any . (`IntSet.notMember` metas) . metaId)
 
   -- Take overlappable candidates into account
   let cands =
diff --git a/src/full/Agda/TypeChecking/MetaVars/Occurs.hs b/src/full/Agda/TypeChecking/MetaVars/Occurs.hs
--- a/src/full/Agda/TypeChecking/MetaVars/Occurs.hs
+++ b/src/full/Agda/TypeChecking/MetaVars/Occurs.hs
@@ -366,8 +366,15 @@
   metaOccurs m d = whenM (defNeedsChecking d) $ do
     tallyDef d
     reportSLn "tc.meta.occurs" 30 $ "Checking for occurrences in " ++ show d
-    metaOccurs m . theDef =<< ignoreAbstractMode (getConstInfo d)
+    metaOccursQName m d
 
+metaOccursQName :: MetaId -> QName -> TCM ()
+metaOccursQName m x = metaOccurs m . theDef =<< do
+  ignoreAbstractMode $ getConstInfo x
+  -- Andreas, 2019-05-03, issue #3742:
+  -- ignoreAbstractMode necessary, as abstract
+  -- constructors are also called up.
+
 instance Occurs Defn where
   occurs red ctx m xs def = __IMPOSSIBLE__
 
@@ -376,9 +383,8 @@
   metaOccurs m Function{ funClauses = cls } = metaOccurs m cls
   -- since a datatype is isomorphic to the sum of its constructor types
   -- we check the constructor types
-  metaOccurs m Datatype{ dataCons = cs }    = mapM_ mocc cs
-    where mocc c = metaOccurs m . defType =<< getConstInfo c
-  metaOccurs m Record{ recConHead = c }     = metaOccurs m . defType =<< getConstInfo (conName c)
+  metaOccurs m Datatype{ dataCons = cs }    = mapM_ (metaOccursQName m) cs
+  metaOccurs m Record{ recConHead = c }     = metaOccursQName m $ conName c
   metaOccurs m Constructor{}                = return ()
   metaOccurs m Primitive{}                  = return ()
   metaOccurs m AbstractDefn{}               = __IMPOSSIBLE__
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
@@ -3046,8 +3046,8 @@
         | BuiltinInParameterisedModule String
         | IllegalLetInTelescope C.TypedBinding
         | NoRHSRequiresAbsurdPattern [NamedArg A.Pattern]
-        | TooFewFields QName [C.Name]
-        | TooManyFields QName [C.Name]
+        | TooManyFields QName [C.Name] [C.Name]
+          -- ^ Record type, fields not supplied by user, non-fields not supplied.
         | DuplicateFields [C.Name]
         | DuplicateConstructors [C.Name]
         | WithOnFreeVariable A.Expr Term
@@ -3612,7 +3612,7 @@
     return = pure
     (>>=)  = bindTCMT
     (>>)   = (*>)
-#if __GLASGOW_HASKELL__ == 710
+#if __GLASGOW_HASKELL__ < 800
     fail   = internalError
 #else
     fail   = Fail.fail
diff --git a/src/full/Agda/TypeChecking/Monad/Builtin.hs b/src/full/Agda/TypeChecking/Monad/Builtin.hs
--- a/src/full/Agda/TypeChecking/Monad/Builtin.hs
+++ b/src/full/Agda/TypeChecking/Monad/Builtin.hs
@@ -35,7 +35,7 @@
 
 class ( Functor m
       , Applicative m
-#if __GLASGOW_HASKELL__ == 710
+#if __GLASGOW_HASKELL__ < 800
       , Monad m
 #else
       , Fail.MonadFail m
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
@@ -19,6 +19,7 @@
 import Data.Set (Set)
 import qualified Data.Set as Set
 import qualified Data.Foldable as Fold
+import Data.Monoid
 
 import Agda.Syntax.Common
 import Agda.Syntax.Internal
@@ -43,6 +44,7 @@
 import Agda.Utils.Permutation
 import Agda.Utils.Pretty (prettyShow)
 import Agda.Utils.Tuple
+import Agda.Utils.Singleton
 import Agda.Utils.Size
 import qualified Agda.Utils.Maybe.Strict as Strict
 
@@ -172,33 +174,67 @@
 
 -- | Returns every meta-variable occurrence in the given type, except
 -- for those in 'Sort's.
-allMetas :: TermLike a => a -> [MetaId]
-allMetas = foldTerm metas
+allMetas :: (TermLike a, Monoid m) => (MetaId -> m) -> a -> m
+allMetas singl = foldTerm metas
   where
-  metas (MetaV m _) = [m]
+  metas (MetaV m _) = singl m
   metas (Level l)   = levelMetas l
-  metas _           = []
+  metas _           = mempty
 
-  levelMetas (Max as) = concatMap plusLevelMetas as
+  levelMetas (Max as) = foldMap plusLevelMetas as
 
-  plusLevelMetas ClosedLevel{} = []
+  plusLevelMetas ClosedLevel{} = mempty
   plusLevelMetas (Plus _ l)    = levelAtomMetas l
 
-  levelAtomMetas (MetaLevel m _) = [m]
-  levelAtomMetas _               = []
+  levelAtomMetas (MetaLevel m _) = singl m
+  levelAtomMetas _               = mempty
 
+-- | Returns 'allMetas' in a list.
+--   @allMetasList = allMetas (:[])@.
+--
+--   Note: this resulting list is computed via difference lists.
+--   Thus, use this function if you actually need the whole list of metas.
+--   Otherwise, use 'allMetas' with a suitable monoid.
+allMetasList :: TermLike a => a -> [MetaId]
+allMetasList t = allMetas singleton t `appEndo` []
+
+-- | 'True' if thing contains no metas.
+--   @noMetas = null . allMetasList@.
+noMetas :: TermLike a => a -> Bool
+noMetas = getAll . allMetas (\ _m -> All False)
+
+-- | Returns the first meta it find in the thing, if any.
+--   @firstMeta == headMaybe . allMetasList@.
+firstMeta :: TermLike a => a -> Maybe MetaId
+firstMeta = getFirst . allMetas (First . Just)
+
 -- | Returns all metavariables in a constraint. Slightly complicated by the
 --   fact that blocked terms are represented by two meta variables. To find the
 --   second one we need to look up the meta listeners for the one in the
 --   UnBlock constraint.
 constraintMetas :: Constraint -> TCM (Set MetaId)
-constraintMetas c = Set.union (Set.fromList $ allMetas c) <$> metas c
+constraintMetas c = metas c
   where
-    -- Dig out constraint-specific meta vars
-    metas (UnBlock x)                    = Set.insert x . Set.unions <$> (mapM listenerMetas =<< getMetaListeners x)
-    metas (Guarded c _)                  = metas c
-    metas (UnquoteTactic (Just x) _ _ _) = return $ Set.singleton x
-    metas _                              = return Set.empty
+    -- We don't use allMetas here since some constraints should not stop us from generalizing. For
+    -- instance CheckSizeLtSat (see #3694). We also have to check meta listeners to get metas of
+    -- UnBlock constraints.
+    metas c = case c of
+      ValueCmp _ t u v         -> return $ allMetas Set.singleton (t, u, v)
+      ValueCmpOnFace _ p t u v -> return $ allMetas Set.singleton (p, t, u, v)
+      ElimCmp _ _ t u es es'   -> return $ allMetas Set.singleton (t, u, es, es')
+      TypeCmp _ t t'           -> return $ allMetas Set.singleton (t, t')
+      LevelCmp _ l l'          -> return $ allMetas Set.singleton (l, l')
+      UnquoteTactic m t h g    -> return $ Set.fromList [x | Just x <- [m]] `Set.union` allMetas Set.singleton (t, h, g)
+      Guarded c _              -> metas c
+      TelCmp _ _ _ tel1 tel2   -> return $ allMetas Set.singleton (tel1, tel2)
+      SortCmp _ s1 s2          -> return $ allMetas Set.singleton (s1, s2)
+      UnBlock x                -> Set.insert x . Set.unions <$> (mapM listenerMetas =<< getMetaListeners x)
+      FindInstance{}           -> return mempty  -- v Ignore these constraints
+      IsEmpty{}                -> return mempty
+      CheckFunDef{}            -> return mempty
+      CheckSizeLtSat{}         -> return mempty
+      HasBiggerSort{}          -> return mempty
+      HasPTSRule{}             -> return mempty
 
     -- For blocked constant twin variables
     listenerMetas EtaExpand{}           = return Set.empty
diff --git a/src/full/Agda/TypeChecking/Monad/Signature.hs b/src/full/Agda/TypeChecking/Monad/Signature.hs
--- a/src/full/Agda/TypeChecking/Monad/Signature.hs
+++ b/src/full/Agda/TypeChecking/Monad/Signature.hs
@@ -636,7 +636,7 @@
 
 class ( Functor m
       , Applicative m
-#if __GLASGOW_HASKELL__ == 710
+#if __GLASGOW_HASKELL__ < 800
       , Monad m
 #else
       , Fail.MonadFail m
diff --git a/src/full/Agda/TypeChecking/Monad/Signature.hs-boot b/src/full/Agda/TypeChecking/Monad/Signature.hs-boot
--- a/src/full/Agda/TypeChecking/Monad/Signature.hs-boot
+++ b/src/full/Agda/TypeChecking/Monad/Signature.hs-boot
@@ -23,7 +23,7 @@
 
 class ( Functor m
       , Applicative m
-#if __GLASGOW_HASKELL__ == 710
+#if __GLASGOW_HASKELL__ < 800
       , Monad m
 #else
       , Fail.MonadFail m
diff --git a/src/full/Agda/TypeChecking/Names.hs b/src/full/Agda/TypeChecking/Names.hs
--- a/src/full/Agda/TypeChecking/Names.hs
+++ b/src/full/Agda/TypeChecking/Names.hs
@@ -130,12 +130,7 @@
 cl :: Monad m => m a -> NamesT m a
 cl = lift
 
-open :: ( Monad m
-#if __GLASGOW_HASKELL__ <= 708
-        , Applicative m
-#endif
-        , Subst t a
-        ) => a -> NamesT m (NamesT m a)
+open :: (Monad m, Subst t a) => a -> NamesT m (NamesT m a)
 open a = do
   ctx <- NamesT ask
   pure $ inCxt ctx a
@@ -146,9 +141,6 @@
   (NamesT . local (n:) . unName $ f (inCxt (n:cxt) (deBruijnVar 0)))
 
 bind :: ( Monad m
-#if __GLASGOW_HASKELL__ <= 708
-        , Functor m
-#endif
         , Subst t' b
         , DeBruijn b
         , Subst t a
@@ -157,11 +149,7 @@
         ArgName -> (NamesT m b -> NamesT m a) -> NamesT m (Abs a)
 bind n f = Abs n <$> bind' n f
 
-#if __GLASGOW_HASKELL__ <= 708
-glam :: (Functor m, Monad m)
-#else
 glam :: Monad m
-#endif
      => ArgInfo -> ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
 glam info n f = Lam info <$> bind n f
 
@@ -170,18 +158,10 @@
 glamN [] f = f $ pure []
 glamN (Arg i n:ns) f = glam i n $ \ x -> glamN ns (\ xs -> f ((:) <$> (Arg i <$> x) <*> xs))
 
-#if __GLASGOW_HASKELL__ <= 708
-lam :: (Functor m, Monad m)
-#else
 lam :: Monad m
-#endif
     => ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
 lam n f = glam defaultArgInfo n f
 
-#if __GLASGOW_HASKELL__ <= 708
-ilam :: (Functor m, Monad m)
-#else
 ilam :: Monad m
-#endif
     => ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
 ilam n f = glam (setRelevance Irrelevant defaultArgInfo) n f
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
@@ -28,6 +28,7 @@
 import Data.Set (Set)
 import qualified Data.Set as Set
 import Data.Maybe
+import Data.Monoid
 import Data.Traversable (traverse)
 import Data.Monoid (mempty)
 import Data.Word
@@ -59,15 +60,16 @@
 import Agda.TypeChecking.Names
 import Agda.TypeChecking.Warnings
 
+import Agda.Utils.Float
 import Agda.Utils.Functor
 import Agda.Utils.List
 import Agda.Utils.Maybe
 import Agda.Utils.Monad
 import Agda.Utils.Pretty (pretty, prettyShow)
+import Agda.Utils.Singleton
 import Agda.Utils.Size
 import Agda.Utils.String ( Str(Str), unStr )
 import Agda.Utils.Tuple
-import Agda.Utils.Float
 
 #include "undefined.h"
 import Agda.Utils.Impossible
@@ -1583,6 +1585,13 @@
   toList <- primFunName <$> getPrimitive "primStringToList"
   mkPrimInjective string chars toList
 
+primWord64ToNatInjective :: TCM PrimitiveImpl
+primWord64ToNatInjective =  do
+  word  <- primType (undefined :: Word64)
+  nat   <- primType (undefined :: Nat)
+  toNat <- primFunName <$> getPrimitive "primWord64ToNat"
+  mkPrimInjective word nat toNat
+
 getRefl :: TCM (Arg Term -> Term)
 getRefl = do
   -- BUILTIN REFL maybe a constructor with one (the principal) argument or only parameters.
@@ -1750,11 +1759,11 @@
     return $ PrimImpl t $ primFun __IMPOSSIBLE__ 1 $ \ts ->
       case ts of
         [v] ->
-          redBind (toA v) (\v' -> [v']) $ \x -> do
+          redBind (toA v) singleton $ \ x -> do
             b <- f x
-            case allMetas b of
-              (m:_) -> return $ NoReduction [reduced (Blocked m v)]
-              []       -> redReturn =<< fromB b
+            case firstMeta b of
+              Just m  -> return $ NoReduction [reduced (Blocked m v)]
+              Nothing -> redReturn =<< fromB b
         _ -> __IMPOSSIBLE__
 
 -- Tying the knot
@@ -1767,8 +1776,7 @@
     return $ PrimImpl t $ primFun __IMPOSSIBLE__ 1 $ \ts ->
       case ts of
         [v] ->
-          redBind (toA v)
-              (\v' -> [v']) $ \x ->
+          redBind (toA v) singleton $ \ x ->
           redReturn $ fromB $ f x
         _ -> __IMPOSSIBLE__
 
@@ -1874,12 +1882,7 @@
    toFinitePi (El s (Pi d b)) = El s $ Pi (setRelevance Irrelevant $ d { domFinite = True }) b
    toFinitePi _               = __IMPOSSIBLE__
 
-#if __GLASGOW_HASKELL__ <= 708
-el' :: (Functor m, Applicative m, Monad m)
-#else
-el' :: Monad m
-#endif
-    => m Term -> m Term -> m Type
+el' :: Monad m => m Term -> m Term -> m Type
 el' l a = El <$> (tmSort <$> l) <*> a
 
 elInf :: Functor m => m Term -> m Type
@@ -2004,6 +2007,7 @@
   -- Machine words
   , "primWord64ToNat"     |-> mkPrimFun1 (fromIntegral :: Word64 -> Nat)
   , "primWord64FromNat"   |-> mkPrimFun1 (fromIntegral :: Nat -> Word64)
+  , "primWord64ToNatInjective" |-> primWord64ToNatInjective
 
   -- Level functions
   , "primLevelZero"       |-> mkPrimLevelZero
diff --git a/src/full/Agda/TypeChecking/Records.hs b/src/full/Agda/TypeChecking/Records.hs
--- a/src/full/Agda/TypeChecking/Records.hs
+++ b/src/full/Agda/TypeChecking/Records.hs
@@ -52,64 +52,62 @@
 mkCon h info args = Con h info (map Apply args)
 
 -- | Order the fields of a record construction.
---   Use the second argument for missing fields.
-orderFields :: QName -> a -> [C.Name] -> [(C.Name, a)] -> TCM [a]
-orderFields r def xs fs = do
-  unlessNull (ys List.\\ List.nub ys) $ typeError . DuplicateFields . List.nub
-  unlessNull (ys List.\\ xs)          $ typeError . TooManyFields r
-  -- shouldBeNull (xs List.\\ ys)     $ TooFewFields r
-  return $ order xs fs
+orderFields
+  :: forall a
+  .  QName             -- ^ Name of record type (for error message).
+  -> (Arg C.Name -> a) -- ^ How to fill a missing field.
+  -> [Arg C.Name]      -- ^ Field names of the record type.
+  -> [(C.Name, a)]     -- ^ Provided fields with content in the record expression.
+  -> TCM [a]           -- ^ Content arranged in official order.
+orderFields r fill axs fs = do
+  reportSDoc "tc.record" 30 $ vcat
+    [ "orderFields"
+    , "  official fields: " <+> sep (map pretty xs)
+    , "  provided fields: " <+> sep (map pretty ys)
+    ]
+  unlessNull duplicate $ typeError . DuplicateFields . List.nub
+  unlessNull alien     $ typeError . TooManyFields r missing
+  return $ for axs $ \ ax -> fromMaybe (fill ax) $ lookup (unArg ax) fs
   where
-    ys = map fst fs
-
-    -- invariant: the first list contains at least the fields of the second list
-    order [] [] = []
-    order [] _  = __IMPOSSIBLE__
-    order (x : xs) ys = case lookup x (assocHoles ys) of
-      Just (e, ys') -> e : order xs ys'
-      Nothing       -> def : order xs ys
-
-    assocHoles xs = [ (x, (v, xs')) | ((x, v), xs') <- holes xs ]
+    xs        = map unArg axs           -- official  fields (accord. record type)
+    ys        = map fst fs              -- provided  fields
+    duplicate = ys List.\\ List.nub ys  -- duplicate fields
+    alien     = ys List.\\ xs           -- spurious  fields
+    missing   = xs List.\\ ys           -- missing   fields
 
 -- | A record field assignment @record{xs = es}@ might not mention all
 --   visible fields.  @insertMissingFields@ inserts placeholders for
 --   the missing visible fields and returns the values in order
 --   of the fields in the record declaration.
 insertMissingFields
-  :: QName                -- ^ Name of record type (for error reporting).
+  :: forall a
+  .  QName                -- ^ Name of record type (for error reporting).
   -> (C.Name -> a)        -- ^ Function to generate a placeholder for missing visible field.
   -> [FieldAssignment' a] -- ^ Given fields.
   -> [Arg C.Name]         -- ^ All record field names with 'ArgInfo'.
   -> TCM [NamedArg a]     -- ^ Given fields enriched by placeholders for missing explicit fields.
 insertMissingFields r placeholder fs axs = do
   -- Compute the list of given fields, decorated with the ArgInfo from the record def.
-  let arg x e =
-        case [ a | a <- axs, unArg a == x ] of
-          [a] -> nameIfHidden a e <$ a
-          _   -> defaultNamedArg e -- we only end up here if the field names are bad
+  let arg x e = caseMaybe (List.find ((x ==) . unArg) axs) (defaultNamedArg e) $ \ a ->
+        nameIfHidden a e <$ a
       givenFields = [ (x, Just $ arg x e) | FieldAssignment x e <- fs ]
-  -- Compute a list of p[aceholders for the missing visible fields.
-  let missingExplicits =
-       [ (x, Just $ setOrigin Inserted $ nameIfHidden a . placeholder <$> a)
-       | a <- filter visible axs
-       , let x = unArg a
-       , x `notElem` map (view nameFieldA) fs
-       ]
-  -- In es omitted explicit fields are replaced by placeholders
-  -- (from missingExplicits). Omitted implicit or instance fields
+
+  -- Omitted explicit fields are filled in with placeholders.
+  -- Omitted implicit or instance fields
   -- are still left out and inserted later by checkArguments_.
-  catMaybes <$> do
-    -- Default value @Nothing@ will only be used for missing hidden fields.
-    -- These can be ignored as they will be inserted by @checkArguments_@.
-    orderFields r Nothing (map unArg axs) $ givenFields ++ missingExplicits
+  catMaybes <$> orderFields r fill axs givenFields
   where
+    fill :: Arg C.Name -> Maybe (NamedArg a)
+    fill ax
+      | visible ax = Just $ setOrigin Inserted $ unnamed . placeholder <$> ax
+      | otherwise  = Nothing
     -- Andreas, 2017-04-13, issue #2494
     -- We need to put the field names as argument names for hidden arguments.
     -- Otherwise, insertImplicit does not do the right thing.
     nameIfHidden :: Arg C.Name -> c -> Named_ c
     nameIfHidden ax
       | visible ax = unnamed
-      | otherwise  = named (Ranged (getRange ax) $ prettyShow $ unArg ax)
+      | otherwise  = named $ Ranged (getRange ax) $ prettyShow $ unArg ax
 
 -- | The name of the module corresponding to a record.
 recordModule :: QName -> ModuleName
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
@@ -11,6 +11,7 @@
 import Data.List ((\\))
 import Data.Maybe
 import Data.Map (Map)
+import Data.Monoid
 import Data.Traversable
 import Data.Hashable
 
@@ -80,7 +81,7 @@
 isFullyInstantiatedMeta m = do
   mv <- TCM.lookupMeta m
   case mvInstantiation mv of
-    InstV _tel v -> null . allMetas <$> instantiateFull v
+    InstV _tel v -> noMetas <$> instantiateFull v
     _ -> return False
 
 -- | Instantiate something.
diff --git a/src/full/Agda/TypeChecking/Rewriting.hs b/src/full/Agda/TypeChecking/Rewriting.hs
--- a/src/full/Agda/TypeChecking/Rewriting.hs
+++ b/src/full/Agda/TypeChecking/Rewriting.hs
@@ -207,8 +207,8 @@
       gamma1 <- instantiateFull gamma1
       let gamma = gamma0 `abstract` gamma1
 
-      unless (null $ allMetas (telToList gamma1)) $ do
-        reportSDoc "rewriting" 30 $ "metas in gamma1: " <+> text (show $ allMetas $ telToList gamma1)
+      unless (noMetas (telToList gamma1)) $ do
+        reportSDoc "rewriting" 30 $ "metas in gamma1: " <+> text (show $ allMetasList $ telToList gamma1)
         failureMetas
 
       -- 2017-06-18, Jesper: Unfold inlined definitions on the LHS.
@@ -236,10 +236,10 @@
 
         checkNoLhsReduction f es
 
-        unless (null $ allMetas (es, rhs, b)) $ do
-          reportSDoc "rewriting" 30 $ "metas in lhs: " <+> text (show $ allMetas es)
-          reportSDoc "rewriting" 30 $ "metas in rhs: " <+> text (show $ allMetas rhs)
-          reportSDoc "rewriting" 30 $ "metas in b  : " <+> text (show $ allMetas b)
+        unless (noMetas (es, rhs, b)) $ do
+          reportSDoc "rewriting" 30 $ "metas in lhs: " <+> text (show $ allMetasList es)
+          reportSDoc "rewriting" 30 $ "metas in rhs: " <+> text (show $ allMetasList rhs)
+          reportSDoc "rewriting" 30 $ "metas in b  : " <+> text (show $ allMetasList b)
           failureMetas
 
         ps <- patternFrom Relevant 0 (t , Def f []) es
diff --git a/src/full/Agda/TypeChecking/Rewriting/NonLinMatch.hs b/src/full/Agda/TypeChecking/Rewriting/NonLinMatch.hs
--- a/src/full/Agda/TypeChecking/Rewriting/NonLinMatch.hs
+++ b/src/full/Agda/TypeChecking/Rewriting/NonLinMatch.hs
@@ -31,6 +31,7 @@
 import System.IO.Unsafe
 
 import Data.Maybe
+import Data.Monoid
 import Data.Traversable (Traversable,traverse)
 import Data.IntMap (IntMap)
 import qualified Data.IntMap as IntMap
@@ -528,10 +529,9 @@
 equal u v = do
   (u, v) <- etaContract =<< normalise (u, v)
   let ok    = u == v
-      metas = allMetas (u, v)
-      block = caseMaybe (headMaybe metas)
+      block = caseMaybe (firstMeta (u, v))
                 (NotBlocked ReallyNotBlocked ())
-                (\m -> Blocked m ())
+                (\ m -> Blocked m ())
   if ok then return Nothing else do
     traceSDoc "rewriting.match" 10 (sep
       [ "mismatch between " <+> prettyTCM u
diff --git a/src/full/Agda/TypeChecking/Rules/Data.hs b/src/full/Agda/TypeChecking/Rules/Data.hs
--- a/src/full/Agda/TypeChecking/Rules/Data.hs
+++ b/src/full/Agda/TypeChecking/Rules/Data.hs
@@ -1,5 +1,6 @@
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE MultiWayIf #-}
+{-# LANGUAGE NondecreasingIndentation #-}
 
 module Agda.TypeChecking.Rules.Data where
 
@@ -7,6 +8,8 @@
 
 import Data.List (genericTake)
 import Data.Maybe (fromMaybe, catMaybes, isJust)
+import Control.Monad.Trans.Maybe
+import Control.Monad.Trans
 import Data.Set (Set)
 import qualified Data.Set as Set
 
@@ -341,10 +344,9 @@
     , builtinPOr
     , builtinItIsOne
     ]
-  sortsOk <- sortOk t `and2M` allM (map unDom (flattenTel fsT)) sortOkField
-  if not sortsOk || not (all isJust required) then return $ emptyCompKit else do
+  if not (all isJust required) then return $ emptyCompKit else do
     hcomp  <- whenDefined (null boundary) [builtinHComp,builtinTrans] (defineTranspOrHCompD DoHComp  d con params names fsT t boundary)
-    transp <- whenDefined True [builtinTrans]              (defineTranspOrHCompD DoTransp d con params names fsT t boundary)
+    transp <- whenDefined True            [builtinTrans]              (defineTranspOrHCompD DoTransp d con params names fsT t boundary)
     return $ CompKit
       { nameOfTransp = transp
       , nameOfHComp  = hcomp
@@ -355,10 +357,12 @@
     withArgInfo tel = zipWith Arg (map domInfo . telToList $ tel)
     defineTranspOrHCompD cmd d con params names fsT t boundary
       = do
-      ((theName, gamma , ty, _cl_types , bodies), theSub) <-
-        (case cmd of DoTransp -> defineTranspForFields' (guard (not $ null boundary) >> (Just $ Con con ConOSystem $ teleElims fsT boundary))
-                     ; DoHComp -> defineHCompForFields)
-          (\ t p -> apply (Def p []) [argN t]) d params fsT (map argN names) t
+      let project = (\ t p -> apply (Def p []) [argN t])
+      stuff <- defineTranspOrHCompForFields cmd
+                 (guard (not $ null boundary) >> (Just $ Con con ConOSystem $ teleElims fsT boundary))
+                 project d params fsT (map argN names) t
+      caseMaybe stuff (return Nothing) $ \ ((theName, gamma , ty, _cl_types , bodies), theSub) -> do
+
       iz <- primIZero
       body <- do
         case cmd of
@@ -538,18 +542,6 @@
       xs <- mapM getTerm' xs
       if all isJust xs then m else return Nothing
 
-    sortOk :: Type -> TCM Bool
-    sortOk a = reduce (getSort a) >>= \case
-      Type{} -> return True
-      _      -> return False
-
-    sortOkField :: Type -> TCM Bool
-    sortOkField a = reduce (getSort a) >>= \case
-      Type{} -> return True
-      -- fields might be elements of the interval
-      Inf    -> return True
-      _      -> return False
-
 -- Andrea: TODO handle Irrelevant fields somehow.
 defineProjections :: QName      -- datatype name
                   -> ConHead
@@ -607,29 +599,88 @@
 freshAbstractQName'_ s = freshAbstractQName noFixity' (C.Name noRange C.InScope [C.Id $ s])
 
 
-defineTranspForFields
-  :: (Term -> QName -> Term) -- ^ how to apply a "projection" to a term
+-- * Special cases of Type
+-----------------------------------------------------------
+
+-- | A @Type@ with sort @Type l@
+--   Such a type supports both hcomp and transp.
+data LType = LEl Level Term deriving (Eq,Show)
+
+fromLType :: LType -> Type
+fromLType (LEl l t) = El (Type l) t
+
+lTypeLevel :: LType -> Level
+lTypeLevel (LEl l t) = l
+
+toLType :: MonadReduce m => Type -> m (Maybe LType)
+toLType ty = do
+  sort <- reduce $ getSort ty
+  case sort of
+    Type l -> return $ Just $ LEl l (unEl ty)
+    _      -> return $ Nothing
+
+instance Subst Term LType where
+  applySubst rho (LEl l t) = LEl (applySubst rho l) (applySubst rho t)
+
+-- | A @Type@ that either has sort @Type l@ or is a closed definition.
+--   Such a type supports some version of transp.
+--   In particular we want to allow the Interval as a @ClosedType@.
+data CType = ClosedType QName | LType LType deriving (Eq,Show)
+
+fromCType :: CType -> Type
+fromCType (ClosedType q) = El Inf (Def q [])
+fromCType (LType t) = fromLType t
+
+toCType :: MonadReduce m => Type -> m (Maybe CType)
+toCType ty = do
+  sort <- reduce $ getSort ty
+  case sort of
+    Type l -> return $ Just $ LType (LEl l (unEl ty))
+    Inf    -> do
+      t <- reduce (unEl ty)
+      case t of
+        Def q [] -> return $ Just $ ClosedType q
+        _        -> return $ Nothing
+    _      -> return $ Nothing
+
+instance Subst Term CType where
+  applySubst rho t@ClosedType{} = t
+  applySubst rho (LType t) = LType $ applySubst rho t
+
+
+defineTranspOrHCompForFields
+  :: TranspOrHComp
+  -> (Maybe Term)            -- ^ PathCons, Δ.Φ ⊢ u : R δ
+  -> (Term -> QName -> Term) -- ^ how to apply a "projection" to a term
   -> QName       -- ^ some name, e.g. record name
   -> Telescope   -- ^ param types Δ
   -> Telescope   -- ^ fields' types Δ ⊢ Φ
   -> [Arg QName] -- ^ fields' names
   -> Type        -- ^ record type Δ ⊢ T
-  -> TCM ((QName, Telescope, Type, [Dom Type], [Term]), Substitution)
-defineTranspForFields = defineTranspForFields' Nothing
+  -> TCM (Maybe ((QName, Telescope, Type, [Dom Type], [Term]), Substitution))
+defineTranspOrHCompForFields cmd pathCons project name params fsT fns rect =
+   case cmd of
+       DoTransp -> runMaybeT $ do
+         fsT' <- traverse (traverse (MaybeT . toCType)) fsT
+         lift $ defineTranspForFields pathCons project name params fsT' fns rect
+       DoHComp -> runMaybeT $ do
+         fsT' <- traverse (traverse (MaybeT . toLType)) fsT
+         rect' <- MaybeT $ toLType rect
+         lift $ defineHCompForFields project name params fsT' fns rect'
 
 
 -- invariant: resulting tel Γ is such that Γ = ... , (φ : I), (a0 : ...)
 --            where a0 has type matching the arguments of primTrans.
-defineTranspForFields'
-  :: (Maybe Term)                    -- ^ PathCons, Δ.Φ ⊢ u : R δ
+defineTranspForFields
+  :: (Maybe Term)            -- ^ PathCons, Δ.Φ ⊢ u : R δ
   -> (Term -> QName -> Term) -- ^ how to apply a "projection" to a term
   -> QName       -- ^ some name, e.g. record name
   -> Telescope   -- ^ param types Δ
-  -> Telescope   -- ^ fields' types Δ ⊢ Φ
+  -> Tele (Dom CType)   -- ^ fields' types Δ ⊢ Φ
   -> [Arg QName] -- ^ fields' names
   -> Type        -- ^ record type Δ ⊢ T
   -> TCM ((QName, Telescope, Type, [Dom Type], [Term]), Substitution)
-defineTranspForFields' pathCons applyProj name params fsT fns rect = do
+defineTranspForFields pathCons applyProj name params fsT fns rect = do
   interval <- elInf primInterval
   let deltaI = expTelescope interval params
   iz <- primIZero
@@ -703,7 +754,7 @@
       (tel,theta,the_phi,the_u0, the_fields) =
         case pathCons of
           -- (δ : Δ).Φ ⊢ u : R δ
-          Just u -> (abstract gamma' (d0 `applySubst` fsT) -- Ξ = δ : Δ^I, φ : F, _ : Φ[δ i0]
+          Just u -> (abstract gamma' (d0 `applySubst` fmap (fmap fromCType) fsT) -- Ξ = δ : Δ^I, φ : F, _ : Φ[δ i0]
                     , (liftS (size fsT) d0 `applySubst` u) `consS` raiseS (size fsT)
                     , raise (size fsT) (var 0)
                     , (liftS (size fsT) d0 `applySubst` u)
@@ -719,11 +770,11 @@
       -- .. ⊢ field : filled_ty' i0
       mkBody (field, filled_ty') = do
         let
-          filled_ty = lam_i $ (unEl . unDom) filled_ty'
+          filled_ty = lam_i $ (unEl . fromCType . unDom) filled_ty'
           -- Γ ⊢ l : I -> Level of filled_ty
-        sort <- reduce $ getSort $ unDom filled_ty'
-        case sort of
-          Type l -> do
+        -- sort <- reduce $ getSort $ unDom filled_ty'
+        case unDom filled_ty' of
+          LType (LEl l _) -> do
             let lvl = lam_i $ Level l
             return $ runNames [] $ do
              lvl <- open lvl
@@ -732,11 +783,10 @@
                                  <@> phi
                                  <@> field
           -- interval arg
-          Inf  ->
+          ClosedType{}  ->
             return $ runNames [] $ do
             [field] <- mapM open [field]
             field
-          _ -> __IMPOSSIBLE__
 
   let
         -- ' Ξ , i : I ⊢ τ = [(\ j → δ (i ∧ j)), φ ∨ ~ i, u] : Ξ
@@ -765,7 +815,7 @@
   let
     -- Ξ, i : I ⊢ ... : Δ.Φ
     theSubst = reverse (tau `applySubst` bodys) ++# (liftS 1 (raiseS (size tel - size deltaI)) `composeS` sub params)
-  return $ ((theName, tel, theta `applySubst` rtype, clause_types, bodys), theSubst)
+  return $ ((theName, tel, theta `applySubst` rtype, map (fmap fromCType) clause_types, bodys), theSubst)
   where
     -- record type in 'exponentiated' context
     -- (params : Δ^I), i : I |- T[params i]
@@ -789,9 +839,9 @@
   :: (Term -> QName -> Term) -- ^ how to apply a "projection" to a term
   -> QName       -- ^ some name, e.g. record name
   -> Telescope   -- ^ param types Δ
-  -> Telescope   -- ^ fields' types Δ ⊢ Φ
+  -> Tele (Dom LType)   -- ^ fields' types Δ ⊢ Φ
   -> [Arg QName] -- ^ fields' names
-  -> Type        -- ^ record type (δ : Δ) ⊢ R[δ]
+  -> LType        -- ^ record type (δ : Δ) ⊢ R[δ]
   -> TCM ((QName, Telescope, Type, [Dom Type], [Term]),Substitution)
 defineHCompForFields applyProj name params fsT fns rect = do
   interval <- elInf primInterval
@@ -816,14 +866,14 @@
   reportSLn "hcomp.rec" 5 $ ("Generated name: " ++ show theName ++ " " ++ showQNameId theName)
 
   theType <- (abstract delta <$>) $ runNamesT [] $ do
-              rect <- open rect
+              rect <- open $ fromLType rect
               nPi' "phi" (elInf $ cl primInterval) $ \ phi ->
                (nPi' "i" (elInf $ cl primInterval) $ \ i ->
                 pPi' "o" phi $ \ _ -> rect) -->
                rect --> rect
 
   reportSDoc "hcomp.rec" 20 $ prettyTCM theType
-  reportSDoc "hcomp.rec" 60 $ text $ "sort = " ++ show (getSort rect)
+  reportSDoc "hcomp.rec" 60 $ text $ "sort = " ++ show (lTypeLevel rect)
 
   noMutualBlock $ addConstant theName $ (defaultDefn defaultArgInfo theName theType
     (emptyFunction { funTerminates = Just True }))
@@ -835,7 +885,7 @@
   let -- Γ ⊢ R δ
       drect_gamma = raiseS (size gamma - size delta) `applySubst` rect
 
-  reportSDoc "hcomp.rec" 60 $ text $ "sort = " ++ show (getSort drect_gamma)
+  reportSDoc "hcomp.rec" 60 $ text $ "sort = " ++ show (lTypeLevel drect_gamma)
 
   let
 
@@ -851,8 +901,8 @@
 
       -- ' (δ, φ, u, u0) : Γ ⊢ fillR Γ : (i : I) → rtype[ δ ↦ (\ j → δ (i ∧ j))]
       fillTerm = runNames [] $ do
-        rect <- open                           $ unEl    drect_gamma
-        lvl  <- open . (\ (Type l) -> Level l) $ getSort drect_gamma
+        rect <- open . unEl  . fromLType  $ drect_gamma
+        lvl  <- open . Level . lTypeLevel $ drect_gamma
         params     <- mapM open $ take (size delta) $ teleArgs gamma
         [phi,w,w0] <- mapM open [the_phi,the_u,the_u0]
         -- (δ : Δ, φ : I, w : .., w0 : R δ) ⊢
@@ -903,9 +953,9 @@
       mkBody (fname, filled_ty') = do
         let
           proj t = (`applyProj` unArg fname) <$> t
-          filled_ty = Lam defaultArgInfo (Abs "i" $ (unEl . unDom) filled_ty')
+          filled_ty = Lam defaultArgInfo (Abs "i" $ (unEl . fromLType . unDom) filled_ty')
           -- Γ ⊢ l : I -> Level of filled_ty
-        Type l <- reduce $ getSort $ unDom filled_ty'
+        l <- reduce $ lTypeLevel $ unDom filled_ty'
         let lvl = Lam defaultArgInfo (Abs "i" $ Level l)
         return $ runNames [] $ do
              lvl <- open lvl
@@ -918,10 +968,10 @@
                   (lam "i" $ \ i -> lam "o" $ \ o -> proj $ w <@> i <@> o) -- TODO wait for phi = 1
                   (proj w0)
 
-  reportSDoc "hcomp.rec" 60 $ text $ "filled_types sorts:" ++ show (map (getSort . unDom) filled_types)
+  reportSDoc "hcomp.rec" 60 $ text $ "filled_types sorts:" ++ show (map (getSort . fromLType . unDom) filled_types)
 
   bodys <- mapM mkBody (zip fns filled_types)
-  return $ ((theName, gamma, rtype, clause_types, bodys),IdS)
+  return $ ((theName, gamma, rtype, map (fmap fromLType) clause_types, bodys),IdS)
 
 
 getGeneralizedParameters :: Set Name -> QName -> TCM [Maybe Name]
diff --git a/src/full/Agda/TypeChecking/Rules/LHS/ProblemRest.hs b/src/full/Agda/TypeChecking/Rules/LHS/ProblemRest.hs
--- a/src/full/Agda/TypeChecking/Rules/LHS/ProblemRest.hs
+++ b/src/full/Agda/TypeChecking/Rules/LHS/ProblemRest.hs
@@ -3,10 +3,6 @@
 
 module Agda.TypeChecking.Rules.LHS.ProblemRest where
 
-#if __GLASGOW_HASKELL__ <= 708
-import Data.Functor ( (<$), (<$>) )
-#endif
-
 import Control.Arrow (first, second)
 import Control.Monad
 
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
@@ -1,4 +1,5 @@
 {-# LANGUAGE CPP #-}
+{-# LANGUAGE NondecreasingIndentation   #-}
 
 module Agda.TypeChecking.Rules.Record where
 
@@ -35,7 +36,7 @@
 import Agda.TypeChecking.CompiledClause.Compile
 
 import Agda.TypeChecking.Rules.Data ( getGeneralizedParameters, bindGeneralizedParameters, bindParameters, fitsIn, forceSort,
-                                      defineCompData, defineTranspForFields, defineHCompForFields )
+                                      defineCompData, defineTranspOrHCompForFields )
 import Agda.TypeChecking.Rules.Term ( isType_ )
 import {-# SOURCE #-} Agda.TypeChecking.Rules.Decl (checkDecl)
 
@@ -374,9 +375,8 @@
         ]
   reportSDoc "tc.rec.cxt" 30 $ prettyTCM params
   reportSDoc "tc.rec.cxt" 30 $ prettyTCM fsT
-  reportSDoc "tc.rec.cxt" 30 $ text $ show rect
-  sortsOk <- allM (rect : map unDom (flattenTel fsT)) sortOk
-  if not $ sortsOk && all isJust required then return $ emptyCompKit else do
+  reportSDoc "tc.rec.cxt" 30 $ pretty rect
+  if not $ all isJust required then return $ emptyCompKit else do
     transp <- whenDefined [builtinTrans]              (defineTranspOrHCompR DoTransp name params fsT fns rect)
     hcomp  <- whenDefined [builtinTrans,builtinHComp] (defineTranspOrHCompR DoHComp name params fsT fns rect)
     return $ CompKit
@@ -387,10 +387,6 @@
     whenDefined xs m = do
       xs <- mapM getTerm' xs
       if all isJust xs then m else return Nothing
-    sortOk :: Type -> TCM Bool
-    sortOk a = reduce (getSort a) >>= \case
-      Type{} -> return True
-      _      -> return False
 
 
 defineTranspOrHCompR ::
@@ -402,10 +398,10 @@
   -> Type        -- ^ record type Δ ⊢ T
   -> TCM (Maybe QName)
 defineTranspOrHCompR cmd name params fsT fns rect = do
-  (theName, gamma, rtype, clause_types, bodies) <- fst <$>
-    (case cmd of DoTransp -> defineTranspForFields; DoHComp -> defineHCompForFields)
-       (\ t fn -> t `applyE` [Proj ProjSystem fn]) name params fsT fns rect
+  let project = (\ t fn -> t `applyE` [Proj ProjSystem fn])
+  stuff <- fmap fst <$> defineTranspOrHCompForFields cmd Nothing project name params fsT fns rect
 
+  caseMaybe stuff (return Nothing) $ \ (theName, gamma, rtype, clause_types, bodies) -> do
   -- phi = 1 clause
   c' <- do
            io <- primIOne
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
@@ -553,9 +553,9 @@
     case unEl t' of
       Pi dom@(Dom{domInfo = info', unDom = a}) b
         | not (sameHiding h info') -> typeError $ WrongHidingInLambda t'
-        | not (null $ allMetas a) ->
+        | not (noMetas a) ->
             postponeTypeCheckingProblem (CheckExpr cmp e t') $
-              null . allMetas <$> instantiateFull a
+              noMetas <$> instantiateFull a
         | otherwise -> blockTerm t' $ do
           ensureEmptyType (getRange i) a
           -- Add helper function
@@ -578,7 +578,7 @@
                     { clauseLHSRange  = getRange e
                     , clauseFullRange = getRange e
                     , clauseTel       = telFromList [fmap (absurdPatternName,) dom]
-                    , namedClausePats = [Arg info' $ Named (Just $ unranged $ absName b) $ VarP PatOAbsurd (DBPatVar absurdPatternName 0)]
+                    , namedClausePats = [Arg info' $ Named (Just $ unranged $ absName b) $ absurdP 0]
                     , clauseBody      = Nothing
                     , clauseType      = Just $ setRelevance rel $ defaultArg $ absBody b
                     , clauseCatchall  = False
@@ -682,7 +682,7 @@
               -- (seems to archieve a bit along @normalize@, but how much??).
               problem <- reduce =<< instantiateFull (flattenTel tel, us, vs)
               -- over-approximating the set of metas actually blocking unification
-              return $ listToMaybe $ allMetas problem
+              return $ firstMeta problem
 
             SplitError (NotADatatype aClosure) ->
               enterClosure aClosure $ \ a -> isBlockedType a
@@ -892,8 +892,9 @@
         -- to their counterpart in the record type definition.
         disambiguateRecordFields (map _nameFieldA fs) (map unArg projs)
 
-        xs <- map unArg <$> getRecordFieldNames r
-        es <- orderFields r Nothing xs $ map (\ (FieldAssignment x e) -> (x, Just e)) fs
+        axs <- getRecordFieldNames r
+        let xs = map unArg axs
+        es <- orderFields r (\ _ -> Nothing) axs $ map (\ (FieldAssignment x e) -> (x, Just e)) fs
         let es' = zipWith (replaceFields name ei) projs es
         checkExpr' cmp (A.Rec ei [ Left (FieldAssignment x e) | (x, Just e) <- zip xs es' ]) t
 
@@ -1194,36 +1195,33 @@
 doQuoteTerm :: Comparison -> Term -> Type -> TCM Term
 doQuoteTerm cmp et t = do
   et'       <- etaContract =<< instantiateFull et
-  let metas = allMetas et'
-  case metas of
-    _:_ -> postponeTypeCheckingProblem (DoQuoteTerm cmp et t) $ andM $ map isInstantiatedMeta metas
+  case allMetasList et' of
     []  -> do
       q  <- quoteTerm et'
       ty <- el primAgdaTerm
       coerce cmp q ty t
+    metas -> postponeTypeCheckingProblem (DoQuoteTerm cmp et t) $ andM $ map isInstantiatedMeta metas
 
 -- | Checking `quoteGoal` (deprecated)
 quoteGoal :: Type -> TCM (Either [MetaId] Term)
 quoteGoal t = do
   t' <- etaContract =<< instantiateFull t
-  let metas = allMetas t'
-  case metas of
-    _:_ -> return $ Left metas
+  case allMetasList t' of
     []  -> do
       quotedGoal <- quoteTerm (unEl t')
       return $ Right quotedGoal
+    metas -> return $ Left metas
 
 -- | Checking `quoteContext` (deprecated)
 quoteContext :: TCM (Either [MetaId] Term)
 quoteContext = do
   contextTypes  <- map (fmap snd) <$> getContext
   contextTypes  <- etaContract =<< instantiateFull contextTypes
-  let metas = allMetas contextTypes
-  case metas of
-    _:_ -> return $ Left metas
+  case allMetasList contextTypes of
     []  -> do
       quotedContext <- buildList <*> mapM quoteDom contextTypes
       return $ Right quotedContext
+    metas -> return $ Left metas
 
 -- | Unquote a TCM computation in a given hole.
 unquoteM :: A.Expr -> Term -> Type -> TCM ()
@@ -1242,10 +1240,10 @@
       mi <- lookupMeta' x
       (r, meta) <- case mi of
         Nothing -> do -- fresh meta: need to block on something else!
-          otherMetas <- allMetas <$> instantiateFull goal
-          case otherMetas of
-            []  -> return (noRange,     Nothing) -- Nothing to block on, leave it yellow. Alternative: fail.
-            x:_ -> return (noRange,     Just x)  -- range?
+          (noRange,) . firstMeta <$> instantiateFull goal
+            -- Remark:
+            -- Nothing:  Nothing to block on, leave it yellow. Alternative: fail.
+            -- Just x:   range?
         Just mi -> return (getRange mi, Just x)
       setCurrentRange r $
         addConstraint (UnquoteTactic meta tac hole goal)
diff --git a/src/full/Agda/TypeChecking/Serialise/Instances/Errors.hs b/src/full/Agda/TypeChecking/Serialise/Instances/Errors.hs
--- a/src/full/Agda/TypeChecking/Serialise/Instances/Errors.hs
+++ b/src/full/Agda/TypeChecking/Serialise/Instances/Errors.hs
@@ -102,6 +102,7 @@
       valu [19, a, b]   = valuN CoInfectiveImport a b
       valu [20, a]      = valuN InstanceNoOutputTypeName a
       valu [21, a]      = valuN InstanceArgWithExplicitArg a
+      valu [22]         = valuN WrongInstanceDeclaration
       valu _ = malformed
 
 instance EmbPrj DeclarationWarning where
diff --git a/src/full/Agda/TypeChecking/SizedTypes/Solve.hs b/src/full/Agda/TypeChecking/SizedTypes/Solve.hs
--- a/src/full/Agda/TypeChecking/SizedTypes/Solve.hs
+++ b/src/full/Agda/TypeChecking/SizedTypes/Solve.hs
@@ -102,6 +102,7 @@
 import Agda.Utils.Null
 import Agda.Utils.Pretty (Pretty, prettyShow)
 import qualified Agda.Utils.Pretty as P
+import Agda.Utils.Singleton
 import Agda.Utils.Size
 import Agda.Utils.Tuple
 import qualified Agda.Utils.VarSet as VarSet
@@ -145,7 +146,7 @@
     -- @allMetas@ does not reduce or instantiate;
     -- this is why we require the size constraints to be normalised.
     return (cl, map metaId . Set.toList $
-      sizeMetaSet `Set.intersection` Set.fromList (allMetas c))
+      sizeMetaSet `Set.intersection` allMetas singleton c)
 
   -- Now, some constraints may have no metas (clcs), the others have at least one (othercs).
   let classify :: (a, [b]) -> Either a (a, NonemptyList b)
diff --git a/src/full/Agda/TypeChecking/Telescope.hs b/src/full/Agda/TypeChecking/Telescope.hs
--- a/src/full/Agda/TypeChecking/Telescope.hs
+++ b/src/full/Agda/TypeChecking/Telescope.hs
@@ -38,10 +38,12 @@
 import Agda.Utils.Impossible
 
 -- | Flatten telescope: (Γ : Tel) -> [Type Γ]
-flattenTel :: Telescope -> [Dom Type]
+flattenTel :: Subst t a => Tele (Dom a) -> [Dom a]
 flattenTel EmptyTel          = []
 flattenTel (ExtendTel a tel) = raise (size tel + 1) a : flattenTel (absBody tel)
 
+{-# SPECIALIZE flattenTel :: Telescope -> [Dom Type] #-}
+
 -- | Order a flattened telescope in the correct dependeny order: Γ ->
 --   Permutation (Γ -> Γ~)
 --
@@ -77,7 +79,7 @@
 teleArgNames :: Telescope -> [Arg ArgName]
 teleArgNames = map (argFromDom . fmap fst) . telToList
 
-teleArgs :: (DeBruijn a) => Telescope -> [Arg a]
+teleArgs :: (DeBruijn a) => Tele (Dom t) -> [Arg a]
 teleArgs tel =
   [ Arg info (deBruijnVar i)
   | (i, Dom {domInfo = info, unDom = (n,_)}) <- zip (downFrom $ size l) l ]
diff --git a/src/full/Agda/Utils/Singleton.hs b/src/full/Agda/Utils/Singleton.hs
--- a/src/full/Agda/Utils/Singleton.hs
+++ b/src/full/Agda/Utils/Singleton.hs
@@ -5,6 +5,8 @@
 
 module Agda.Utils.Singleton where
 
+import Data.Monoid (Endo(..))
+
 import Data.Hashable (Hashable)
 import Data.HashMap.Strict (HashMap)
 import qualified Data.HashMap.Strict as HashMap
@@ -30,6 +32,8 @@
 
 instance Singleton a   (Maybe a)   where singleton = Just
 instance Singleton a   [a]         where singleton = (:[])
+instance Singleton a  ([a] -> [a]) where singleton = (:)
+instance Singleton a   (Endo [a])  where singleton = Endo . (:)
 instance Singleton a   (NonemptyList a)
                                    where singleton = (:! [])
 instance Singleton a   (Seq a)     where singleton = Seq.singleton
diff --git a/stack-8.6.4.yaml b/stack-8.6.4.yaml
deleted file mode 100644
--- a/stack-8.6.4.yaml
+++ /dev/null
@@ -1,20 +0,0 @@
-resolver: lts-13.16
-
-extra-deps:
-- EdisonCore-1.3.2.1
-- data-hash-0.2.0.1
-- equivalence-0.3.4
-- geniplate-mirror-0.7.6
-- EdisonAPI-1.3.1
-- STMonadTrans-0.4.3
-
-flags:
-  time-locale-compat:
-    old-locale: false
-
-  transformers-compat:
-    five-three: true
-
-# Local packages, usually specified by relative directory name
-packages:
-- '.'
diff --git a/stack-8.6.5.yaml b/stack-8.6.5.yaml
new file mode 100644
--- /dev/null
+++ b/stack-8.6.5.yaml
@@ -0,0 +1,9 @@
+resolver: lts-13.21
+
+extra-deps:
+- EdisonCore-1.3.2.1
+- data-hash-0.2.0.1
+- equivalence-0.3.4
+- geniplate-mirror-0.7.6
+- EdisonAPI-1.3.1
+- STMonadTrans-0.4.3