Changes between Version 348 and Version 349 of TypeFunctionsStatus


Ignore:
Timestamp:
Jul 8, 2008 6:07:08 AM (6 years ago)
Author:
chak
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctionsStatus

    v348 v349  
    66 * Add the program of #1900 & #1999 and #1834 (but needs to use ghci) 
    77 
    8 '''Open Trac bugs related to type families''' 
     8'''Open bugs related to type families''' 
    99 
    1010 * Well-formedness of declarations involving families: 
     
    1313   * `tcFamInstDecl1` needs to allow family GADT instances. 
    1414  * #2157 (solution: lhs of type instances may not contain partially applied vanilla type synonyms) 
     15  * Check that the restrictions on equality constraints in instance and class contexts are enforced.  We should have tests for that in the testsuite.  Document the exact restrictions on the Haskell wiki tutorial page. 
    1516   * Addition to user manual, see [http://www.haskell.org/pipermail/haskell-cafe/2008-March/040989.html] and [http://www.haskell.org/ghc/docs/latest/html/users_guide/data-type-extensions.html#type-synonyms] 
    1617  * #2203 (TFs in class instance heads) 
     
    3738   * #1897: If you infer a type for a function, then should check the function against that sigature, to check that if the user gave that signature, then typechecking would again succeed.  See this thread http://www.haskell.org/pipermail/haskell-cafe/2008-April/041385.html.  #2418 suggests that for higher-kinded TFs, we could use decomposition more aggressively. 
    3839   * #1769 (deriving typeable for data families) 
     40   * When a `type instance` changes (in an orphan modules), currently clients are not properly recompiled at least by `--make`. 
    3941 
    4042'''Failing testsuite tests''' 
     
    4951''Check whether these still fail.'' 
    5052 
    51 '''Feature requests:''' 
     53'''Additional feature:''' 
    5254 * #2101 
     55 * Total families 
     56 * Allow repeated variable occurrences in lhses of type instances (see paper). 
     57 * Implementing FDs by TFs: 
     58   * 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`. 
     59   * Step 2: Desugar FDs into TFs and superclass equalities. 
     60   * ghci command to print normalised type and add [http://article.gmane.org/gmane.comp.lang.haskell.cafe/28799] as a test to the testsuite. 
    5361 
    5462'''Debugging of type families:''' 
    55  0. Total families 
    56  0. Allow repeated variable occurrences in lhses of type instances (see paper). 
     63 0. Single phase algorithm; cf `single_phase_algorithm.tex`. 
     64   * 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`. 
     65   * `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. 
     66   * 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 
     67{{{ 
     68type family F x 
     69type instance F [x] = [F x] 
     70 
     71t :: a -> a -> Bool 
     72t _ _ = True 
     73 
     74f :: a -> F [a] 
     75f = undefined 
     76 
     77test :: ([F a] ~ a) => a -> Bool 
     78test x = t x (f x) 
     79}}} 
     80  It is reject if the signature for `test` is present, but accepted if the signature is omitted (and inferred). 
    5781 0. Replacing GADT refinements by explicit equality constraints: 
    5882    * Regressions that remain to be fixed:  
     
    6993      2. check that the ... can be unified with t1..tn 
    7094     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. 
    71  0. Single phase algorithm; cf `single_phase_algorithm.tex`. 
    72  0. When a `type instance` changes (in an orphan modules), currently clients are not properly recompiled at least by `--make`. 
    73  0. Implementing FDs by TFs: 
    74    * 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`. 
    75    * Step 2: Desugar FDs into TFs and superclass equalities. 
    76  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`. 
    77  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. 
    78  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 
    79 {{{ 
    80 type family F x 
    81 type instance F [x] = [F x] 
    82  
    83 t :: a -> a -> Bool 
    84 t _ _ = True 
    85  
    86 f :: a -> F [a] 
    87 f = undefined 
    88  
    89 test :: ([F a] ~ a) => a -> Bool 
    90 test x = t x (f x) 
    91 }}} 
    92   It is reject if the signature for `test` is present, but accepted if the signature is omitted (and inferred). 
    9395 0. Comments: 
    9496   * When we raise a mismatch error in `TcSimplify` for unresolvable equalities, we effectively tidy the two non-matching types twice.  Add a comment to highlight this and say way it is ok (i.e., they are never grouped together with `groupErrs` or similar). 
    9597 0. `:t` in ghci doesn't print equalities in contexts properly. 
    96  0. ghci command to print normalised type and add [http://article.gmane.org/gmane.comp.lang.haskell.cafe/28799] as a test to the testsuite. 
    97  0. Check that the restrictions on equality constraints in instance and class contexts are enforced.  We should have tests for that in the testsuite.  Document the exact restrictions on the Haskell wiki tutorial page. 
    9898 0. When can foralls appear in equalities?  What constraints does that place on GADTs?  Also, the code in `TcTyFuns` doesn't really deal with rank-n types properly, esp `decompRule`. 
    9999 0. To fix `Simple8`: