fail to reduce imported functions when name could be ambiguous

[abailly]

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

Create file Data/List/Extra.idr containing:

module Data.List.Extra

public export
find : (a -> Bool) -> List a -> Maybe a
find p []      = Nothing
find p (x::xs) =
  if p x then
    Just x
  else
    find p xs

create a test.idr file with:

module test

import Data.List.Extra as E

foo : List Nat -> Nat -> Maybe Nat
foo list bound = E.find (\ n => n < bound) list

Load test.idr in the real and evaluate call to foo [0 .. 5 ] 2

Expected Behavior

Should output Just Z

Observed Behavior

outputs:

> foo [ 0 .. 5 ] 2
find Nat (\n => (== (compare n (S (S Z))) LT)) [Z, S Z, S (S Z), S (S (S Z)), S (S (S (S Z))), S (S (S (S (S Z))))]

When inlining the find function in the test.idr file, it works as expected.

[edwinb]

This is (probably) because import ... as doesn't actually do anything yet. Really it should complain about two things: firstly, import...as not doing anything yet, and E.find not existing. I don't know why it doesn't complaim about the latter.