"Panic: uncaught pattern violation" involving holes and with

[meithecatte]

I have encountered a Panic: uncaught pattern violation error when refactoring my development. This is the furthest I could minimize it:

module Minimal where

open import Agda.Primitive
open import Relation.Binary.PropositionalEquality

record Category (o m : Level) : Set (lsuc (o ⊔ m)) where
  infixr 40 _∘_
  infixr 10 _⇒_

  field
    Ob  : Set o
    _⇒_ : Ob → Ob → Set m
    _∘_ : ∀ {x y z} → y ⇒ z → x ⇒ y → x ⇒ z
  
  mono : {X Y : Ob} → X ⇒ Y → Set _
  mono {X} {Y} f = ∀ {Z : Ob} {g : Z ⇒ X} → f ∘ g ≡ f ∘ g → Set

Sets : (ℓ : Level) → Category (lsuc ℓ) ℓ
Sets ℓ = record
    { Ob = Set ℓ
    ; _⇒_ = ?
    ; _∘_ = λ f g x → f (g x)
    }

module SetCat {o} where
  open Category (Sets o)
  postulate
    X Y : Ob
    f : X ⇒ Y

  mono-f : mono f
  mono-f fg≡ with fgz≡ ← cong ? fg≡ = ? 

Notably, moving the definition of mono into module SetCat stops reproducing, as does this variation that avoids with:

  mono-f : mono f
  mono-f fg≡ = ?
    where
    fgz≡ = cong ? fg≡ 

I am using Agda 2.6.2.1.

[andreasabel]

This correctly reports unsolved metas with Agda 2.6.1.
Running a bisect with this slightly modified testcase (changed first 7 lines so it does not depend on the standard library):

