[GHC] #15557: Reduce type families in equations' RHS when testing equation compatibility

[GHC]

#15557: Reduce type families in equations' RHS when testing equation compatibility
-------------------------------------+-------------------------------------
        Reporter:  mniip             |                Owner:  (none)
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:  8.6.1
       Component:  Compiler (Type    |              Version:  8.4.3
  checker)                           |
      Resolution:                    |             Keywords:  TypeFamilies
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  GHC rejects       |  Unknown/Multiple
  valid program                      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #8423 #15546      |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by goldfire):

 I'm not sure what you're suggesting here. comment:3 and comment:4 seem (I
 didn't fully dig through them) to be a restatement of some of the
 arguments in #8423. Is that correct?

 The algorithm in comment:10:ticket:8423 is long lost on some probably-
 obliterated git branch. Do you think it would address your use case?

 Maybe what you're suggesting is that (for closed type families at least)
 we can reduce fully-known (i.e. not in the same recursive group) type
 families on the RHS. That may indeed be true. For open type families,
 though, we're stuck, because they're never fully known. And if there is a
 way for these type families not to terminate, I'm lost as to what the
 answer is.

 My bottom line: I'm sure there is room for improvement in this direction,
 but the path forward is narrow and bordered by heffalump traps. The CTFwOE
 team got mired in many of them. I'd want a solid proof before implementing
 any new ideas in this area.

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15557#comment:5>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler