<div dir="ltr">Hi all,<div><br></div><div>Here's an interesting bug/feature of CakeML's type system due to the way signatures are handled (and the value restriction):</div><div><br></div><div>Consider:</div><div><br></div><div>structure foo :> sig val f : int list -> int list ref val z:int list ref end = </div><div>struct fun f x = ref x val z = f [] end<br></div><div><br></div><div>Without the signature, the declaration val z = f [] violates the value restriction and doesn't type check.</div><div><br></div><div>This makes the declaration of foo a type error in the current CakeML type system implementation because we first type check the structure before constraining it with the signature.</div><div><br></div><div>This is accepted in Poly/ML (not sure about other ML implementations):</div><div><div>> structure foo :> sig val f : int list -> int list ref val z:int list ref end = struct fun f x = ref x val z = f [] end;</div><div>structure foo : sig val f : int list -> int list ref val z : int list ref end</div></div><div><br></div><div>There might be an easy fix if we have type annotations: convert the annotations in signatures to actual annotations on the structure's values before type checking.</div><div><br></div></div>