Declaring data type in the `where` clause gives a unification error

[timmyjose]

Idris2 version (HEAD as of the time of raising the issue):

$ idris2 --version
Idris 2, version 0.2.1-df4c454f4

Steps to Reproduce

Here is the code:

module WhereError 

-- source: https://idris2.readthedocs.io/en/latest/tutorial/typesfuns.html
foo : Int -> Int
foo x = case isLT of
            Yes => x*2
            No => x*4
    where
       data MyLT = Yes | No

       isLT : MyLT
       isLT = if x < 20 then Yes else No

Expected Behavior

Program compiles and runs correctly when supplied an Int.

Observed Behavior

1/1: Building WhereError (WhereError.idr)
WhereError.idr:5:14--5:18:While processing right hand side of foo at WhereError.idr:5:1--12:41:
When unifying MyLT x and Dec ?_
Mismatch between:
        MyLT x
and
        Dec ?_
at:
5       foo x = case isLT of
                     ^^^^

[Russoul]

It has something to do with ambiguous name resolution, this typechecks:

foo : Int -> Int
foo x = case isLT of
            Yes' => x*2
            No' => x*4
    where
       data MyLT = Yes' | No'

       isLT : MyLT
       isLT = if x < 20 then Yes' else No'

Yes and No are also constructors of Dec type.

[timmyjose]

It has something to do with ambiguous name resolution, this typechecks:

foo : Int -> Int
foo x = case isLT of
            Yes' => x*2
            No' => x*4
    where
       data MyLT = Yes' | No'

       isLT : MyLT
       isLT = if x < 20 then Yes' else No'

Yes and No are also constructors of Dec type.

Interesting! I think then that at least the error message must be suitably improved, or the name resolution, or both?

EDIT: Especially since lifting the declaration to the top-level fixes the issue as well:

module WhereDemo

data MyLT = Yes | No

foo : Int -> Int
foo x = case isLT of
             Yes => x * 2
             No => x * 4
    where
      isLT : MyLT
      isLT = if x < 20 then Yes else No

Test:

1/1: Building WhereDemo (WhereDemo.idr)
WhereDemo> foo 100
400
WhereDemo> foo 19
38

[ngeiswei]

Just stumbled on this error while following https://idris2.readthedocs.io/en/latest/tutorial/typesfuns.html#where-clauses could we move forward with its resolution?

To sum-up we have at least two options:

1. Wrapping wheres.idr in a module as suggested here https://github.com/idris-lang/Idris2/issues/588#issuecomment-678779247
2. Rename Yes and No to avoid clashing.

I don't mind doing it but as a noob I need to be told what to do.

[gallais]

I think it may be caused in part by

https://github.com/idris-lang/Idris2/blob/05c9029b35c64873ab3ea13822039f004acd1101/src/TTImp/Elab/Case.idr#L243-L245

we throw out the nested names that were carried until we hit the case. It's strange though because we don't get an out of scope error if we rename the constructors. Very confusing.

I wonder whether this is related to #694 too.

[scarf005]

was following crash course, got confused at the error message, and eventually landed here.

sorry for necroposting, but it'd be really nice to update documentation with workarounds before fix lands as it may confuse future idris2 beginners. that is, @gallais should i make a PR for adding workaround in the doc?