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

[Andreas Abel]

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/