... | ... | @@ -147,6 +147,23 @@ The essentials of a module after type checking are in `HscTypes.ModGuts`; in par |
|
|
|
|
|
Refined idea: Instead of duplicating the `InstInfo`/`Instance` infrastructure for instances of indexed types, we could just add a second variant to `InstInfo`. This has the advantage that functions, such as `tcInstDecls1`, still only have to return a list of `InstInfo` and not two different lists.
|
|
|
|
|
|
## Type checking equational constraints
|
|
|
|
|
|
|
|
|
Constraints are turned into dictionaries by `Inst.newDictBndrs`. For equational constraints, that is the place where *given* equalities are introduced.
|
|
|
|
|
|
**TODO** Where do we perform the detailed check of well-formedness of equalities? In `check_pred_ty` or when adding given equalities?
|
|
|
|
|
|
## Unification in the presence of type functions
|
|
|
|
|
|
|
|
|
We do *not* rewrite type function applications implicitly during unification. Instead, unifcation returns all *required* equalities that are non-syntactic. That has two advantages: (1) the computation of coercions is completely decoupled from unification and (2) unification does not have to know anything about equality axioms and given equalities.
|
|
|
|
|
|
**TODO** The whole extension would be a lot less invasive if we could arrange for unification to enter the required constraints into a pool in the monad instead of returning them (as the type of the unification routines would stay the same). Is this possible?
|
|
|
|
|
|
|
|
|
Required equalities are then checked against the axioms and given equalities during context simplification, much like class predicates.
|
|
|
|
|
|
## Type checking expressions
|
|
|
|
|
|
### Pattern matching indexed data types
|
... | ... | |