68 | | 0. Single phase algorithm; cf `single_phase_algorithm.tex`. |

69 | | * 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`. |

70 | | * `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. |

71 | | * 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 that is rejected if the signature for `test` is present, but accepted if the signature is omitted (and inferred), consider |

72 | | {{{ |

73 | | type family F x |

74 | | type instance F [x] = [F x] |

75 | | |

76 | | t :: a -> a -> Bool |

77 | | t _ _ = True |

78 | | |

79 | | f :: a -> F [a] |

80 | | f = undefined |

81 | | |

82 | | test :: ([F a] ~ a) => a -> Bool |

83 | | test x = t x (f x) |

84 | | }}} |

| 68 | 0. Open points in the new `TcTyFuns` code: |

| 69 | * extract from `TODO`s in `TcTyFuns` |

| 70 | 0. Issues in `TcSimplify`: |

| 71 | * Why does the call to `reduceList` (in `reduceContext`) extend the LIE? What are the produced `extra_eqs`? (Put an assert there and run the testsuite to see whether `extra_eqs` is non-empty in any of the tests.) |