Implicit (type) variables inconsistent resolution

[jonaprieto]

Consider the following program.

module Example;

f {A} : A -> A
 | a :=  a; -- OK

Here, we have a function that takes in a type A (implicitly)
and spits out a function of type A -> A. All good. Notice we
did not type A, i.e., skip {A : Type}.

After learning this, one may attempt the following
to find out that it does not type check.

g : {A} -> A -> A -- Fail
 | a := a;

The error says

Symbol not in scope: A
Perhaps you meant f
                   g

In other words, what I expect is g to be interpreted as:

g : {A : Type} -> A -> A
 | a := a;

PS. Feel free to change the title, I couldn't find a better one.

[lukaszcz]

g : {A} -> A -> A -- Fail
 | a := a;

This is not legal in our syntax currently. You can omit Type in implicit arguments but not the type signature. Perhaps it's an inconsistency.

[lukaszcz]

But this conflicts with the possibility of having implicit unnamed function type parameters (though I think we don't support this ATM):

{Nat} -> Nat

You don't know whether this should be

{_ : Nat} -> Nat

or

{Nat : Type} -> Nat

When it's on the left you know, because then you're not allowed to omit the argument name like in types.