Re #6097: checkApplication: retry check target analysis less eagerly.

[andreasabel]

Andreas & Ulf: Only retry the analysis (isRigid) whether it makes sense to check against the target first when there is evidence that it could be successful the next time.

So far, the bias was in the other direction: retry unless there was evidence it would not change.

Closes #6097, at least the OP (toy case, regression in 2.5.4).

NB: does not help with regression in 2.5.4 (serious case) reported in:

• #5066

[andreasabel]

An unsolved meta is introduced in the standard library: https://github.com/agda/agda-stdlib/blob/6f884ddd704cfff00d33744b40c13912ffce447b/src/Data/Vec/Properties.agda#L1319-L1320

fromList-reverse : (xs : List A) → cast (List.length-reverse xs) (fromList (List.reverse xs)) ≡ reverse (fromList xs)
fromList-reverse List.[] = refl
fromList-reverse (x List.∷ xs) = begin
  fromList (List.reverse (x List.∷ xs))         ≈⟨ cast-fromList (List.ʳ++-defn xs) ⟩
  fromList (List.reverse xs List.++ List.[ x ]) ≈⟨ fromList-++ (List.reverse xs) ⟩
  fromList (List.reverse xs) ++ [ x ]           ≈⟨ unfold-∷ʳ (+-comm 1 _) x (fromList (List.reverse xs)) ⟨
  fromList (List.reverse xs) ∷ʳ x               ≈⟨ ≈-cong (_∷ʳ x) (cast-∷ʳ (cong suc (List.length-reverse xs)) _ _)
                                                          (fromList-reverse xs) ⟩
  reverse (fromList xs) ∷ʳ x                    ≂⟨ reverse-∷ x (fromList xs) ⟨
  reverse (x ∷ fromList xs)                     ≈⟨⟩
  reverse (fromList (x List.∷ xs))              ∎
  where open CastReasoning

The proof ≈-cong (_∷ʳ x) (cast-∷ʳ (cong suc (List.length-reverse xs)) _ _) (fromList-reverse xs) solves this meta but the type checker keeps it yellow.

Would be good to harvest a test case from this.