Is there a difference between
foo: {len : _} -> Int -> Vect len Int
and
foo: Int -> {len : _} -> Vect len Int
and similar for data constructors, type constructors etc? Sometimes I find my code compiles with implicits in one position but not in another, and I'm not quite clear on why.
It would matter if you use the value of one implicit in the type of another like:
x : {n : Nat} -> {ts : Vect n Type} -> HVect ts
In this case n must be before ts.
One minor difference: it appears implicits are only in scope if preceding arguments are also in scope. For example, in
foo : {len : _} -> Int -> Vect len Int
foo = ?rhs -- len IS in scope here
while
foo : Int -> {len : _} -> Vect len Int
foo = ?rhs -- len is NOT in scope here
and
foo : Int -> {len : _} -> Vect len Int
foo x = ?rhs -- len IS in scope here