GHC panic with a code with type equality constraints with doubly applied type family
Summary
With the following code which should not pass type checking, GHC panic at PostTc phase when doing lookupIdSubst
.
The code has type equality of form F1 (F2 x) ~ F3 y, and I think that's where the bug is triggered, but the panic happens only when combined with other statements in do-notation. (otherwise, usual type error happened, so this is my best minimization up to now).
Steps to reproduce
{-# LANGUAGE Haskell2010 #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
module Main where
class C1 b where
type F1 b
class C2 (m :: * -> *) where
type F2 m
class C3 r where
type F3 r
class G t m where
g :: m a -> t m a
data Y
data X e a
data H a
data S a
fun1 :: X e ()
fun1 = undefined
fun2 :: S ()
fun2 = undefined
fun3 :: H ()
fun3 = undefined
fun4 :: (F3 r ~ F1 (F2 m)) => r -> m ()
fun4 = undefined
test :: (C2 m, F2 m ~ Y) => m ()
test = do
fun1
fun2
g fun3
fun4 undefined
main :: IO ()
main = pure ()
when running GHC, one will see the following panic error.
$ ghc Panic.hs
[1 of 2] Compiling Main ( Panic.hs, Panic.o )
Panic.hs:11:16: warning: [GHC-39567] [-Wstar-is-type]
Using ‘*’ (or its Unicode variant) to mean ‘Data.Kind.Type’
relies on the StarIsType extension, which will become
deprecated in the future.
Suggested fix: Use ‘Type’ from ‘Data.Kind’ instead.
|
11 | class C2 (m :: * -> *) where
| ^
Panic.hs:11:21: warning: [GHC-39567] [-Wstar-is-type]
Using ‘*’ (or its Unicode variant) to mean ‘Data.Kind.Type’
relies on the StarIsType extension, which will become
deprecated in the future.
Suggested fix: Use ‘Type’ from ‘Data.Kind’ instead.
|
11 | class C2 (m :: * -> *) where
| ^
Panic.hs:37:15: warning: [GHC-58520] [-Wtype-equality-requires-operators]
The use of ‘~’ without TypeOperators
will become an error in a future GHC release.
Suggested fix: Perhaps you intended to use TypeOperators
|
37 | fun4 :: (F3 r ~ F1 (F2 m)) => r -> m ()
| ^
Panic.hs:40:21: warning: [GHC-58520] [-Wtype-equality-requires-operators]
The use of ‘~’ without TypeOperators
will become an error in a future GHC release.
Suggested fix: Perhaps you intended to use TypeOperators
|
40 | test :: (C2 m, F2 m ~ Y) => m ()
| ^
<no location info>: error:
panic! (the 'impossible' happened)
GHC version 9.6.2:
lookupIdSubst
$dMonad_aWA
InScope {$dIP_aUI $dIP_aUN m_aUW $dC2_aUX $d~_aUY $krep_aWW
$krep_aWX $krep_aWY $krep_aWZ $krep_aX0 $krep_aX1 $krep_aX2
$krep_aX3 $krep_aX4 fun1 fun2 fun3 fun4 $tcC1 $tc'C:C1 $tcC2
$tc'C:C2 $tcC3 $tc'C:C3 $tcG $tcY $tcX $tcH $tcS $trModule}
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/GHC/Utils/Panic.hs:189:37 in ghc:GHC.Utils.Panic
pprPanic, called at compiler/GHC/Core/Subst.hs:197:17 in ghc:GHC.Core.Subst
CallStack (from HasCallStack):
panic, called at compiler/GHC/Utils/Error.hs:454:29 in ghc:GHC.Utils.Error
Expected behavior
This should give a type error and stop there, not proceeding to PostTc phase.
Environment
-
GHC version used: ghc 9.6.2
-
Operating System: macOS Ventura 13.5.2