[GHC] #9376: More informative error messages when closed type families fail to simplify (was: Recursive closed type families fails)

[GHC]

#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