I admit I got a bit confused about how parsing would get confused on the pi vs type annotation bit. It’s mostly about grammar power right ?
Conversation
Correct. GLL or something could be able to resolve it, or a ton of backtracking, if using PEG.
2
What’s the tiniest example program that has this ambiguity and uses both flavors ?
1
literally just `(a : A) -> A`
1
Wait, I'm not sure backtracking could prevent it - because both interpretations are valid. You want to race them, and prioritise the dependent interpretation.
1
Things get even uglier when you add in Agda's additional sugar:
(A B : Type) (C : Type -> Type) -> C A
It could be either function application or a dependent function, up until you get to the arrow. Then you go with the dependent function interpretation.
2
1
So yeah, the parser needs to take into account that any time, something starting with `(` could suddenly turn into a dependent function type - but only sometimes. `(A) -> A` is non-dependent, for example.
2
seems like the real issue is overloading of parens!
2
1
1