dhall-haskell icon indicating copy to clipboard operation
dhall-haskell copied to clipboard

Explain attempt to annotate keywords like `Some`

Open TristanCacqueray opened this issue 5 years ago • 5 comments

Hi,

It's quite neat to be able to annotate Optional or None, but when trying to do the same for Some it fails:

$ dhall --ascii type <<< "None"
forall (A : Type) -> Optional A

$ dhall --ascii type <<< "Some"
dhall: 
Error: Invalid input

(stdin):2:1:
  |
2 | <empty line>
  | ^
unexpected end of input
expecting (, import, keyword, label, literal, or whitespace


Would it be possible to somehow detect attempt to annotate such internal keywords, and perhaps print a pointer to know more about it instead of the current parse failure?

TristanCacqueray avatar Feb 03 '20 12:02 TristanCacqueray

Here's the relevant parser for Some:

https://github.com/dhall-lang/dhall-haskell/blob/7aed7cf286ef245ce34acad6301b4fe0cdcc5271/dhall/src/Dhall/Parser/Expression.hs#L294-L309

Not sure how to best improve the error though…

sjakobi avatar Feb 03 '20 13:02 sjakobi

@sjakobi: You can do something very similar to what we do for merge:

https://github.com/dhall-lang/dhall-haskell/blob/7aed7cf286ef245ce34acad6301b4fe0cdcc5271/dhall/src/Dhall/Parser/Expression.hs#L410

Gabriella439 avatar Feb 03 '20 14:02 Gabriella439

@Gabriel439 Actually that label doesn't really help users who want to try merge on its own:

⊢ merge {=}

Error: Invalid input

(stdin):1:10:
  |
1 | merge {=}
  |          ^
unexpected end of input
expecting operator or whitespace

It's only useful when the second argument can't be parsed as an import-expression:

⊢ let x = merge {=} in x

Error: Invalid input

(stdin):1:21:
  |
1 | let x = merge {=} in x
  |                     ^
expecting second argument to ❰merge❱ or whitespace

sjakobi avatar Feb 03 '20 19:02 sjakobi

@sjakobi: Right, but we can apply the same trick to the first argument of merge, too

Gabriella439 avatar Feb 03 '20 19:02 Gabriella439

I added the <?> operator in https://github.com/dhall-lang/dhall-haskell/pull/1656, though I don't how it works :) Running dhall type <<< 'Some' still results in an Error: Invalid input and the parser also abort on the next line (e.g. stdin:2 instead of stdin:1). I also don't know what would be a good explanation for why Some doesn't have a type like None. Is it some sort of syntax sugar that could be documented as Some value => Some forall (t: type of value) -> forall (value : t) -> Optional t ?

TristanCacqueray avatar Feb 04 '20 19:02 TristanCacqueray