Weird error message "no such variable" when function is defined outside

[Ptival]

I know there are a lot of "no such variable" errors on the issue tracker already, but the first few I looked at seemed unrelated to what I am experiencing. Here is a very minimized version of the problem I encouter:

Steps to Reproduce

In Foo.idr

module Foo

import Data.List

public export
data Foo : Nat -> Type where
  Zero : Elem n [ 0 ] -> Foo n

a : Foo 0 -> Bool
a foo = case foo of
  Zero e => True

Definition a is happily accepted. Now in file Bar.idr:

module Bar

import Data.List
import Foo

b : Foo 0 -> Bool
b foo = case foo of
  Zero e => True

yields the following error:

Bar.idr:10:3-8:
   |
10 |   Zero e => True
   |   ~~~~~~
When checking left hand side of Bar.case block in b at Bar.idr:9:14-16:
No such variable Data.List.Elem

This error message seems really fishy to me.

[dmalikov]

Most likely you need to import public Data.List in Foo.idr.