Agda 2.5.1 → 2.5.1.1

raw patch · 28 files changed

+397/−197 lines, 28 filesdep ~Agdadep ~EdisonAPIdep ~uhc-utilPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependency ranges changed: Agda, EdisonAPI, uhc-util

API changes (from Hackage documentation)

Files

• Agda.cabal +13/−10
• CHANGELOG +56/−0
• dist/build/Agda/Syntax/Parser/Lexer.hs +0/−21
• dist/build/Agda/Syntax/Parser/Parser.hs +0/−21
• src/data/emacs-mode/agda2-mode.el +1/−1
• src/full/Agda/Interaction/BasicOps.hs +1/−1
• src/full/Agda/Interaction/Imports.hs +7/−1
• src/full/Agda/Syntax/Common.hs +30/−12
• src/full/Agda/Syntax/Concrete/Operators.hs +6/−6
• src/full/Agda/Syntax/Concrete/Operators/Parser.hs +79/−28
• src/full/Agda/Syntax/Concrete/Pretty.hs +5/−4
• src/full/Agda/Syntax/Translation/AbstractToConcrete.hs +1/−1
• src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs +3/−3
• src/full/Agda/Syntax/Translation/InternalToAbstract.hs +25/−6
• src/full/Agda/TypeChecking/Constraints.hs +10/−0
• src/full/Agda/TypeChecking/Constraints.hs-boot +1/−0
• src/full/Agda/TypeChecking/Coverage.hs +10/−3
• src/full/Agda/TypeChecking/Errors.hs +4/−4
• src/full/Agda/TypeChecking/Implicit.hs +3/−3
• src/full/Agda/TypeChecking/InstanceArguments.hs +61/−26
• src/full/Agda/TypeChecking/InstanceArguments.hs-boot +0/−7
• src/full/Agda/TypeChecking/MetaVars.hs +9/−10
• src/full/Agda/TypeChecking/MetaVars.hs-boot +1/−1
• src/full/Agda/TypeChecking/Monad/Base.hs +2/−2
• src/full/Agda/TypeChecking/Monad/Constraints.hs +41/−18
• src/full/Agda/TypeChecking/Pretty.hs +1/−1
• src/full/Agda/TypeChecking/Rules/LHS/Unify.hs +2/−2
• src/full/Agda/TypeChecking/Serialise/Instances/Common.hs +25/−5

@@ -1,5 +1,5 @@ name:            Agda-version:         2.5.1+version:         2.5.1.1 cabal-version:   >= 1.8 build-type:      Custom license:         OtherLicense@@ -35,6 +35,7 @@ tested-with:        GHC == 7.6.3                     GHC == 7.8.4                     GHC == 7.10.3+                    GHC == 8.0.1 extra-source-files: src/full/undefined.h                     README.md                     CHANGELOG@@ -76,8 +77,8 @@  source-repository this   type:     git-  location: https://github.com/agda/agda/tree/2.5.1-  tag:      2.5.1+  location: https://github.com/agda/agda/tree/v2.5.1.1+  tag:      v2.5.1.1  flag cpphs   default:     True@@ -99,12 +100,13 @@     ghc-options: -pgmP cpphs -optP --cpp    if flag(uhc)-    build-depends:    shuffle >= 0.1.3.3-                    , uhc-light >= 1.1.9.2 && < 1.2-                    , uhc-util >= 0.1.6.3 && < 0.1.6.6-                    , uulib >= 0.9.20-    -- we use the CPP processor to conditionally import the UHC Light modules. If UHC Light is not-    -- present, we instead create dummy definitions, see module Agda.Compiler.UHC.Bridge.+    build-depends:  shuffle >= 0.1.3.3+                  , uhc-light >= 1.1.9.2 && < 1.2+                  , uhc-util >= 0.1.6.3 && < 0.1.6.7+                  , uulib >= 0.9.20+    -- we use the CPP processor to conditionally import the UHC Light+    -- modules. If UHC Light is not present, we instead create dummy+    -- definitions, see module Agda.Compiler.UHC.Bridge.     cpp-options:    -DUHC_BACKEND    if os(windows)@@ -534,7 +536,7 @@   hs-source-dirs: src/main   main-is:        Main.hs   build-depends:-    Agda == 2.5.1+    Agda == 2.5.1.1     -- Nothing is used from the following package, except for the     -- prelude.     , base >= 4.6.0.1 && < 6@@ -572,3 +574,4 @@     , mtl >= 2.1.1 && <= 2.1.3.1 || >= 2.2.1 && < 2.3     , filepath >= 1.3.0.1 && < 1.5   ghc-options:  -rtsopts+

@@ -1,4 +1,60 @@ ------------------------------------------------------------------------+-- Release notes for Agda version 2.5.1.1+------------------------------------------------------------------------++Important changes since 2.5.1:++Installation and infrastructure+===============================++* Added support for GHC 8.0.1.++Bug fixes+=========++* Fixed a serious performance problem with instance search++  Issues #1952 and #1998. Also related: #1955 and #2025++* Interactively splitting variable with C-c C-c no longer introduces+  new trailing patterns.  This fixes issue #1950.++    data Ty : Set where+      _⇒_ : Ty → Ty → Ty++    ⟦_⟧ : Ty → Set+    ⟦ A ⇒ B ⟧ = ⟦ A ⟧ → ⟦ B ⟧++    data Term : Ty → Set where+      K : (A B : Ty) → Term (A ⇒ (B ⇒ A))++    test : (A : Ty) (a : Term A) → ⟦ A ⟧+    test A a = {!a!}++  Before change, case splitting on `a` would give++    test .(A ⇒ (B ⇒ A)) (K A B) x x₁ = ?++  Now, it yields++    test .(A ⇒ (B ⇒ A)) (K A B) = ?++* Other issues fixed ( see https://github.com/agda/agda/issues ):+  - #1322 (Missing error for attempted higher order instance)+  - #1951 (mixfix binders not working in 'syntax')+  - #1967 (too eager insteance search error)+  - #1974 (lost constraint dependencies)+  - #1982 (internal error in unifier)+  - #2034 (function type instance goals)++Compiler backends+=================++* UHC compiler backend++  Added support for UHC 1.1.9.4.++------------------------------------------------------------------------ -- Release notes for Agda version 2.5.1 ------------------------------------------------------------------------ 

