If an identifier is unknown don't print any other error information about sail HOT 7 CLOSED

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

from sail.

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

from sail.

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.

from sail.

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.

from sail.

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!

from sail.

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

from sail.

Much better, thanks!

from sail.