Re: [Caml-list] Expansion of type-constructors in ctype.ml

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

On 2015/08/24 19:15, Christoph Höger wrote:
> 
> find attached a patch against the 4.02.3 tree that solves my issue with
> compiling the problematic examples.
> 
> I am pretty confident that the change to eqtype is sound, I do not know
> exactly what moregen() is intended to do, though and it seems that its
> side-effects are required (that is why I expand the types there in any
> case).
> 
> I appreciate any further comments,
> 
> Christoph

Do you mean that modifying moregen and eqtype (but not unify)
in a conservative way would be enough to solve your problem?
Then indeed we could do that.
At least your code for eqtype seems fine. For moregen, this is not sufficient, due to non-local side effects.
By the way, we should keep your example around to prevent regressions.

On 2015/08/24 15:22, Christoph Höger wrote:
> Am 24.08.2015 um 00:18 schrieb Jacques Garrigue:
>> This is indeed a pretty difficult problem, as you must be careful of not
>> changing the semantics of unification.
>> Until recently, the only solution was to expand the type, as there was
>> no static information cacheing whether an argument was used in the
>> body or not.
>> However, since relatively recent changes about variance information
>> (the switch to 7 flags…), we actually have at least an approximation
>> of which unifications must be done imperatively, and which needn’t
>> be done at all.
>> So it might be doable at least for part of the parameters.
> 
> That sounds interesting. What are the relevant variance flags?
> 
You should read the following paper:
http://www.math.nagoya-u.ac.jp/~garrigue/papers/injectivity.pdf

If all the flags were always correct then it would be simple: any flag being
set would mean that the variable really appears in the type, so you must
recurse on it (at least for eqtype and moregen).
However, variance inference for the result of functors is not exact,
meaning that to be sure that a variable will not disappear, you must check
that inj is set (meaning that there is a concrete occurence).
In a nutshell:
may_pos and may_neg are both unset (i.e. nothing is set) => no need to recurse
inj is set => must recurse
otherwise => must expand

 Jacques Garrigue