inference in case requires extra let

[shmish111]

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]

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]

(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.

[shmish111]

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