Soundness bug in a program-level type inference

[aqjune-aws]

Found by @joscoh

def fooPgm : Program := { decls := [
  .func { name := "foo",
          typeArgs := ["a"],
          inputs := [("x", .ftvar "a")],
          output := .ftvar "a",
          body := some eb[((~Int.Add x) #1)] },
  .proc { header := { name := "callFoo",
                      typeArgs := [],
                      inputs := [],
                      outputs := [] },
          spec := { modifies := [],
                    preconditions := [],
                    postconditions := [] },
          body := [
            Statement.init "s" (.forAll [] .string) (some eb[#hello]) .empty,
            Statement.init "r" (.forAll [] .string) (some eb[(~foo s)]) .empty
          ]
  }
]}

/-- info: [Strata.Core] Type checking succeeded.

---
info: ok: function foo<$__ty0> (x : $__ty0) : $__ty0 {
  x + 1
}
procedure callFoo () returns ()
{
  var s : string := "hello";
  var r : string := foo(s);
  };-/
#guard_msgs in
#eval (typeCheck .default fooPgm)

A copied message:

Since type inference is only run at the expression level, the type of the overall function remains \forall a, a -> a even though the body has been inferred to have type int -> int. This means that we can subsequently call it on a string and the typechecker is fine with this.
In OCaml, for example, the type of foo would be inferred as int -> int which prevents this. But to fix this we would need to modify type inference to be able to change the types of functions and procedures, which could be a very large refactor and extremely tricky for mutually recursive functions.

My suggestion was:

I think another easy solution is to consider the $__ty0 as a generic of Java. In the case of Java generic, $__ty0 is more like an arbitrarily named type constructor. Since it is not a free type variable, Java cannot unify x 's type with int , instead considers $__ty0 as an opaque type that cannot be handled. Therefore, foo will simply fail type checking.

The Java/Boogie style will still allow polymorphic type. It will simply state that if an expression like x + 1 is found, it will raise an error stating that "we only know that x has some polymorphic type, but we cannot ensure that it can be unified to int".

Actually, this bug that Josh found is pretty connected to the definition of well-formedness that I had to specify in the soundness of type inference algorithm - it states that no input variable like x will have a free type variable like $__ty0. Without this LExpr.resolve had a counterexample... I was somewhat not fully confident that once we allow this LExpr.resolve can be fixed to be a bug-free.

So, in a high level, if we allow this LExpr.resolve will have to be fixed. A concern is the gain compared to the amount of effort we need to put in... In this case I wanted to carefully suggest that probably letting the user put more correct type annotation might be an efficient way to resolve this program-level typing bug.