inference in case requires extra let

[edwinb]

Issue by shmish111
Sunday Apr 26, 2020 at 15:01 GMT
Originally opened as edwinb/Idris2-boot#328

---

Steps to Reproduce

Check

f : Ord k => SortedMap k v -> List (k, v)                        
f m = case sortBy (\(x, _), (y, _) => compare x y) (toList m) of
    as => as

g : Ord k => SortedMap k v -> List (k, v)                        
g m = 
    let kvs = toList m
    in case sortBy (\(x, _), (y, _) => compare x y) kvs of
        as => as

Expected Behavior

f and g both type check successfully

Observed Behavior

Errors (1)
Test.idr:19:20
While processing right hand side of f at Test.idr:19:1--22:1:
Can't infer type for case scrutinee

If I had to provide a type annotation in the let then I would understand that the compiler just couldn't work it out but the fact that the inference is successful in the let but not in the case seems very counter-intuitive.

[edwinb]

Comment by edwinb
Monday Apr 27, 2020 at 12:45 GMT

---

It can't resolve the ambiguity of toList, although it doesn't say that explicitly. Idris 2 won't try to resolve ambiguities which rely on interface resolution, unlike Idris 1, so you need to be explicit. See https://idris2.readthedocs.io/en/latest/updates/updates.html#ambiguous-name-resolution

Please can you include a complete failing example with reports, ideally minimised? It's so much easier, and so much more likely that I'll investigate an issue quickly, if I can just paste it into a file rather than having to work out what imports are needed, what extra definitions might be needed, etc.

[edwinb]

Comment by edwinb
Monday Apr 27, 2020 at 12:46 GMT

---

(I don't actually know on first looking why g works, by the way...)

EDIT: Yes I do, in fact, it's to do with when it reruns delayed elaboration problems (if it encounters ambiguity, it will postpone elaboration). It needs to resolve the type of the scrutinee before it goes into the case block, but doesn't retry the delayed problems first.

[edwinb]

Comment by shmish111
Monday Apr 27, 2020 at 13:16 GMT

---

You need to include -p contrib because of SortedMap.

import Data.SortedMap
import Data.List

f : Ord k => SortedMap k v -> List (k, v)                        
f m = case sortBy (\(x, _), (y, _) => compare x y) (toList m) of
    as => as

g : Ord k => SortedMap k v -> List (k, v)                        
g m = 
    let kvs = toList m
    in case sortBy (\(x, _), (y, _) => compare x y) kvs of
        as => as

[edwinb]

I just had a closer look at this (finally) and it is genuinely ambiguous because SortedMap implements Foldable which gives it toList. Even if it didn't, ambiguity resolution would still consider this ambiguous because of the unresolved interface (it'll only prioritise concrete definitions if the interface in question is in the return type, though I may refine that later). I'm not sure how much I like that since toList in that case only gives the values and throws away the keys, but that's what it is. I'm tweaking the way delayed elaborators work to give the ambiguity error rather than the case error, but otherwise I think this works as it should so I'll close.