... | ... | @@ -313,17 +313,21 @@ The finalisation step instantiates as many flexible type variables as possible, |
|
|
- **Step A:** For any (local or wanted) variable equality of the form `co :: x ~ t`, we apply the substitution `[t/x]` to the **right-hand side** of all equalities (wanteds only to wanteds). We also perform the same substitution on class constraints (again, wanteds only to wanteds).
|
|
|
- **Step B:** We have two cases:
|
|
|
|
|
|
- *In checking mode,* for any wanted family equality of the form `co :: F t1..tn ~ alpha`, we apply the substitution `[F t1..tn/alpha]` to the right-hand side of all wanted variable equalities and to both sides of all wanted family equalities with the exception that, if `alpha` is a local flexible (introduced during flattening of wanteds), we do **not** substitute into family equalities of the form `co' :: G s1..sm ~ delta`, where `delta` is a non-local flexible.
|
|
|
- *In checking mode,* for any wanted family equality of the form `co :: F t1..tn ~ alpha`, where `alpha` is a skolem flexible, we apply the substitution `[F t1..tn/alpha]` to the right-hand side of all wanted variable equalities and to both sides of all wanted family equalities.
|
|
|
- *In inference mode,* we proceed as in checking mode, but we do not substitute into variable equalities.
|
|
|
1. **Instantiation:** For any variable equality of the form `co :: alpha ~ t` or `co :: a ~ alpha`, where `co` is wanted, we instantiate `alpha` with `t` or `a`, respectively, and set `co := id`. Moreover, we have to do the same for equalities of the form `co :: F t1..tn ~ alpha` unless we are in inference mode and `alpha` appears in the environment or any other wanteds. (We never instantiate any flexibles introduced by flattening locals.) **!!FIXME: Take the escaped locals into account!!'''
|
|
|
**
|
|
|
- **Step C:** Same as Step B, but `alpha` is not a skolem flexible.
|
|
|
|
|
|
>
|
|
|
> At this point all variables bound in the next step have disappeared from the constraint set; it is as if the variables have been locally instantiated.
|
|
|
|
|
|
1. **Instantiation:** For any variable equality of the form `co :: alpha ~ t` or `co :: a ~ alpha`, where `co` is wanted, we instantiate `alpha` with `t` or `a`, respectively, and set `co := id`. Moreover, we have to do the same for equalities of the form `co :: F t1..tn ~ alpha` unless we are in inference mode and `alpha` appears in the environment or is a local skolem flexible that is propagated into the environment by another binding.
|
|
|
|
|
|
|
|
|
Important points are the following:
|
|
|
|
|
|
- The substitution step can lead to recursive equalities; i.e., we need to apply an occurs check after each substitution.
|
|
|
- We perform substitutions in two steps due to situations as ` F s ~ alpha, alpha ~ t`. Here, we want to substitute `alpha ~ t` first as `alpha` may occur in class dictionaries where a rigid type may help to select a class instance.
|
|
|
- We need to substitute all flexibles that arose as skolems during flattening of wanteds *before* we substitute any other flexibles. Consider `F delta ~ alpha, F alpha ~ delta`, where `alpha` is a skolem and `delta` a free flexible. We need to produce `F (F delta) ~ delta` (and not `F (F alpha) ~ alpha`). Otherwise, we may wrongly claim to having performed an improvement, which can lead to non-termination of the combined class-family solver.
|
|
|
- We need to substitute all flexibles that arose as skolems during flattening of wanteds *before* we substitute any other flexibles. Consider `F delta ~ alpha, F alpha ~ delta`, where `alpha` is a skolem and `delta` a free flexible. We need to produce `F (F delta) ~ delta` (and not `F (F alpha) ~ alpha`). Otherwise, we may wrongly claim to having performed an improvement, which can lead to non-termination of the combined class-family solver — this is the reason for separating Step B and Step C.
|
|
|
- We need to substitute family equalities into both sides of family equalities; consider, `F t1..tn ~ alpha, G s1..sm ~ alpha`.
|
|
|
- We must not substitute family equalities into right-hand sides of variable equalities. (If the variable equality directly or indirectly instantiates a flexible that is free in the environment, we would instantiate it with a family application, which we set out to avoid.)
|
|
|
- There is no need to substitute family equalities into dictionaries as they cannot influence instance selection.
|
... | ... | |