Comment author: @garrigue

I've added 2 patches.
shortcut_known_occurences implements the strategy I described, of using the variance information. Unfortunately, this does not work in your case, because your are using constraints:
class ['a] c : 'a ->
object constraint 'a = < foo : 'b; .. > method m_1 : 'b method m_2 : 'b end
Here, [t1 c = t2 c] is not equivalent to [t1 = t2], because only the type of the method foo is used in the body.
This patch can be made to work by changing the type annotations in the generated code:
class ['a] c (a : <foo : 'a; ..>) = ...
But it is still slower than your patch.

large_classes2 is a fix of your patch. It registers the type pair, for recursion going through parameters (see tests/typing-labels/mixin.ml), and backtracks in moregen to undo side-effects. It seems correct to me, but I have a slight concern about performance: it may actually be slower than just expanding in some cases. It is hard to measure. Also, currently the testsuite goes through (everything compiles), but some types are printed wrongly. Try doing
cd testsuite; make list FILE=typing
Need to look into that.
Also I don't understand your comment about the need to expand afterwards. Do you have a concrete example?

Comment author: choeger

The seemingly redundant expansion was required in practice, since compiling the 4.02.3 branch without yielded a "incosistent assumptions" error regarding the signature of hashtabl. I really do not understand why this occured, maybe I just misused the build system ;).

Comment author: choeger

Here, [t1 c = t2 c] is not equivalent to [t1 = t2], because only the type of the method foo is used in the body.

That is one aspect, I do not understand about injectivity analysis: When 'a is constrained by some type variable 'b and 'b is injective, how can 'a ever vanish through expansion?

Comment author: @garrigue

That is one aspect, I do not understand about injectivity analysis: When 'a is constrained by some type variable 'b and 'b is injective, how can 'a ever vanish through expansion?

This is the other way round: the expanded type is <m_1 : 'b; m_2 : 'b>.
'a doesn't appear in it, so it is not inferred as injective.
For instance <foo: int; bar: bool> c and <foo: int; bar: string> c are equal,
since they expand both to <m_1 : int; m_2 : int>

Comment author: choeger

True. But that is not a problem, since (my understanding of) injectivity only gives

t1 = t2 => t1 c = t2 c

So IMO c is injective in its argument, since there exists a type variable that is bound by some constraint on its argument and appears in the expansion. Is that not correct?

Comment author: @garrigue

This one is not injectivity, but just functional equality, which is valid for any type definition (a type is entirely determined by its parameters).
It's fine, but it requires backtracking.

Comment author: choeger

Of course. Sorry, that was plain wrong.

Comment author: @garrigue

Downgrade to feature, as it's not clear how big are the types we should actively support.

This issue has been open one year with no activity. Consequently, it is being marked with the "stale" label. What this means is that the issue will be automatically closed in 30 days unless more comments are added or the "stale" label is removed. Comments that provide new information on the issue are especially welcome: is it still reproducible? did it appear in other contexts? how critical is it? etc.