#14154: Some cocktail of features causes GHC panic -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * cc: RyanGlScott (removed) * version: 8.0.1 => 8.3 Old description:
{{{#!hs {-# Language RankNTypes, TypeApplications, ScopedTypeVariables, GADTs, PolyKinds #-}
module T14154 where
newtype Ran g h a = MkRan (forall b. (a -> g b) -> h b)
newtype Swap p f g a where MkSwap :: p g f a -> Swap p f g a
ireturn :: forall m i a. a -> m i i a ireturn = undefined
xs = case ireturn @(Swap Ran) 'a' of MkSwap (MkRan f) -> f print }}}
{{{ $ ghci -ignore-dot-ghci /tmp/bug.hs GHCi, version 8.3.20170605: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( /tmp/bug.hs, interpreted ) ghc: panic! (the 'impossible' happened) (GHC version 8.3.20170605 for x86_64-unknown-linux): piResultTy k0_a1Ki[tau:2] b0_a1Kt[tau:2] Call stack: CallStack (from HasCallStack): prettyCurrentCallStack, called at compiler/utils/Outputable.hs:1133:58 in ghc:Outputable callStackDoc, called at compiler/utils/Outputable.hs:1137:37 in ghc:Outputable pprPanic, called at compiler/types/Type.hs:949:35 in ghc:Type
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
}}}
New description: {{{#!hs {-# Language RankNTypes, DerivingStrategies, TypeApplications, ScopedTypeVariables, GADTs, PolyKinds #-} module T14154 where newtype Ran g h a = MkRan (forall b. (a -> g b) -> h b) newtype Swap p f g a where MkSwap :: p g f a -> Swap p f g a ireturn :: forall m i a. a -> m i i a ireturn = undefined xs = case ireturn @(Swap Ran) 'a' of MkSwap (MkRan f) -> f print }}} {{{ $ ghci -ignore-dot-ghci /tmp/bug.hs GHCi, version 8.3.20170605: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( /tmp/bug.hs, interpreted ) ghc: panic! (the 'impossible' happened) (GHC version 8.3.20170605 for x86_64-unknown-linux): piResultTy k0_a1Ki[tau:2] b0_a1Kt[tau:2] Call stack: CallStack (from HasCallStack): prettyCurrentCallStack, called at compiler/utils/Outputable.hs:1133:58 in ghc:Outputable callStackDoc, called at compiler/utils/Outputable.hs:1137:37 in ghc:Outputable pprPanic, called at compiler/types/Type.hs:949:35 in ghc:Type Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
}}} -- Comment: I have worked out what is happening here. * We have {{{ ireturn :: forall k (m :: k -> k -> * -> *) a (i :: k). a -> m i i a }}} * At the call of `ireturn` in `xs` we instantiate `k`,`m`,`a`,`i` with unification variables `k0`, `m0 :: k0 -> k0 -> k* -> *`, `a0`, `i0 :: k0`. * The visible type application ends up forcing `k0 := k1 -> *` * In the pattern `MkRan f` we end up with expected type `Ran k0 i0 i0 a0` * The definition of `Ran` is {{{ newtype Ran k (g :: k -> *) (h :: k -> *) a where MkRan :: forall k (g :: k -> *) (h :: k -> *) a. (forall (b :: k). (a -> g b) -> h b) -> Ran k g h a }}} * So, in `TcPat.tcDataConPat` we instantiate `k :-> k0, g :-> i0, h :-> i0, a :-> a0`. * But now, in the instantiated version of `MkRan`'s type we have `i0 b`, ''which is ill-kinded''. At least, it's ill-kinded until we zonk everything. But the type constraint solver calls `typeKind` on un-zonked types quite a bit. * `typeKind` is non-monadic and crashes on ill-kinded types, via the call to `piResultTy` {{{ typeKind (AppTy fun arg) = piResultTy (typeKind fun) arg }}} * FWIW the crashing call to `typeKind` is in `TcUnify.promoteTcType`. Now, I believe our invariant is that ''we never form an ill-kinded type'', zonked or unzonked. In this example we don't obey the invariant. What could we do? * In the offending `tcDataConPat` we could instantiate the data contructor's type with fresh unification variables, and emit equalities to link it up with the "expected" type `ctxt_res_tys`. * We could do that in the general case, but have a short-cut for the common case where the kinds do actually match up. * We could give up on the invariant; where we need `typeKind` and it fails, we could generate a unification variable, and emit a new kind of delayed constraint that means `kappa ~ kindof( ty )`. Yuk. Richard, any other ideas? What is unsettling is that I can't see how to be sure there are no other lurking cases of this same problem, elsewhere in the typechecker. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14154#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler