Opened 3 months ago

Last modified 3 weeks ago

#14174 new bug

GHC panic with TypeInType and type family

Reported by: dfeuer Owned by:
Priority: normal Milestone: 8.2.3
Component: Compiler (Type checker) Version: 8.2.1
Keywords: TypeInType Cc: goldfire, Iceland_jack
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Compile-time crash or panic Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

This rather simple type family,

{-# LANGUAGE TypeFamilies, TypeOperators, TypeInType #-}

module GenWhoops where
import GHC.Generics

type family GenComp k (x :: k) (y :: k) :: Ordering where
  GenComp ((x :+: y) p) ('L1 x) ('L1 y) = GenComp (x p) x y

produces the following panic:

ghc-stage2: panic! (the 'impossible' happened)
  (GHC version 8.3.20170828 for x86_64-unknown-linux):
        piResultTy
  k_a1LK[tau:1]
  p_a1Lz[sk:1]
  Call stack:
      CallStack (from HasCallStack):
        callStackDoc, called at compiler/utils/Outputable.hs:1138:37 in ghc:Outputable
        pprPanic, called at compiler/types/Type.hs:949:35 in ghc:Type

This happens with both GHC 8.2.1 and something very close to HEAD.

Change History (5)

comment:1 Changed 3 months ago by dfeuer

This really should just be an error, I imagine. It's an (accidental) non-linear pattern where the two types have different kinds.

comment:2 Changed 3 months ago by Iceland_jack

Cc: Iceland_jack added

comment:3 Changed 3 months ago by simonpj

Here is a simpler way to trigger the same panic

{-# LANGUAGE  TypeInType, RankNTypes, KindSignatures, PolyKinds #-}
module Foo where

data T k (x :: k) = MkT

data S x = MkS (T (x Int) x)

comment:4 Changed 4 weeks ago by bgamari

Milestone: 8.2.28.2.3

It looks like this won't be fixed in 8.2.2.

comment:5 Changed 3 weeks ago by RyanGlScott

This might be another occurrence of this bug:

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Bug where

import Data.Kind

data TyFun :: * -> * -> *
type a ~> b = TyFun a b -> *
infixr 0 ~>

type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
type a @@ b = Apply a b
infixl 9 @@

data FunArrow = (:->) | (:~>)

class FunType (arr :: FunArrow) where
  type Fun (k1 :: Type) arr (k2 :: Type) :: Type

class FunType arr => AppType (arr :: FunArrow) where
  type App k1 arr k2 (f :: Fun k1 arr k2) (x :: k1) :: k2

type FunApp arr = (FunType arr, AppType arr)

instance FunType (:->) where
  type Fun k1 (:->) k2 = k1 -> k2

instance AppType (:->) where
  type App k1 (:->) k2 (f :: k1 -> k2) x = f x

instance FunType (:~>) where
  type Fun k1 (:~>) k2 = k1 ~> k2

instance AppType (:~>) where
  type App k1 (:~>) k2 (f :: k1 ~> k2) x = f @@ x

infixr 0 -?>
type (-?>) (k1 :: Type) (k2 :: Type) (arr :: FunArrow) = Fun k1 arr k2

type family ElimBool (p :: Bool -> Type)
                     (z :: Bool)
                     (pFalse :: p False)
                     (pTrue  :: p True)
                     :: p z where
  -- Commenting out the line below makes the panic go away
  ElimBool p z pFalse pTrue = ElimBoolPoly (:->) p z pFalse pTrue

type family ElimBoolTyFun (p :: Bool ~> Type)
                          (z :: Bool)
                          (pFalse :: p @@ False)
                          (pTrue  :: p @@ True)
                          :: p @@ z where
  ElimBoolTyFun p z pFalse pTrue = ElimBoolPoly (:~>) p z pFalse pTrue

type family ElimBoolPoly (arr :: FunArrow)
                         (p :: (Bool -?> Type) arr)
                         (z :: Bool)
                         (pFalse :: App Bool arr Type p False)
                         (pTrue  :: App Bool arr Type p True)
                         :: App Bool arr Type p z where
  ElimBoolPoly _ _ False pFalse _     = pFalse
  ElimBoolPoly _ _ True  _      pTrue = pTrue
$ /opt/ghc/8.2.1/bin/ghc Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )
ghc: panic! (the 'impossible' happened)
  (GHC version 8.2.1 for x86_64-unknown-linux):
        piResultTy
  k0_a1Zd[tau:1]
  z_aS3[sk:1]
  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:948:35 in ghc:Type
Note: See TracTickets for help on using tickets.