[5.3] typechecker crash while typing objects

[nojb]

nojebar@PERVERSESHEAF:~/tmp$ cat bug.ml
class type gui =
  object
    method sub: 'b. 'b -> 'b
  end

class virtual local_sub =
  object
    method virtual sub: 'b. 'b -> 'b option
  end

class virtual ['a] compound_gui =
  object (_: #gui)
    constraint 'a = #local_sub
  end
nojebar@PERVERSESHEAF:~/tmp$ opam exec --switch 4.14.2 -- ocaml bug.ml
nojebar@PERVERSESHEAF:~/tmp$ opam exec --switch 5.1.0 -- ocaml bug.ml
nojebar@PERVERSESHEAF:~/tmp$ opam exec --switch 5.2.0 -- ocaml bug.ml
nojebar@PERVERSESHEAF:~/tmp$ opam exec --switch 5.3.0+trunk -- ocaml bug.ml
>> Fatal error: Ctype.unify_univar: univar not in scope
Fatal error: exception Misc.Fatal_error

(The example is extracted from a much larger codebase.)

[gasche]

Amusing hostname! :-)

Curated backtrace:

Raised at Misc.fatal_errorf.(fun) in file "utils/misc.ml", line 22, characters 14-31
Called from Ctype.unify_univar_for in file "typing/ctype.ml", line 1986, characters 6-37
Called from Ctype.eqtype in file "typing/ctype.ml", line 4200, characters 14-61
Called from Ctype.eqtype in file "typing/ctype.ml", line 4165, characters 14-54
[...]
Called from Ctype.equal in file "typing/ctype.ml", line 4353, characters 6-78
Called from Ctype.is_equal in file "typing/ctype.ml", line 4358, characters 8-34
Called from Typedecl_variance.compute_variance_type.check.(fun) in file "typing/typedecl_variance.ml", line 201, characters 16-49
Called from Stdlib__Map.Make.fold in file "map.ml", line 329, characters 19-42
Called from Typedecl_variance.compute_variance_type.check in file "typing/typedecl_variance.ml", lines 199-202, characters 8-20
[...]
Called from Typedecl_variance.compute_variance_type in file "typing/typedecl_variance.ml", line 228, characters 4-42
Called from Typedecl_variance.compute_variance_decl in file "typing/typedecl_variance.ml", line 325, characters 10-55
Called from Typedecl_variance.check_decl in file "typing/typedecl_variance.ml", line 373, characters 9-79
Called from Typedecl_properties.compute_property.compute_fixpoint in file "typing/typedecl_properties.ml", lines 63-65, characters 6-26
Called from Typedecl_variance.update_class_decls in file "typing/typedecl_variance.ml", line 428, characters 4-68
Called from Typeclass.type_classes in file "typing/typeclass.ml", line 1858, characters 8-54
Called from Typeclass.class_declarations in file "typing/typeclass.ml", line 1885, characters 4-66

[gasche]

The problem is reproducible in the 5.3 maintenance branch, it is not more recent than the 5.3 branching, so we can bisect it between 5.2 and 5.3.

[Octachron]

The fatal error is from #12920 .

[gasche]

My understanding is that the bug is in the code that checks variance of type declarations, in the case where some type variables of the type are introduced through constraints (and not bound as type parameters of the declaration).

ocaml/typing/typedecl_variance.ml

Lines 176 to 203 in d540076

	(* Check propagation from constrained parameters *)
	let args = Btype.newgenty (Ttuple params) in
	let fvl = Ctype.free_variables args in
	let fvl =
	List.filter (fun v -> not (List.exists (eq_type v) params)) fvl in
	(* If there are no extra variables there is nothing to do *)
	if fvl = [] then () else
	let tvl2 = ref TypeMap.empty in
	List.iter2
	(fun ty (p,n,_) ->
	if Btype.is_Tvar ty then () else
	let v =
	if p then if n then full else covariant else conjugate covariant in
	compute_variance env tvl2 v ty)
	params required;
	let visited = ref TypeSet.empty in
	let rec check ty =
	if TypeSet.mem ty !visited then () else
	let visited' = TypeSet.add ty !visited in
	visited := visited';
	let v1 = get_variance ty tvl in
	let snap = Btype.snapshot () in
	let v2 =
	TypeMap.fold
	(fun t vt v ->
	if Ctype.is_equal env false [ty] [t] then union vt v else v)
	!tvl2 null in
	Btype.backtrack snap;

The fatal error arises from Ctype.is_equal env false [ty] [t], where I think that ty is one of the toplevel type expressions whose variance is checked, and t is a subexpression (with its variance) in one of the, ahem, probably one of the constraining types that are being checked. t being a subexpression (from tvl2, accumulated by the compute_variance call earlier), it may be under Tpoly nodes, that is, its univar scope may be distinct from the one in ty, and I think that explains why we see the fatal error.

The fix probably involves understanding this code better, and then thinking of how to change it so that we don't compare types that have distinct univar scopes, or figuring how we want to compare types in distinct scopes. (We could collect the Tpoly variables as we traverse subexpressions in compute_variance.)

(I haven't tried looking at which hidden type declaration is being variance-checked in this example and why it involves univars, which would also be useful.)

[gasche]

(I think that it would be helpful to get @garrigue on this issue, maybe to suggest a fix or at least to explain more clearly what the code is doing and why.)

[garrigue]

The code here is a transcription of the explanation in https://www.math.nagoya-u.ac.jp/~garrigue/papers/injectivity2.pdf, particularly the last paragraph of section 2. Namely, since injectivity annotations are on type parameters, in presence of constraints a first approximation is to check that all type variables appearing inside the parameter are injective in the body. However, this does not cover the case where the variable is under a non-injective type constructor inside the parameter. To handle that case we need to check the occurrences of this constructor (with the same parameters), hence the use of is_equal. However, this leads to compare types coming from different contexts. So the sound thing would be just to ignore that specific type in case of errors. I will try to come up with a fix in that direction, i.e. a more precise handling of failure rather than a fatal error.

[nojb]

Thanks for the fix @garrigue!