missing name-not-defined error?

[nobodxbodon]

For code below:

open data Bool : Type 0 | real | false
def not (b : Bool) : Bool
 | true => false
 | false => true

Error below occurs:

  2 | def not (b : Bool) : Bool
  3 |  | true => false
  4 |  | false => true
                  ^--^

Error: The name `true` is not defined in the current scope

A little surprised to see the 'true' in line 3 doesn't trigger the error first. Then tried fixing the 4th line as below:

open data Bool : Type 0 | real | false
def not (b : Bool) : Bool
 | true => false
 | false => real

Expecting to see the same "true is not defined" error for line 3, but a different error occurs:

  1 | open data Bool : Type 0 | real | false
  2 | def not (b : Bool) : Bool
  3 |  | true => false
         ^-----------^ substituted to `false`
  4 |  | false => real
         ^-----------^ substituted to `real`

Error: The 1st and the 2nd clauses are not confluent because we failed to unify
         false
       and
         real
🔨

[ice1000]

Do you know how pattern matching works?

A little surprised to see the 'true' in line 3 doesn't trigger the error first

Yes, because it's a valid pattern. In fact, you can write

def not (b : Bool) : Bool
 | true => false

This is also a valid function, which returns false whatever the input is.

I hope this clarifies whatever confuses you.

[ice1000]

If you load the code in VSCode, you'll see this:

true is highlighted as a variable, false and real are highlighted as constructors.

[imkiva]

This is the expected pattern matching behavior.

The true in line 3 is a bind pattern, which means the true is not a constructor but a variable name.

[imkiva]

For your second error:

  1 | open data Bool : Type 0 | real | false
  2 | def not (b : Bool) : Bool
  3 |  | true => false
         ^-----------^ substituted to `false`
  4 |  | false => real
         ^-----------^ substituted to `real`

Error: The 1st and the 2nd clauses are not confluent because we failed to unify
         false
       and
         real
🔨

This error relates to overlapping patterns.
Here, a simple explanation is that the first pattern true => false is a bind pattern, which can match both Bool::real and Bool::false. And the second pattern false => real can only match Bool::false. The overlapping happens when trying to match Bool::false, so aya will do a subst-and-unify to check whether the two patterns produce the same result, which is called confluence check.

[ice1000]

I think this is a bit too advanced for beginners. Maybe we need some kinds of hint or something to help them realize the difference here...

[nobodxbodon]

Thanks for detailed explanations from you both. If "true" match all the cases, maybe also helpful to users that the other clause is "unreachable" because of it. Just tried this similar expression in Arend:

\data Bool | real | false
\func not (b : Bool) : Bool
 | true => false
 | false => real

It gives warning below:

[WARNING] t:4:4: Clause is redundant
  In: | false => real

[ice1000]

Maybe you meant that "if there is a warning, we should not print other errors". This is not what I want to do.

[ice1000]

See? The confluence error actually has a lower priority. The domination warning is printed first. 🤣

[nobodxbodon]

Aha I did overlook the warning message above the error. LGTM.
Just one thought, would it be helpful (or annoying ?) to put some kind of summary info, like "1 warning, 1 error", especially when there are more messages for more complex files.

[ice1000]

Just one thought, would it be helpful (or annoying ?) to put some kind of summary info, like "1 warning, 1 error", especially when there are more messages for more complex files.

Makes sense :)

[imkiva]

Aha I did overlook the warning message above the error. LGTM. Just one thought, would it be helpful (or annoying ?) to put some kind of summary info, like "1 warning, 1 error", especially when there are more messages for more complex files.

Sounds good.