Much simpler example:

default Order dec

$include <prelude.sail>

mapping bool_bit : bool <-> bit = {
  true <-> bitone,
  false <-> bitzero,
}

let x : bool = bool_bit(bitzero)

I believe the error originates with this line in src/lib/effects.ml:221:

    | DEF_aux (DEF_mapdef _, _) -> effects := EffectSet.add IncompleteMatch !effects

If I comment it out then it compiles without any issues, though presumably this isn't sound. It looks like although match is checked for completeness, mapping isn't, so the code just assumes it might be incomplete. This probably also explains why this doesn't produce a The following expression is unmatched warning:

mapping bool_bit : bool <-> bit = {
  true <-> bitone,
}

Hi, I have some idea about this:

• reuse match's complete check on mapping's both sides

  • there would be something like this:

    mapping Foo : bits(2) <-> int = {
      0b00 <-> 10,
      0b01 <-> 1,
      forwards _ => 5,
      backwards _ => 0b11
    }
    

    commit
  • and type_check ignore guard now， but this is acceptable? rustc can't do it either
    

• add $[complete] addribute for mapping

  • which can be very easy here
    

• add something like $[allow(incomplete)] for let exp, like #[allow(xxx)] in rust

I personally like the first

Update: trying to implement the first method. add something like PC.is_complete_mapcls_wildcarded.