#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