[GHC] #10079: Coercible solver regression: Couldn't match rep of () with Const () b

[GHC]

#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