@@ -267,27 +267,6 @@ {-# LINE 1 "templates/GenericTemplate.hs" #-} {-# LINE 1 "<built-in>" #-} {-# LINE 1 "<command-line>" #-}-{-# LINE 9 "<command-line>" #-}-{-# LINE 1 "/usr/local/stow/ghc-8.0-upstream/lib/ghc-8.0.0.20160316/include/ghcversion.h" #-}-------------------{-# LINE 9 "<command-line>" #-} {-# LINE 1 "templates/GenericTemplate.hs" #-} -- ----------------------------------------------------------------------------- -- ALEX TEMPLATE

@@ -6324,27 +6324,6 @@ {-# LINE 1 "templates/GenericTemplate.hs" #-} {-# LINE 1 "<built-in>" #-} {-# LINE 1 "<command-line>" #-}-{-# LINE 11 "<command-line>" #-}-{-# LINE 1 "/usr/local/stow/ghc-8.0-upstream/lib/ghc-8.0.0.20160316/include/ghcversion.h" #-}-------------------{-# LINE 11 "<command-line>" #-} {-# LINE 1 "templates/GenericTemplate.hs" #-} -- Id: GenericTemplate.hs,v 1.26 2005/01/14 14:47:22 simonmar Exp  

@@ -10,7 +10,7 @@  ;;; Code: -(defvar agda2-version "2.5.1"+(defvar agda2-version "2.5.1.1"   "The version of the Agda mode. Note that the same version of the Agda executable must be used.") 

@@ -295,7 +295,7 @@       FindInScopeOF _ _ _        -> __IMPOSSIBLE__  instance Reify ProblemConstraint (Closure (OutputForm Expr Expr)) where-  reify (PConstr pid cl) = enterClosure cl $ \c -> buildClosure =<< (OutputForm (getRange c) pid <$> reify c)+  reify (PConstr pids cl) = enterClosure cl $ \c -> buildClosure =<< (OutputForm (getRange c) (last pids) <$> reify c)  instance Reify Constraint (OutputConstraint Expr Expr) where     reify (ValueCmp cmp t u v)   = CmpInType cmp <$> reify t <*> reify u <*> reify v

@@ -726,6 +726,11 @@     -- Andreas, Makoto, 2014-10-18 AIM XX: repeating the experiment     -- with discarding also the nameBindingSite in QName:     -- Saves 10% on serialization time (and file size)!+    --+    -- NOTE: We no longer discard all nameBindingSites (but the commit+    -- that introduced this change seems to have made Agda a bit+    -- faster and interface file sizes a bit smaller, at least for the+    -- standard library).     builtin <- use stLocalBuiltins     ms      <- getImports     mhs     <- mapM (\ m -> (m,) <$> moduleHash m) $ Set.toList ms@@ -736,7 +741,8 @@     -- Non-closed display forms are not applicable outside the module anyway,     -- and should be dead-code eliminated (#1928).     display <- HMap.filter (not . null) . HMap.map (filter isClosed) <$> use stImportsDisplayForms-    (display, sig) <- second killRange <$> (eliminateDeadCode display =<< getSignature)+    -- TODO: Kill some ranges?+    (display, sig) <- eliminateDeadCode display =<< getSignature     -- Andreas, 2015-02-09 kill ranges in pattern synonyms before     -- serialization to avoid error locations pointing to external files     -- when expanding a pattern synoym.

@@ -18,6 +18,7 @@ import qualified Data.ByteString.Char8 as ByteString import Data.Foldable import Data.Hashable+import qualified Data.Strict.Maybe as Strict import Data.Monoid import Data.Traversable import Data.Typeable (Typeable)@@ -768,32 +769,49 @@  newtype Constr a = Constr a -data Placeholder+------------------------------------------------------------------------+-- * Placeholders (used to parse sections)+------------------------------------------------------------------------++-- | The position of a name part or underscore in a name.++data PositionInName   = Beginning-    -- ^ @_foo@.+    -- ^ The following underscore is at the beginning of the name:+    -- @_foo@.   | Middle-    -- ^ @foo_bar@.+    -- ^ The following underscore is in the middle of the name:+    -- @foo_bar@.   | End-    -- ^ @foo_@.+    -- ^ The following underscore is at the end of the name: @foo_@.   deriving (Show, Eq, Ord)  -- | Placeholders are used to represent the underscores in a section.+ data MaybePlaceholder e-  = Placeholder !Placeholder-  | NoPlaceholder e+  = Placeholder !PositionInName+  | NoPlaceholder !(Strict.Maybe PositionInName) e+    -- ^ The second argument is used only (but not always) for name+    -- parts other than underscores.   deriving (Typeable, Eq, Ord, Functor, Foldable, Traversable, Show) +-- | An abbreviation: @noPlaceholder = 'NoPlaceholder'+-- 'Strict.Nothing'@.++noPlaceholder :: e -> MaybePlaceholder e+noPlaceholder = NoPlaceholder Strict.Nothing+ instance HasRange a => HasRange (MaybePlaceholder a) where-  getRange Placeholder{}     = noRange-  getRange (NoPlaceholder e) = getRange e+  getRange Placeholder{}       = noRange+  getRange (NoPlaceholder _ e) = getRange e  instance KillRange a => KillRange (MaybePlaceholder a) where-  killRange p@Placeholder{}   = p-  killRange (NoPlaceholder e) = killRange1 NoPlaceholder e+  killRange p@Placeholder{}     = p+  killRange (NoPlaceholder p e) = killRange1 (NoPlaceholder p) e  instance NFData a => NFData (MaybePlaceholder a) where-  rnf (Placeholder _)   = ()-  rnf (NoPlaceholder a) = rnf a+  rnf (Placeholder _)     = ()+  rnf (NoPlaceholder _ a) = rnf a  --------------------------------------------------------------------------- -- * Interaction meta variables

@@ -452,9 +452,9 @@             nonAssoc = case filter (isInfix NonAssoc) ops of               []  -> Nothing               ops -> Just $ do-                x <- NoPlaceholder <$> higher+                x <- noPlaceholder <$> higher                 f <- choice In ops-                y <- NoPlaceholder <$> higher+                y <- noPlaceholder <$> higher                 return (f x y)              or p1 []   p2 []   = Nothing@@ -466,7 +466,7 @@             preRight =               or (choice Pre)                  (filter isPrefix ops)-                 (\ops -> flip ($) <$> (NoPlaceholder <$> higher)+                 (\ops -> flip ($) <$> (noPlaceholder <$> higher)                                    <*> choice In ops)                  (filter (isInfix RightAssoc) ops) @@ -474,14 +474,14 @@             preRights = do               preRight <- preRight               return $ Data.Function.fix $ \preRights ->-                preRight <*> (NoPlaceholder <$> (preRights <|> higher))+                preRight <*> (noPlaceholder <$> (preRights <|> higher))              postLeft :: Maybe (Parser e (MaybePlaceholder e -> e))             postLeft =               or (choice Post)                  (filter isPostfix ops)                  (\ops -> flip <$> choice In ops-                               <*> (NoPlaceholder <$> higher))+                               <*> (noPlaceholder <$> higher))                  (filter (isInfix LeftAssoc) ops)              postLefts :: Maybe (Parser e e)@@ -489,7 +489,7 @@               postLeft <- postLeft               return $ Data.Function.fix $ \postLefts ->                 memoise (PostLeftsK key) $-                  flip ($) <$> (NoPlaceholder <$> (postLefts <|> higher))+                  flip ($) <$> (noPlaceholder <$> (postLefts <|> higher))                            <*> postLeft  ---------------------------------------------------------------------------

@@ -12,6 +12,7 @@ import Data.Either import Data.Hashable import Data.Maybe+import qualified Data.Strict.Maybe as Strict import Data.Set (Set)  import GHC.Generics (Generic)@@ -42,26 +43,26 @@ type Parser tok a =   MemoisedCPS.Parser MemoKey tok (MaybePlaceholder tok) a -placeholder :: Placeholder -> Parser e (MaybePlaceholder e)+placeholder :: PositionInName -> Parser e (MaybePlaceholder e) placeholder p = sat $ \t ->   case t of     Placeholder p' | p' == p -> True     _                        -> False  maybePlaceholder ::-  Maybe Placeholder -> Parser e e -> Parser e (MaybePlaceholder e)+  Maybe PositionInName -> Parser e e -> Parser e (MaybePlaceholder e) maybePlaceholder mp p = case mp of   Nothing -> p'   Just h  -> placeholder h <|> p'   where-  p' = NoPlaceholder <$> p+  p' = noPlaceholder <$> p  notPlaceholder :: Parser e e notPlaceholder = do   tok <- token   case tok of-    Placeholder _   -> empty-    NoPlaceholder e -> return e+    Placeholder _     -> empty+    NoPlaceholder _ e -> return e  sat' :: (e -> Bool) -> Parser e e sat' p = do@@ -116,7 +117,7 @@         IdentP x         -> LocalV x         AppP e1 e2       -> AppV e1 e2         OpAppP r d ns es -> OpAppV d ns ((map . fmap . fmap)-                                           (NoPlaceholder . Ordinary) es)+                                           (noPlaceholder . Ordinary) es)         HiddenP _ e      -> HiddenArgV e         InstanceP _ e    -> InstanceArgV e         ParenP _ e       -> ParenV e@@ -128,8 +129,8 @@         OpAppV d ns es -> let ess :: [NamedArg Pattern]                               ess = (map . fmap . fmap)                                       (\x -> case x of-                                          Placeholder{}   -> __IMPOSSIBLE__-                                          NoPlaceholder x -> fromOrdinary __IMPOSSIBLE__ x)+                                          Placeholder{}     -> __IMPOSSIBLE__+                                          NoPlaceholder _ x -> fromOrdinary __IMPOSSIBLE__ x)                                       es                           in OpAppP (fuseRange d ess) d ns ess         HiddenArgV e   -> HiddenP (getRange e) e@@ -143,8 +144,13 @@ data ParseSections = ParseSections | DoNotParseSections   deriving (Eq, Show) +-- | Runs a parser. If sections should be parsed, then identifiers+-- with at least two name parts are split up into multiple tokens,+-- using 'PositionInName' to record the tokens' original positions+-- within their respective identifiers.+ parse :: IsExpr e => (ParseSections, Parser e a) -> [e] -> [a]-parse (DoNotParseSections, p) es = Parser.parse p (map NoPlaceholder es)+parse (DoNotParseSections, p) es = Parser.parse p (map noPlaceholder es) parse (ParseSections,      p) es = Parser.parse p                                      (concat $ map splitExpr es)   where@@ -153,11 +159,11 @@     LocalV n -> splitName n     _        -> noSplit     where-    noSplit = [NoPlaceholder e]+    noSplit = [noPlaceholder e]      splitName n = case last ns of-      NoName{}  -> noSplit-      Name r ps -> splitParts r (init ns) Beginning ps+      Name r ps@(_ : _ : _) -> splitParts r (init ns) Beginning ps+      _                     -> noSplit       where       ns = qnameParts n @@ -168,14 +174,17 @@       -- Note also that the module qualifier, if any, is only applied       -- to the first name part. -      splitParts _ _ _ []          = []+      splitParts _ _ _ []          = __IMPOSSIBLE__       splitParts _ _ _ (Hole : []) = [Placeholder End]+      splitParts r m _ (Id s : []) = [part r m End s]       splitParts r m w (Hole : ps) = Placeholder w : splitParts r m  Middle ps-      splitParts r m _ (Id s : ps) = part          : splitParts r [] Middle ps-        where-        part = NoPlaceholder $ unExprView $ LocalV $-                 foldr Qual (QName (Name r [Id s])) m+      splitParts r m w (Id s : ps) = part r m w s  : splitParts r [] Middle ps +      part r m w s =+        NoPlaceholder (Strict.Just w)+                      (unExprView $ LocalV $+                         foldr Qual (QName (Name r [Id s])) m)+ --------------------------------------------------------------------------- -- * Parser combinators ---------------------------------------------------------------------------@@ -196,6 +205,51 @@             LocalV y | str == show y -> Just (getRange y)             _                        -> Nothing +-- | Parses a split-up, unqualified name consisting of at least two+-- name parts.+--+-- The parser does not check that underscores and other name parts+-- alternate. The range of the resulting name is the range of the+-- first name part that is not an underscore.++atLeastTwoParts :: IsExpr e => Parser e Name+atLeastTwoParts = do+  (r, ps) <- parts Beginning+  case r of+    Nothing -> __IMPOSSIBLE__+    Just r  -> return (Name r ps)+  where+  parts pos = do+    tok          <- token+    (pos', r, p) <- case tok of+      Placeholder pos'                   -> return (pos', Nothing, Hole)+      NoPlaceholder (Strict.Just pos') e -> case exprView e of+        LocalV (QName (Name r [Id s])) -> return (pos', Just r, Id s)+        _                              -> empty+      _ -> empty+    if pos == Middle && pos' == End then+      return (r, [p])+     else if pos' == pos then do+      (r', ps) <- parts Middle+      return (maybe r' Just r, p : ps)+     else+      empty++-- | Either a wildcard (@_@), or an unqualified name (possibly+-- containing multiple name parts).++wildOrUnqualifiedName :: IsExpr e => Parser e (Maybe Name)+wildOrUnqualifiedName =+  (Nothing <$ partP [] "_")+    <|>+  (do e <- notPlaceholder+      case exprView e of+        LocalV (QName n) -> return (Just n)+        WildV _          -> return Nothing+        _                -> empty)+    <|>+  Just <$> atLeastTwoParts+ -- | Used to define the return type of 'opP'.  type family OperatorType (k :: NotationKind) (e :: *) :: *@@ -288,13 +342,10 @@     (r, es) <- worker ms xs     return (r, Right (mkBinding h $ Name noRange [Hole]) : es)   worker ms (BindHole h : xs) = do-    e <- notPlaceholder-    case exprView e of-      LocalV (QName name) -> ret name-      WildV e             -> ret (Name noRange [Hole])-      _                   -> empty-        -- Old error message: "Expected variable name in binding-        -- position".+    e <- wildOrUnqualifiedName+    case e of+      Just name -> ret name+      Nothing   -> ret (Name noRange [Hole])     where     ret x = do       (r, es) <- worker ms xs@@ -311,10 +362,10 @@     NamedArg (MaybePlaceholder (OpApp e))   findExprFor normalHoles binders n =     case [ h | h@(_, m) <- normalHoles, namedArg m == n ] of-      [(Placeholder p,   arg)] -> set (Placeholder p) arg-      [(NoPlaceholder e, arg)] -> case [b | (b, m) <- binders, m == n] of-        [] -> set (NoPlaceholder (Ordinary e)) arg -- no variable to bind-        bs -> set (NoPlaceholder (SyntaxBindingLambda (fuseRange bs e) bs e)) arg+      [(Placeholder p,     arg)] -> set (Placeholder p) arg+      [(NoPlaceholder _ e, arg)] -> case [b | (b, m) <- binders, m == n] of+        [] -> set (noPlaceholder (Ordinary e)) arg -- no variable to bind+        bs -> set (noPlaceholder (SyntaxBindingLambda (fuseRange bs e) bs e)) arg       _ -> __IMPOSSIBLE__    noPlaceholders :: [NamedArg (MaybePlaceholder (OpApp e))] -> Int

