Adding fields to a record can cause Agda to reject previous definitions

[identicalsnowflake]

data ⊤ : Set where
  tt : ⊤

flip : ∀ {t₁ t₂ t₃ : Set} → (t₁ → t₂ → t₃) → t₂ → t₁ → t₃
flip f x y = f y x

record R : Set₁ where
  field
    f : ∀ {a b c : Set} → {{_ : ⊤}} → (a → b) → (b → c) → ⊤

  g : ∀ {a b c : Set} → (b → c) → (a → b) → ⊤
  g = flip (f {{tt}})

  -- field
  --   top : ⊤

Agda accepts the above code, but rejects it if you uncomment the final top : ⊤ field. Strangely, changing the definition of g to the following (adding a single {_} pattern) causes it to be accepted again:

  g : ∀ {a b c : Set} → (b → c) → (a → b) → ⊤
  g {_} = flip (f {{tt}})

[andreasabel]

CONGRATS, YOU FILED ISSUE 2500! YOU WON 50 HOURS OF FREE AGDA BUG FIXING! START NOW! IT IS COMPLETELY FREE!!

[andreasabel]

This is just good old #434. I had heroic plans to fix it at the last AIM. For various reasons I lacked the concentration to attack it. But the next AIM is coming up soon.

[identicalsnowflake]

Did you ever hear the tragedy of Darth Abel the Wise? I thought not. It’s not a story the Haskellers would tell you. It’s an Agda legend. Darth Abel was a Dark Lord of the Types, so powerful and so wise he could use the Types to influence the terms to create... types. He had such a knowledge of the types that he could even keep the ones he cared about from bugs.

He became so powerful that the only thing he was afraid of was losing his types, which eventually, of course, he did.

Ironic. Agda could save others from bugs, but not itself.

[andreasabel]

Alas, we are still far from being able to bootstrap Agda in Agda. For one, Agda is not efficient enough for feasible development of a 300 module piece of software. For two, we probably would need 60 very active developers instead of the 6 we have. Even developing a verified kernel would be a heroic effort. While this would prevent bugs like proving false, it would not weed out all the usability bugs (which are the great majority).

[identicalsnowflake]

Oh I'm under no delusion that it's going to happen any time soon. But to the latter point, I think there's lots of untapped potential in formalizing (or at least stating basic properties of) "non-mathy" stuff: things like quote compose unquote should form the identity, case splitting should generate only valid syntax, etc..

An example I encountered: I wrote a JSONEncoding typeclass which entails ∀ (x : t) → fromJSON (toJSON x) ≡≡ Ok x. When I first wrote it, I just postulated this property away because it was annoying to have to prove it, but I quickly became overcome with guilt and went back to make the proof for all my types. And guess what? It turns out I'm much less skilled at writing JSON instances than I thought! I probably caught at least 3-4 latent bugs in my tiny codebase just from that simple theorem.

So while sure, it's not feasible to write Agda in Agda (for now!), I think you underestimate just how much benefit could be there. Even very simple guarantees can go a long way.

[andreasabel]

I am totally on your side. Even doing a pen and paper proof for a significant fragment of Agda would be a revolution. Just documenting invariants of the code does make a huge difference. I think in the beginning, @nad put some effort into writing quick-check properties. I try to document invariants where I can. But of course, yes, trying to prove them would bring many issues to light.

I think in an open source project without formal responsibilities it is very difficult to retrofit correctness properties. Say I add some asserts to code I have not written myself and expose sleeping bugs in Agda, then I have to fix them myself, since I cannot force the author to fix them. And I cannot just add these assertions that let Agda crash with an internal error where it did not before.

[UlfNorell]

Closing this as duplicate of #434.

[UlfNorell]

Actually it's a combo of #434 and #1079. Here's the failing example without the record:

data ⊤ : Set where
  tt : ⊤

flip : ∀ {t₁ t₂ t₃ : Set} → (t₁ → t₂ → t₃) → t₂ → t₁ → t₃
flip f x y = f y x

R : Set₁
R = (f : ∀ {a b c : Set} → {{_ : ⊤}} → (a → b) → (b → c) → ⊤)
    (let g : ∀ {a b c : Set} → (b → c) → (a → b) → ⊤
         g = flip (f {{tt}})) →
    Set