Opened 6 months ago

Closed 2 months ago

#14174 closed bug (fixed)

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: polykinds/T14174.hs, T14174a
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 (9)

comment:1 Changed 6 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 6 months ago by Iceland_jack

Cc: Iceland_jack added

comment:3 Changed 6 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 months ago by bgamari

Milestone: 8.2.28.2.3

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

comment:5 Changed 4 months 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

comment:6 Changed 2 months ago by Simon Peyton Jones <simonpj@…>

In 8b36ed1/ghc:

Build only well-kinded types in type checker

During type inference, we maintain the invariant that every type is
well-kinded /without/ zonking; and in particular that typeKind does
not fail (as it can for ill-kinded types).

But TcHsType.tcInferApps was not guaranteeing this invariant,
resulting in Trac #14174 and #14520.

This patch fixes it, making things better -- but it does /not/
fix the program in Trac #14174 comment:5, which still crashes.
So more work to be done.

See Note [Ensure well-kinded types] in TcHsType

comment:7 Changed 2 months ago by simonpj

Test Case: polykinds/T14174.hs, T14174a

Still open because I need to fix the example in comment:5 (which is T14174a).

comment:8 Changed 2 months ago by Simon Peyton Jones <simonpj@…>

In 0a12d92a/ghc:

Further improvements to well-kinded types

The typechecker has the invariant that every type should be well-kinded
as it stands, without zonking.  See Note [The well-kinded type invariant]
in TcType.

That invariant was not being upheld, which led to Trac #14174.  I fixed
part of it, but T14174a showed that there was more.  This patch finishes
the job.

* See Note [The tcType invariant] in TcHsType, which articulates an
  invariant that was very nearly, but not quite, true.  One place that
  falisified it was the HsWildCardTy case of tc_hs_type, so I fixed that.

* mkNakedCastTy now makes no attempt to eliminate casts; indeed it cannot
  lest it break Note [The well-kinded type invariant].  The prior comment
  suggested that it was crucial for performance but happily it seems not
  to be. The extra Refls are eliminated by the zonker.

* I found I could tidy up TcHsType.instantiateTyN and instantiateTyUntilN
  by eliminating one of its parameters.  That led to a cascade of minor
  improvements in TcTyClsDecls. Hooray.

comment:9 Changed 2 months ago by simonpj

Resolution: fixed
Status: newclosed

OK, finally fixed I believe. Hurrah.

Note: See TracTickets for help on using tickets.