[Agda-dev] Clauses and trailing implicit arguments

[Philipp Hausmann]

Hi,

I have a question about the internal Clauses/CompiledClauses 
representation of Agda. I just learned that for certain corner-cases,
different clauses of the same function may take a different number of 
arguments. This seems to break the Epic (and my own new) backend; 
MAlonzo  isn't affected.

It happens when an implicit argument is in trailing position, for example:

data Nat : Set where
   Z : Nat
   S : Nat -> Nat

f : (k : Nat) {l : Nat} -> Nat
f Z {l = q} = q
f (S a) = a

This will yield the following clause patterns:
[[]r(ConP Test.Nat.Z(inductive)[] Nothing []),[]r{VarP "l"}] => length 2
[[]r(ConP Test.Nat.S(inductive)[] Nothing [[]r(a = VarP "a")])] => length 1

And the following CompiledClauses:
case 0 of
   Test.Nat.Z -> done[[]r{"l"}] Var 0 []
   Test.Nat.S ->
     done[[]r("a")] Shared #44{Lam (ArgInfo {argInfoHiding = Hidden, 
argInfoRelevance = Relevant, argInfoColors = []}) (Abs ".l" Var 1 [])}

For the "f Z {l = q}", the clause has 2 arguments. For the "f (S a)" 
case, the clause has only one argument. Instead, a new lambda is 
introduced inside the clause itself.

It seems to happen very rarely, the only two places I've seen it so far 
in the stdlib are:
Data.Nat.DivMod._divMod_.dm
Data.Vec.Properties.sum-++-commuteFun


I think I can work around this in my own code, but I was wondering if 
this is indeed the intended behavior?

Cheers,
Philipp