[Agda] optional dot in dot patterns?

[Nils Anders Danielsson]

On 2012-11-19 10:05, Peter Divianszky wrote:
> Function calls could be recognized by checking whether there is a
> function with that name in scope.

What about shadowing?

> In case of constructor calls (like .6) the expression and the pattern
> should be the same so maybe the compiler could figure out that 6 is a
> pattern match or a dot pattern. Is this true?

Sometimes it matters where you put the dots. Consider the following data
type:

   data D : Set where
     d₁ d₂ : D

The following definition is OK:

   foo : (x y : D) → x ≡ y → D
   foo .d₁ d₁ refl = d₁
   foo _   d₂ _    = d₂

However, the following isn't (incomplete pattern matching):

   bar : (x y : D) → x ≡ y → D
   bar d₁ .d₁ refl = d₁
   bar _   d₂ _    = d₂

Let's add a final absurd clause:

   bar : (x y : D) → x ≡ y → D
   bar d₁ .d₁ refl = d₁
   bar _   d₂ _    = d₂
   bar d₂  d₁ ()

Now we have foo x d₂ eq = d₂ (definitionally, for variables x and eq),
but not bar x d₂ eq = d₂.

-- 
/NAD