Type checker silently stuck on missing import.

[yellowsquid]

Steps to Reproduce

We have two files, Foo.idr and Bar.idr:

Foo.idr:

module Foo

import Data.Vect

public export
ThisIsOne : Nat
ThisIsOne = head [1] + 0

Bar.idr:

module Bar

import Foo

ItIsOne : ThisIsOne = 1
ItIsOne = ?a

We then have the following session in the repl:

Main> :load Bar.idr
1/2: Building Foo (Foo.idr)
2/2: Building Bar (Bar.idr)
Loaded file Bar.idr
Bar> :m
1 hole: Bar.a : 1 = 1
Bar> ThisIsOne
1

Observed Behaviour

We then fill the hole ?a with Refl.

Bar> :reload
2/2: Building Bar (Bar.idr)
Error: While processing right hand side of ItIsOne. Can't solve constraint
between: S (assert_total (integerToNat 0)) and plus (head Nat 0 ((::) 0 Nat 1 ([] Nat))) 0.

Bar:6:11--6:15
 2 | 
 3 | import Foo
 4 | 
 5 | ItIsOne : ThisIsOne = 1
 6 | ItIsOne = Refl
               ^^^^

Error(s) building file Bar.idr

Expected Behavior

Idris to either: 1) accept Refl as valid 2) identify that Data.Vect.head is not imported.

To justify 2, consider this varaint of Foo.idr:

module Foo

import Data.Vect

public export
ThisIsOne : Nat
ThisIsOne = head [1]

When we go back to the repl (with Refl still in place), we get the more useful error:

Bar> :r
1/2: Building Foo (Foo.idr)
2/2: Building Bar (Bar.idr)
Error: While processing right hand side of ItIsOne. When unifying:
    1 = 1
and:
    ThisIsOne = 1
Undefined name Data.Vect.head. 

Bar:6:11--6:15
 2 | 
 3 | import Foo
 4 | 
 5 | ItIsOne : ThisIsOne = 1
 6 | ItIsOne = Refl
               ^^^^
Did you mean: Prelude.Types.head?
Error(s) building file Bar.idr

Environment

> idris2 --version
Idris 2, version 0.7.0-034f1e89c
> chez-scheme --version
10.0.0

[ohad]

I'm not sure this is a bug, although it is a non-intuitive/bad design of the module system/namespace management. We do know we want a better one, but currently we do not have resources to allocate to design it. @jacobjwalters has given it some thought in his UG dissertation, but it's somewhat hard.

Workarounds:

1. import Data.Vect in client modules (Bar in this example).
2. import public Data.Vect in exporing module (Foo in this example).

I'm going to tag this as expected behaviour, but happy to be overruled following a decent a discussion.

[ohad]

Another option would be to propose a mechanism for detecting this and issuing a warning. Note that issued warning ought to have a corresponding mechanism for suppressing it when the warned-against situation is desired by the user.

[andrevidela]

Maybe an easier way to deal with this would be to communicate where the term is stuck:

Bar> :reload
2/2: Building Bar (Bar.idr)
Error: While processing right hand side of ItIsOne. Can't solve constraint
between: S (assert_total (integerToNat 0)) 
and: plus (head Nat 0 ((::) 0 Nat 1 ([] Nat))) 0.
           ^^^^
           └ Stuck here

Bar:6:11--6:15
 2 | 
 3 | import Foo
 4 | 
 5 | ItIsOne : ThisIsOne = 1
 6 | ItIsOne = Refl
               ^^^^

Error(s) building file Bar.idr