GitLab

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.