[ #3435 ] postpone instance constraints while checking applications

src/full/Agda/TypeChecking/Constraints.hs

@@ -151,7 +151,10 @@ solveAwakeConstraints :: TCM ()
 solveAwakeConstraints = solveAwakeConstraints' False
 
 solveAwakeConstraints' :: Bool -> TCM ()
-solveAwakeConstraints' force = do
+solveAwakeConstraints' = solveSomeAwakeConstraints (const True)
+
+solveSomeAwakeConstraints :: (ProblemConstraint -> Bool) -> Bool -> TCM ()
+solveSomeAwakeConstraints solveThis force = do
     verboseS "profile.constraints" 10 $ liftTCM $ tickMax "max-open-constraints" . List.genericLength =<< getAllConstraints
     whenM ((force ||) . not <$> isSolvingConstraints) $ nowSolvingConstraints $ do
      -- solveSizeConstraints -- Andreas, 2012-09-27 attacks size constrs too early
@@ -163,7 +166,7 @@ solveAwakeConstraints' force = do
       reportSDoc "tc.constr.solve" 10 $ hsep [ "Solving awake constraints."
                                              , text . show . length =<< getAwakeConstraints
                                              , "remaining." ]
-      whenJustM takeAwakeConstraint $ \ c -> do
+      whenJustM (takeAwakeConstraint' solveThis) $ \ c -> do
         withConstraint solveConstraint c
         solve
 

src/full/Agda/TypeChecking/Constraints.hs-boot

@@ -6,6 +6,7 @@ addConstraint          :: Constraint -> TCM ()
 catchConstraint        :: Constraint -> TCM () -> TCM ()
 solveConstraint        :: Constraint -> TCM ()
 solveAwakeConstraints' :: Bool -> TCM ()
+solveSomeAwakeConstraints :: (ProblemConstraint -> Bool) -> Bool -> TCM ()
 noConstraints          :: TCM a -> TCM a
 ifNoConstraints_       :: TCM () -> TCM a -> (ProblemId -> TCM a) -> TCM a
 guardConstraint        :: Constraint -> TCM () -> TCM ()

src/full/Agda/TypeChecking/InstanceArguments.hs

@@ -1,7 +1,11 @@
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE NondecreasingIndentation #-}
 
-module Agda.TypeChecking.InstanceArguments (findInstance, isInstanceConstraint) where
+module Agda.TypeChecking.InstanceArguments
+  ( findInstance
+  , isInstanceConstraint
+  , postponeInstanceConstraints
+  ) where
 
 #if MIN_VERSION_base(4,11,0)
 import Prelude hiding ((<>))
@@ -461,6 +465,13 @@ isConsideringInstance = (^. stConsideringInstance) <$> getTCState
 nowConsideringInstance :: (MonadTCState m) => m a -> m a
 nowConsideringInstance = locallyTCState stConsideringInstance $ const True
 
+postponeInstanceConstraints :: TCM a -> TCM a
+postponeInstanceConstraints m =
+  nowConsideringInstance m <* do
+    wakeConstraints (return . isInstance)
+    solveSomeAwakeConstraints isInstance False
+  where
+    isInstance = isInstanceConstraint . clValue . theConstraint
 
 -- | To preserve the invariant that a constructor is not applied to its
 --   parameter arguments, we explicitly check whether function term

src/full/Agda/TypeChecking/Monad/Constraints.hs

@@ -111,12 +111,15 @@ holdConstraints p m = do
   catchError (m <* restore) (\ err -> restore *> throwError err)
 
 takeAwakeConstraint :: TCM (Maybe ProblemConstraint)
-takeAwakeConstraint = do
+takeAwakeConstraint = takeAwakeConstraint' (const True)
+
+takeAwakeConstraint' :: (ProblemConstraint -> Bool) -> TCM (Maybe ProblemConstraint)
+takeAwakeConstraint' p = do
   cs <- getAwakeConstraints
-  case cs of
-    []     -> return Nothing
-    c : cs -> do
-      modifyAwakeConstraints $ const cs
+  case break p cs of
+    (_, [])       -> return Nothing
+    (cs0, c : cs) -> do
+      modifyAwakeConstraints $ const (cs0 ++ cs)
       return $ Just c
 
 getAllConstraints :: TCM Constraints

src/full/Agda/TypeChecking/Rules/Application.hs

@@ -45,6 +45,7 @@ import Agda.TypeChecking.Free
 import Agda.TypeChecking.Implicit
 import Agda.TypeChecking.Injectivity
 import Agda.TypeChecking.Irrelevance
+import Agda.TypeChecking.InstanceArguments (postponeInstanceConstraints)
 import Agda.TypeChecking.Level
 import Agda.TypeChecking.MetaVars
 import Agda.TypeChecking.Names
@@ -87,7 +88,7 @@ import Agda.Utils.Impossible
 --   (and continues to 'checkConstructorApplication')
 --   and resolves pattern synonyms.
 checkApplication :: Comparison -> A.Expr -> A.Args -> A.Expr -> Type -> TCM Term
-checkApplication cmp hd args e t = do
+checkApplication cmp hd args e t = postponeInstanceConstraints $ do
   reportSDoc "tc.check.app" 20 $ vcat
     [ "checkApplication"
     , nest 2 $ "hd   = " <+> prettyA hd
@@ -217,7 +218,7 @@ inferApplication exh hd args e | not (defOrVar hd) = do
   t <- workOnTypes $ newTypeMeta_
   v <- checkExpr' CmpEq e t
   return (v, t)
-inferApplication exh hd args e =
+inferApplication exh hd args e = postponeInstanceConstraints $
   case unScope hd of
     A.Proj o p | isAmbiguous p -> inferProjApp e o (unAmbQ p) args
     _ -> do
@@ -603,7 +604,7 @@ checkArguments_
   -> Telescope            -- ^ Telescope to check arguments against.
   -> TCM (Elims, Telescope)
      -- ^ Checked arguments and remaining telescope if successful.
-checkArguments_ exh r args tel = do
+checkArguments_ exh r args tel = postponeInstanceConstraints $ do
     z <- runExceptT $
       checkArgumentsE exh r args (telePi tel __DUMMY_TYPE__) Nothing
     case z of
@@ -621,7 +622,7 @@ checkArguments_ exh r args tel = do
 checkArguments ::
   ExpandHidden -> Range -> [NamedArg A.Expr] -> Type -> Type ->
   (Elims -> Type -> CheckedTarget -> TCM Term) -> TCM Term
-checkArguments exph r args t0 t k = do
+checkArguments exph r args t0 t k = postponeInstanceConstraints $ do
   z <- runExceptT $ checkArgumentsE exph r args t0 (Just t)
   case z of
     Right (vs, t1, pid) -> k vs t1 pid

test/Fail/Issue2993.err

@@ -1,14 +1,4 @@
 Failed to solve the following constraints:
-  Resolve instance argument
-    _AF_165
-      : {n = n₁ : Nat} {F : Set → Set} {A B : Set}
-        ⦃ AF : Applicative F ⦄ →
-        Applicative (λ v → _F_166 v)
-  Candidates
-    AF₁ : Applicative F₁
-    applicativeComp :
-      {F G : Set → Set} ⦃ _ : Applicative F ⦄ ⦃ _ : Applicative G ⦄ →
-      Applicative ((λ {a} → F) o G)
   Resolve instance argument
     _AF_153
       : {n = n₂ : Nat} {n = n₃ : Nat} {F = F₁ : Set → Set}
@@ -21,6 +11,16 @@ Failed to solve the following constraints:
       {F = F₁ : Set → Set} {G : Set → Set} ⦃ _ : Applicative F₁ ⦄
       ⦃ _ : Applicative G ⦄ →
       Applicative ((λ {a} → F₁) o G)
+  Resolve instance argument
+    _AF_165
+      : {n = n₁ : Nat} {F : Set → Set} {A B : Set}
+        ⦃ AF : Applicative F ⦄ →
+        Applicative (λ v → _F_166 v)
+  Candidates
+    AF₁ : Applicative F₁
+    applicativeComp :
+      {F G : Set → Set} ⦃ _ : Applicative F ⦄ ⦃ _ : Applicative G ⦄ →
+      Applicative ((λ {a} → F) o G)
   _167 := λ {n} {F} {A} {B} ⦃ AF ⦄ → vtr [blocked on problem 242]
   [242, 243] F₁ B₁ =< _F_166 _B_164 : Set
   [242] _F_166 (Vec _B_164 n) =< F₁ (Vec B₁ n) : Set