@@ -12,6 +12,7 @@  import Data.Functor import Data.Maybe+import qualified Data.Strict.Maybe as Strict  import Agda.Syntax.Common import Agda.Syntax.Concrete@@ -105,8 +106,8 @@   pretty (SyntaxBindingLambda r bs e) = pretty (Lam r bs e)  instance Pretty a => Pretty (MaybePlaceholder a) where-  pretty Placeholder{}     = text "_"-  pretty (NoPlaceholder e) = pretty e+  pretty Placeholder{}       = text "_"+  pretty (NoPlaceholder _ e) = pretty e  instance Pretty Expr where     pretty e =@@ -511,7 +512,7 @@             IdentP x        -> pretty x             AppP p1 p2      -> sep [ pretty p1, nest 2 $ pretty p2 ]             RawAppP _ ps    -> fsep $ map pretty ps-            OpAppP _ q _ ps -> fsep $ prettyOpApp q (fmap (fmap (fmap NoPlaceholder)) ps)+            OpAppP _ q _ ps -> fsep $ prettyOpApp q (fmap (fmap (fmap (NoPlaceholder Strict.Nothing))) ps)             HiddenP _ p     -> braces' $ pretty p             InstanceP _ p   -> dbraces $ pretty p             ParenP _ p      -> parens $ pretty p@@ -545,7 +546,7 @@      -- Section underscores should be printed without surrounding     -- whitespace. This function takes care of that.-    merge :: [Doc] -> [(Doc, Maybe Placeholder)] -> [Doc]+    merge :: [Doc] -> [(Doc, Maybe PositionInName)] -> [Doc]     merge before []                            = reverse before     merge before ((d, Nothing) : after)        = merge (d : before) after     merge before ((d, Just Beginning) : after) = mergeRight before d after

