If an identifier is unknown don't print any other error information

[Timmmm]

I've noticed this a few times, but occasionally I get a big confusing error message like this:

Type error:
sail-riscv/model/riscv_vmem_pte.sail:87.8-96.36:
87 |        pte_flags[V] == 0b0
   |        ^------------------
96 |      | pte_ext[reserved] != zeros()
   |-----------------------------------^
   | No overloading for (operator |), tried:
   | * or_bool
   |    No overloading for (operator |), tried:
   |    * or_bool
   |       No overloading for (operator |), tried:
   |       * or_bool
   |          No overloading for (operator &), tried:
   |          * and_bool
   |             No overloading for (operator |), tried:
   |             * or_bool
   |                No function type found for is_pte_ptr
   |             * or_vec
   |                Could not unify bitvector('n) and bool(not('ex5571#))
   |             * or_vec
   |                Could not unify bitvector('n) and bool(not('ex5574#))
   |          * and_vec
   |             Could not unify bitvector('n) and bool('ex5575#)
   |          * and_vec
   |             Could not unify bitvector('n) and bool('ex5576#)
   |       * or_vec
   |          No overloading for (operator &), tried:
   |          * and_bool
   |             No overloading for (operator |), tried:
   |             * or_bool
   |                No function type found for is_pte_ptr
   |             * or_vec
   |                Could not unify bitvector('n) and bool(not('ex5592#))
   |             * or_vec
   |                Could not unify bitvector('n) and bool(not('ex5595#))
   |          * and_vec
   |             Could not unify bitvector('n) and bool('ex5596#)
   |          * and_vec
   |             Could not unify bitvector('n) and bool('ex5597#)
   |       * or_vec
   |          No overloading for (operator &), tried:
   |          * and_bool
   |             No overloading for (operator |), tried:
   |             * or_bool
   |                No function type found for is_pte_ptr
   |             * or_vec
   |                Could not unify bitvector('n) and bool(not('ex5613#))
   |             * or_vec
   |                Could not unify bitvector('n) and bool(not('ex5616#))
   |          * and_vec
   |             Could not unify bitvector('n) and bool('ex5617#)
   |          * and_vec
   |             Could not unify bitvector('n) and bool('ex5618#)
   |    * or_vec
   |       Could not unify bitvector('n) and bool('ex5622#)
   |    * or_vec
   |       Could not unify bitvector('n) and bool('ex5626#)
   | * or_vec
   |    Could not unify bitvector('n) and bool('ex5627#)
   | * or_vec
   |    Could not unify bitvector('n) and bool('ex5628#)

This is pretty much big enough that I interpret it as "eh something went wrong; and it's complaining about bitvector and bool a lot so maybe I did some_bitvector == some_bool by mistake.

Nope. The error is actually No function type found for is_pte_ptr. It is in there, but it's kind of hard to spot! Also it's a slightly confusingly worded error - "no function type found..." when really it means there's literally no function at all! I meant to type pte_is_ptr.

I think it would make sense that if any identifier isn't found, it just ignores all other errors and prints that. If it can't find an identifier that is definitely the mistake! Or at least the first mistake you should fix. Something like this:

Unknown identifier:
sail-riscv/model/riscv_vmem_pte.sail:87.8-96.36:
88 |        is_pte_ptr
   |        ^------------^
   | `is_pte_ptr` not found. Did you mean `pte_is_ptr`?

Btw, it could be worse - with SystemVerilog Assertions, if you have a variable name typo it will just silently create a new variable for you with the value x!

[Alasdair]

Good timing, I was just working on improving the overload errors yesterday! I just added a heuristic that prefers other errors other the unify errors (which I also changed to 'type mismatch' and added more location info.

This is another good heuristic, so I will add it as well

[Timmmm]

which I also changed to 'type mismatch'

Ah yeah I was going to suggest that too. I assume "unify" is some standard PL theory term, and it's kind of clear from the context what it means but it did confuse me for a second! Type mismatch is much clearer.

[Alasdair]

I think maybe the way to go is to do the following when we encounter an overload:

• Construct an 'overload tree' of subexpressions
• (Partially) infer the type of any obvious leaves, where obvious leaves are things like identifiers, function calls, etc
• Use those partial types to rule out any overloads that cannot apply, pruning the tree down to a smaller set of possibilities.

If we checked overloads like that, we'd essentially get this heuristic for free just from the way the typing rule worked. It would also be a performance optimisation, because we would rule out impossible cases earlier and not waste time exploring them.

[Timmmm]

Maybe I'm being dumb, but when you get to an identifier and try to figure out what it is and you don't find any definitions for that identifier or any type (variable, function, etc), can't you immediately stop?

I wouldn't be surprised if the error is more confusing if that item exists but is the wrong type (e.g. trying to call a variable) but if literally no item exists with the name it seems like you could do an early stop and report that very clearly.

I have never written a compiler though (does a WASM to TCL transpiler count? 😄), let alone a fancy dependently typed one so sorry if I am spewing nonsense!

[Alasdair]

Yes, in the scheme I described that would cause us to stop immediately on the second bullet point.

[Alasdair]

With #526 the following:

default Order dec

$include <prelude.sail>

val main : unit -> unit

function main() = {
    let bv: bits(32) = 0xFFFF_FFFF;
    let _ = bv | bv | bv | bv | b;
    ()
}

now prints:

Type error:
test.sail:9.32-33:
9 |    let _ = bv | bv | bv | bv | b;
  |                                ^
  | Identifier b is unbound. Did you mean bv?

whereas before it printed:

Type error:
test.sail:9.12-33:
9 |    let _ = bv | bv | bv | bv | b;
  |            ^-------------------^ (operator |)
  | No overloading for (operator |), tried:
  | * or_vec
  |   test.sail:9.17-33:
  |   9 |    let _ = bv | bv | bv | bv | b;
  |     |                 ^--------------^ checking function argument has type bitvector(32)
  |     | No overloading for (operator |), tried:
  |     | * or_vec
  |     |   test.sail:9.22-33:
  |     |   9 |    let _ = bv | bv | bv | bv | b;
  |     |     |                      ^---------^ checking function argument has type bitvector(32)
  |     |     | No overloading for (operator |), tried:
  |     |     | * or_vec
  |     |     |   test.sail:9.27-33:
  |     |     |   9 |    let _ = bv | bv | bv | bv | b;
  |     |     |     |                           ^----^ checking function argument has type bitvector(32)
  |     |     |     | No overloading for (operator |), tried:
  |     |     |     | * or_vec
  |     |     |     |   test.sail:9.32-33:
  |     |     |     |   9 |    let _ = bv | bv | bv | bv | b;
  |     |     |     |     |                                ^ checking function argument has type bitvector(32)
  |     |     |     |     | Identifier b is unbound. Did you mean bv?
  |     |     |     | 
  |     |     |     | Also tried or_bool
  |     |     | 
  |     |     | Also tried or_bool
  |     | 
  |     | Also tried or_bool
  | 
  | Also tried or_bool
  | This seems less likely, use --explain-all-overloads to see full details

[Timmmm]

Much better, thanks!