Hidden arguments inserted too eagerly when checking against meta

[jamesmckinna]

This kind of thing has been hitting me repeatedly recently (eg in agda/agda-stdlib#2782): bad interaction between using a lemma from stdlib, with 'obvious' instantiation, but implicit/explicit argument checking seems to trigger an error. Very poor UX! Message is incomprehensible, and reason for triggering error also incomprehensible. If there's a fix that makes the stdlib UX smoother for users, please advise!

module MWE where

open import Relation.Nullary.Negation.Core using (¬_; contradiction)

postulate
  A   : Set
  P   : A → Set
  ∀P  : ∀ {a} → P a
  ¬∀P : ¬ (∀ {a} → P a)

test = contradiction ∀P ¬∀P

Tested with:

• v2.8.0
• current master of stdlib, but any v2.x version should reproduce

[plt-amy]

So this is #4105/#2099/etc again: we insert a meta _A for the A argument to contradiction, then check ∀P against _A. ∀P is a postulate, so an inferring, rather than checking, form; this means that we infer a type for it, and inferring the type of a variable inserts metas for all the hidden quantifiers; so we insert some _a in ∀P; so our term looks like contradiction {A = P _a} (∀P {_a}), and we'll try to check ¬∀P against ¬ (P {_a}) which fails.

(For Whatever it's worth here's a version with the stdlib stuff inlined:

open Agda.Primitive

variable
  a : Level
  X Whatever : Set a

data ⊥ : Set where

infix 3 ¬_
¬_ : Set a → Set a
¬ A = A → ⊥

contradiction : X → ¬ X → Whatever
contradiction a ¬a with () ← ¬a a

postulate
  A   : Set
  P   : A → Set
  ∀P  : ∀ {a} → P a
  ¬∀P : ¬ (∀ {a} → P a)

test = contradiction ∀P ¬∀P

)

[andreasabel]

Workaround: You would not get this problem if contradiction had the opposite argument ordering:

contradiction : ¬ X → X → Whatever
contradiction ¬a a with () ← ¬a a

test : Whatever
test = contradiction ¬∀P ∀P

Here, the equation ¬ X = ¬ (∀ {a} → P a) is produced which solves correctly to X = ∀ {a} → P a.

[andreasabel]

When checking ∀P (of type ∀ {a} → P a) against meta ?X Agda should ideally postpone the insertion of implicit arguments.
Basically, we have the subtyping problem ∀ {a} → P a <= ?X which a the source of undecidability, and we could postpone the reduction to P ?a <= ?X in the hope of getting more information about ?X. However, we cannot really block it on ?X since sometimes we won't get any new information.

I wonder how Agda would look like if we just never eagerly inserted hidden arguments, but added a special syntax like f {} if you wanted to insert hidden arguments without actually applying f to a visible argument.
Could be worth trying out in a language variant, say --lazy-hidden-arguments.

Either way, users will complain, because they expect Agda be "reasonable", meaning "to reason", which Agda does not. 😆

[jamesmckinna]

@andreasabel : I like the workaround (very much), but that would have unacceptable breaking knock-on changes for stdlib, so would have to wait for at least v3.0 (hence my emphasis on the stdlib UX for client users...)

@plt-amy NB my MEW was taken form an example where there were no postulates, but defined constants, so I don't understand why the inference is happening rather than checking against an already announced type, but that may betray more (naive) (mis-)understanding on my part. Does it make a difference if ∀P and ¬∀P are (names of) definitions?

@andreasabel "Progress depends on the unreasonable man!" (with apologies for GBS's outdated gender politics, and more...)

[plt-amy]

Names in general, other than those of overloaded constructors, are inferring forms.

[andreasabel]

@jamesmckinna wrote:

"Progress depends on the unreasonable man!" (with apologies for GBS's outdated gender politics, and more...)

I can very much identify with the quote. Germans are (stereotypically) known for their unreasonable idealism which causes them to suffer and to lack success...