Missing source context for incompatible type definitions

[Timmmm]

In this code:

val foo : (bits(32)) -> unit

// Lots of code

function foo(addr : bits(64)) -> unit = ()

You get this error:

7 |function foo(addr : bits(64)) -> unit = ()
  |             ^-------------^
  | Failed to prove constraint: 32 == 64

It is unfortunately missing context about where the cause of the error comes from. I had this error and the val foo was in a completely separate file that I didn't know about (yeah it's a bit of a mess), so figuring out the problem was quite difficult! It would be nice if the error referred to the val foo too.

[Alasdair]

I've improved this case to:

Type error:
missing_loc.sail:4.30-32:
4 |function foo(addr : bitvector(64)) -> unit = ()
  |                              ^^
  | Failed to prove constraint: 32 == 64
  | 
  | constraint from missing_loc.sail:2.20-22:
  | 2 |val foo : bitvector(32) -> unit
  |   |                    ^^ This type argument

[jordancarlin]

That's very helpful! I ran into this vague error before several times when working on Q for the riscv model.

[Timmmm]

Thanks!

[Alasdair]

Should be fixed by c2fe0d4

[Timmmm]

Actually I think that broke things slightly. With this code (it could probably be simplified further; I haven't tried):

type xlenbits = bits(32)
type physaddrbits = bits(34)

newtype physaddr = physaddr : physaddrbits

function physaddr_bits(physaddr(paddr) : physaddr) -> physaddrbits = paddr

struct Track_MemoryAccess = {
  physical_address : xlenbits,
}

register track_memory_accesses : list(Track_MemoryAccess) = [||]

function track_read(paddr : physaddr) -> unit = {
  track_memory_accesses = struct {
    physical_address = physaddr_bits(paddr),
  } :: track_memory_accesses;
}

With the 0.18 release:

Type error:
main.sail:16.23-43:
16 |    physical_address = physaddr_bits(paddr),
   |                       ^------------------^
   | Failed to prove constraint: 34 == 32

But with c2fe0d4:

Type error:
main.sail:1.21-23:
1 |type xlenbits = bits(32)
  |                     ^^
  | Failed to prove constraint: 34 == 32
  | 
  | constraint from main.sail:2.25-27:
  | 2 |type physaddrbits = bits(34)
  |   |                         ^^ This type argument

(That also took me a while to track down!)

I did a bit of debugging and the call stack for this failure is

Called from Libsail__Type_check.subtyp_arg.raise_failed_constraint in file "src/lib/type_check.ml", line 1093, characters 12-32
Called from Stdlib__List.iter2 in file "list.ml", line 147, characters 24-31
Called from Libsail__Type_check.expect_subtype in file "src/lib/type_check.ml", line 2643, characters 2-41
Called from Libsail__Type_check.crule in file "src/lib/type_check.ml", line 1912, characters 22-35
Called from Libsail__Type_check.check_exp.check_fexp in file "src/lib/type_check.ml", line 2160, characters 26-60
Called from Stdlib__List.map in file "list.ml", line 92, characters 20-23
Called from Stdlib__List.map in file "list.ml", line 92, characters 32-39
Called from Libsail__Type_check.check_exp in file "src/lib/type_check.ml", line 2163, characters 18-43
Called from Libsail__Type_check.crule in file "src/lib/type_check.ml", line 1912, characters 22-35

In expect_subtype:

and expect_subtype env (E_aux (_, (l, _)) as annotated_exp) typ =

l is correct (points to the function call) but somehow by the type it gets to subtyp_arg it just points to one of the types (not sure how since it seems to be passed through unchanged, so I've probably got something wrong somewhere).

[Timmmm]

If I just delete this line from subtype_arg:

    let l = if Reporting.is_unknown_loc arg_l1 || Reporting.is_unknown_loc arg_l2 then l else arg_l2 in

Then it actually works in both of the above test cases. I'm not sure that's correct though.