idrisidris2

Can I avoid lower-case global variables being shadowed in types?

The following code compiles okay in Idris2:

C : Nat
C = 2

claim : C = 2
claim = Refl

but it fails if C is not capitalized:

c : Nat
c = 2

claim : c = 2
claim = Refl

The error message is

Warning: We are about to implicitly bind the following lowercase names. You may be unintentionally shadowing the associated global definitions: c is shadowing Main.c Error: While processing right hand side of claim. When unifying: 2 = 2 and: c = 2 Mismatch between: 2 and c.

Is there a way to tell Idris compiler not to shadow lowercase global names in types?

Solution

  • I don't know if there's a compiler option or the like, but you can qualify c. If it's in module Foo, use

    c : Nat
c = 2

claim : Foo.c = 2
claim = Refl