Erroneous "Constraints are not satisfied in this type" with mutually recursive abbreviations

[goldfirere]

When I say

type 'a t = 'a foo foo
and 'a foo = int constraint 'a = int

ocaml says

File "scratch.ml", line 1, characters 0-22:
1 | type 'a t = 'a foo foo
    ^^^^^^^^^^^^^^^^^^^^^^
Error: Constraints are not satisfied in this type.
       Type int should be an instance of 'a foo
       foo is abstract because no corresponding cmi file was found in path.

But this program should be accepted, I think, with something like this signature:

type 'a t = int constraint 'a = int
type 'a foo = int constraint 'a = int

I think the problem is that Typedecl.check_regularity uses the orig_env when checking arguments -- but the orig_env doesn't know that 'a foo is an abbreviation for int when checking the manifest of t. I don't know enough of what's going on here to suggest a fix. But even if a proper fix is out of reach, the error message definitely has room for improvement: int is an instance of 'a foo (because they're equal) and there is no missing cmi file involved.

[garrigue]

The use of orig_env is intentional: in order to allow polymorphic recursion between types, constraints have to be checked without looking at the actual definition; we just distinguish between nominal types (that cannot be expanded) and abbreviations (that expand to a type variable). So yes, you cannot assume that foo is int when checking constraints inside the definition of t.

This said, the error message is really bad. I don't know who added this logic, I suppose it needs to be tuned to recognize that foo is not yet defined.

[goldfirere]

Thanks for that explanation. It definitely looked like the orig_env was intentional. Do you have an example of the kind of polymorphic recursion you're thinking of? I would expect polymorphic recursion in type definitions to arise only when there is some aspect of kind polymorphism, but OCaml lacks that.

[xavierleroy]

I don't know about you, but I'm definitely not expecting the typechecker to deduce

type 'a t = int constraint 'a = int
type 'a foo = int constraint 'a = int

as the only solution of

type 'a t = 'a foo foo
and 'a foo = int constraint 'a = int

As much as I like type inference and constraint resolution, for type declarations I'd prefer the typechecker to just check them but not transform them that much.

[goldfirere]

I've found it odd that this is accepted:

type 'a t1 = 'a constraint 'a = int
type 'a t2 = 'a t1

which is inferred to have signature

type 'a t1 = 'a constraint 'a = int
type 'a t2 = 'a t1 constraint 'a = int

Inferring the constraint on t2 came as a surprise to me -- but it's what's already there (and I see how it's useful in the context of the object system). Given this, though, I do think inferring constraints on my original program is reasonable. The signature I gave also expanded right-hand sides (e.g. replacing 'a foo foo with int); that might be a step too far and goes beyond what OCaml does today.

[garrigue]

@goldfirere I don't quite recall the motivating example, but you can have polymorphic recursion by using distinct instances of the same abbreviation in the same mutually recursive definition.

type 'a located = 'a * string * int
and pattern = pattern_desc located
and pattern_desc = ...
and expression = expression_desc located
and expression_desc = ...

Of course, in this case you can easily break the recursion, but with more contrived examples this becomes difficult.

[gasche]

Naive questions arising from following this discussion.

And what would go wrong if we checked constraints in a mutually-recursive nest with the definitions in scope? I suppose that the problem would be non-termination due to non-well-founded definitions. This gives two questions:

1. Do I correctly understand that constraint-checking happens before checking for well-foundedness, then? Could we solve the problem by checking for well-foundedness and constraint-well-formedness at the same time?
2. In fact, do we need to assume well-foundedness to check constraints in a correct and terminating way? What if we allowed the unifications involved in constraint checking to create cyclic structural types, and count on a later well-foundedness check to detect and prevent this?

[goldfirere]

In response to @garrigue: I think the issue here is really the definition of "polymorphic recursion". Moving to the more familiar territory of terms, I consider polymorphic recursion to have happened when you have a recursive function whose recursive uses are inferred to have different type instantiation. To me, there are three essential aspects of polymorphic recursion (at least as it affects inference -- or the lack thereof): (1) the instantiation is inferred, and (2) the instantiated parameter is dependent, and (3) the instantiated parameter is different than it was at the definition site. In the mutually-recursive types example above, we have (3) but neither (1) nor (2) (though maybe (2) is a bit squishy in the case of abbreviations).

