Solving blocked terms loses the user-written code

[nad]

Consider the following code:

postulate
  A  : Set
  F  : Set → Set
  P  : F A → Set
  id : F A → F A

f : (x : F A) → P x → P x
f _ p = p

⟨_⟩ : F A → F A
⟨ x ⟩ = x

{-# NOINLINE ⟨_⟩ #-}

record R (F : Set → Set) : Set₁ where
  field
    g : F A → F A

open R ⦃ … ⦄

postulate
  instance
    r : R F

works : (x : F A) → P x
works x = f ⟨ x ⟩ ?

also-works : (x : F A) → P (id x)
also-works x = f (id ⟨ x ⟩) ?

fails : (x : F A) → P (g x)
fails x = f (g ⟨ x ⟩) ?

The three goal types:

?0 : P ⟨ x ⟩
?1 : P (id ⟨ x ⟩)
?2 : P (R.g r x)

Note that the final goal contains x instead of ⟨ x ⟩. This is unfortunate, because some tactics rely on being able to mark subterms in this way (see, for instance, Bradley Hardy's (@bch29) library holes).

This is a regression, Agda 2.5.4.2 computes the following goal types:

?0 : P ⟨ x ⟩
?1 : P (id ⟨ x ⟩)
?2 : P (R.g r ⟨ x ⟩)

[nad]

Bisection points to 47358b3 ("[ #3435 ] postpone instance constraints while checking applications").

[UlfNorell]

The culprit here is the way we handle blocked terms.

When the user writes a term t : A and we expect something of type B, but A = B cannot be solved at the moment, we replace t by a fresh meta variable X : B and add a constraint X = t guarded by A = B. Thus once we know A = B we can go ahead and solve X = t. However, X is a free metavariable that can be solved by unification. For instance, unification might solve X := t' and then once we know A = B we'd check t' = t. In this case we end up with the result t' : A instead of the t that the user wrote.

This makes constraint solving more robust, according to this comment:

agda/src/full/Agda/TypeChecking/MetaVars.hs

Lines 391 to 394 in 4af7b92

	-- We don't return the blocked term instead create a fresh metavariable
	-- that we compare against the blocked term once it's unblocked. This way
	-- blocked terms can be instantiated before they are unblocked, thus making
	-- constraint solving a bit more robust against instantiation order.

However, I can't construct an example were it makes an important difference. Disabling it makestest/Fail/Issue1427.agda gives unsolved constraints instead of a type error, which doesn't seem too bad.

I'll turn it off and run through the complete test suite.

[UlfNorell]

Test suite goes through, but I get a bunch of unsolved constraints in http://www.cse.chalmers.se/~nad/repos/equality/ (master@da311d9). @nad can you check the issue4067 branch and see if those constraints are reasonable?

Some of them might print funny (e.g. section = section) since @Saizan's change to instantiate blocked terms before printing constraints, but ignore those.

[nad]

That file is easy to fix, just replace

cong (_ ,_) (trans (sym $ subst-refl _ _) (subst-refl _ _))  ≡⟨ cong (cong _) (trans-symˡ _) ⟩

with the following line (and add {p = p} to the left-hand side):

cong (_ ,_) (trans (sym $ subst-refl _ _) (subst-refl _ _))  ≡⟨ cong (cong (proj₁ p ,_)) (trans-symˡ _) ⟩

However, fixing the lemma dcong≡hcong in Equality.Path.Isomorphisms is less trivial. The following code type-checks quickly:

dcong≡hcong :
  {x≡y : x P.≡ y} (f : (x : A) → B x) →
  dcong f (_↔_.from ≡↔≡ x≡y) ≡ _↔_.from subst≡↔[]≡ (P.hcong f x≡y)
dcong≡hcong {B = B} {x≡y = x≡y} f =
  dcong f (_↔_.from ≡↔≡ x≡y)                                     ≡⟨ sym $ _↔_.from-to (inverse subst≡↔subst≡) {!dcong≡dcong!} ⟩

  _↔_.from subst≡↔subst≡ (P.dcong f x≡y)                         ≡⟨ cong (_↔_.from subst≡↔subst≡) $ _↔_.from ≡↔≡ $ P.dcong≡hcong f ⟩

  _↔_.from (subst≡↔subst≡ {B = B})
    (PB._↔_.to (P.heterogeneous↔homogeneous _) (P.hcong f x≡y))  ≡⟨⟩

  _↔_.from subst≡↔[]≡ (P.hcong f x≡y)                            ∎

If I fill the hole with the given term, then Agda quickly accepts the code. However, reloading takes a lot of time, or fails to terminate.

[nad]

An aside: If I turn on --no-syntactic-equality, then there are unsolved constraints in many type signatures in that file. The option is described as a shortcut, and I thought that the idea was that, ignoring efficiency (and reflection, I guess), Agda should behave exactly the same with --no-syntactic-equality on or off. However, perhaps that is too much to hope for.

[nad]

I opened a new ticket for the issue with --no-syntactic-equality (#4265).

[UlfNorell]

This might be worthwhile, but since it's a non-trivial change of the internals I'm not comfortable doing it so close to the release.

Also, it's not really a regression. Different versions of Agda will just drop the user code in different cases, so bumping it to 2.6.2 is the right move.

[nad]

Is it time to go ahead with this change now?

Here is another test case:

{-# OPTIONS --cubical #-}

open import Agda.Builtin.Cubical.Path

postulate
  trans : {A : Set} {x y z : A} → x ≡ y → y ≡ z → x ≡ z

infix  -1 finally
infixr -2 _≡⟨⟩_

_≡⟨⟩_ : {A : Set} (x {y} : A) → x ≡ y → x ≡ y
_ ≡⟨⟩ x≡y = x≡y

finally : {A : Set} (x y : A) → x ≡ y → x ≡ y
finally _ _ x≡y = x≡y

syntax finally x y x≡y = x ≡⟨ x≡y ⟩∎ y ∎

⟨_⟩ : {A : Set} → A → A
⟨ x ⟩ = x

{-# NOINLINE ⟨_⟩ #-}

record R (F : Set → Set) : Set₁ where
  field
    p : {A : Set} {x : F A} → x ≡ x

open R ⦃ … ⦄ public

test :
  {F : Set → Set} ⦃ r : R F ⦄ {A : Set} {x₁ x₂ : F A}
  (p₁ p₂ : x₁ ≡ x₂) (assumption : p₁ ≡ p₂) →
  trans p p₁ ≡ trans p p₂
test p₁ p₂ assumption =
  trans p p₁      ≡⟨⟩
  trans p ⟨ p₁ ⟩  ≡⟨ ? ⟩∎
  trans p p₂      ∎

[nad]

I'm trying to merge the master branch into the issue4067 branch.

[nad]

@vlopezj, how would Tog handle this situation?

[nad]

I'm not convinced that it makes sense to fix this issue by making constraint solving less robust. However, I do think it makes sense to preserve user-written code.

Is it possible to construct an example in which Agda replaces code (4, say) with less efficient but definitionally equal code (like primForce (fib 25) (λ _ → 4))? A more realistic example might involve code which is expected to be optimised by GHC's rewrite rule machinery.

[nad]

I'm trying to merge the master branch into the issue4067 branch.

Done.

[vlopezj]

@vlopezj, how would Tog handle this situation?

@nad The blocking mechanism in Tog is the same as Ulf describes, so you could have the same issues there.

[nad]

I saw that cubical-test fails for the issue4067 branch. (I failed to notice this before pushing because the test was not set up properly, but I have fixed that on the master branch (c0b4c61).) Agda fails to solve some constraints:

Failed to solve the following constraints:
  q i = q i : A
  p i = p i : A
  y = y : A
  x = x : A
  _x.A_445 = _≡_ {A.ℓ} {A} (_a₋₀₁_426 i) (_a₋₁₁_433 i) : Set A.ℓ
  _x.A_440 = _≡_ {A.ℓ} {A} (_a₋₀₀_425 i) (_a₋₁₀_432 i) : Set A.ℓ
  _x.A_435 = _≡_ {A.ℓ} {A} (_a₋₁₀_432 i) (_a₋₁₁_433 i) : Set A.ℓ
  _x.A_428 = _≡_ {A.ℓ} {A} (_a₋₀₀_425 i) (_a₋₀₁_426 i) : Set A.ℓ

I used --show-implicit, so it would appear as if some of the constraints above can be solved. However, perhaps they are not reproduced faithfully.

[Saizan]

@nad can you get the constraints from M-x agda2-show-constraints ? Those are closer to the internal representation.

[nad]

_438 i₁ i = q i : A (problems 918, 920)
_431 i₁ i = p i : A (problems 918, 920)
_448 i₁ i = y : A (problems 918, 920, 922)
_443 i₁ i = x : A (problems 918, 920, 922)
_x.A_445 = _≡_ {A.ℓ} {A} (_a₋₀₁_426 i) (_a₋₁₁_433 i) : Set A.ℓ
  (problems 913, 915)
_x.A_440 = _≡_ {A.ℓ} {A} (_a₋₀₀_425 i) (_a₋₁₀_432 i) : Set A.ℓ
  (problems 908, 910)
_x.A_435 = _≡_ {A.ℓ} {A} (_a₋₁₀_432 i) (_a₋₁₁_433 i) : Set A.ℓ
  (problems 903, 905)
_x.A_428 = _≡_ {A.ℓ} {A} (_a₋₀₀_425 i) (_a₋₀₁_426 i) : Set A.ℓ
  (problems 898, 900)
_455
  := λ {A.ℓ} {A} Agpd' x y p q r s →
       Agpd' {x} {y} {p} {x} {y} {q} {λ i → x} {λ i → y} r {x} {y} {p} {x}
       {y} {q} {λ i → x} {λ i → y} s
       {_a₋₀₀_425 {A.ℓ = A.ℓ} {A = A} (Agpd' = Agpd') (x = x) (y = y)
        (p = p) (q = q) (r = r) (s = s)}
       {_a₋₀₁_426 {A.ℓ = A.ℓ} {A = A} (Agpd' = Agpd') (x = x) (y = y)
        (p = p) (q = q) (r = r) (s = s)}
       (_431 {A.ℓ = A.ℓ} {A = A} (Agpd' = Agpd') (x = x) (y = y) (p = p)
        (q = q) (r = r) (s = s))
       {_a₋₁₀_432 {A.ℓ = A.ℓ} {A = A} (Agpd' = Agpd') (x = x) (y = y)
        (p = p) (q = q) (r = r) (s = s)}
       {_a₋₁₁_433 {A.ℓ = A.ℓ} {A = A} (Agpd' = Agpd') (x = x) (y = y)
        (p = p) (q = q) (r = r) (s = s)}
       (_438 {A.ℓ = A.ℓ} {A = A} (Agpd' = Agpd') (x = x) (y = y) (p = p)
        (q = q) (r = r) (s = s))
       (_443 {A.ℓ = A.ℓ} {A = A} (Agpd' = Agpd') (x = x) (y = y) (p = p)
        (q = q) (r = r) (s = s))
       (_448 {A.ℓ = A.ℓ} {A = A} (Agpd' = Agpd') (x = x) (y = y) (p = p)
        (q = q) (r = r) (s = s))
  (blocked by problem 918)
_454
  := λ {A.ℓ} {A} Agpd' x y p q r s z →
       _438 {A.ℓ = A.ℓ} {A = A} (Agpd' = Agpd') (x = x) (y = y) (p = p)
       (q = q) (r = r) (s = s) z
  (blocked by problem 920)
  (problem 918)
_453
  := λ {A.ℓ} {A} Agpd' x y p q r s z →
       _431 {A.ℓ = A.ℓ} {A = A} (Agpd' = Agpd') (x = x) (y = y) (p = p)
       (q = q) (r = r) (s = s) z
  (blocked by problem 920)
  (problem 918)
_452
  := λ {A.ℓ} {A} Agpd' x y p q r s z z₁ →
       _448 {A.ℓ = A.ℓ} {A = A} (Agpd' = Agpd') (x = x) (y = y) (p = p)
       (q = q) (r = r) (s = s) z z₁
  (blocked by problem 920)
  (problem 918)
_451
  := λ {A.ℓ} {A} Agpd' x y p q r s z z₁ →
       _443 {A.ℓ = A.ℓ} {A = A} (Agpd' = Agpd') (x = x) (y = y) (p = p)
       (q = q) (r = r) (s = s) z z₁
  (blocked by problem 920)
  (problem 918)
_450
  := λ {A.ℓ} {A} Agpd' x y p q r s i z →
       _448 {A.ℓ = A.ℓ} {A = A} (Agpd' = Agpd') (x = x) (y = y) (p = p)
       (q = q) (r = r) (s = s) i z
  (blocked by problem 922)
  (problems 918, 920)
_449
  := λ {A.ℓ} {A} Agpd' x y p q r s i z →
       _443 {A.ℓ = A.ℓ} {A = A} (Agpd' = Agpd') (x = x) (y = y) (p = p)
       (q = q) (r = r) (s = s) i z
  (blocked by problem 922)
  (problems 918, 920)
_448 := λ {A.ℓ} {A} Agpd' x y p q r s _ i → y
  (blocked by problem 913)
_447
  := λ {A.ℓ} {A} Agpd' x y p q r s _ →
       _x.A_445 {A.ℓ = A.ℓ} {A = A} (Agpd' = Agpd') (x = x) (y = y)
       (p = p) (q = q) (r = r) (s = s)
  (blocked by problem 915)
  (problem 913)
_443 := λ {A.ℓ} {A} Agpd' x y p q r s _ i → x
  (blocked by problem 908)
_442
  := λ {A.ℓ} {A} Agpd' x y p q r s _ →
       _x.A_440 {A.ℓ = A.ℓ} {A = A} (Agpd' = Agpd') (x = x) (y = y)
       (p = p) (q = q) (r = r) (s = s)
  (blocked by problem 910)
  (problem 908)
_438 := λ {A.ℓ} {A} Agpd' x y p q r s _ → q
  (blocked by problem 903)
_437
  := λ {A.ℓ} {A} Agpd' x y p q r s _ →
       _x.A_435 {A.ℓ = A.ℓ} {A = A} (Agpd' = Agpd') (x = x) (y = y)
       (p = p) (q = q) (r = r) (s = s)
  (blocked by problem 905)
  (problem 903)
_431 := λ {A.ℓ} {A} Agpd' x y p q r s _ → p
  (blocked by problem 898)
_430
  := λ {A.ℓ} {A} Agpd' x y p q r s _ →
       _x.A_428 {A.ℓ = A.ℓ} {A = A} (Agpd' = Agpd') (x = x) (y = y)
       (p = p) (q = q) (r = r) (s = s)
  (blocked by problem 900)
  (problem 898)

[UlfNorell]

As far as I can tell the problems with cubical are legit. We block some occurrences of refl that do get solved if we allow them to be, and their solutions are required to solve the problem that blocked the refl in the first place.