Regression related to the auto command

[nad]

Martin Escardo reported that the hole in the following piece of code can be filled using the auto command when Agda 2.5.1.1 is used, but not with Agda 2.5.2:

-- Martin Escardo, 6 Jan 2017
-- The large propositional truncation is a large monad in a suitable sense.
--
-- Simplified 10 Jan 2017 to give an example to the Agda developers.

{-# OPTIONS --without-K #-}

module largemonad-simplified where

open import Agda.Primitive using (Level ; lzero ; lsuc ; _⊔_) public

id : {i : Level} {X : Set i} → X → X
id x = x

_∘_ : {i j k : Level} {X : Set i} {Y : Set j} {Z : Y → Set k}
      → ((y : Y) → Z y)
      → (f : X → Y) (x : X) → Z(f x)
g ∘ f = λ x → g(f x)

data _≡_ {i : Level} {A : Set i} : A → A → Set i where
 refl : (a : A) → a ≡ a

infix 6 _≡_

-- T : {i j : Level} → Set j → Set (j ⊔ lsuc i)
T : {i j : Level} → Set j → Set {!!}  -- HOLE HERE
T {i} {j} X = (P : Set i) → (X → P) → P

η : {i j : Level} {X : Set j} → X → T {i} {j} X
η x = λ _ u → u x

record Lift {i j : Level} (X : Set i) : Set (i ⊔ j) where
  constructor lift
  field lower : X

open Lift public


down : {i : Level} {X : Set i} → T {i} {i} X → X
down {i} {X} xt = xt X id

du : {i : Level} {X : Set i} (x : X) (P : Set i) (u : X → P)
   → down (η x) ≡ x
du {i} {X} x P u = refl x

T-extend : {i j k : Level} {X : Set j} {Y : Set k}
         → (X → T {i} {k} Y)
         → (T {i} {j} X → T {i} {k} Y)
T-extend f = λ xt P u → xt P (λ x → f x P u)

kleisli-law₀ : {i j : Level} {X : Set j}
            → T-extend η ≡ id
kleisli-law₀ {i} {j} {X} = refl (T-extend {i} {j} {j} {X} η)

kleisli-law₁ : {i j k : Level} {X : Set j} {Y : Set k}
               (f : X → T {i} {k} Y)
            → T-extend f ∘ η ≡ f
kleisli-law₁ f = refl f

kleisli-law₂ : {i j k l : Level} {X : Set j} {Y : Set k} {Z : Set l}
                (f : X → T {i} {k} Y)
                (g : Y → T {i} {l} Z)
             → T-extend(T-extend g ∘ f) ≡ (T-extend g) ∘ (T-extend f)
kleisli-law₂ f g = refl (λ xt P u → xt P (λ x → f x P (λ y → g y P u)))

μ : {i j : Level} {X : Set j}
  → T {i} {j ⊔ lsuc i} (T {i} {j} X) → T {i} {j} X
μ = T-extend(λ xt → xt)

μ-explicitly : {i j : Level} {X : Set j}
             → μ ≡ (λ xtt P u → xtt P (λ xt → xt P u))
μ-explicitly {i} {j} {X} = refl (μ {i} {j} {X})

T-functor : {i j k : Level} {X : Set j} {Y : Set k} → (X → Y) → (T {i} {j} X → T {i} {k} Y)
T-functor f = T-extend(η ∘ f)

[nad]

Here is a cut-down test case:

open import Agda.Primitive

A : Set {!!}
A = Set

The auto command's error message:

Cannot apply the auto tactic here, we are not in a function clause

[nad]

Bisection indicates that the problem was introduced by @andreasabel in 6a83085:

$ cat Bug.agda
open import Agda.Primitive

A : Set {!!}
A = Set
$ cat script
#!/bin/sh

AGDA=$1

$AGDA --interaction --ignore-interfaces <<EOF
IOTCM "Bug.agda" None Indirect (Cmd_load "Bug.agda" [])
IOTCM "Bug.agda" None Indirect (Cmd_auto 0 noRange "")
EOF
$ agda-bisect --bad v2.5.2 --good v2.5.1.1 --must-output '(agda2-give-action 0 "(lsuc lzero)")' --script ./script --log log --compiler [ghc-7.8.4]
[...]
6a83085da5d80720a79043ae4515e737131f3c27 is the first bad commit
commit 6a83085da5d80720a79043ae4515e737131f3c27
Author: Andreas Abel <andreas.abel@ifi.lmu.de>
Date:   Wed Jun 8 11:05:20 2016 +0200

    Fixed #1349 (was same problem as #289).

    Agsy now also no longer searches the whole signature to find the
    meta-variable it was invoked in.

[...]

[andreasabel]

I can see that I introduced the regression, but I do not understand why. How did the original code find the meta? It is only looking in function clauses. But the meta is in a type signature.
[My (new) code only looks in function clauses (and of course does not find it).]

[andreasabel]

@nad: It seems that I am struck by blindness. I cannot see how the code that I replaced in 6a83085 could have possibly worked for holes which are not in function clauses. Do you have a clue?

[nad]

I'm not familiar with this part of the code base. I have not checked the code carefully, so this is a guess: Perhaps some part of the body was blocked by an interaction meta, and the code found this meta.

[andreasabel]

@nad: In the test case you give, the interaction meta is part of a type signature. My code only looks for interaction metas in function clauses, thus, cannot refer to this meta. As far as I can tell, the old code also only looks inside function clauses (and there, not in sorts or sort annotations), so how can it possibly find it??

[andreasabel]

I can confirm that the blamed patch introduced the regression. However, I do not understand how.

Now I understand: Agsy is fine if findClauseDeep returns Nothing. My patch introduced an unnecessary error throwing.