Changes between Version 348 and Version 349 of TypeFunctionsStatus
 Timestamp:
 Jul 8, 2008 6:07:08 AM (9 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

TypeFunctionsStatus
v348 v349 6 6 * Add the program of #1900 & #1999 and #1834 (but needs to use ghci) 7 7 8 '''Open Tracbugs related to type families'''8 '''Open bugs related to type families''' 9 9 10 10 * Wellformedness of declarations involving families: … … 13 13 * `tcFamInstDecl1` needs to allow family GADT instances. 14 14 * #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. 15 16 * Addition to user manual, see [http://www.haskell.org/pipermail/haskellcafe/2008March/040989.html] and [http://www.haskell.org/ghc/docs/latest/html/users_guide/datatypeextensions.html#typesynonyms] 16 17 * #2203 (TFs in class instance heads) … … 37 38 * #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/haskellcafe/2008April/041385.html. #2418 suggests that for higherkinded TFs, we could use decomposition more aggressively. 38 39 * #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`. 39 41 40 42 '''Failing testsuite tests''' … … 49 51 ''Check whether these still fail.'' 50 52 51 ''' Feature requests:'''53 '''Additional feature:''' 52 54 * #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. 53 61 54 62 '''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 righttoleft rules); try to reuse 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 {{{ 68 type family F x 69 type instance F [x] = [F x] 70 71 t :: a > a > Bool 72 t _ _ = True 73 74 f :: a > F [a] 75 f = undefined 76 77 test :: ([F a] ~ a) => a > Bool 78 test 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). 57 81 0. Replacing GADT refinements by explicit equality constraints: 58 82 * Regressions that remain to be fixed: … … 69 93 2. check that the ... can be unified with t1..tn 70 94 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 failsfast 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 righttoleft rules); try to reuse 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 consider79 {{{80 type family F x81 type instance F [x] = [F x]82 83 t :: a > a > Bool84 t _ _ = True85 86 f :: a > F [a]87 f = undefined88 89 test :: ([F a] ~ a) => a > Bool90 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).93 95 0. Comments: 94 96 * When we raise a mismatch error in `TcSimplify` for unresolvable equalities, we effectively tidy the two nonmatching 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). 95 97 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.98 98 0. When can foralls appear in equalities? What constraints does that place on GADTs? Also, the code in `TcTyFuns` doesn't really deal with rankn types properly, esp `decompRule`. 99 99 0. To fix `Simple8`: