Constraint solving fails unless an unused variable is marked as erased

[nad]

This issue has been broken out of issue #4525.

Agda accepts the following code:

open import Agda.Builtin.Sigma
open import Agda.Builtin.Equality

_∘_ : {A : Set} {B : A → Set} {C : {x : A} → B x → Set} →
      (∀ {x} (y : B x) → C y) → (g : (x : A) → B x) →
      ((x : A) → C (g x))
f ∘ g = λ x → f (g x)

subst : {A : Set} {x y : A} (P : A → Set) → x ≡ y → P x → P y
subst _ refl p = p

postulate
  Proofs : {A B : Set} → (A → B) → (B → A) → Set

record _≃_ (A B : Set) : Set where
  constructor ⟨_,_⟩
  field
    to             : A → B
    is-equivalence : Σ (B → A) (Proofs to)

  from : B → A
  from = fst is-equivalence

  proofs : Proofs to from
  proofs = snd is-equivalence

  postulate
    to-from : ∀ x → to (from x) ≡ x

record _≃ᴱ_ (A B : Set) : Set where
  field
    to        : A → B
    from      : B → A
    @0 proofs : Proofs to from

@0 ≃ᴱ→≃ : {A B : Set} → A ≃ᴱ B → A ≃ B
≃ᴱ→≃ A≃B = ⟨ to , (from , proofs) ⟩
  where
  open _≃ᴱ_ A≃B

postulate
  [≃]→≃ᴱ : {A B : Set} (to : A → B) (from : B → A) →
           @0 Proofs to from → A ≃ᴱ B
  A      : Set
  P      : A → Set
  A≃A    : A ≃ A

Π-cong-≃ :
  (Q : A → Set) →
  (∀ x → P x ≃ Q (_≃_.to A≃A x)) →
  ((x : A) → P x) ≃ ((x : A) → Q x)
Π-cong-≃ Q P≃Q =
  ⟨ (λ h x → subst Q (_≃_.to-from A≃A x)
               (_≃_.to (P≃Q (_≃_.from A≃A x)) (h (_≃_.from A≃A x))))
  , ( (λ h x → _≃_.from (P≃Q x) (h (_≃_.to A≃A x)))
    , easy
    )
  ⟩
  where
  postulate
    easy : _

Π-cong-≃ᴱ :
  {@0 _ : Set}
  (Q : A → Set) →
  (∀ x → P x ≃ᴱ Q (_≃_.to A≃A x)) →
  ((x : A) → P x) ≃ᴱ ((x : A) → Q x)
Π-cong-≃ᴱ Q P≃Q =
  [≃]→≃ᴱ
    (λ h x → subst Q (_≃_.to-from A≃A x)
               (_≃ᴱ_.to (P≃Q (_≃_.from A≃A x)) (h (_≃_.from A≃A x))))
    _
    (_≃_.proofs (Π-cong-≃ _ (≃ᴱ→≃ ∘ P≃Q)))

However, if the final occurrence of @0 is removed, then the code is rejected. Given that this annotation applies to an unused argument this seems like a bug to me. (The code is accepted again if the last underscore is replaced with Q.)

I compared the debug printout (-vtc:20 -vtc.meta:40) for the code above with the code where the last instance of @0 has been removed, and it appears as if in the former case the meta-variable _140 is η-expanded, but not in the latter case. The meta-variable is η-expanded after the following message:

offending variable:  _
  of type  Set
  (after singleton test)
error during flexible occurs check, we are StronglyRigid
Pattern violation (you shouldn't see this)
oops, pattern violation for _140

There is no occurrence of oops in the debug printout for the failing code.

Some information related to the instantiation of _140 seems to be missing:

Debug printing tc.meta.eta:15 failed due to exception:
  An internal error has occurred. Please report this as a bug.
  Location of the error: impossible, called at src/full/Agda/TypeChecking/Rules/LHS.hs:746:95 in Agda-2.6.2-CCl7tl6DGn2DkWiAPP1T9:Agda.TypeChecking.Rules.LHS
completed assignment of _140

This error message refers to an empty substitution:

agda/src/full/Agda/TypeChecking/Rules/LHS.hs

Line 746 in aea2c53

patSub = map (patternToTerm . namedArg) (reverse $ take numPats qs0) ++# EmptyS impossible

I don't know if this internal error is benign or indicative of a broken invariant. Is the right context used?

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

Lines 579 to 583 in aea2c53

	inTopContext $ do
	reportSDoc "tc.meta.eta" 15 $ sep
	[ "eta expanding: " <+> pretty m <+> " --> "
	, nest 2 $ prettyTCM u
	]

Note that if the change that I suggest in issue #5341 is adopted, then it does not matter whether @0 is present or not, the code is always rejected.

[nad]

Note that if the change that I suggest in issue #5341 is adopted, then it does not matter whether @0 is present or not, the code is always rejected.

It was adopted, so I suppose that we could close this issue.