[ fix #3672 ] prune unsolved metas that are not generalized over

also fixes #3655 and fixes #3673 which are the same issue

src/full/Agda/TypeChecking/Generalize.hs

@@ -21,6 +21,7 @@ import Agda.Syntax.Common
 import Agda.Syntax.Concrete.Name (LensInScope(..))
 import Agda.Syntax.Position
 import Agda.Syntax.Internal
+import Agda.Syntax.Internal.Generic
 import Agda.Syntax.Literal
 import Agda.Syntax.Scope.Monad (bindVariable)
 import Agda.Syntax.Scope.Base (Binder(..))
@@ -169,7 +170,7 @@ computeGeneralization genRecMeta nameMap allmetas = postponeInstanceConstraints
   let (generalizable, nongeneralizable)         = partition isGeneralizable mvs
       (generalizableOpen', generalizableClosed) = partition isOpen generalizable
       (openSortMetas, generalizableOpen)        = partition isSort generalizableOpen'
-      nongeneralizableOpen                      = filter isOpen nongeneralizable
+      nongeneralizableOpen                      = filter (not . isSort) $ filter isOpen nongeneralizable
 
   -- Issue 3301: We can't generalize over sorts
   case openSortMetas of
@@ -224,9 +225,15 @@ computeGeneralization genRecMeta nameMap allmetas = postponeInstanceConstraints
 
   let (alsoGeneralize, reallyDontGeneralize) = partition (`Set.member` inherited) $ map fst nongeneralizableOpen
       generalizeOver = map fst generalizableOpen ++ alsoGeneralize
+      shouldGeneralize = (`Set.member` Set.fromList generalizeOver)
 
-  -- Sort metas in dependency order
-  sortedMetas <- sortMetas generalizeOver
+  -- Sort metas in dependency order. Include open metas that we are not
+  -- generalizing over, since they will need to be pruned appropriately (see
+  -- Issue 3672).
+  allSortedMetas0 <- sortMetas (generalizeOver ++ reallyDontGeneralize)
+  let sortedMetas = filter shouldGeneralize allSortedMetas0
+      -- We can skip metas that depend on all the generalized variables.
+      allSortedMetas = reverse . dropWhile (not . shouldGeneralize) . reverse $ allSortedMetas0
 
   let dropCxt err = updateContext (strengthenS err 1) (drop 1)
 
@@ -257,9 +264,14 @@ computeGeneralization genRecMeta nameMap allmetas = postponeInstanceConstraints
           HasType{ jMetaType = t } = mvJudgement mv
       return [(Arg info $ miNameSuggestion $ mvInfo mv, piApply t args)]
   let genTel = buildGeneralizeTel genRecCon teleTypes
+
   reportSDoc "tc.generalize" 40 $ vcat
     [ text "genTel =" <+> prettyTCM genTel ]
 
+  -- Now we need to prune the unsolved metas to make sure they respect the new
+  -- dependencies (#3672).
+  pruneUnsolvedMetas genRecName genRecCon genTel genRecFields shouldGeneralize allSortedMetas
+
   -- Fill in the missing details of the telescope record.
   dropCxt __IMPOSSIBLE__ $ fillInGenRecordDetails genRecName genRecCon genRecFields genRecMeta genTel
 
@@ -402,6 +414,123 @@ computeGeneralization genRecMeta nameMap allmetas = postponeInstanceConstraints
 
   return (genTel, telNames, sub)
 
+-- | Prune unsolved metas (#3672). The input includes also the generalized
+--   metas and is sorted in dependency order. The telescope is the generalized
+--   telescope.
+pruneUnsolvedMetas :: QName -> ConHead -> Telescope -> [QName] -> (MetaId -> Bool) -> [MetaId] -> TCM ()
+pruneUnsolvedMetas genRecName genRecCon genTel genRecFields isGeneralized metas
+  | all isGeneralized metas = return ()
+  | otherwise               =
+    -- We start this in the context Γ (g : GenRec), but since we want to create
+    -- new metas not depending on GenRec we drop g from the context.
+    updateContext (strengthenS __IMPOSSIBLE__ 1) (drop 1) $
+      prune [] genTel metas
+  where
+    sub = unpackSub genRecCon $ map getArgInfo $ telToList genTel
+
+    -- It's possible that the meta has already been pruned, in which case
+    -- there's nothing to do. See test/Fail/Issue3274.agda for a test case.
+    getTypeOfMeta m = do
+      mTy <- instantiateFull =<< getMetaTypeInContext m
+      case unEl mTy of
+        Pi _A (Abs _ _B)
+          | Def q _ <- unEl $ unDom _A,
+            q == genRecName -> return $ Just (mTy, _B)
+        _ -> return Nothing
+
+    prune _ _ [] = return ()
+    prune cxt tel (m : ms) | not (isGeneralized m) =
+
+      caseMaybeM (getTypeOfMeta m) (prune cxt tel ms) $ \ (mTy, _B) -> do
+
+      -- We have
+      --   current context: Γ
+      --   Γ ⊢ m : (genTel : GenRec) → B
+      --   Γ ⊢ Δ is the telescope of the fields in scope of this meta
+      _Γ <- getContextTelescope
+      let rcxt = reverse cxt
+          _Δ   = telFromList rcxt
+
+      -- Now we want a fresh meta
+      --   Γ ⊢ β : Δ → Bσ    where Γ Δ ⊢ σ : Γ (g : GenRec)
+      --                           σ = unpackSub |Δ|
+      let σ    = sub (length cxt)
+          βty  = telePi _Δ $ applySubst σ _B
+      (_, β) <- newValueMeta DontRunMetaOccursCheck βty
+
+      -- and instantiate
+      --   m := λ r → β r.f₁ r.f₂ .. r.fᵢ
+      let mkArg dom f = Var 0 [Proj ProjSystem f] <$ argFromDom dom
+          args        = zipWith mkArg rcxt genRecFields
+          v           = Lam defaultArgInfo $ Abs "genTel" $ raise 1 β `apply` args
+      reportSDoc "tc.generalize.prune" 80 $ vcat
+        [ "pruning" <+> prettyTCM m <+> ":" <+> pretty _B
+        , nest 2 $ "Γ =" <+> pretty _Γ
+        , nest 2 $ "Δ =" <+> pretty _Δ
+        , nest 2 $ "σ =" <+> pretty σ
+        , nest 2 $ "β :" <+> pretty βty
+        , nest 2 $ "β =" <+> pretty β
+        , nest 2 $ "v =" <+> pretty v
+        ]
+
+      -- m might have been instantiated by some constraint unblocked by previous pruning or
+      -- generalization, so use equalTerm rather than assigning directly to m. If this fails (see
+      -- test/Fail/Issue3655b.agda for a test case), we need to give an error. This can happen if
+      -- there are dependencies between generalized variables that are hidden by constraints and the
+      -- dependency sorting happens to pick the wrong order. For instance, if we have
+      --    α : Nat   (unsolved meta)
+      --    t : F α   (named variable)
+      --    n : Nat   (named variable)
+      -- and a constraint F α == F n, where F does some pattern matching preventing the constraint
+      -- to be solved when n is still a meta. If t appears before n in the type these will be sorted
+      -- as α, t, n, but we will solve α := n before we get to the pruning here. It's good that we
+      -- solve first though, because that means we can give a more informative error message than
+      -- the "Cannot instantiate..." we would otherwise get.
+      xs <- getContextArgs
+      let u = MetaV m [] `apply` xs
+      reportSDoc "tc.generalize.prune" 80 $ nest 2 $ "m =" <+> (pretty =<< instantiateFull u)
+      noConstraints (equalTerm mTy u v) `catchError` \ _ -> do
+        u' <- instantiateFull u
+        let telList = telToList genTel
+            names   = map (fst . unDom) telList
+            late    = map (fst . unDom) $ filter (elem m . allMetas) telList
+            projs (Proj _ q)
+              | elem q genRecFields = Set.fromList [x | Just x <- [getGeneralizedFieldName q]]
+            projs _                 = Set.empty
+            early = Set.toList $ flip foldTerm u' $ \ case
+                    Var _ es   -> foldMap projs es
+                    Def _ es   -> foldMap projs es
+                    MetaV _ es -> foldMap projs es
+                    _          -> Set.empty
+            commas []       = __IMPOSSIBLE__
+            commas [x]      = x
+            commas [x, y]   = x ++ ", and " ++ y
+            commas (x : xs) = x ++ ", " ++ commas xs
+            cause = "There were unsolved constraints that obscured the " ++
+                    "dependencies between the generalized variables."
+            solution = "The most reliable solution is to provide enough information to make the dependencies " ++
+                       "clear, but simply mentioning the variables in the right order should also work."
+            order = sep [ fwords "Dependency analysis suggested this (likely incorrect) order:",
+                          nest 2 $ fwords (unwords names) ]
+            guess = "After constraint solving it looks like " ++ commas late ++ " actually depend" ++ s ++
+                    " on " ++ commas early
+              where
+                s | length late == 1 = "s"
+                  | otherwise        = ""
+        genericDocError =<< vcat
+          [ fwords $ "Variable generalization failed."
+          , nest 2 $ sep ["- Probable cause", nest 4 $ fwords cause]
+          , nest 2 $ sep ["- Suggestion", nest 4 $ fwords solution]
+          , nest 2 $ sep $ ["- Further information"
+                           , nest 2 $ "-" <+> order ] ++
+                           [ nest 2 $ "-" <+> fwords guess | not (null late), not (null early) ]
+          ]
+
+      prune cxt tel ms
+    prune cxt (ExtendTel a tel) (m : ms) = prune (fmap (x,) a : cxt) (unAbs tel) ms
+      where x = absName tel
+    prune _ _ _ = __IMPOSSIBLE__
+
 -- | Create a substition from a context where the i first record fields are variables to a context
 --   where you have a single variable of the record type. Packs up the field variables in a record
 --   constructor and pads with __DUMMY_TERM__s for the missing fields. Important that you apply this

test/Fail/Issue3340.err

@@ -1,8 +1,8 @@
 Failed to solve the following constraints:
   _49 := λ {x.A.ℓ} {x.A} {x} {f.P.ℓ} {f} → refl
-    [blocked on problem 29]
-  [29, 33] f x = _48 : _f.P_47 x
-  [22] _f.P_47 y =< _f.P_47 x : Set f.P.ℓ
+    [blocked on problem 30]
+  [30, 34] f x = _48 : _47 x
+  [22] _47 y =< _47 x : Set f.P.ℓ
   _45 := λ genTel → f y [blocked on problem 22]
 Unsolved metas at the following locations:
   Issue3340.agda:12,22-25

test/Fail/Issue3401.err

@@ -1,5 +1,5 @@
 Failed to solve the following constraints:
-  [11] _v.T_22 _v.i_23 =< _T_24 _i_25 : Set
+  [11] _22 _23 =< _T_24 _i_25 : Set
   _20 := λ {I} genTel → v [blocked on problem 11]
 Unsolved metas at the following locations:
   Issue3401.agda:12,7-8

test/Fail/Issue3655b.agda

@@ -0,0 +1,19 @@
+{-# OPTIONS --allow-unsolved-metas #-}
+
+open import Agda.Builtin.Bool
+
+postulate
+  A : Set
+
+F : Bool → Set
+F true  = A
+F false = A
+
+data D {b : Bool} (x : F b) : Set where
+
+variable
+  b : Bool
+  x : F b
+
+postulate
+  f : D x → (P : F b → Set) → P x

test/Fail/Issue3655b.err

@@ -0,0 +1,14 @@
+Issue3655b.agda:19,7-34
+Variable generalization failed.
+  - Probable cause
+      There were unsolved constraints that obscured the dependencies
+      between the generalized variables.
+  - Suggestion
+      The most reliable solution is to provide enough information to make
+      the dependencies clear, but simply mentioning the variables in the
+      right order should also work.
+  - Further information
+    - Dependency analysis suggested this (likely incorrect) order: x b
+    - After constraint solving it looks like x actually depends on b
+when checking that the expression D x → (P : F b → Set) → P x has
+type _9

test/Succeed/Issue3672.agda

@@ -0,0 +1,35 @@
+{-# OPTIONS --allow-unsolved-metas #-}
+
+data C (A : Set) : Set where
+  c : (x : A) → C A
+
+data D : Set where
+
+data E (A : Set) : Set where
+  e : A → E A
+
+postulate
+  F : {A : Set} → A → Set
+
+G : {A : Set} → C A → Set
+G (c x) = E (F x)
+
+postulate
+  H : {A : Set} → (A → Set) → C A → Set
+  f : {A : Set} {P : A → Set} {y : C A} → H P y → (x : A) → G y → P x
+  g : {A : Set} {y : C A} {P : A → Set} → ((x : A) → G y → P x) → H P y
+
+variable
+  A : Set
+  P : A → Set
+  x : A
+  y : C A
+
+postulate
+  h : {p : ∀ x → G y → P x} → (∀ x (g : G y) → F (p x g)) → F (g p)
+
+id : (A : Set) → A → A
+id _ x = x
+
+-- i : (h : H P y) → (∀ x (g : G y) → F (f h x g)) → F (g (f h))
+-- i x y = id (F (g (f x))) (h y)

test/Succeed/Issue3673.agda

@@ -0,0 +1,23 @@
+{-# OPTIONS --allow-unsolved-metas #-}
+
+postulate
+  A : Set
+
+data Unit : Set where
+  unit : Unit
+
+F : Unit → Set
+F unit = A
+
+postulate
+  P : {A : Set} → A → Set
+  Q : ∀ {x} → F x → Set
+  f : ∀ {x} {y : F x} (z : Q y) → P z
+
+variable
+  x : Unit
+  y : F x
+
+g : (z : Q y) → P z
+g z with f z
+... | p = p