edwinb
inference in case requires extra let
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.
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.
(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.
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