Type ascription precedence inconsistency

[nanotech]

Typed lists and optionals are a different syntax construct than normal type ascription and bind tighter than expected:

\(x : Natural) -> [x] : List Natural
∀(x : Natural) → List Natural

λ(x : Natural) → [x] : List Natural

\(x : Natural) -> x : Natural
^D
Use "dhall --explain" for detailed errors

Error: Expression doesn't match annotation

\(x : Natural) -> (x : Natural)
∀(x : Natural) → Natural

λ(x : Natural) → x

The function arrow also binds tighter than Haskell’s, although that’s only a bit suprising and not an internal inconsistency:

\(x : Natural) -> x : Natural -> Natural
Natural → Natural

λ(x : Natural) → x

---

I ran into this while trying to port the new unannotated list syntax to my Dhall implementation in Rust. I’m using the LALRPOP library for parsing and hit a shift/reduce conflict between the annotated list rule and the top level type ascription rule after parsing an '[' Elements ']' token sequence.

I’m sure there’s a way to fix the conflict that I haven’t discovered yet, but it would be nice if Dhall’s grammar could be as straightforward to translate into an LALR(1) or LR(1) grammar as it was previously. I’ve experimented with a branch that only has the single top parse rule for type ascription and merges the annotation type into the list AST after parsing, but that would parse differently from your library.

Thanks for the nice language!

[Gabriel439]

Yes, I agree that Dhall's parser should be encodable as an LALR grammar. This is actually how I originally wrote Dhall before I switched to using trifecta (which provides better support for error messages, but is an unrestricted parser combinator library).

For the inconsistent treatment of type annotation under lambda abstraction, the correct behavior should be that the type annotation binds tighter than the lambda abstraction, meaning that this:

\(x : Natural) -> x : Natural

... should be equivalent to this:

\(x : Natural) -> (x : Natural)

Like you mentioned, this would then make them consistent with Haskell, where the type annotation also binds tighter than lambda abstraction:

>>> :type (\x -> x :: Int)
(\x -> x :: Int) :: Int -> Int

I'll make the required change soon to this repository

Also, thanks for porting Dhall to Rust! :)

[Gabriel439]

I have a pull request out for this here: #30

If you have time could you take a look at that and see if it introduces any new shift-reduce or reduce-reduce conflicts?

[nanotech]

That solves it. Doing a one-to-one translation still produces a shift/reduce error between the two '[' Elements ']' rules, but as the ':' rules are at the same precedence now, that's easy to work around by replacing the '[' Elements ']' ':' ListLike ExprE rule with some post-parse pattern matching in the ExprC ':' ExprA rule as I tried to do previously.

Thanks!