Pack parameters to unification in unification_environment
#12109
Conversation
|
cc @goldfirere |
|
|
||
|
|
||
| (* a local constraint can be added only if the rhs | ||
| of the constraint does not contain any Tvars. | ||
| They need to be removed using this function *) | ||
| let reify env t = | ||
| let fresh_constr_scope = get_gadt_equations_level () in | ||
| let reify uenv t = |
There was a problem hiding this comment.
Could you add a comment saying this can be called only in Pattern mode?
| @@ -2466,30 +2469,23 @@ let find_lowest_level ty = | |||
| end | |||
| in find ty; unmark_type ty; !lowest | |||
|
|
|||
| let add_gadt_equation env source destination = | |||
| let add_gadt_equation uenv source destination = | |||
There was a problem hiding this comment.
Could you add a comment saying this can be called only in Pattern mode? Perhaps this is obvious from the name of the function, but I still think stating preconditions like this help newcomers to the codebase.
typing/ctype.ml
Outdated
| | Pattern r -> TypePairs.mem r.unify_eq_set (order_type_pair t1 t2) | ||
|
|
||
| (* unification during type constructor expansion; more | ||
| relaxed than [Expression] in some cases. *) |
There was a problem hiding this comment.
Though I see that this comment is just moved, could you maybe make "in some cases" more explicit? On the call this morning, you had a nice description of what this means, so putting that here -- or on the in_subst field declaration -- would be helpful.
typing/ctype.ml
Outdated
| @@ -2571,16 +2567,13 @@ let unify_package env unify_list lv1 p1 fl1 lv2 p2 fl2 = | |||
|
|
|||
|
|
|||
| (* force unification in Reither when one side has a non-conjunctive type *) | |||
| (* TODO: this could also be put in unification_environment? *) | |||
There was a problem hiding this comment.
Looks to me that this would go somewhere else -- maybe just a (labeled) boolean that gets passed around the eqtype functions? Those functions don't otherwise need the new env type available, so it seems that putting rigid_variants there would be a poor fit.`
| | Pattern r -> | ||
| let new_umode = Pattern { r with equations_generation = Forbidden } in | ||
| Misc.protect_refs [ Misc.R (umode, new_umode) ] f | ||
| let without_assume_injective uenv f = |
There was a problem hiding this comment.
Should these functions be non-CPS'd now? That would seem a little simpler.
Could be done in a separate PR, I suppose.
There was a problem hiding this comment.
Are there plans to do this?
|
Rebased and added comments according to Richard's requests. |
|
@goldfirere I wonder if you are happy with the revised state of this PR. |
typing/ctype.ml
Outdated
| @@ -2571,16 +2567,13 @@ let unify_package env unify_list lv1 p1 fl1 lv2 p2 fl2 = | |||
|
|
|||
|
|
|||
| (* force unification in Reither when one side has a non-conjunctive type *) | |||
| (* TODO: this could also be put in unification_environment? *) | |||
| | Pattern r -> | ||
| let new_umode = Pattern { r with equations_generation = Forbidden } in | ||
| Misc.protect_refs [ Misc.R (umode, new_umode) ] f | ||
| let without_assume_injective uenv f = |
There was a problem hiding this comment.
Are there plans to do this?
|
Is it possible for me to get enough rights in GitHub to Resolve my own conversations (at least)? It's very nice to clear conversations that arise from reviewing as the issues are addressed. Thanks! |
|
@goldfirere I have added comments related to your questions. We do not plan to modify without_* functions or rigid_variants immediately. |
|
Merged, thank you both for the PR and review work. |
Ctype.unifyand related functions used to take a reference to the environment as a parameter and some additional flags via global variables.This PR packs them in a type
unification_environmentwhose contents depend on the unification mode.We have uniformly used the variable name
uenvfor values of typeunification_environmentandenvforEnv.t.