Bug in SimpleChecker for Recursive Types

[0npv527yh9]

Problem

The function is_rec_assign in simpleChecker.ml:

(* 
checks whether an assignemnt to (or read from) of type t' to constructor c
requires a fold or unfold. Simply put, we walk the assigned type, and see
if (the canonical representation of) c appears anywhere in t'. If it does, this is
a folding or unfolding assignment/read.
*)
let is_rec_assign sub c t' =

is_rec_assign returns true for a given constructor c and type t' if c appears in t', and false otherwise.

Currently, this function returns true in the case of Var v (a type variable) if the representative of it is not registered in the hash table from type variable to types. (See the last program.)

However, this is WRONG.

As you can see from the function resolve_with_rec in simpleChecker.ml, unknown types will eventually become Int, and is_rec_assign returns false in the case of Int.

(* simpleChecker.ml *)

let rec resolve_with_rec sub v_set k t =
  match canonicalize sub t with
  ...
  | `Var v when not @@ Hashtbl.mem sub.resolv v ->
    k IS.empty `Int


let is_rec_assign sub c t' =
  ...
    match canonicalize sub t with
    ...
    | `Int -> false

Therefore, is_rec_assign has to return false in the case of unknown type variables.

Example

This bug is problematic for the following program:

{
    let n = (_: ~ > 0) in 
    let r1 = mkref mkarray n in
    let r2 = r1 in {
        alias(*r1 = *r2); 
    }
}

The two terms (*r1, *r2) in the alias expression are typed Array t, but t remains unknown until resolve_with_rec assigns Int to it. Then, is_rec_assign WRONGLY determines t to be such α as appearing in the body of μ α. ....

Therefore, even though no recursive types are used, the above program raises the following error:

Fatal error: exception Failure("Multiple recursive type operations at the same point")

How to fix

let is_rec_assign sub c t' =
  ...
    match canonicalize sub t with
    | `Var v ->
      Hashtbl.find_opt sub.resolv v
      |> Option.map [%cast: typ]
      |> Option.map @@ check_loop h_rec
-     |> Option.value ~default:true
+     |> Option.value ~default:false