... | ... | @@ -306,23 +306,30 @@ propagate eqs = prop eqs [] |
|
|
## Finalisation
|
|
|
|
|
|
|
|
|
The finalisation step instantiates as many flexible type variables as possible, but it takes care not to instantiate variables occurring in the global environment with types containing synonym family applications. This is important to obtain principle types (c.f., Andrew Kennedy's thesis). We perform finalisation in two phases:
|
|
|
The finalisation step instantiates as many flexible type variables as possible, but it takes care not to instantiate variables occurring in the global environment with types containing synonym family applications. This is important to obtain principle types (c.f., Andrew Kennedy's thesis). We perform finalisation in two steps:
|
|
|
|
|
|
1. **Substitution:**
|
|
|
|
|
|
- **Pass A:** For any variable equality of the form `co :: x ~ t` (both local and wanted), we apply the substitution `[t/x]` to the **right-hand side** of all equalities. We also perform the same substitution on class constraints.
|
|
|
- **Pass B:** Unless we are in inference mode, for any wanted family equality of the form `co :: F t1..tn ~ alpha`, we apply the substitution `[F t1..tn/alpha]` to **both sides** of all family equalities. We need to substitute all flexibles that arose as skolems during flattening of wanteds *before* we substitute any other flexibles.
|
|
|
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.)
|
|
|
- **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 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!!'''
|
|
|
**
|
|
|
|
|
|
|
|
|
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 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.
|
|
|
|
|
|
|
|
|
Note that it is an important property of propagation that we only need to substitute into right-hand sides during finalisation. After finalisation and zonking all flattening of locals is undone (c.f., note below the flattening code above).
|
|
|
Note that it is an important property of propagation that we need to substitute variable equalities only into right-hand sides during finalisation. After finalisation and zonking all flattening of locals is undone (c.f., note below the flattening code above).
|
|
|
|
|
|
## Examples
|
|
|
|
... | ... | |