#9376: More informative error messages when closed type families fail to simplify -------------------------------------+------------------------------------- Reporter: | Owner: MikeIzbicki | Status: new Type: feature | Milestone: request | Version: 7.8.2 Priority: normal | Keywords: Component: Compiler | Architecture: Unknown/Multiple (Type checker) | Difficulty: Unknown Resolution: | Blocked By: Operating System: | Related Tickets: Unknown/Multiple | Type of failure: | None/Unknown | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Changes (by goldfire): * type: bug => feature request Comment: The behavior seen here is as "expected", for a sufficiently nuanced expectation. I don't see an implementation bug here. Let's look at the two different definitions in play: {{{ type family OrdRec1 f a b where -- closed families do kind inference! OrdRec1 f a (f b) = (Ord a, Ord (f b), OrdRec1 f a b) OrdRec1 f a b = (Ord a, Ord b) type family OrdRec2 f a b where OrdRec2 f1 a1 (f1 b1) = (Ord a1, Ord (f1 b1)) OrdRec2 f2 a2 b2 = (Ord a2, Ord b2) }}} Let's try to simplify `OrdRec1 Set.Set a b`, for some universally- quantified `a` and `b`. The first equation of `OrdRec1` clearly doesn't apply, and the second equation doesn't clearly apply. What I mean here is that we don't know enough about `b`: if we later learn that `b` is `Set.Set Int`, then we really should have used the first equation. GHC will not commit to a later equation when there's a possibility of using an earlier one, if it learns more about the variables involved. So, GHC gives up and refuses to simplify. When testing with concrete types, as you have done in GHCi, `OrdRec1` works just fine, as then it can be quite sure of which equation to pick. But how does `OrdRec2` work? As kosmikus guesses, GHC notices that the two cases are, in the terminology of the paper, ''compatible''. Specifically, GHC looks at the LHSs and finds that they unify, under the substitution `[f2 |-> f1, a2 |-> a1, b2 |-> f1 b1]`. Then, GHC asks: will the RHSs then become the same under that substitution? In this case, the answer is '''yes''', so GHC marks the equations as ''compatible''. The benefit of compatibility is that GHC then isn't so sensitive about premature commitment among compatible equations. After all, if GHC chooses the second equation, but later learns that the first should be used, it wouldn't have gotten a different answer, as long as the equations are compatible. For better or worse, you can observe some of this reasoning in `OrdRec1` if you reorder either RHS. Even though constraint tuples are considered to be order-less sets, the compatibility algorithm doesn't know this, and if one of the RHSs is reordered, the compatibility check fails and GHC becomes more careful about committing to an equation during simplification. I'm going to leave this ticket open as a request for a better error message, as this issue comes up every so often, and I'd like not to have to answer it individually each time. I think that it should be possible to note when GHC is hesitant to commit to an equation and then suggest to a user to learn more about closed type families, with a helpful link. The error message, or perhaps a new facility in GHCI, might also point out the compatibility relationships among equations, as these relationships are sometimes key to understanding a closed type family's behavior and are sometimes non-trivial for a human to derive. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9376#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler