#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