|
# Normalising and Solving Type Equalities
|
|
# Normalising and Solving Type Equalities
|
|
|
|
|
|
|
|
|
|
The following is based on ideas for the new, post-ICFP'08 solving algorithm described in CVS `papers/type-synonym/new-single.tex`. Most of the code is in the module `TcTyFuns`.
|
|
The following is based on ideas for the new, post-ICFP'08 solving algorithm described in CVS `papers/type-synonym/new-single.tex`. A revised version of `new-single.tex` that integrates the core ideas from this wiki page is in `papers/type-synonym/normalised_equations_algorithm.tex`. Most of the code is in the module `TcTyFuns`.
|
|
|
|
|
|
## Terminology
|
|
## Terminology
|
|
|
|
|
... | @@ -25,12 +25,15 @@ Type variable that cannot be globally instantiated, but it may be **locally** re |
... | @@ -25,12 +25,15 @@ Type variable that cannot be globally instantiated, but it may be **locally** re |
|
## Overall algorithm
|
|
## Overall algorithm
|
|
|
|
|
|
|
|
|
|
The overall algorithm is as in `new-single.tex`, namely
|
|
The overall structure is as in `new-single.tex`, namely
|
|
|
|
|
|
1. normalise all constraints (both locals and wanteds),
|
|
1. normalise all constraints (both locals and wanteds),
|
|
1. solve the wanteds, and
|
|
1. solve the wanteds, and
|
|
1. finalise.
|
|
1. finalise.
|
|
|
|
|
|
|
|
|
|
|
|
However, the three phases differ in important ways. In particular, normalisation includes decompositions & the occurs check, and we don't instantiate any flexible type variables before we finalise (i.e., solving is purely local).
|
|
|
|
|
|
## Normal equalities
|
|
## Normal equalities
|
|
|
|
|
|
|
|
|
... | @@ -56,7 +59,7 @@ The following is interesting to note: |
... | @@ -56,7 +59,7 @@ The following is interesting to note: |
|
|
|
|
|
- We explicitly permit equalities of the form `x ~ y` and `a ~ b`, where both sides are either flexible or rigid type variables.
|
|
- We explicitly permit equalities of the form `x ~ y` and `a ~ b`, where both sides are either flexible or rigid type variables.
|
|
- Normal equalities are similar to equalities meeting the Orientation Invariant and Flattening Invariant of new-single, but they are not the same.
|
|
- Normal equalities are similar to equalities meeting the Orientation Invariant and Flattening Invariant of new-single, but they are not the same.
|
|
- Normal equalities are **never** self-recursive. They can be mutually recursive. A mutually recursive group will exclusively contain variable equalities. **SLPJ** why. What prevents `a ~ [b], b ~ [a]`?
|
|
- Normal equalities are **never** self-recursive. They can be mutually recursive. A mutually recursive group will exclusively contain variable equalities.
|
|
|
|
|
|
### Coercions
|
|
### Coercions
|
|
|
|
|
... | @@ -137,40 +140,97 @@ Notes: |
... | @@ -137,40 +140,97 @@ Notes: |
|
|
|
|
|
## Solving
|
|
## Solving
|
|
|
|
|
|
|
|
|
|
|
|
A significant difference to new-single is that solving is a purely local operation. We never instantiate any flexible variables.
|
|
|
|
|
|
**TODO**
|
|
**TODO**
|
|
|
|
|
|
- Rules applying to family equalities:
|
|
- Rules applying to family equalities:
|
|
|
|
|
|
- IdenticalLHS only applies to family equalities (both local and wanteds) - MAYBE only when at least one of the equalities is a local (see email).
|
|
- SubstFam (formerly, IdenticalLHS) only applies to family equalities (both local and wanteds)
|
|
- Top only applies to family equalities (both locals and wanteds)
|
|
- Top only applies to family equalities (both locals and wanteds)
|
|
|
|
|
|
>
|
|
>
|
|
> We should apply IdenticalLHS first as it cheaper and potentially reduces the number of applications of Top.
|
|
> We should apply SubstFam first as it cheaper and potentially reduces the number of applications of Top. On the other hand, for each family equality, we may want to try to reduce it with Top, and if that fails, use it with SubstFam. (That strategy should lend itself well to an implementation.) But be careful, we need to apply Top exhaustively, to avoid non-termination. More precisely, if we interleave Top and SubstFam, we can easily diverge.
|
|
|
|
|
|
- Rules applying to variable equalities:
|
|
- Rules applying to variable equalities:
|
|
|
|
|
|
- Unify only applies to all wanted flexible variable equalities
|
|
- SubstVar (formerly, Local) applies to variable equalities (both locals and wanteds)
|
|
- Subst (= local for variable equalities) applies to all variable equalities, where local variable equalities are substituted into all equalities, but wanted variable equalities are only substituted into wanted equalities.
|
|
- With SubstFam and SubstVar, we always substitute locals into wanteds and never the other way around. We perform substitutions exhaustively. For SubstVar, this is crucial to avoid non-termination.
|
|
|
|
- We should probably use SubstVar on all variable equalities before using SubstFam, as the former may refine the left-hand sides of family equalities, and hence, lead to Top being applicable where it wasn't before.
|
|
|
|
- We use SubstFam and SubstVar to substitute wanted equalities **only** if their right-hand side contains a flexible type variables (which for variable equalities means that we apply SubstVar only to flexible variable equalities).
|
|
|
|
|
|
|
|
|
|
|
|
Notes:
|
|
|
|
|
|
|
|
- In principle, a variable equality could be discarded after an exhaustive application of SubstVar. However, while the set of class constraints is kept separate, we may always have some occurrences of the supposedly eliminated variable in a class constraint, and hence, need to keep all local equalities around. That reasoning definitely applies to local equalities, but I think it also applies to wanteds (and I think that GHC so far never applies wanteds to class dictionaries, which might explain some of the failing tests.) Flexible variable equalities cannot be discarded in any case as we need them for finalisation.
|
|
|
|
|
|
|
|
### Observations
|
|
|
|
|
|
|
|
- SubstVar is the most expensive rule as it needs to traverse all type terms.
|
|
|
|
- Only SubstVar when replacing a variable in a family equality can lead to recursion with (Top).
|
|
|
|
|
|
|
|
## Finalisation
|
|
|
|
|
|
>
|
|
|
|
> We should first apply Unify where possible and, only when that is exhausted, apply Subst. This is as Unify is cheaper and has global impact (instantiates variables in the environment, too).
|
|
If only flexible type equalities remain as wanted equalities, the locals entail the wanteds. We can now instantiate type variables in flexible type equalities where possible to propagate constraints into the environment. In GHC, we may wrap any remaining equalities (of any form) into an implication constraint to be propagated outwards (where it may be solved under an extended set of local equalities.)
|
|
|
|
|
|
|
|
|
|
Notes:
|
|
Notes:
|
|
|
|
|
|
- (Unify) is an asymmetric rule, and hence, only fires for equalities of the form `x ~ c`, where `c` is free of synonym families. Moreover, it only applies to wanted equalities. (Rationale: Local equality constraints don't justify global instantiation of flexible type variables - just as in new-single.)
|
|
- (Unify) is an asymmetric rule, and hence, only fires for equalities of the form `x ~ c`, where `c` is free of synonym families. Moreover, it only applies to wanted equalities. (Rationale: Local equality constraints don't justify global instantiation of flexible type variables - just as in new-single.)
|
|
|
|
|
|
- (Local) only substitutes normal variable equalities - and currently also only local equalities, not wanteds. (We should call this Rule (Subst) again.)
|
|
- **TODO** Now that we delay instantiation until after solving, do we still need to prioritise flexible variables equalities over rigid ones? (Probably not.)
|
|
|
|
|
|
>
|
|
## Examples
|
|
> In principle, a rewrite rule could be discarded after an exhaustive application of (Local). However, while the set of class constraints is kept separate, we may always have some occurrences of the supposedly eliminated variable in a class constraint, and hence, need to keep all local equalities around.
|
|
|
|
|
|
|
|
- (IdenticalLHS) I don't think it is useful to apply that rule when both equalities are wanted, which makes it a variant of (Local). BUT as SLPJ points out what about `F a ~ x1, F a ~ Int`? Then we could unify the HM variable `x` with `Int`.
|
|
### Substituting wanted family equalities with SubstFam is crucial if the right-hand side contains a flexible type variable
|
|
|
|
|
|
### Observations
|
|
```wiki
|
|
|
|
Top: F Int ~ [Int]
|
|
|
|
|
|
|
|
|- F delta ~ [delta], F delta ~ [Int]
|
|
|
|
(SubstFam)
|
|
|
|
|- F delta ~ [delta], norm [[ [delta] ~ [Int] ]]
|
|
|
|
==>
|
|
|
|
|- F delta ~ [delta], delta ~ Int
|
|
|
|
(SubstVar)
|
|
|
|
|- norm [[ F Int ~ [Int] ]], delta ~ Int
|
|
|
|
==>
|
|
|
|
|- F Int ~ [Int], delta ~ Int
|
|
|
|
(Top)
|
|
|
|
|- norm [[ [Int] ~ [Int] ]], delta ~ Int
|
|
|
|
==>
|
|
|
|
|- delta ~ Int
|
|
|
|
QED
|
|
|
|
```
|
|
|
|
|
|
|
|
### Interaction between local and wanted family equalities
|
|
|
|
|
|
|
|
|
|
|
|
Example 4 of Page 9 of the ICFP'09 paper.
|
|
|
|
|
|
|
|
```wiki
|
|
|
|
F [Int] ~ F (G Int) |- G Int ~ [Int], H (F [Int]) ~ Bool
|
|
|
|
=(norm)=>
|
|
|
|
F [Int] ~ a, F b ~ a, G Int ~ b
|
|
|
|
|-
|
|
|
|
G Int ~ [Int], H x ~ Bool, F [Int] ~ x
|
|
|
|
(SubstFam w/ F [Int])
|
|
|
|
F [Int] ~ a, F b ~ a, G Int ~ b
|
|
|
|
|-
|
|
|
|
G Int ~ [Int], H x ~ Bool, x ~ a
|
|
|
|
(SubstFam w/ G Int)
|
|
|
|
F [Int] ~ a, F b ~ a, G Int ~ b
|
|
|
|
|-
|
|
|
|
b ~ [Int], H x ~ Bool, x ~ a
|
|
|
|
(SubstVar w/ x)
|
|
|
|
F [Int] ~ a, F b ~ a, G Int ~ b
|
|
|
|
|-
|
|
|
|
b ~ [Int], H a ~ Bool, x ~ a
|
|
|
|
```
|
|
|
|
|
|
- Rule (Local) -substituting variable equalities- is the most expensive rule as it needs to traverse all type terms.
|
|
**TODO** If we use flexible variables for the flattening of the wanteds, too, the equality corresponding to `x ~ a` above will be oriented the other way around. That can be a problem because of the asymmetry of the SubstVar and SubstFun rules (i.e., wanted equalities are not substituted into locals).
|
|
- Only (Local) when replacing a variable in the *left-hand side* of an equality of Form (1) can lead to recursion with (Top).
|
|
|
|
|
|
|
|
## Termination
|
|
## Termination
|
|
|
|
|
... | | ... | |