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

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

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