#10079: Coercible solver regression: Couldn't match rep of () with Const () b -------------------------------------+------------------------------------- Reporter: glguy | Owner: goldfire Type: bug | Status: new Priority: high | Milestone: 7.10.1 Component: Compiler (Type | Version: 7.10.1-rc1 checker) | Keywords: Resolution: | Architecture: Operating System: Unknown/Multiple | Unknown/Multiple Type of failure: GHC rejects | Test Case: indexed- valid program | types/should_compile/T10079 Blocked By: | Blocking: Related Tickets: #7788, #8550 | Differential Revisions: Phab:D653 -------------------------------------+------------------------------------- Comment (by goldfire): I'm stalled here. :( The work I've done in Phab:D653 works quite well on fixing the bugs listed there, but it fails utterly if it sees a recursive newtype. Consider test case typecheck/should_compile/tc159: {{{ newtype A = A [A] deriving (Eq) }}} GHC naturally tries to use GND here but then gives up when it can't flatten `A` w.r.t. representational equality. Before Phab:D653, this case was handled by the `rec_nts` trick -- a newtype could be unwrapped only once. The problem with this trick is that it makes type inference a little wonky: canonicalization wasn't idempotent! For example, canonicalizing `Coercible skolem A` would get you `Coercible skolem [A]`. Canonicalizing again would give you `Coercible skolem [[A]]` and so on. Putting the `rec_nts` logic in the flattener would make that algorithm non-idempotent. This seems bad. I've flailed around looking for a solution but am coming up dry. (The solution was around this idea: if flattening were stuck in a loop, just return the original unflattened type. This didn't work out in practice, though, because usually the first few steps of flattening were not loopy (i.e., following filled tyvars) and then the flattener would loop. But detecting the loop isn't exactly straightforward.) I see a few possible ways forward: - Accept that representational equality simply omits recursive newtypes. This means that `Note [Recursive newtypes]` in !TcDeriv would have to change, and some programs that compile today would fail to do so. - Continue to use the `rec_nts` trick, meaning that the flattener is not idempotent. Recursive newtypes will still be problematic, though, because the canonicalizer will see a newtype, try to flatten it away, partially succeed (unwrapping one level) and then loop, doing the same thing. Somehow, the canonicalizer would have to be taught not to do this. - Give up on moving unwrapping newtypes into the flattener and devise another way to fix comment:9. The flattener would retain the code I've put there to track type function depths, still fixing some of the tickets listed in comment:22. Thoughts? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10079#comment:23 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler