Changes between Version 298 and Version 299 of TypeFunctionsStatus


Ignore:
Timestamp:
Feb 28, 2008 1:52:41 AM (6 years ago)
Author:
chak
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctionsStatus

    v298 v299  
    3030 0. Allow overlapping instances disambiguated by textual order if they are in the same model (maybe only when an extra flag is given).  Instances from differnt modules still need to have coinciding rhses if they overlap. 
    3131 0. Replacing GADT refinements by explicit equality constraints: 
     32    * CLEANUP: 
     33     * `TcGadt.tcUnifyTys` can now probably be replaced again by the non-side-effecting unifier that was in `types/Unify.hs` (recover from previous repo states). 
     34     * `TcPat.refineAlt`: This function is now dead code, so is all its support code. 
     35     * `pat_reft` field of `TcPat.PatState`: Not needed anymore and code maintaining can go, too. 
     36     * We can remove the `CoVars` and `Refinement` argument of `TcSimplify.tcSimplifyCheckPat`. 
    3237    * Regressions that remain to be fixed:  
    3338      * `gadt/lazypatok` needs to be fixed (are irrefutable patterns really ok, see http://okmij.org/ftp/Haskell/GADT-problem.hs]?) 
     
    4045      * we  need to know of types whether they are rigid (not only whether they contain unification variables, but by a flag in the environment that indicates whether the computation of that type involved non-rigid type variables) 
    4146    * In `TcUnify`, make all occurs checks more elaborate.  They should only '''defer''' if the checked variable occurs as part of an argument to a type family application; in other cases, still fail right away.  DONE? 
    42     * `TcGadt.tcUnifyTys` can now probably be replaced again by the non-side-effecting unifier that was in `types/Unify.hs` (recover from previous repo states). 
    43     * CLEANUP: 
    44      * `TcPat.refineAlt`: This function is now dead code, so is all its support code. 
    45      * `pat_reft` field of `TcPat.PatState`: Not needed anymore and code maintaining can go, too. 
    46      * We can remove the `CoVars` and `Refinement` argument of `TcSimplify.tcSimplifyCheckPat`. 
    4747    * Re `tcfail167`, SPJ proposes that could generate a better error message, at least most of the time.  If the "expected type" of a pattern is 's', and we meet a constructor with result type (T t1 ..tn), then one could imagine a 2-step process: 
    4848      1. check that 's' is (or can be made to be) of form (T ....) 
    4949      2. check that the ... can be unified with t1..tn 
    5050     If (1) succeeds but (2) fails, the alternative is in accessible.  Of course, (2) might fail "later" by generating a constraint that later can't be satisfied, and we won't report that well, but we'd get a good message in the common fails-fast case.  We could even improve the message from (1) to say: "Constructor C is from data type T, but a pattern of type s is expected. 
     51 0. Implementing FDs by TFs: 
     52   * Step 1: Replace the existing improvement machinery for FDs by code that generates explicit equalities from the two FD rules.  Then, all improvement is by normalisation of equalities, which hopefully allows us to simplify `TcSimplify.reduceContext`. 
     53   * Step 2: Desugar FDs into TFs and superclass equalities. 
     54 0. Clean up `TcSimplify.reduceContext` and try to get rid of of having two loops, namely the ones used in `TcTyFuns` and the one implemented by `checkLoop`. 
    5155 0. `substEqInDict` needs to be symmetric (i.e., also apply right-to-left rules); try to re-use existing infrastructure.  It would be neater, easier to understand, and more efficient to have one loop that goes for a fixed point of simultaneously rewriting with given_eqs, wanted_eqs, and type instances. 
    5256 0. skolemOccurs for wanteds?  At least `F a ~ [G (F a)]` and similar currently result in an occurs check error.  Without skolemOccurs in wanted, the occurs check for wanted would need to be smarter (and just prevent cyclic substitutions of the outlined form silently).  However, when inferring a type, having the rewrites enabled by skolemOccurs available will leads to potentially simpler contexts.  As an example consider 
     
    149153 
    150154Todo (high-level):  
    151  1. Type checking of type families; routines in `TcUnify` that still need to be extended: 
    152    * `boxySplitTyConApp`: The second argument (`BoxyRhoType`) can be a synonym family application.  Then, we must produce a wanted coercion and return a `HsWrapper` value that applies that coercion. 
    153    * `boxySplitAppTy`: Basically, the same deal as the previous. 
    154  2. Type checking in the presence of associated synonym defaults.  (Default AT synonyms are only allowed for ATs defined in the same class.) 
    155  3. Type check functional dependencies as type functions. 
     155 1. Type checking in the presence of associated synonym defaults.  (Default AT synonyms are only allowed for ATs defined in the same class.) 
     156 2. Type check functional dependencies as type functions. 
    156157 
    157158Done:  
     
    161162 * Consistency checking for family instances. 
    162163 * Enforce syntactic constraints on type instances needed to ensure the termination of constraint entailment checking. 
     164 * Equality constraint normalisation and coercion term generation. 
    163165 
    164166== Desugaring ==