In any case, GHC needs to worry about polymorphic recursion only in the presence of its kind inference. The closest GHC equivalent to the check we're worrying about here is its abbreviation cyclicity check, which is just a fairly straightforward look for cycles, stopping whenever a non-abbreviation is hit.

So maybe a better question to aid my understanding is: why do we need to check for regularity in this way? Or, if it's more helpful and implementation-oriented: couldn't we just do a cyclicity check without unification first, and then check the constraints later?

[gasche]

Or, if it's more helpful and implementation-oriented: couldn't we just do a cyclicity check without unification first, and then check the constraints later?

We have to be careful because constraints can introduce cycles:

type 'a t = 'a -> 'a constraint 'a = 'a t

I looked at the typedecl.ml code again and here are some extra remarks mostly for myself:

• Constraints are in fact "checked" in check_constraints that is called after the check for well-foundedness.
• The example of this PR fails in check_regularity which is called before check_constraints but after the check for well-foundedness.
• I'm not sure how cycles involving constraints are detected by the well-foundedness checker, if constraints are only enforced later. (This may be related to the it_type_declaration visitor also visiting params, which in general are type expressions that constrain the parameters; or to the expansions performed during well-foundedness checking applying constraints as substitutions on the fly.)

[garrigue]

So maybe a better question to aid my understanding is: why do we need to check for regularity in this way? Or, if it's more helpful and implementation-oriented: couldn't we just do a cyclicity check without unification first, and then check the constraints later?

Due to the presence of equi-recursive types and constraints on type parameters, the cyclicity check in ocaml is much more complex than in GHC.
Actually, it is not even correct currently (see #9314, and #11648 which fixes it by a large change to the handling of type expansion).
The problem here is that type parameter constraints are enforced through unification on the fly when we translate syntactic types. Which is all well as long as there are no recursive definitions. In presence of recursive definitions, there are two conceptually easy solution: either (1) require that all parameter constraints be explicit in the definition, so that they are already enforced when we translate types, or (2) propagate constraints a posteriori through unification. OCaml used to do (2), at the cost that type abbreviations included in a mutual recursion had to be monomorphic to allow back propagation through unification. So we moved to (1), still allowing constraints inherited from already existing definitions (not involved in the recursion). This still requires a lot of work to check a posteriori that all constraints are correctly enforced, and that recursion is regular (i.e. equi-recursive types can be expanded to finite graphs).

[goldfirere]

Aha -- so OCaml does not allow propagation of constraints within a mutually recursive group of type definitions. I did not know that. But it nicely explains why my original program is rejected. Is this design decision documented anywhere? It would be great for it to appear in the manual, but maybe is too detailed (given that there are other aspects of the type system not accurately described there)?

If we're happy with "do not propagate constraints within a mutually recursive group" (I am), then this bug is just a request for a better error message (and something I perhaps could take on myself).

However, this conversation then opens a question for me: I've been thinking about Jane Street's layout system as closely analogous to constraints. Whenever there has been a design question, we look at constraints to see what happens there to get an intuition. But I had not understood about the lack of constraint propagation, and so layouts do propagate within mutually recursive definitions. For example:

type 'a t = 'a t2
and 'b t2 = { x : int; y : ('b : float64); z : 'b t option }

This would infer that 'b has layout float64, which would then propagate to 'a. This is all implemented and works just fine. But maybe we're missing something here and should cut off propagation? I think it's probably fine to propagate layouts because layouts cannot depend on types (unlike constraints), but there's a chance I've overlooked something.

[garrigue]

For the first point, this was indeed a bad interaction between a not-so-legit use of an original environment and improved error messages reporting the absence of actual definition. This is fixed in #12368, which you're welcome to review if you are willing to delve into this part of the code. Fortunately the change is relatively trivial, once you understand that undefined types already behaved as abstract types for the type checker. I also fixed a wrong parameter order.

For your second question, the problem is just whether you can separate your propagation phase from the wellformedness check. If you can check the wellformedness of types, and then propagate, I believe this should be fine. We also do this kind of propagation for variance for instance.