[GHC] #13910: Inlining a definition causes GHC to panic (repSplitTyConApp_maybe)

[GHC]

#13910: Inlining a definition causes GHC to panic (repSplitTyConApp_maybe)
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.2.1-rc2
  checker)                           |
      Resolution:                    |             Keywords:  TypeInType
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Compile-time      |  Unknown/Multiple
  crash or panic                     |            Test Case:
      Blocked By:  14119             |             Blocking:
 Related Tickets:  #13877, #14038,   |  Differential Rev(s):
  #14175                             |
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 Richard, I need your help on this.

 I don't know whtether this problem is ultimately the source of the crash,
 but with my stage-1 compiler I get a earlier ASSERT failure, and some
 investigation shows that a type-family reduction is leading to an entirely
 bogus result. It's like this.  We have an axiom
 {{{
 forall (k1 :: Type)
        (k2 :: Type)
        (f :: k1 ~> k2)
        (x :: k1).
     App k1 (':~>) k2 (f |> Sym (D:R:Funk1:~>k2{tc r14K}[0] <k1>_N <k2>_N))
 x
       = @@ k1 k2 f x
 }}}
 But then we come across a call which we give to `reduceTyFamApp_maybe`:
 {{{
   App w_a2c6 (':~>) Type ((p :: t ~> Type) |> HoleCo {a2cb}) w_a2c6
 }}}
 This is alraedy odd.  I expected the arguments to be zonked before this
 attempt to do type-family reduction, but they aren't.  In this case
 `w_a2c6` is already unified with `p`.

 But it gets worse.  When we reduce the application, we get a result
 looking like
 {{{
 @@ w_a2c6 Type
    (p |> Sym (Sym (D:R:Funk1:~>k2
                       <k1>_N
                       <k2>_N) ; Sym (HoleCo {a2cb})))
    w_a2ca
 }}}
 Yes, you saw it right.  The `k1` and `k2` from the LHS of the axiom have
 shown up in the result!!!

 Turns out that this is because of the treatment of cases in matching.  In
 `Unify.hs` we see
 {{{
 unify_ty env ty1 ty2 kco
     -- TODO: More commentary needed here
   | CastTy ty1' co <- ty1     = unify_ty env ty1' ty2 (co `mkTransCo` kco)
   | CastTy ty2' co <- ty2     = unify_ty env ty1 ty2' (kco `mkTransCo`
 mkSymCo co)
 }}}
 So coercions from the LHS and RHS both end up mixed together in that
 `kco`; and it ultimately shows up in the result subsitution.

 I'm not sure what the fix is.  Maybe we can just apply the ambient
 substition to the `co`; but what if template variables it mentions have
 not yet been bound yet?  Or maybe we need to take the fixpoint of the
 returned substitution; we do this for unification, maybe we need it for
 matching too?

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