@@ -914,7 +914,7 @@ cOpApp :: Range -> C.QName -> A.Name -> [C.Expr] -> C.Expr cOpApp r x n es =   C.OpApp r x (Set.singleton n)-          (map (defaultNamedArg . NoPlaceholder . Ordinary) es)+          (map (defaultNamedArg . noPlaceholder . Ordinary) es)  tryToRecoverOpApp :: A.Expr -> AbsToCon C.Expr -> AbsToCon C.Expr tryToRecoverOpApp e def = caseMaybeM (recoverOpApp bracket cOpApp view e) def return

@@ -2049,9 +2049,9 @@       ScopeM ([A.LamBinding], [NamedArg (Either A.Expr (OpApp e))])     replacePlaceholders []       = return ([], [])     replacePlaceholders (a : as) = case namedArg a of-      NoPlaceholder x -> mapSnd (set (Right x) a :) <$>-                           replacePlaceholders as-      Placeholder p   -> do+      NoPlaceholder _ x -> mapSnd (set (Right x) a :) <$>+                             replacePlaceholders as+      Placeholder _     -> do         x <- freshName noRange "section"         let i = argInfo a         (ls, ns) <- replacePlaceholders as

@@ -46,6 +46,7 @@ import Agda.Syntax.Concrete (FieldAssignment'(..), exprFieldA) import Agda.Syntax.Info as Info import Agda.Syntax.Abstract as A+import Agda.Syntax.Abstract.Pretty import Agda.Syntax.Internal as I import Agda.Syntax.Internal.Pattern as I import Agda.Syntax.Scope.Base (isNameInScope, inverseScopeLookupName)@@ -69,6 +70,7 @@ import Agda.Utils.Maybe import Agda.Utils.Monad import Agda.Utils.Permutation+import Agda.Utils.Pretty import Agda.Utils.Size import Agda.Utils.Tuple @@ -198,16 +200,25 @@     -- Ulf, can you add an explanation?     md <- liftTCM $ -- addContext (replicate (length ps) "x") $       displayForm f vs-    reportSLn "reify.display" 20 $+    reportSLn "reify.display" 60 $       "display form of " ++ show f ++ " " ++ show ps ++ " " ++ show wps ++ ":\n  " ++ show md     case md of-      Just d  | okDisplayForm d ->+      Just d  | okDisplayForm d -> do         -- In the display term @d@, @var i@ should be a placeholder         -- for the @i@th pattern of @ps@.         -- Andreas, 2014-06-11:         -- Are we sure that @d@ did not use @var i@ otherwise?-        reifyDisplayFormP =<< displayLHS (map namedArg ps) wps d-      _ -> return lhs+        lhs' <- displayLHS (map namedArg ps) wps d+        reportSDoc "reify.display" 70 $ do+          doc <- prettyA lhs'+          return $ vcat+            [ text "rewritten lhs to"+            , text "  lhs' = " <+> doc+            ]+        reifyDisplayFormP lhs'+      _ -> do+        reportSLn "reify.display" 70 $ "display form absent or not valid as lhs"+        return lhs   where     -- Andreas, 2015-05-03: Ulf, please comment on what     -- is the idea behind okDisplayForm.@@ -215,13 +226,15 @@     -- can serve as a valid left-hand side. That means checking that it is a     -- defined name applied to valid lhs eliminators (projections or     -- applications to constructor patterns).-    okDisplayForm (DWithApp d ds [])   = okDisplayForm d && all okDisplayTerm ds+    okDisplayForm (DWithApp d ds args) =+      okDisplayForm d && all okDisplayTerm ds  && all okToDrop args+      -- Andreas, 2016-05-03, issue #1950.+      -- We might drop trailing hidden trivial (=variable) patterns.     okDisplayForm (DTerm (I.Def f vs)) = all okElim vs     okDisplayForm (DDef f es)          = all okDElim es     okDisplayForm DDot{}               = False     okDisplayForm DCon{}               = False     okDisplayForm DTerm{}              = False-    okDisplayForm DWithApp{}           = False      okDisplayTerm (DTerm v) = okTerm v     okDisplayTerm DDot{}    = True@@ -231,6 +244,12 @@      okDElim (I.Apply v) = okDisplayTerm $ unArg v     okDElim I.Proj{}    = True++    okToDrop arg = notVisible arg && case ignoreSharing $ unArg arg of+      I.Var _ []   -> True+      I.DontCare{} -> True  -- no matching on irrelevant things.  __IMPOSSIBLE__ anyway?+      I.Level{}    -> True  -- no matching on levels. __IMPOSSIBLE__ anyway?+      _ -> False      okArg = okTerm . unArg 

@@ -25,6 +25,7 @@ import Agda.Utils.Maybe import Agda.Utils.Monad import Agda.Utils.Pretty (prettyShow)+import Agda.Utils.Lens  #include "undefined.h" import Agda.Utils.Impossible@@ -205,4 +206,13 @@   CheckArgs eh r args t0 t1 k    -> checkArguments' eh r args t0 t1 k   CheckLambda args body target   -> checkPostponedLambda args body target   UnquoteTactic tac hole t       -> unquoteTactic tac hole t $ return hole++debugConstraints :: TCM ()+debugConstraints = verboseS "tc.constr" 50 $ do+  awake    <- use stAwakeConstraints+  sleeping <- use stSleepingConstraints+  reportSDoc "" 0 $ vcat+    [ text "Current constraints"+    , nest 2 $ vcat [ text "awake " <+> vcat (map prettyTCM awake)+                    , text "asleep" <+> vcat (map prettyTCM sleeping) ] ] 

@@ -9,3 +9,4 @@ noConstraints          :: TCM a -> TCM a ifNoConstraints_       :: TCM () -> TCM a -> (ProblemId -> TCM a) -> TCM a guardConstraint        :: Constraint -> TCM () -> TCM ()+debugConstraints       :: TCM ()

@@ -551,7 +551,10 @@  -- | Entry point from @Interaction.MakeCase@. splitClauseWithAbsurd :: SplitClause -> Nat -> TCM (Either SplitError (Either SplitClause Covering))-splitClauseWithAbsurd c x = split' Inductive c (BlockingVar x Nothing)+splitClauseWithAbsurd c x = split' Inductive False c (BlockingVar x Nothing)+  -- Andreas, 2016-05-03, issue 1950:+  -- Do not introduce trailing pattern vars after split,+  -- because this does not work for with-clauses.  -- | Entry point from @TypeChecking.Empty@ and @Interaction.BasicOps@. --   @splitLast CoInductive@ is used in the @refine@ tactics.@@ -578,7 +581,7 @@       -> SplitClause       -> BlockingVar       -> TCM (Either SplitError Covering)-split ind sc x = fmap blendInAbsurdClause <$> split' ind sc x+split ind sc x = fmap blendInAbsurdClause <$> split' ind True sc x   where     n = lookupPatternVar sc $ blockingVarNo x     blendInAbsurdClause :: Either SplitClause Covering -> Covering@@ -613,10 +616,13 @@ split' :: Induction           -- ^ Coinductive constructors are allowed if this argument is           -- 'CoInductive'.+       -> Bool+          -- ^ If 'True', introduce new trailing variable patterns via+          --   'fixTarget'.        -> SplitClause        -> BlockingVar        -> TCM (Either SplitError (Either SplitClause Covering))-split' ind sc@(SClause tel ps _ target) (BlockingVar x mcons) = liftTCM $ runExceptionT $ do+split' ind fixtarget sc@(SClause tel ps _ target) (BlockingVar x mcons) = liftTCM $ runExceptionT $ do    debugInit tel x ps @@ -636,6 +642,7 @@     forM cons $ \ con ->       fmap (con,) <$> do         msc <- computeNeighbourhood delta1 n delta2 d pars ixs x ps con+        if not fixtarget then return msc else do         Trav.forM msc $ \ sc -> lift $ snd <$> fixTarget sc{ scTarget = target }    case ns of

@@ -839,12 +839,12 @@         unambiguous e = pretty e          isOrdinary :: MaybePlaceholder (C.OpApp e) -> Bool-        isOrdinary (NoPlaceholder (C.Ordinary _)) = True-        isOrdinary _                              = False+        isOrdinary (NoPlaceholder _ (C.Ordinary _)) = True+        isOrdinary _                                = False          fromOrdinary :: MaybePlaceholder (C.OpApp e) -> e-        fromOrdinary (NoPlaceholder (C.Ordinary e)) = e-        fromOrdinary _                              = __IMPOSSIBLE__+        fromOrdinary (NoPlaceholder _ (C.Ordinary e)) = e+        fromOrdinary _                                = __IMPOSSIBLE__          isPlaceholder :: MaybePlaceholder a -> Bool         isPlaceholder Placeholder{}   = True

@@ -16,7 +16,6 @@ import Agda.TypeChecking.Monad import Agda.TypeChecking.Reduce import Agda.TypeChecking.Substitute-import {-# SOURCE #-} Agda.TypeChecking.InstanceArguments import Agda.TypeChecking.Pretty  import Agda.Utils.Tuple@@ -53,9 +52,10 @@           mapFst (narg :) <$> implicitNamedArgs (n-1) expand (absApp b v)       _ -> return ([], t0')   where+    newMeta :: Hiding -> String -> Type -> TCM Term     newMeta Hidden   = newNamedValueMeta RunMetaOccursCheck-    newMeta Instance = initializeIFSMeta-    newMeta NotHidden = initializeIFSMeta+    newMeta Instance = newIFSMeta+    newMeta NotHidden = newIFSMeta  --------------------------------------------------------------------------- 

@@ -111,14 +111,6 @@         handle (TypeError _ (Closure {clValue = InternalError _})) = return Nothing         handle err                                                 = throwError err --- | @initializeIFSMeta s t@ generates an instance meta of type @t@---   with suggested name @s@, possibly with leading lambdas.-initializeIFSMeta :: String -> Type -> TCM Term-initializeIFSMeta s t = do-  t <- reduce t  -- see Issue 1321-  cands <- initialIFSCandidates t-  newIFSMeta s t cands- -- | @findInScope m (v,a)s@ tries to instantiate on of the types @a@s --   of the candidate terms @v@s to the type @t@ of the metavariable @m@. --   If successful, meta @m@ is solved with the instantiation of @v@.@@ -169,6 +161,7 @@       reportSDoc "tc.instance" 70 $ nest 2 $ vcat         [ sep [ prettyTCM v <+> text ":", nest 2 $ prettyTCM t ] | Candidate v t _ <- cands ]       t <- normalise =<< getMetaTypeInContext m+      insidePi t $ \ t -> do       reportSDoc "tc.instance" 15 $ text "findInScope 3: t =" <+> prettyTCM t       reportSLn "tc.instance" 70 $ "findInScope 3: t: " ++ show t @@ -177,6 +170,7 @@       ifJustM (areThereNonRigidMetaArguments (unEl t)) (\ m -> return (Just (cands, Just m))) $ do          mcands <- checkCandidates m t cands+        debugConstraints         case mcands of            Just [] -> do@@ -192,6 +186,10 @@               , text "for type" <+> prettyTCM t               ] +            -- If we actually solved the constraints we should wake up any held+            -- instance constraints, to make sure we don't forget about them.+            wakeConstraints (return . const True)+            solveAwakeConstraints' False             return Nothing  -- We’re done            _ -> do@@ -201,6 +199,22 @@               prettyTCM (List.map candidateTerm cs)             return (Just (cs, Nothing)) +-- | Precondition: type is spine reduced and ends in a Def or a Var.+insidePi :: Type -> (Type -> TCM a) -> TCM a+insidePi t ret =+  case ignoreSharing $ unEl t of+    Pi a b     -> addContext (absName b, a) $ insidePi (unAbs b) ret+    Def{}      -> ret t+    Var{}      -> ret t+    Sort{}     -> __IMPOSSIBLE__+    Con{}      -> __IMPOSSIBLE__+    Lam{}      -> __IMPOSSIBLE__+    Lit{}      -> __IMPOSSIBLE__+    Level{}    -> __IMPOSSIBLE__+    MetaV{}    -> __IMPOSSIBLE__+    Shared{}   -> __IMPOSSIBLE__+    DontCare{} -> __IMPOSSIBLE__+ -- | A meta _M is rigidly constrained if there is a constraint _M us == D vs, -- for inert D. Such metas can safely be instantiated by recursive instance -- search, since the constraint limits the solution space.@@ -309,18 +323,21 @@ --   If the resulting list contains exactly one element, then the state is the --   same as the one obtained after running the corresponding computation. In --   all the other cases, the state is reseted.-filterResetingState :: MetaId -> [Candidate] -> (Candidate -> TCM Bool) -> TCM [Candidate]+filterResetingState :: MetaId -> [Candidate] -> (Candidate -> TCM YesNoMaybe) -> TCM [Candidate] filterResetingState m cands f = disableDestructiveUpdate $ do   ctxArgs  <- getContextArgs   let ctxElims = map Apply ctxArgs       tryC c = do         ok <- f c         v  <- instantiateFull (MetaV m ctxElims)-        a  <- instantiateFull =<< (`piApply` ctxArgs) <$> getMetaType m+        a  <- instantiateFull =<< (`piApplyM` ctxArgs) =<< getMetaType m         return (ok, v, a)   result <- mapM (\c -> do bs <- localTCStateSaving (tryC c); return (c, bs)) cands-  let result' = [ (c, v, a, s) | (c, ((True, v, a), s)) <- result ]-  result <- dropSameCandidates m result'+  let result' = [ (c, v, a, s) | (c, ((r, v, a), s)) <- result, r /= No ]+      noMaybes = null [ Maybe | (_, ((Maybe, _, _), _)) <- result ]+            -- It's not safe to compare maybes for equality because they might+            -- not have instantiated at all.+  result <- if noMaybes then dropSameCandidates m result' else return result'   case result of     [(c, _, _, s)] -> [c] <$ put s     _              -> return [ c | (c, _, _, _) <- result ]@@ -355,12 +372,16 @@                              {- else -} (\ _ -> return False)                              `catchError` (\ _ -> return False) +data YesNoMaybe = Yes | No | Maybe+  deriving (Show, Eq)+ -- | Given a meta @m@ of type @t@ and a list of candidates @cands@, -- @checkCandidates m t cands@ returns a refined list of valid candidates. checkCandidates :: MetaId -> Type -> [Candidate] -> TCM (Maybe [Candidate]) checkCandidates m t cands = disableDestructiveUpdate $   verboseBracket "tc.instance.candidates" 20 ("checkCandidates " ++ prettyShow m) $-  ifM (anyMetaTypes cands) (return Nothing) $ Just <$> do+  ifM (anyMetaTypes cands) (return Nothing) $+  holdConstraints (\ _ -> isIFSConstraint . clValue . theConstraint) $ Just <$> do     reportSDoc "tc.instance.candidates" 20 $ nest 2 $ text "target:" <+> prettyTCM t     reportSDoc "tc.instance.candidates" 20 $ nest 2 $ vcat       [ text "candidates"@@ -379,14 +400,15 @@         MetaV{} -> return True         _       -> anyMetaTypes cands -    checkCandidateForMeta :: MetaId -> Type -> Candidate -> TCM Bool+    checkCandidateForMeta :: MetaId -> Type -> Candidate -> TCM YesNoMaybe     checkCandidateForMeta m t (Candidate term t' eti) = do       -- Andreas, 2015-02-07: New metas should be created with range of the       -- current instance meta, thus, we set the range.       mv <- lookupMeta m       setCurrentRange mv $ do-        verboseBracket "tc.instance" 20 ("checkCandidateForMeta " ++ prettyShow m) $ do-          liftTCM $ flip catchError handle $ do+        debugConstraints+        verboseBracket "tc.instance" 20 ("checkCandidateForMeta " ++ prettyShow m) $+          liftTCM $ runCandidateCheck $ do             reportSLn "tc.instance" 70 $ "  t: " ++ show t ++ "\n  t':" ++ show t' ++ "\n  term: " ++ show term ++ "."             reportSDoc "tc.instance" 20 $ vcat               [ text "checkCandidateForMeta"@@ -415,24 +437,37 @@             -- unsolvable by the assignment, but don't do this for FindInScope's             -- to prevent loops. We currently also ignore UnBlock constraints             -- to be on the safe side.+            debugConstraints             solveAwakeConstraints' True+             verboseS "tc.instance" 15 $ do               sol <- instantiateFull (MetaV m ctxElims)-              reportSDoc "tc.instance" 15 $-                sep [ text "instance search: found solution for" <+> prettyTCM m <> text ":"-                    , nest 2 $ prettyTCM sol ]-            return True+              case sol of+                MetaV m' _ | m == m' ->+                  reportSDoc "tc.instance" 15 $+                    sep [ text "instance search: maybe solution for" <+> prettyTCM m <> text ":"+                        , nest 2 $ prettyTCM v ]+                _ ->+                  reportSDoc "tc.instance" 15 $+                    sep [ text "instance search: found solution for" <+> prettyTCM m <> text ":"+                        , nest 2 $ prettyTCM sol ]         where-          handle :: TCErr -> TCM Bool+          runCandidateCheck check =+            flip catchError handle $+            ifNoConstraints_ check+              (return Yes)+              (\ _ -> Maybe <$ reportSLn "tc.instance" 50 "assignment inconclusive")++          handle :: TCErr -> TCM YesNoMaybe           handle err = do             reportSDoc "tc.instance" 50 $               text "assignment failed:" <+> prettyTCM err-            return False+            return No -    isIFSConstraint :: Constraint -> Bool-    isIFSConstraint FindInScope{} = True-    isIFSConstraint UnBlock{}     = True -- otherwise test/fail/Issue723 loops-    isIFSConstraint _             = False+isIFSConstraint :: Constraint -> Bool+isIFSConstraint FindInScope{} = True+isIFSConstraint UnBlock{}     = True -- otherwise test/fail/Issue723 loops+isIFSConstraint _             = False  -- | To preserve the invariant that a constructor is not applied to its --   parameter arguments, we explicitly check whether function term

@@ -1,7 +0,0 @@--module Agda.TypeChecking.InstanceArguments where--import Agda.TypeChecking.Monad.Base (TCM)-import Agda.Syntax.Internal (Type, Term)--initializeIFSMeta :: String -> Type -> TCM Term

@@ -177,20 +177,19 @@ -- newTypeMeta_  = newTypeMeta Inf  -- | @newIFSMeta s t cands@ creates a new "implicit from scope" metavariable---   of type the output type of @t@ with name suggestion @s@ and initial---   solution candidates @cands@. If @t@ is a function type, then insert enough+--   of type the output type of @t@ with name suggestion @s@.+--   If @t@ is a function type, then insert enough --   lambdas in front of it.-newIFSMeta :: MetaNameSuggestion -> Type -> Maybe [Candidate] -> TCM Term-newIFSMeta s t cands = do+newIFSMeta :: MetaNameSuggestion -> Type -> TCM Term+newIFSMeta s t = do   TelV tel t' <- telView t   addCtxTel tel $ do     vs  <- getContextArgs     ctx <- getContextTelescope-    teleLam tel <$> newIFSMetaCtx s (telePi_ ctx t') vs (raise (size tel) cands)+    teleLam tel <$> newIFSMetaCtx s (telePi_ ctx t') vs --- | Create a new value meta with specific dependencies.-newIFSMetaCtx :: MetaNameSuggestion -> Type -> Args -> Maybe [Candidate] -> TCM Term-newIFSMetaCtx s t vs cands = do+newIFSMetaCtx :: MetaNameSuggestion -> Type -> Args -> TCM Term+newIFSMetaCtx s t vs = do   reportSDoc "tc.meta.new" 50 $ fsep     [ text "new ifs meta:"     , nest 2 $ prettyTCM vs <+> text "|-"@@ -203,11 +202,11 @@   reportSDoc "tc.meta.new" 50 $ fsep     [ nest 2 $ pretty x <+> text ":" <+> prettyTCM t     ]-  addConstraint $ FindInScope x Nothing cands+  addConstraint $ FindInScope x Nothing Nothing   etaExpandMetaSafe x   return $ MetaV x $ map Apply vs -+-- | Create a new value meta with specific dependencies. newNamedValueMeta :: RunMetaOccursCheck -> MetaNameSuggestion -> Type -> TCM Term newNamedValueMeta b s t = do   v <- newValueMeta b t

@@ -12,7 +12,7 @@ etaExpandMetaSafe :: MetaId -> TCM () assignV           :: CompareDirection -> MetaId -> Args -> Term -> TCM () assign            :: CompareDirection -> MetaId -> Args -> Term -> TCM ()-newIFSMeta        :: String -> Type -> Maybe [Candidate] -> TCM Term+newIFSMeta        :: String -> Type -> TCM Term newValueMeta      :: RunMetaOccursCheck -> Type -> TCM Term newNamedValueMeta :: RunMetaOccursCheck -> String -> Type -> TCM Term newTelMeta        :: Telescope -> TCM Args

@@ -713,8 +713,8 @@ type Constraints = [ProblemConstraint]  data ProblemConstraint = PConstr-  { constraintProblem :: ProblemId-  , theConstraint     :: Closure Constraint+  { constraintProblems :: [ProblemId]+  , theConstraint      :: Closure Constraint   }   deriving (Typeable, Show) 

@@ -16,6 +16,7 @@ import Agda.Utils.Lens import Agda.Utils.List import Agda.Utils.Monad+import Agda.Utils.Except  #include "undefined.h" import Agda.Utils.Impossible@@ -30,21 +31,26 @@   current <- currentProblem   reportSLn "tc.constr.steal" 50 $ "problem " ++ show current ++ " is stealing problem " ++ show pid ++ "'s constraints!"   -- Rename @pid@ to @current@ in all constraints.-  let rename pc@(PConstr pid' c) | pid' == pid = PConstr current c-                                 | otherwise   = pc+  let rename pc@(PConstr pids c) | elem pid pids = PConstr (current : pids) c+                                 | otherwise     = pc   -- We should never steal from an active problem.   whenM (elem pid <$> asks envActiveProblems) __IMPOSSIBLE__   modifyAwakeConstraints    $ List.map rename   modifySleepingConstraints $ List.map rename  solvingProblem :: ProblemId -> TCM a -> TCM a-solvingProblem pid m = verboseBracket "tc.constr.solve" 50 ("working on problem " ++ show pid) $ do-  x <- local (\e -> e { envActiveProblems = pid : envActiveProblems e }) m-  ifNotM (isProblemSolved pid)-    (reportSLn "tc.constr.solve" 50 $ "problem " ++ show pid ++ " was not solved.")-    $ {- else -} do-      reportSLn "tc.constr.solve" 50 $ "problem " ++ show pid ++ " was solved!"-      wakeConstraints (return . blockedOn pid . clValue . theConstraint)+solvingProblem pid = solvingProblems [pid]++solvingProblems :: [ProblemId] -> TCM a -> TCM a+solvingProblems pids m = verboseBracket "tc.constr.solve" 50 ("working on problems " ++ show pids) $ do+  x <- local (\e -> e { envActiveProblems = pids ++ envActiveProblems e }) m+  sequence_+    [ ifNotM (isProblemSolved pid)+        (reportSLn "tc.constr.solve" 50 $ "problem " ++ show pid ++ " was not solved.")+      $ {- else -} do+        reportSLn "tc.constr.solve" 50 $ "problem " ++ show pid ++ " was solved!"+        wakeConstraints (return . blockedOn pid . clValue . theConstraint)+    | pid <- pids ]   return x   where     blockedOn pid (Guarded _ pid') = pid == pid'@@ -53,10 +59,10 @@ isProblemSolved :: ProblemId -> TCM Bool isProblemSolved pid =   and2M (notElem pid <$> asks envActiveProblems)-        (all ((/= pid) . constraintProblem) <$> getAllConstraints)+        (all (notElem pid . constraintProblems) <$> getAllConstraints)  getConstraintsForProblem :: ProblemId -> TCM Constraints-getConstraintsForProblem pid = List.filter ((== pid) . constraintProblem) <$> getAllConstraints+getConstraintsForProblem pid = List.filter (elem pid . constraintProblems) <$> getAllConstraints  -- | Get the awake constraints getAwakeConstraints :: TCM Constraints@@ -67,8 +73,8 @@   c <- use stSleepingConstraints   (wakeup, sleepin) <- partitionM wake c   reportSLn "tc.constr.wake" 50 $-    "waking up         " ++ show (List.map constraintProblem wakeup) ++ "\n" ++-    "  still sleeping: " ++ show (List.map constraintProblem sleepin)+    "waking up         " ++ show (List.map constraintProblems wakeup) ++ "\n" +++    "  still sleeping: " ++ show (List.map constraintProblems sleepin)   modifySleepingConstraints $ const sleepin   modifyAwakeConstraints (++ wakeup) @@ -92,6 +98,23 @@   modifySleepingConstraints $ (++ awakeOnes)   modifyAwakeConstraints    $ const [] +data ConstraintStatus = AwakeConstraint | SleepingConstraint+  deriving (Eq, Show)++-- | Suspend constraints matching the predicate during the execution of the+--   second argument. Caution: held sleeping constraints will not be woken up+--   by events that would normally trigger a wakeup call.+holdConstraints :: (ConstraintStatus -> ProblemConstraint -> Bool) -> TCM a -> TCM a+holdConstraints p m = do+  (holdAwake, stillAwake)   <- partition (p AwakeConstraint)    <$> use stAwakeConstraints+  (holdAsleep, stillAsleep) <- partition (p SleepingConstraint) <$> use stSleepingConstraints+  stAwakeConstraints    .= stillAwake+  stSleepingConstraints .= stillAsleep+  let restore = do+        stAwakeConstraints    %= (holdAwake ++)+        stSleepingConstraints %= (holdAsleep ++)+  catchError (m <* restore) (\ err -> restore *> throwError err)+ takeAwakeConstraint :: TCM (Maybe ProblemConstraint) takeAwakeConstraint = do   cs <- getAwakeConstraints@@ -105,15 +128,15 @@ getAllConstraints = gets $ \s -> s^.stAwakeConstraints ++ s^.stSleepingConstraints  withConstraint :: (Constraint -> TCM a) -> ProblemConstraint -> TCM a-withConstraint f (PConstr pid c) = do+withConstraint f (PConstr pids c) = do   -- We should preserve the problem stack and the isSolvingConstraint flag-  (pids, isSolving) <- asks $ envActiveProblems &&& envSolvingConstraints+  (pids', isSolving) <- asks $ envActiveProblems &&& envSolvingConstraints   enterClosure c $ \c ->-    local (\e -> e { envActiveProblems = pids, envSolvingConstraints = isSolving }) $-    solvingProblem pid (f c)+    local (\e -> e { envActiveProblems = pids', envSolvingConstraints = isSolving }) $+    solvingProblems pids (f c)  buildProblemConstraint :: ProblemId -> Constraint -> TCM ProblemConstraint-buildProblemConstraint pid c = PConstr pid <$> buildClosure c+buildProblemConstraint pid c = PConstr [pid] <$> buildClosure c  buildConstraint :: Constraint -> TCM ProblemConstraint buildConstraint c = flip buildProblemConstraint c =<< currentProblem

@@ -221,7 +221,7 @@   prettyTCM UnusedArg  = empty  instance PrettyTCM ProblemConstraint where-  prettyTCM (PConstr pid c) = brackets (prettyTCM pid) <+> prettyTCM c+  prettyTCM (PConstr pid c) = prettyList (map prettyTCM pid) <+> prettyTCM c  instance PrettyTCM Constraint where     prettyTCM c = case c of

@@ -602,10 +602,10 @@             reportSDoc "tc.lhs.unify" 80 $ text "Type of constructor: " <+> prettyTCM ctype             withMetaInfo' mv $ do               let perm = mvPermutation mv-              tel <- permuteTel perm <$> getContextTelescope+              tel <- permuteTel perm <$> (instantiateFull =<< getContextTelescope)               reportSDoc "tc.lhs.unify" 100 $ text "Context tel (for new metas): " <+> prettyTCM tel               -- important: create the meta in the same environment as the original meta-              newArgsMetaCtx ctype tel (mvPermutation mv) us+              newArgsMetaCtx ctype tel perm us           reportSDoc "tc.lhs.unify" 80 $ text "Generated meta args: " <+> prettyTCM margs           noConstraints $ assignV DirEq m us (Con c margs)           return $ Just margs

@@ -1,6 +1,8 @@ {-# LANGUAGE CPP                       #-}+{-# LANGUAGE DeriveDataTypeable        #-} {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE FlexibleInstances         #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE ScopedTypeVariables       #-}  #if __GLASGOW_HASKELL__ >= 710@@ -13,7 +15,7 @@  {-# OPTIONS_GHC -fno-warn-orphans #-} -module Agda.TypeChecking.Serialise.Instances.Common where+module Agda.TypeChecking.Serialise.Instances.Common () where  import Control.Applicative import Control.Monad.Reader@@ -33,6 +35,7 @@ import qualified Data.Set as Set import Data.Sequence (Seq) import qualified Data.Sequence as Seq+import Data.Typeable (Typeable) import Data.Void  import Agda.Syntax.Common@@ -224,10 +227,25 @@     valu [p, q] = valu2 P.Interval p q     valu _      = malformed +-- | Ranges are always deserialised as 'noRange'.+ instance EmbPrj Range where-  icod_ r = icode (P.rangeFile r, P.rangeIntervals r)-  value r = uncurry P.intervalsToRange `fmap` value r+  icod_ _ = icode0'+  value _ = return noRange +-- | Ranges that should be serialised properly.++newtype SerialisedRange = SerialisedRange { underlyingRange :: Range }+  deriving (Typeable)++instance EmbPrj SerialisedRange where+  icod_ (SerialisedRange r) =+    icode2' (P.rangeFile r) (P.rangeIntervals r)++  value = vcase valu where+    valu [a, b] = SerialisedRange <$> valu2 P.intervalsToRange a b+    valu _      = malformed+ instance EmbPrj C.Name where   icod_ (C.NoName a b) = icode2 0 a b   icod_ (C.Name r xs)  = icode2' r xs@@ -322,10 +340,12 @@   value n           = A.MName `fmap` value n  instance EmbPrj A.Name where-  icod_ (A.Name a b c d) = icodeMemo nameD nameC a $ icode4' a b c d+  icod_ (A.Name a b c d) = icodeMemo nameD nameC a $+    icode4' a b (SerialisedRange c) d    value = vcase valu where-    valu [a, b, c, d] = valu4 A.Name a b c d+    valu [a, b, c, d] = valu4 (\a b c -> A.Name a b (underlyingRange c))+                              a b c d     valu _            = malformed  instance EmbPrj a => EmbPrj (C.FieldAssignment' a) where