Better error messages for generalize easter eggs

[nad]

The following code triggers an internal error:

data C (A : Set) : Set where
  c : (x : A) → C A

data D : Set where

data E (A : Set) : Set where
  e : A → E A

postulate
  F : {A : Set} → A → Set

G : {A : Set} → C A → Set
G (c x) = E (F x)

postulate
  H : {A : Set} → (A → Set) → C A → Set
  f : {A : Set} {P : A → Set} {y : C A} → H P y → (x : A) → G y → P x
  g : {A : Set} {y : C A} {P : A → Set} → ((x : A) → G y → P x) → H P y

variable
  A : Set
  P : A → Set
  x : A
  y : C A

postulate
  h : {p : ∀ x → G y → P x} → (∀ x (g : G y) → F (p x g)) → F (g p)

id : (A : Set) → A → A
id _ x = x

i : (h : H P y) → (∀ x (g : G y) → F (f h x g)) → F (g (f h))
i x y = id (F (g (f x))) (h y)

An internal error has occurred. Please report this as a bug.
Location of the error: src/full/Agda/TypeChecking/Substitute.hs:81

This error is not triggered by Agda 2.5.4.2.20190310.

[UlfNorell]

I have a PR that fixes this (including its duplicates #3655 and #3673): #3681. @nad can you try to break it again?

[nad]

I'm compiling it now.

[nad]

open import Agda.Primitive

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

data D {a} (A : Set a) : Set a where
  d : D A → D A

data E {a} (A : Set a) : Set a where
  e : A → E A

F : ∀ {a} {A : Set a} → A → D A → Set a
F x (d ys) = E (F x ys)

G : ∀ {a} {A : Set a} → D A → D A → Set a
G xs ys = ∀ x → F x xs → F x ys

postulate
  H : ∀ {a} {A : Set a} {xs ys : D A} → G xs ys → Set

variable
  a  : Level
  A  : Set a
  P  : A → Set a
  x  : A
  xs : D A

postulate
  h : {f : G xs xs} (_ : P x) → F x xs → H (λ _ → e ∘ f _)

An internal error has occurred. Please report this as a bug.
Location of the error: src/full/Agda/TypeChecking/Substitute.hs:81

[UlfNorell]

@nad I've pushed a fix to this problem to the PR branch.

[nad]

I tested the previous commit (before your force-push) and only found one problem. This problem still exists:

open import Agda.Builtin.Equality
open import Agda.Builtin.List
open import Agda.Builtin.Sigma
open import Agda.Primitive

data ⊥ {ℓ} : Set ℓ where

record ⊤ {ℓ} : Set ℓ where

data _⊎_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
  inj₁ : A → A ⊎ B
  inj₂ : B → A ⊎ B

_×_ : ∀ {a b} (A : Set a) (B : Set b) → Set (a ⊔ b)
A × B = Σ A (λ _ → B)

Any : ∀ {a p} {A : Set a} (P : A → Set p) (xs : List A) → Set p
Any P []       = ⊥
Any P (x ∷ xs) = P x ⊎ Any P xs

All : ∀ {a p} {A : Set a} → (A → Set p) → List A → Set p
All P []       = ⊤
All P (x ∷ xs) = P x × All P xs

_∈_ : ∀ {a} {A : Set a} → A → List A → Set a
x ∈ xs = Any (x ≡_) xs

index : ∀ {a p} {A : Set a} {P : A → Set p} {x : A} {xs : List A} →
        All P xs → x ∈ xs → P x
index {xs = _ ∷ _} (p , _)  (inj₁ refl) = p
index {xs = _ ∷ _} (_ , ps) (inj₂ q)    = index ps q

tabulate : ∀ {a p} {A : Set a} {P : A → Set p} {xs : List A} →
           (∀ {x} → x ∈ xs → P x) → All P xs
tabulate {xs = []}    _ = _
tabulate {xs = _ ∷ _} f = f (inj₁ refl) , tabulate (λ p → f (inj₂ p))

variable
  a p : Level
  A   : Set a
  P   : A → Set p
  xs  : List A

index∘tabulate :
  {x : A} (f : ∀ {x} → x ∈ xs → P x) (×∈xs : x ∈ xs) →
  index (tabulate f) ×∈xs ≡ f ×∈xs
index∘tabulate {xs = _ ∷ _} f (inj₁ refl) = refl
index∘tabulate {xs = _ ∷ _} f (inj₂ p)    = index∘tabulate _ p

_A.a_172 : Level  [ at [...]/Bug.agda:45,8-9 ]
_P.p_173 : Level  [ at [...]/Bug.agda:45,33-34 ]

———— Errors ————————————————————————————————————————————————
Failed to solve the following constraints:
  _P.p_173 = _P.p_173

It should be easy to solve this constraint.

[UlfNorell]

Not that easy. With --show-implicit:

(_P.p_173 {A = A} {xs = xs}) = (_P.p_173 {A = A} {xs = x ∷ xs})

[nad]

Ah, OK. Perhaps we should always display implicit arguments (to some depth) when two terms are claimed to be distinct, but are printed in the same way.

[nad]

{-# OPTIONS --cubical #-}

open import Agda.Builtin.Cubical.Path
open import Agda.Primitive
open import Agda.Primitive.Cubical

variable
  a : Level
  A : Set a
  x : A

refl : x ≡ x
refl {x = x} = λ _ → x

lemma : primTransp (λ i → refl i) i0 x ≡ x
lemma = ?

Congratulations! You have found an easter egg (#FVTY). Be the first
to submit a self-contained test case (max 50 lines of code)
producing this error message to
https://github.com/agda/agda/issues/3672 to receive a small prize.
The error is caused by complicated dependencies between unsolved
metavariables and generalized variables. In particular, this meta:
  _x_27 at […]/Bug.agda:15,27-31
when checking that the expression
primTransp (λ i → refl i) i0 x ≡ x has type _16

[andreasabel]

Please keep milestone 2.6.0.1 clear of issues that concern the new features of Agda 2.6.0.

[nad]

The following short piece of code triggers an internal error:

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

variable
  ℓ     : Level
  A     : Set ℓ
  P     : A → Set ℓ
  B x y : A

postulate
  subst       : (P : A → Set ℓ) → x ≡ y → P x → P y
  subst-const : ∀ (x≡y : x ≡ y) {b} → subst (λ _ → B) x≡y b ≡ b

An internal error has occurred. Please report this as a bug.
Location of the error: src/full/Agda/TypeChecking/Serialise/Instances/Internal.hs:100

The inferred type of subst-const:

{x.A.ℓ : Level} {x.A : Set x.A.ℓ} {x y : x.A}
{B : Set "dummyTerm: src/full/Agda/TypeChecking/Generalize.hs:602"}
{a : Level} (x≡y : x ≡ y) {b : B} →
subst (λ _ → B) x≡y b ≡ b

[omelkonian]

Found an easter egg!

λ> agda --version
Agda version 2.6.0

open import Agda.Builtin.Bool     using (Bool; true)
open import Agda.Builtin.Sigma    using (Σ; _,_)
open import Agda.Builtin.Equality using (_≡_)

Bool² : Set
Bool² = Σ Bool (λ _ → Bool)

data F : Bool² → Set where
  mk : ∀ {a b} → F (a , b)

variable
  x : Bool²
  X : F x

postulate
  f : ∀ {A B : Set} → (A → B) → Bool

fail : let _ = f (λ { _ → _ , _ }) in X ≡ mk
fail = {!!}

Checking RFCX (../RFCX.agda).
../RFCX.agda:18,29-30
Congratulations! You have found an easter egg (#RFCX). Be the first
to submit a self-contained test case (max 50 lines of code)
producing this error message to
https://github.com/agda/agda/issues/3672 to receive a small prize.
The error is caused by complicated dependencies between unsolved
metavariables and generalized variables. In particular, this meta:
  _a_36 at ../RFCX.agda:18,29-30
when checking that _ _ are valid arguments to a function of type
{a b : Agda.Primitive.Level} {A : Set a} {B : A → Set b} (fst : A)
(snd : B fst) →
Σ A B

[laMudri]

This one seems to be quite complicated (#FVTY).

$ agda --version
Agda version 2.6.0.1

module Scratch where

postulate
  List : (A : Set) → Set
  Interleaving : {A : Set} (xs ys zs : List A) → Set

private
  variable
    L : Set
    xs zs : List L

module _ {L : Set} (A : (xs ys : List L) → Set) where

  data SizedDag : (xs ys : List L) → Set
  record ConsCell (xs zs : List L) : Set

  data SizedDag where
    cons : ConsCell xs zs → SizedDag xs zs

  record ConsCell xs zs where
    inductive
    constructor consCell
    field
      {ys ms xs′ ys′} : List L
      x : A xs′ ys′
      i : Interleaving ms xs′ xs
      j : Interleaving ms ys′ ys
      rest : SizedDag ys zs

private
  variable
    x : L
    ys : List L

module _ {L : Set} {A : (xs ys : List L) → Set} where

  data El : SizedDag A xs ys → Set where
    here : (cell : ConsCell A xs zs) → El (cons cell)

  data IsNear : {d : SizedDag A xs ys} (e : El d) → Set where
    here : ∀ {i : Interleaving ? ? ?} {j : Interleaving ? ? ?} {d} →
           IsNear (here (consCell x i j d))

/sharedhome/home/james/Documents/agda/Scratch.agda:41,5-42,44
Congratulations! You have found an easter egg (#FVTY). Be the first
to submit a self-contained test case (max 50 lines of code)
producing this error message to
https://github.com/agda/agda/issues/3672 to receive a small prize.
The error is caused by complicated dependencies between unsolved
metavariables and generalized variables. In particular, this meta:
  ?5 at /sharedhome/home/james/Documents/agda/Scratch.agda:41,61-62
when checking the constructor here in the declaration of IsNear