Typed holes panic: simplifyArgsWorker wandered into deeper water than usual
The following code should not be expected to typecheck. But GHC does a fair bit worse and panics when it tries to typecheck it:
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Bug where
import Data.Kind (Type)
import Data.Type.Equality ((:~:)(..))
import GHC.Generics (U1(..))
type family Sing :: k -> Type
data SU1 :: forall k (p :: k). U1 p -> Type where
SU1 :: SU1 'U1
type instance Sing = SU1
class PSAlternative (f :: Type -> Type) where
type (x :: f a) <|> (y :: f a) :: f a
type Empty :: f a
(%<|>) :: forall a (x :: f a) (y :: f a).
Sing x -> Sing y -> Sing (x <|> y)
sEmpty :: forall a. Sing (Empty :: f a)
class PSAlternative f => PSMonadPlus (f :: Type -> Type) where
type Mplus (x :: f a) (y :: f a) :: f a
type Mzero :: f a
sMplus :: forall a (x :: f a) (y :: f a).
Sing x -> Sing y -> Sing (Mplus x y)
sMzero :: forall a. Sing (Mzero :: f a)
instance PSAlternative U1 where
type x <|> y = 'U1
type Empty = 'U1
_ %<|> _ = SU1
sEmpty = SU1
instance PSMonadPlus U1 where
type Mplus x y = x <|> y
type Mzero = Empty
sMplus = (%<|>)
sMzero = sEmpty
class PSMonadPlus f => VMonadPlus f where
monadPlusMplus :: forall a (x :: f a) (y :: f a).
Sing x -> Sing y
-> Mzero x y :~: (x <|> y)
-- The mistake is above: it should actually be
-- -> Mplus x y :~: (x <|> y)
instance VMonadPlus U1 where
monadPlusMplus _ _ = _Refl
On GHC 8.8.2, the panic is:
$ /opt/ghc/8.8.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
ghc: panic! (the 'impossible' happened)
(GHC version 8.8.2 for x86_64-unknown-linux):
simplifyArgsWorker wandered into deeper water than usual
Please report this as a GHC bug: https://www.haskell.org/ghc/reportabug
Older versions of GHC (dating back to 8.2.2) also panic on this program, although the exact message the panic prints out differs slightly between versions.