{-# OPTIONS --allow-unsolved-metas #-}

open import Agda.Primitive
open import Agda.Builtin.Equality

cong : ∀{a b} {A : Set a} {B : Set b} (f : A → B) {x y : A} (eq : x ≡ y) → f x ≡ f y
cong f refl = refl

record Category (o m : Level) : Set (lsuc (o ⊔ m)) where
  infixr 40 _∘_
  infixr 10 _⇒_

  field
    Ob  : Set o
    _⇒_ : Ob → Ob → Set m
    _∘_ : ∀ {x y z} → y ⇒ z → x ⇒ y → x ⇒ z

  mono : {X Y : Ob} → X ⇒ Y → Set _
  mono {X} {Y} f = ∀ {Z : Ob} {g : Z ⇒ X} → f ∘ g ≡ f ∘ g → Set

Sets : (ℓ : Level) → Category (lsuc ℓ) ℓ
Sets ℓ = record
    { Ob = Set ℓ
    ; _⇒_ = ?
    ; _∘_ = λ f g x → f (g x)
    }

module SetCat {o} where
  open Category (Sets o)
  postulate
    X Y : Ob
    f : X ⇒ Y

  mono-f : mono f
  mono-f fg≡ with fgz≡ ← cong ? fg≡ = ?

[andreasabel]

Bisection blames commit d1a9d7d (ping @jespercockx).

Date: Fri Oct 16 16:52:33 2020 +0200
[ re #4727 ] Promote metavariable from irrelevant to relevant or from erased to non-erased during Occurs check

Debug printing with -v tc.meta.occurs:35 gives:

initOccursCheck: we look into the following definitions:
mono-f
occursCheck: meta variable _X_77 has relevance and quantity @0
Meta occurs check found bad relevance
aborting because occurrence is flexible
initOccursCheck: we look into the following definitions:
mono-f

So it seems that erasure-stuff is leaking into type-checking code that does not use erasure. I wonder whether this calls for an option --erasure (with default --no-erasure) so that we can ensure by simple means that "basic Agda" isn't plagued by bugs that happen during the formation of the erasure feature. We have made similar decisions for other experimental features. (Ping @nad @jespercockx @UlfNorell.)

[andreasabel]

We can shrink away the universe levels:

open import Agda.Builtin.Equality

cong : ∀{a b} {A : Set a} {B : Set b} (f : A → B) {x y : A} (eq : x ≡ y) → f x ≡ f y
cong f refl = refl

record Category : Set₂ where
  field
    Ob  : Set₁
    _⇒_ : Ob → Ob → Set
    _∘_ : ∀ {O P Q} → P ⇒ Q → O ⇒ P → O ⇒ Q

  -- Moving this out of the record fixes the problem.
  idem : {X : Ob} → X ⇒ X → Set₁
  idem {X} f = f ∘ f ≡ f → Set

Sets : Category
Sets = record
    { Ob = Set
    ; _⇒_ = {!!}
    ; _∘_ = λ f g x → f (g x)
    }
open Category Sets

postulate
  Y : Ob
  f : Y ⇒ Y

idem-f : idem {X = _} f  -- Solving the _ fixes the problem
idem-f ff≡f
  with ffx≡fx ← cong {!!} ff≡f
  = Y

[nad]

I wonder whether this calls for an option --erasure (with default --no-erasure) so that we can ensure by simple means that "basic Agda" isn't plagued by bugs that happen during the formation of the erasure feature.

We have discussed --erasure before (#4786). A problem came up: When --erasure is used I want parameters to be erased in the types of constructors and projections. I want this to apply also to builtin types like Agda.Builtin.Sigma.Σ, but I don't want to have two different builtin Σ-types. Because the use of --erasure presumably does not rule out any models, and no-one objected, I did not implement --erasure.

[andreasabel]

Yes, the problem with --erasure is that it changes the semantics of code even it if does not explicitly erase anything. So, flag --erasure would have to be treated like it was a different version of Agda. If you have this in your project, you need a separate build-tree. Maybe we have enough of the infrastructure (like separate build directories for separate Agda version) so that such a feature is within reach. The builtin modules would cause some headache, though.

[nad]

If you were to go down that route, would you also fork the standard library? That does not sound like a good idea to me.

[andreasabel]

If you were to go down that route, would you also fork the standard library?

Would this be necessary? As long as the standard library does not use @erased, it would suffice to maintain two build trees for it, one with --erasure on and one with --no-erasure. E.g. that would be _build/agda-2.6.3-erasure/... and _build/agda-2.6.3/....

[nad]

Let's say that we start using erasure in some standard library modules. Consider the following scenario:

• You have no .agdai files for the standard library.
• You load a module that uses --erasure. Then all the dependencies are type-checked as if --erasure had been turned on (if I understand you correctly).
• Now you load one of these dependencies which does not use --erasure. In that case this module, and all its dependencies from the standard library, are re-checked.

This does not sound very nice to me.

[andreasabel]

Well, I would think that --erasure would be a project-wide flag (in the .agda-lib file---we don't have those yet), not a per-module one.

[nad]

If we start to use @0 in the standard library, and enable --erasure for all files in the library, then the library is unusable for those who do not use --erasure.

[andreasabel]

I see, I get your point. So a just project-wide flag would not work for the standard library once it starts using erasure. We need to retain the possibility to apply it module-wise. The flag would be coinfective.
Still I think the penalty could be kept low. If you are working a mixed project (like in the scenario of #5805 (comment)), you could set --erasure in your project file to avoid length reloads of interfaces. If you are working in a no-erasure project, you would set --no-erasure.

[andreasabel]

@jespercockx : Do you think you can look into this issue for a soonish release of 2.6.2.2 (#5831).

[jespercockx]

I'm taking a look now, if it doesn't take too much time I'll try to fix it. So far, I found that the actual problem seems to be not in the part of the occurs check that I changed, but in checkInternal which calls elimView, which can throw a pattern violation that is not caught by the checkInternal. Somehow the change to the occurs check causes metas to be solved in a different order which calls checkInternal on a different term which triggers the bug. I'll investigate further.

[jespercockx]

I found the cause of the problem: the call to checkType at https://github.com/agda/agda/blob/master/src/full/Agda/TypeChecking/Rules/Def.hs#L1174

The problem here is that checkType calls checkInternal, which can throw uncaught pattern violations when it gets blocked on a meta. The best solution looks to me to catch pattern violations in the definition of checkType and turn them into a proper error, as it is not expected that this function throws pattern violations.

[andreasabel]

Continue discussion at #5832.