Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

"Can't find an implementation for Range Type" #258

Open
Pytheas01 opened this issue Apr 2, 2020 · 2 comments
Open

"Can't find an implementation for Range Type" #258

Pytheas01 opened this issue Apr 2, 2020 · 2 comments

Comments

@Pytheas01
Copy link

If possible, please include complete self contained source files (for example by uploading to https://gist.github.com) that exhibit the issue in addition to quoting from them here. The smaller the example the better!

Steps to Reproduce

[ [(i,0),(0,i)] | i <- [1..10] ] in Idris REPL

Expected Behavior

[[(1, 0), (0, 1)],
 [(2, 0), (0, 2)],
 [(3, 0), (0, 3)],
 [(4, 0), (0, 4)],
 [(5, 0), (0, 5)],
 [(6, 0), (0, 6)],
 [(7, 0), (0, 7)],
 [(8, 0), (0, 8)],
 [(9, 0), (0, 9)],
 [(10, 0), (0, 10)]] : List (List (Integer, Integer))

Observed Behavior

(interactive):1:24--1:32:Can't find an implementation for Range Type

@gallais
Copy link
Collaborator

gallais commented Apr 2, 2020

The issue is that (a, b) can stand both for the pair type of a & b or the
pair of values a & b whose type is a pair type. Idris disambiguates to the
wrong thing it seems.

If you explicitly annotate i by using the, you get the result you were
expecting: [ [(0, the Integer i), (i, 0)] | i <- [1..10] ].

Worth noting that Idris 1 does get this one right.

@edwinb
Copy link
Owner

edwinb commented Apr 3, 2020

Idris 1 works a bit harder to disambiguate, but there should at least be an error message that explains what the ambiguity is.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

3 participants