[GHC] #13333: Typeable regression in GHC HEAD

[GHC]

#13333: Typeable regression in GHC HEAD
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  bgamari
            Type:  bug               |               Status:  new
        Priority:  high              |            Milestone:  8.2.1
       Component:  Compiler (Type    |              Version:  8.1
  checker)                           |
      Resolution:                    |             Keywords:  typeable
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  GHC rejects       |  Unknown/Multiple
  valid program                      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):  Phab:D3424
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Changes (by goldfire):

 * differential:   => Phab:D3424


Comment:

 I now think I know what's going on here, but unsure the best way to fix
 it. Interestingly, the problem has nothing to do with `Typeable` or
 `TypeInType`. Indeed it's amazing we've never hit this problem before.

 We have

 {{{
   [G] c1 :: k1[tau] ~ j1[tau]
 }}}

 in an implication. Both `k1` and `j1` are filled in at this point: `k1 :=
 Type` and `j1 := k2[sk]`. This constraint is then passed through
 `solveSimpleGivens`, where it is canonicalized. `can_eq_nc'` flattens both
 sides, following both `k1` and `j1` to find `Type`. `can_eq_nc'` then
 calls `rewriteEqEvidence` which creates a new

 {{{
   [G] c2 :: Type ~ k2[sk]
 }}}

 Of course, GHC produces evidence for `c2`: `c2 = g1 ; c1 ; g2`, where `g1`
 and `g2` are the coercions that come from flattening `k1` and `j1`.

 The problem is that these coercions, `g1` and `g2` are both reflexive, as
 they arise simply from zonking. See the line of code
 [https://github.com/ghc/ghc/blob/master/compiler/typecheck/TcFlatten.hs#L1288
 here]. When `c2` is stitched together from `g1`, `c1`, and `g2`, the calls
 to `mkTcTransCo` notice that some of the arguments are `Refl`, and so
 ignores the reflexive arguments. The end result is that `c2 = c1`. And
 then, when `c2` gets put in the inert set, its kind still mentions
 unzonked variables. (Even though the associated `ctPred` is just fine.)

 What to do? Here are some ideas:

 1. Stop `mkTcTransCo` (but not `mkTransCo`) from optimizing this case.

 2. Add a zonk somewhere (`addInertEq`? seems better than
 `rewriteEqEvidence`) to fix this problem.

 3. Add a new coercion form `ZonkCo` that relates an unzonked tyvar to its
 contents. This way, we can have the invariant that, whenever `(ty', co) <-
 flatten ty`, we have `co :: ty' ~ ty`. (Right now, that final equality is
 true only modulo zonking. But the new `ZonkCo` would allow it to be true
 without needing to zonk.) In fully-typechecked Core, `ZonkCo` would zonk
 to become reflexive, and so Core would have no `ZonkCo`s.

 4. Add a new `castTcCoercion` function that stitches three coercions
 together using transitivity; this `castTcCoercion` would cleverly not
 optimize the `Refl` away.

 I favor (1) but am worried about performance implications. (3) is probably
 the most principled, but it seems like a sledgehammer to tap in a nail.
 (4) is a middle ground, but I'm worried that what's happening here (a
 coercion returned from the flattener having an unzonked kind) happens
 elsewhere where we wouldn't use `castTcCoercion`.

 What are your thoughts?

 (NB: The patch linked to here does not have any of these fixes. I posted
 that patch some time ago but never added the link from this ticket.)

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