Agda 2.6.0 → 2.6.0.1

raw patch · 50 files changed

+503/−753 lines, 50 filessetup-changedPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• Agda.cabal +37/−37
• CHANGELOG.md +33/−11
• Setup.hs +2/−2
• dist/build/Agda/Syntax/Parser/Parser.hs +2/−405
• doc/user-manual.pdf binary
• src/data/MAlonzo/src/MAlonzo/RTE.hs +6/−4
• src/data/emacs-mode/agda2-mode-pkg.el +1/−1
• src/data/emacs-mode/agda2-mode.el +1/−1
• src/data/lib/prim/Agda/Builtin/Word/Properties.agda +10/−0
• src/full/Agda/Compiler/Backend.hs +4/−4
• src/full/Agda/Compiler/Common.hs +1/−0
• src/full/Agda/Compiler/JS/Compiler.hs +2/−2
• src/full/Agda/Compiler/MAlonzo/Compiler.hs +15/−8
• src/full/Agda/Compiler/MAlonzo/Pragmas.hs +10/−0
• src/full/Agda/Compiler/MAlonzo/Primitives.hs +29/−11
• src/full/Agda/Interaction/BasicOps.hs +5/−2
• src/full/Agda/Interaction/Highlighting/Generate.hs +13/−2
• src/full/Agda/Interaction/InteractionTop.hs +9/−2
• src/full/Agda/Interaction/Options/Lenses.hs +1/−0
• src/full/Agda/Syntax/Internal.hs +5/−1
• src/full/Agda/TypeChecking/Conversion.hs +3/−7
• src/full/Agda/TypeChecking/Coverage.hs +16/−3
• src/full/Agda/TypeChecking/Empty.hs +12/−12
• src/full/Agda/TypeChecking/Empty.hs-boot +3/−0
• src/full/Agda/TypeChecking/Errors.hs +4/−7
• src/full/Agda/TypeChecking/Generalize.hs +8/−6
• src/full/Agda/TypeChecking/IApplyConfluence.hs +0/−17
• src/full/Agda/TypeChecking/InstanceArguments.hs +2/−1
• src/full/Agda/TypeChecking/MetaVars/Occurs.hs +10/−4
• src/full/Agda/TypeChecking/Monad/Base.hs +3/−3
• src/full/Agda/TypeChecking/Monad/Builtin.hs +1/−1
• src/full/Agda/TypeChecking/Monad/MetaVars.hs +50/−14
• src/full/Agda/TypeChecking/Monad/Signature.hs +1/−1
• src/full/Agda/TypeChecking/Monad/Signature.hs-boot +1/−1
• src/full/Agda/TypeChecking/Names.hs +1/−21
• src/full/Agda/TypeChecking/Primitive.hs +17/−13
• src/full/Agda/TypeChecking/Records.hs +34/−36
• src/full/Agda/TypeChecking/Reduce.hs +2/−1
• src/full/Agda/TypeChecking/Rewriting.hs +6/−6
• src/full/Agda/TypeChecking/Rewriting/NonLinMatch.hs +3/−3
• src/full/Agda/TypeChecking/Rules/Data.hs +96/−46
• src/full/Agda/TypeChecking/Rules/LHS/ProblemRest.hs +0/−4
• src/full/Agda/TypeChecking/Rules/Record.hs +7/−11
• src/full/Agda/TypeChecking/Rules/Term.hs +17/−19
• src/full/Agda/TypeChecking/Serialise/Instances/Errors.hs +1/−0
• src/full/Agda/TypeChecking/SizedTypes/Solve.hs +2/−1
• src/full/Agda/TypeChecking/Telescope.hs +4/−2
• src/full/Agda/Utils/Singleton.hs +4/−0
• stack-8.6.4.yaml +0/−20
• stack-8.6.5.yaml +9/−0

@@ -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

@@ -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 -------------------------------

@@ -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

@@ -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" #-}   

binary file changed (872344 → 872824 bytes)

@@ -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

@@ -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")

@@ -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.") 

@@ -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

@@ -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

@@ -44,6 +44,7 @@ data IsMain = IsMain | NotMain   deriving (Eq, Show) +-- | Conjunctive semigroup ('NotMain' is absorbing). instance Semigroup IsMain where   NotMain <> _ = NotMain   _       <> NotMain = NotMain

@@ -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

@@ -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

@@ -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"

@@ -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)"

@@ -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_

@@ -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.

@@ -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.

@@ -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

@@ -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__

@@ -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

@@ -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 

@@ -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)+    ]

@@ -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)

@@ -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) ++

@@ -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 }-

@@ -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

@@ -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 =

@@ -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__

@@ -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

@@ -35,7 +35,7 @@  class ( Functor m       , Applicative m-#if __GLASGOW_HASKELL__ == 710+#if __GLASGOW_HASKELL__ < 800       , Monad m #else       , Fail.MonadFail m

@@ -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

@@ -636,7 +636,7 @@  class ( Functor m       , Applicative m-#if __GLASGOW_HASKELL__ == 710+#if __GLASGOW_HASKELL__ < 800       , Monad m #else       , Fail.MonadFail m

@@ -23,7 +23,7 @@  class ( Functor m       , Applicative m-#if __GLASGOW_HASKELL__ == 710+#if __GLASGOW_HASKELL__ < 800       , Monad m #else       , Fail.MonadFail m

@@ -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

@@ -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

@@ -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

@@ -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.

@@ -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

@@ -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

@@ -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]

@@ -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 

@@ -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

@@ -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)

@@ -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

@@ -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)

@@ -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 ]

@@ -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

@@ -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:-- '.'

@@ -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