Can't infer argument ... for explicit arguments! Expected behavior?

[nicolabotta]

I get a "Can't infer argument ..." error for an explicit argument while attempting at compiling

https://github.com/nicolabotta/SeqDecProbs/blob/master/frameworks/14-/SeqDecProbMonadicSmallTheoryRVExample2.lidr

You should be able to reproduce the error by just entering make example in

https://github.com/nicolabotta/SeqDecProbs/tree/master/frameworks/14-

This yields

nicola@cirrus:~/github/SeqDecProbs/frameworks/14-$ make example
idris +RTS -K32000000 -RTS -p contrib -p effects SeqDecProbMonadicSmallTheoryRVExample2.lidr -o example
SeqDecProbMonadicSmallTheoryRVExample2.lidr:402:40:
Can't infer argument t to fYAV, Can't infer argument t to neYAV
SeqDecProbMonadicSmallTheoryRVExample2.lidr:409:40:
Can't infer argument t to fYAV, Can't infer argument t to neYAV
Makefile:8: recipe for target 'example' failed
make: *** [example] Error 1
nicola@cirrus:~/github/SeqDecProbs/frameworks/14-$

The error seems a bit suspicious because t is an explicit argument of both fYAV and neYAV. It seems to me that nothing needs to be inferred here. Any idea what the error means and how to avoid it? Thanks, Nicola

[nicolabotta]

The error can be avoided by replacing line 343

> fYAV : (t : Nat) -> (n : Nat) -> (x : X t) -> Viable (S n) x ->

with

> fYAV : (t : Nat) -> (n : Nat) -> (x : X t) -> Viable {t = t} (S n) x ->

With this modification, the program type checks. Notice, however, that the original errors are at lines 402 and 409. Maybe a problem that should have caught at line 343 showing up later?

[ahmadsalim]

@nicolabotta The file pointed at seems to no longer be available. Could you please confirm whether the issue is still there?

Thanks!

[nicolabotta]

@ahmadsalim Thanks for looking into this issue Ahmad! It took me a while to port the old example to 0.11-git:34c8e1f but now I can confirm that the issue is still there. On a fresh installation of https://github.com/nicolabotta/SeqDecProbs, you should be able to do

cd SeqDecProbs-master/frameworks/14-/
idris -p contrib -p effects -V SeqDecProbMonadicSmallTheoryRVExample2.lidr

this should yield

Type checking ./Sigma.lidr
Type checking ./PairsOperations.lidr
...
Type checking ./SeqDecProbMonadicSmallTheoryRVExample2.lidr
SeqDecProbMonadicSmallTheoryRVExample2.lidr:425:37:Can't infer argument t to fYAV, 
                                                   Can't infer argument t to neYAV
SeqDecProbMonadicSmallTheoryRVExample2.lidr:432:40:Can't infer argument t to fYAV, 
                                                   Can't infer argument t to neYAV
Holes: SeqDecProbMonadicSmallTheoryRV.argmax, SeqDecProbMonadicSmallTheoryRV.max

Now replacing line 366 of SeqDecProbMonadicSmallTheoryRVExample2.lidr

> fYAV : (t : Nat) -> (n : Nat) -> (x : X t) -> Viable (S n) x ->

with

> fYAV : (t : Nat) -> (n : Nat) -> (x : X t) -> Viable {t = t} (S n) x ->

makes the program type check fine. This is with 0.11-git:34c8e1f. I am now going to pull the latest Idris version and report.

[ahmadsalim]

I have changed this to confirmed now, then.