#9082: Unexpected behavior involving closed type families and repeat occurrences of variables ----------------------------------------------+---------------------------- Reporter: haasn | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type checker) | Version: 7.8.2 Resolution: invalid | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects valid program | Unknown/Multiple Test Case: | Difficulty: Unknown Blocking: | Blocked By: | Related Tickets: ----------------------------------------------+---------------------------- Comment (by goldfire): I'm confident that any ill-behaved `G` ''would'' require `UndecidableInstances`. But, note that while that extension is needed in order to ''define'' `G`, it is not needed in order to ''use'' `G`. So, even if you do not have `UndecidableInstances` in your module, you are still under threat from such an attack. Looking at the example in #8162, the problem would be exactly the same if the family `F` (the equivalent to your `Bad`) were a closed type family. Open type families `LA` and `LB` are used to expose the crash, but the family with the overlap could be made closed, as all of its instances are declared together. Note that `F` is defined ''without'' `UndecidableInstances`. There is the possibility that some very clever analysis (and restrictions on things like `G` and/or `UndecidableInstances`) could allow `Bad` to behave as you might like. Indeed, we haven't actually proved type safety in the presence of non-linear (i.e., with a repeated variable on the LHS) and non-terminating type families, even taking infinite unification into account. That proof seems to require a solution to a recognized [http://www.win.tue.nl/rtaloop/problems/79.html open problem]. This lack of a proof actually extends to ''open'' type families as well -- the published proofs about non-terminating open type families implicitly (and very subtly) assumed linear patterns. After spending a Long Time working on this proof and failing to either find a proof or a counterexample, we (the authors of the "Closed Type Families" paper) were happy enough to conjecture type safety and keep non-linear patterns in the language. All of this does add up to a slightly bumpy surface area for the closed type families feature. I'm quite aware of this and am somewhat disappointed about it. But, my thought is not to let the great become the enemy of the good here -- most uses of closed type families work in an intuitive way and are really helpful to people. Then, some uses work in a really unintuitive way, and people get confused. I still think it's a good trade-off. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9082#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler