Short form for implicit parameters

[fmease]

Writing polymorphic functions is cumbersome as it is very explicit. Consider these examples:

constant '(A B: Type) (a: A) (_: B): A = a
append '(A: Type) '(n m: Nat) (u: Vector n A) (v: Vector m A): Vector (+ n m) A = ?append

In Idris for example, you solely need to write a lower-case letter inside the types of other parameters and that automatically adds implicit parameters. NB: Those implicit parameters don't need to be annotated with a type, that gets inferred, even though any top-level binding (in Idris and Lushui) need to be annotated with a type. Hence, this seems to be an exception to this rule.

It's worthwhile to consider something similar for Lushui, albeit with some syntactic marker, not just via casing.

1^st Design

Using the symbol $:

constant (a: $A) (_: $B): A = a
append (u: Vector $A $n) (v: Vector A $m): Vector (+ n m) A = ?append

Lowered form:

constant: '(A: _) ->'(B: _) -> (a: A) -> (_: B) -> A = \'(A: _) => \'(B: _) => \(a: A) => \(_: B): A => a
append: '(A: _) -> '(n: _) -> '(m: _) -> (u: Vector A n) -> (v: Vector A m) -> Vector (+ n m) A =
     \'(A: _) => \'(n: _) => \'(m: _) => \(u: Vector A n) => \(v: Vector A m): Vector (+ n m) A => ?append

An erroneous example:

stuff (A: $A): ?_ = ?_

Message (draft):

error[EXXX]: inline implicit parameter shadows earlier parameter
...
LL | stuff (A: $A): ?_ = ?_
   |        - ttt
...
LL | stuff (A: $A): ?_ = ?_
   |            ^ ttt'
... 

[fmease]

Superseded by #102.