Fixed tags with recursive type definitions

[rajdakin]

This PR fixes the following MWE:

(module
  (rec
    (type (func (param (ref null 1))))
    (type (cont 0))
  )
  (tag (type 0))
)

[rossberg]

I can see why the example needs the change to check_cont_type, but are the others actually necessary? I would expect that validation never hits a deftype.

Also, can you add the example to the test suite?

[rossberg]

Suggested change

	| DefT (RecT sts, i) -> assert Int32.(compare i (of_int (List.length sts)) < 0)
	| DefT (RecT sts, i) -> assert (i < Lib.List32.length sts)

But this isn't actually checking anything (only asserting), it seems to be redundant, and you could just do nothing at the call site?

[rajdakin]

I did not know about Lib.List32, that is useful. I have fixed this.

I asserted the condition, since I am pretty sure an error at this location is an internal error and not an error the end-user can fix. I tried to think of an error message to provide to the user, but I did not find a good error message. What would you propose? (I could also remove the assert and do nothing; I would still prefer to keep the function call, much like eg. check_num_type).

[rossberg]

The implementation of the validator is meant to be a faithful transliteration of the on-paper typing rules. This is intended as a way to make the paper semantics executable. Consequently, the implementation should not add rules that do not exist on paper.

Deftypes always come from the environment. It is supposed to be an invariant that their well-formedness is guaranteed separately, by checking the underlying rectype where they are formed. It should never be necessary to check an actual deftype afterwards during validation. Hence these changes don't look right to me — these functions intentionally asserted that these cases are never hit.

Inspecting the implementation, I think the root of the problem instead is the check_tag function, which invokes check_func_type on a type derived from a deftype. That is essentially re-checking (parts of) the deftype, contrary to the assumption above, and that's why we are running into the unexpected cases. And indeed, the following one-line patch makes your example go through:

diff --git a/interpreter/valid/valid.ml b/interpreter/valid/valid.ml
index 90bf74a09..64a0fae25 100644
--- a/interpreter/valid/valid.ml
+++ b/interpreter/valid/valid.ml
@@ -205,7 +205,7 @@ let check_memory_type (c : context) (mt : memory_type) at =
 
 let check_tag_type (c : context) (et : tag_type) at =
   match et with
-  | TagT dt -> check_func_type c (as_func_str_type (expand_def_type dt)) at
+  | TagT dt -> let _ft = as_func_str_type (expand_def_type dt) in ()
 
 let check_global_type (c : context) (gt : global_type) at =
   let GlobalT (_mut, t) = gt in

Could you try that and see if it solves the problem on your end as well?

[rajdakin]

Indeed, your patch works for me. I have pushed a commit reverting my changes and adding yours.

[rossberg]

Cool, thanks for looking into this!