Changes between Version 271 and Version 272 of TypeFunctionsStatus

Nov 20, 2007 7:08:29 AM (7 years ago)



  • TypeFunctionsStatus

    v271 v272  
    3232'''Debugging of type families:''' 
    33  0. To move GADT type checking from refinements to equalities, proceed as follows (as suggested by SPJ): 
    34     * Results: 
    35       * Impact on testsuite:  
     33 0. Replacing GADT refinements by explicit equality constraints: 
     34    * Impact on testsuite:  
    3736== indexed-types/ == 
    7675     * `pat_reft` field of `TcPat.PatState`: Not needed anymore and code maintaining can go, too. 
    7776     * We can remove the `CoVars` and `Refinement` argument of `TcSimplify.tcSimplifyCheckPat`. 
     77    * 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, then one could imagine a 2-step process: 
     78      1. check that 's' is (or can be made to be) of form (T ....) 
     79      2. check that the ... can be unified with 
     80     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. 
    7881 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. 
    7982 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.