[Agda] Should not _ patterns be resolvable by inaccessible patterns?

[Andreas Abel]

This is now issue 1605.

I implemented this fix, but it opened a can of worms, see issue 1608. 
Especially with the current fix for issue 473, eager eta-expansion of 
record ImplicitPs, this is not unproblematic.

For instance, record variables introduced by _ are not found by instance 
search (because they have been expanded).  These variables have be given 
a name now.  Seems not completely unreasonable, because _ variables are 
not in scope for manual use, so one could justify they are not in scope 
for instance search either.

diff --git a/test/succeed/RecursiveInstanceSearch.agda 
b/test/succeed/RecursiveInstanceSearch.agda
index ab15f04..167ffed 100644
--- a/test/succeed/RecursiveInstanceSearch.agda
+++ b/test/succeed/RecursiveInstanceSearch.agda
@@ -35,7 +35,7 @@ instance
      aux _ _ = false

    eq-Maybe : {A : Set} → Eq A → Eq (Maybe A)
-  eq-Maybe {A} _ = eq aux  where
+  eq-Maybe {A} eqA = eq aux  where

      aux : Maybe A → Maybe A → Bool
      aux Nothing Nothing = true

I am not so sure anymore if the union of _ and ImplicitP was such a good 
idea at this point (the bad fix of issue 473).

Cheers,
Andreas

On 06.07.2015 23:03, Ulf Norell wrote:
> I don't see any obvious problems with having _ mean ImplicitP. There
> might be something to be said for being explicit about the fact that a
> visible argument is dotted, but since it's clearly confusing people it's
> probably better to change it.
>
> / Ulf
>
> On Mon, Jul 6, 2015 at 11:02 AM, Andreas Abel <abela at chalmers.se
> <mailto:abela at chalmers.se>> wrote:
>
>     Agda only case splits when there is a literal, constructor or absurd
>     pattern.  Variable and dot pattern do not induce splitting.
>
>     Allowing _ to become a dot pattern would make it easier to explain
>     hidden patterns, e.g. transH below could be said to simply mean
>
>        transH {A = _}{a = _}{b = _}{c = _} refl refl = refl
>
>     Currently, it is magic, meaning either of three things.
>
>     Cheers,
>     Andreas
>
>
>     On 06.07.2015 10:33, Andrea Vezzosi wrote:
>
>         The need for "._" is certainly something that puzzles people
>         learning
>         Agda, this change would help for that.
>
>         It makes "_" just a bit more special which might make it less
>         intuitive in other ways, but as long as it's a backwards compatible
>         change I think it's a good one.
>
>         Do the dot patterns affect the generated case splitting tree?
>         If so some proofs might break.
>
>         Best,
>         Andrea
>
>         On Mon, Jul 6, 2015 at 10:25 AM, Andreas Abel <abela at chalmers.se
>         <mailto:abela at chalmers.se>> wrote:
>
>             P.S.: The standard library checks fine if one let _ stand
>             for ImplicitP.
>
>
>             On 06.07.2015 09:33, Andreas Abel wrote:
>
>
>                 If you define transitivity of propositional equality
>                 without hiding
>                 value arguments, you have to explicitly choose where to
>                 put the dots:
>
>                      transV1 : ∀{A : Set} (a b c : A) → a ≡ b → b ≡ c →
>                 a ≡ c
>                      transV1 _ ._ ._ refl refl = refl
>
>                      transV2 : ∀{A : Set} (a b c : A) → a ≡ b → b ≡ c →
>                 a ≡ c
>                      transV2 ._ _ ._ refl refl = refl
>
>                      transV3 : ∀{A : Set} (a b c : A) → a ≡ b → b ≡ c →
>                 a ≡ c
>                      transV3 ._ ._ _ refl refl = refl
>
>                 With hidden arguments, you need not care:
>
>                      transH : ∀{A : Set}{a b c : A} → a ≡ b → b ≡ c → a ≡ c
>                      transH refl refl = refl
>
>                 Of course, when giving the hidden arguments, it is the
>                 same as for
>                 visible arguments:
>
>                      transH1 : ∀{A : Set}{a b c : A} → a ≡ b → b ≡ c → a ≡ c
>                      transH1 {a = _}{b = ._}{c = ._} refl refl = refl
>                      ...
>
>                 The user has more flexibility when an argument is
>                 hidden.  When an
>                 argument is given, the user has to actively make a
>                 decision whether a
>                 pattern must be a dot pattern or must not be one.  There
>                 is no "I don't
>                 care, please figure it out for me" as there is for
>                 hidden arguments.
>                 This seems to be a mismatch.
>
>                 I think it would be simpler for the user if pattern "_"
>                 stood for "don't
>                 care" rather than "unnamed variable".  The need for
>                 writing "._" would
>                 vanish.
>
>                 Does anything speak against this change?  Is there a
>                 situation where it
>                 is essential to tell Agda not to let something be a dot
>                 pattern in order
>                 for type-checking to succeed?  (In the end this could
>                 still be done by
>                 writing a named variable instead of _!)
>
>                 Internally, Agda has four kinds of trivial patterns:
>
>                      DotP       ._ is (DotP MetaVariable)
>                      VarP       x  is (VarP "x") where x cannot be "_"
>                      WildP      _  is WildP
>                      ImplicitP  the user wrote no pattern (argument is
>                 hidden)
>
>                 The change would be to let _ stand for ImplicitP, which
>                 can become
>                 either a dot pattern or a variable pattern (or a record
>                 pattern if issue
>                 473 is fixed).
>
>                 Cheers,
>                 Andreas

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/