No longer allowed function parameter names that clash with record field names if accessing that field within the function

[jakeelituv]

Steps to reproduce

record TestRecord where
  constructor MkRec
  n : Int

testFunc : Int -> TestRecord -> Bool
testFunc n testRecord =
    n == testRecord.n

results in:

Mismatch between:
	Int
and
	TestRecord -> ?ty

If instead I rename the parameter in the function to m it compiles

record TestRecord where
  constructor MkRec
  n : Int

testFunc : Int -> TestRecord -> Bool
testFunc m testRecord =
    m == testRecord.n

Alternatively, if I don't ever call the ".n" function the following compiles, even if my function uses n as a parameter:

record TestRecord where
  constructor MkRec
  n : Int

testFunc : Int -> TestRecord -> Bool
testFunc n testRecord =
    n == 2

Expected Behavior

This didn't happen until a commit from a few days ago so I assume this isn't supposed to happen.

[ziman]

Indeed, a recent merge removed the distinction between record projections and other functions.

I'm surprised that disambiguation does not consider the global n. This should be fixed.

[ziman]

It seems that the disambiguator will always pick the local variable if there's one.

Maybe .field should not consider locals at all and you'd have to write .(f) to apply the local f?

[ziman]

I can see a few ways to address this. I think that the common theme is that we want x.field to behave differently than field x, namely in the presence of a local variable named field.

• Put RF back in. Then x.field would parse as App (RF "field") (UN "x"), and x.(field) would parse as App (UN "field") (UN "x") because the bracketed thing is an ordinary expression. You would not be able to say "string".length anymore, though.
• Extend TTImp with projections. Since desugaring of x.field happens in Idris, TTImp cannot tell the difference between x.field and field x when disambiguating identifiers later. We'd have to extend the AST of TTImp to preserve the information that the disambiguation of field in x.field should not prioritise the locals.
• Make disambiguation not prefer the locals in all situations. Then both field x and x.field would behave exactly the same, and try both globals and locals. That's probably undesirable and might be annoying.

Maybe there are better solutions?

[ziman]

If we put RF back in, we'd have to write "string".(length). On the other hand, you could define

.length : String -> Nat
.length = length

or even

interface HasLength a where
  .length : a -> Nat

and then you would be able to write "string".length again.

Similarly,

f : (Nat -> Nat -> Nat) -> (String -> Nat) -> String -> Nat
f (+) (.length) str = str.length + "foo".length

would allow binding projections on the LHS so they can be used on the RHS.

The overall idea is that postfix projections live in a separate namespace from other functions, and you have to declare them explicitly. But that would decrease the value/usefulness of postfix projections?

This is pretty much the behaviour we'd get by reverting the postfix projections patch, except that we'd also lose the .(arbitrary expr) syntax, which was added by the patch.

[ziman]

There's also the hack that disambiguation could include also UN candidates for RF queries.

[gallais]

#662 revert postfix application and this is fixed AFAICT