`Can't infer type for {x504}` and file/repl parser inconsistency

[ulidtko]

Given this file:

data AT = A

fact_A_is_A : A = A
fact_A_is_A = proof trivial

at Idris REPL:

Idris> :total fact_A_is_A 
Main.fact_A_is_A is Total
Idris> :t fact_A_is_A 
Main.fact_A_is_A : A = A
Idris> :t proof trivial
Can't infer type for {x504}
Idris> :t proof
(input):1:9: error: unexpected
    EOF, expected: ")",
    end of "proof", start of block,
    tactic
:t proof<EOF> 
        ^     

Version 0.9.15.1-git:941ba6e

[edwinb]

We haven’t fully documented ‘proof’ and the theorem prover mode yet, but this is expected. “proof” is a keyword which introduces a goal directed proof script, so if there’s no script you’ll get a parse error, and if there’s nothing to prove then it won’t know what the type is.

There could always be better error messages, of course.

On 15 Dec 2014, at 01:58, Maxim Ivanov notifications@github.com wrote:

Given this file:

data AT = A

fact_A_is_A : A = A fact_A_is_A = proof trivial

at Idris REPL:

Idris> :total fact_A_is_A Main.fact_A_is_A is Total Idris> :t fact_A_is_A Main.fact_A_is_A : A = A Idris> :t proof trivial Can't infer type for {x504} Idris> :t proof (input):1:9: error: unexpected EOF, expected: ")", end of "proof", start of block, tactic :t proof ^

Version 0.9.15.1-git:941ba6e

— Reply to this email directly or view it on GitHub.

[ulidtko]

I just wanted to note that it's best to preserve the grammar as much consistent between file parser and repl parser as possible. Any difference creates massive confusion since people tend to rely on the REPL, and it's irritatingly unhelpful to see something work in the saved code and not work on the prompt.

Source code wise, can you please point out some places where one could start improving the error messages for this specific case? I think it would be very helpful.

[edwinb]

That’s going to be very hard in general in a language that requires top level type annotations. The REPL tries to infer a type, but this doesn’t work in general.

The grammar is identical between the file and the REPL. But if there’s nothing to prove, the REPL is not going to infer what you’re wanting it to prove. Sorry that it’s irritating.

On 15 Dec 2014, at 10:08, Maxim Ivanov notifications@github.com wrote:

I just wanted to note that it's best to preserve the grammar as much consistent between file parser and repl parser as possible. Any difference creates massive confusion since people tend to rely on the REPL, and it's irritatingly unhelpful to see something work in the saved code and not work on the prompt.

Source code wise, can you please point out some places where one could start improving the error messages for this specific case? I think it would be very helpful.

— Reply to this email directly or view it on GitHub.