Type checker (ex-)bug

Type checker (ex-)bug

[Mark Shinwell]

The following program:

    type 'a s = 'a
    type 'a t = unit
    
    let g (_ : 'a s -> unit) (_ : 'a t) = ()
    let f t = g (fun x -> x; ()) t

fails to typecheck using ocamlc 3.10.0 but succeeds (as would surely be
expected) under 3.10.1 and 3.10.2.  The 3.10.0 compiler complains:

    File "foo.ml", line 5, characters 6-30:
    The type of this expression, '_a t -> unit,
    contains type variables that cannot be generalized

The fix for this bug doesn't appear to be explicitly noted in the Changes
file, but it was fixed by this patch, which was introduced between 3.10.0
and 3.10.1:

@@ -585,8 +585,11 @@
 let add_delayed_check f = delayed_checks := f :: !delayed_checks
 let force_delayed_checks () =
+  (* checks may change type levels *)
+  let snap = Btype.snapshot () in
   List.iter (fun f -> f ()) (List.rev !delayed_checks);
-  reset_delayed_checks ()
+  reset_delayed_checks ();
+  Btype.backtrack snap

Could someone comment whether this patch is indeed the correct fix for
this problem (I assume it was written to fix something else)?  Or is
there perhaps still something wrong that is being masked by this patch?

Thanks in advance.
Mark

Re: [Caml-list] Type checker (ex-)bug

[Jacques Garrigue]

From: "Mark Shinwell" <mshinwell@janestcapital.com>

> The following program:
> 
>     type 'a s = 'a
>     type 'a t = unit
>     
>     let g (_ : 'a s -> unit) (_ : 'a t) = ()
>     let f t = g (fun x -> x; ()) t
> 
> fails to typecheck using ocamlc 3.10.0 but succeeds (as would surely be
> expected) under 3.10.1 and 3.10.2.  The 3.10.0 compiler complains:
> 
>     File "foo.ml", line 5, characters 6-30:
>     The type of this expression, '_a t -> unit,
>     contains type variables that cannot be generalized
> 
> The fix for this bug doesn't appear to be explicitly noted in the Changes
> file, but it was fixed by this patch, which was introduced between 3.10.0
> and 3.10.1:
> 
> @@ -585,8 +585,11 @@
>  let add_delayed_check f = delayed_checks := f :: !delayed_checks
>  let force_delayed_checks () =
> +  (* checks may change type levels *)
> +  let snap = Btype.snapshot () in
>    List.iter (fun f -> f ()) (List.rev !delayed_checks);
> -  reset_delayed_checks ()
> +  reset_delayed_checks ();
> +  Btype.backtrack snap
> 
> Could someone comment whether this patch is indeed the correct fix for
> this problem (I assume it was written to fix something else)?  Or is
> there perhaps still something wrong that is being masked by this patch?

Indeed, the fix for PR#4350 is in typecore.ml/1.190.2.5, and it is
about delayed checks changing type levels, and losing polymorphism.
In you specific case, this is the delayed check about sequences
(here you should have a warning if x has a concrete type other than
unit).

So yes, this is the fix you need to avoid the above problem, and
other loss of polymorphism related to delayed checks.

Jacques Garrigue