Can't solve constraint between: or' z False and or' z False

[johannes-riecken]

Here's a very small file that fails to type-check.

import Data.Vect
import Syntax.PreorderReasoning

public export
or' : Bool -> Bool -> Bool
or' False False = False
or' False True = True
or' True False = True
or' True True = True

public export
g : (x : Bool) -> or' x False = x
g False = Refl
g True = Refl

f : (z : Bool) -> foldl or' z (the (Vect 2 Bool) [False, False]) = z
f z = Calc $
      |~ or' (or' z False) False
      ~~ or' z False ...(cong (\x => or' x False) $ g z)
      ~~ z ...(g z)

Steps to Reproduce

Type-check the file with Idris2 0.7.0. Notice that type-checking succeeds when changing to a Vect of size 1 and adapting things accordingly.

Expected Behavior

Type-checking succeeds (or an understandable error message if it should fail here).

Observed Behavior

xor:19:10--20:20 19 | ~~ or' z False ...(cong (\x => or' x False) $ g z) 20 | ~~ z ...(g z) Can't solve constraint between: or' z False and or' z False

[gallais]

There's a warning about shadowing:

 |-- Issue3379.idr line 16 col 0:
 |   We are about to implicitly bind the following lowercase names.
 |   You may be unintentionally shadowing the associated global definitions:
 |     or' is shadowing Main.or'
 |   
 |   Issue3379:16:1--16:2
 |    12 | g : (x : Bool) -> or' x False = x
 |    13 | g False = Refl
 |    14 | g True = Refl
 |    15 | 
 |    16 | f : (z : Bool) -> foldl or' z (the (Vect 2 Bool) [False, False]) = z
 |         ^

so you wrote something you did not mean: or' is universally quantified in the type of f but when you call g you talk about the one defined earlier in the file.

[johannes-riecken]

Thanks for the explanation. My bad, I didn't see the warning as I just used the reload functionality of the Vim plugin instead of running Idris2 Issue3379.idr, and with Main.odr' in the type of f it works. So an imported definition will always be in scope, but lowercase definitions in the Main module always need to be qualified in type signatures? Feel free to close the issue.

[gallais]

It's only an issue when it's not applied (that's why it's an issue when it's passed as an argument to foldl but not in or' x False where it's applied to 2 arguments).

Cf. https://idris2.readthedocs.io/en/latest/faq/faq.html#why-can-t-i-use-a-function-with-no-arguments-in-a-type

IMO the automatic generalisation of implicit names should be declare before use but unfortunately it's not the case.