Opened 15 months ago

Closed 11 months ago

Last modified 4 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 (11)

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

Cc: Iceland_jack added

comment:3 Changed 15 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 13 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 13 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 11 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 11 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 11 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 11 months ago by simonpj

Resolution: fixed
Status: newclosed

OK, finally fixed I believe. Hurrah.

comment:10 Changed 9 months ago by Simon Peyton Jones <simonpj@…>

In 3d252037/ghc:

Respect Note [The tcType invariant]

I tried to do this with

    commit 0a12d92a8f65d374f9317af2759af2b46267ad5c
    Author: Simon Peyton Jones <simonpj@microsoft.com>
    Date:   Wed Dec 13 12:53:26 2017 +0000

    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.

But I didn't get it quite right as Trac #14873 showed.

This patch fixes the problem; although I am still a bit unhappy.
(See "A worry" in the HsApp case of tc_infer_hs_type.)

comment:11 Changed 4 months ago by Simon Peyton Jones <simonpj@…>

In 5067b20/ghc:

Add nakedSubstTy and use it in TcHsType.tcInferApps

This was a tricky one.

During type checking we maintain TcType:
   Note [The well-kinded type invariant]
That is, types are well-kinded /without/ zonking.

But in tcInferApps we were destroying that invariant by calling
substTy, which in turn uses smart constructors, which eliminate
apparently-redundant Refl casts.

This is horribly hard to debug beause they really are Refls and
so it "ought" to be OK to discard them. But it isn't, as the
above Note describes in some detail.

Maybe we should review the invariant?  But for now I just followed
it, tricky thought it is.

This popped up because (for some reason) when I fixed Trac #15343,
that exposed this bug by making test polykinds/T14174a fail (in
Trac #14174 which indeed has the same origin).

So this patch fixes a long standing and very subtle bug.

One interesting point: I defined nakedSubstTy in a few lines by
using the generic mapType stuff.  I note that the "normal"
TyCoRep.substTy does /not/ use mapType.  But perhaps it should:
substTy has lots of $! strict applications in it, and they could
all be eliminated just by useing the StrictIdentity monad.  And
that'd make it much easier to experiment with switching between
strict and lazy versions.
Note: See TracTickets for help on using tickets.