[Agda] Implicit variables on data constructors

[Simon Foster]

Hi,

A slightly technical question about the Agda core - why do (some?)  
implicit variables which are applied to a data constructor get  
converted into anonymous meta-variables when converting from the  
internal syntax to the abstract syntax? e.g. If I have a function

++-rzero : ∀ {A : Set} → (xs : List A) → xs ++ [] ≡ xs

and ask for the type of ++-rzero {A} I get shown

(x : A) (xs : List A) → _≡_ {List A} (_∷_ {_} x xs) (_∷_ {_} x  
xs)

I assume this is down to the "whocares" assignment in  
InternalToAbstract.hs, because AFAICS the variables are represented  
explicitly in the internal syntax (i.e. when I do inferExpr on the  
name of ++-rzero).

I ask because I'm trying to rewrite my equational reasoner integration  
such that, from a set of lemmas (function names) and a goal, the  
operations (functions/data constructors) and their monomorphic types  
can be inferred. But it's proving harder because for data constructors  
I loose the implicits and therefore don't get a type which is fully  
instantiated in the proof hole's context for decomposed subterms. That  
is, I want to get _∷_ {A} rather than _∷_ {_} because the former  
has the type A -> List A -> List A.

Thanks,

-Si.