#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