Opened 5 months ago

Closed 5 months ago

#15419 closed bug (fixed)

GHC 8.6.1 regression (buildKindCoercion)

Reported by: RyanGlScott Owned by: goldfire
Priority: highest Milestone: 8.6.1
Component: Compiler (Type checker) Version: 8.5
Keywords: TypeInType Cc: goldfire
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Compile-time crash or panic Test Case: dependent/should_compile/T15419
Blocked By: Blocking:
Related Tickets: #15346 Differential Rev(s):
Wiki Page:

Description

The following program typechecks on GHC 8.4.1, but panics on GHC 8.6.1 and HEAD:

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE UndecidableInstances #-}
module Bug where

import Data.Kind

data family Sing :: forall k. k -> Type
data TyFun :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>
type family Apply (f :: k1 ~> k2) (x :: k1) :: k2

data instance Sing :: forall a b. (a, b) -> Type where
  STuple2 :: Sing x -> Sing y -> Sing '(x, y)
newtype instance Sing (f :: k1 ~> k2) =
  SLambda { applySing :: forall t. Sing t -> Sing (f `Apply` t) }

-----

newtype Par1 p = Par1 p
newtype K1 c p = K1 c
data (f :*: g) p = f p :*: g p

data instance Sing :: forall p. Par1 p -> Type where
  SPar1 :: Sing x -> Sing ('Par1 x)
data instance Sing :: forall k c (p :: k). K1 c p -> Type where
  SK1 :: Sing x -> Sing ('K1 x)
data instance Sing :: forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
                      (f :*: g) p -> Type where
  (:%*:) :: Sing x -> Sing y -> Sing (x ':*: y)

class Generic1 (f :: k -> Type) where
  type Rep1 f :: k -> Type
  from1 :: f a -> Rep1 f a
  to1 :: Rep1 f a -> f a

class PGeneric1 (f :: k -> Type) where
  type From1 (z :: f a)      :: Rep1 f a
  type To1   (z :: Rep1 f a) :: f a

class SGeneric1 (f :: k -> Type) where
  sFrom1 :: forall (a :: k) (z :: f a).      Sing z -> Sing (From1 z)
  sTo1   :: forall (a :: k) (r :: Rep1 f a). Sing r -> Sing (To1 r :: f a)

instance Generic1 ((,) a) where
  type Rep1 ((,) a) = K1 a :*: Par1
  from1 (x, y)          = K1 x :*: Par1 y
  to1 (K1 x :*: Par1 y) = (x, y)

instance PGeneric1 ((,) a) where
  type From1 '(x, y)              = 'K1 x ':*: 'Par1 y
  type To1   ('K1 x ':*: 'Par1 y) = '(x, y)

instance SGeneric1 ((,) a) where
  sFrom1 (STuple2 x y)        = SK1 x :%*: SPar1 y
  sTo1   (SK1 x :%*: SPar1 y) = STuple2 x y

-----

type family GenericFmap (g :: a ~> b) (x :: f a) :: f b where
  GenericFmap g x = To1 (Fmap g (From1 x))

class PFunctor (f :: Type -> Type) where
  type Fmap (g :: a ~> b) (x :: f a) :: f b
  type Fmap g x = GenericFmap g x

class SFunctor (f :: Type -> Type) where
  sFmap         :: forall a b (g :: a ~> b) (x :: f a).
                   Sing g -> Sing x -> Sing (Fmap g x)
  default sFmap :: forall a b (g :: a ~> b) (x :: f a).
                   ( SGeneric1 f, SFunctor (Rep1 f)
                   , Fmap g x ~ GenericFmap g x )
                => Sing g -> Sing x -> Sing (Fmap g x)
  sFmap sg sx = sTo1 (sFmap sg (sFrom1 sx))

-----

instance PFunctor Par1 where
  type Fmap f ('Par1 x) = 'Par1 (f `Apply` x)
instance PFunctor (K1 c) where
  type Fmap _ ('K1 x) = 'K1 x
instance PFunctor (f :*: g) where
  type Fmap h (x ':*: y) = Fmap h x ':*: Fmap h y

instance SFunctor Par1 where
  sFmap sf (SPar1 sx) = SPar1 (sf `applySing` sx)
instance SFunctor (K1 c) where
  sFmap _ (SK1 sx) = SK1 sx
instance (SFunctor f, SFunctor g) => SFunctor (f :*: g) where
  sFmap sh (sx :%*: sy) = sFmap sh sx :%*: sFmap sh sy

-----

instance PFunctor ((,) a)
-- The line below causes the panic
instance SFunctor ((,) a)
$ /opt/ghc/8.6.1/bin/ghc Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )
ghc: panic! (the 'impossible' happened)
  (GHC version 8.6.0.20180714 for x86_64-unknown-linux):
        buildKindCoercion
  K1 a_a1Nj :*: Par1
  Rep1 ((,) a_a1Nj)
  *
  a_a1Nj
  Call stack:
      CallStack (from HasCallStack):
        callStackDoc, called at compiler/utils/Outputable.hs:1164:37 in ghc:Outputable
        pprPanic, called at compiler/types/Coercion.hs:2069:9 in ghc:Coercion

Change History (6)

comment:1 Changed 5 months ago by RyanGlScott

Cc: goldfire added

Commit 3eaa55dcbcd860a035dfe2cae96866e96b008f67 (Apply Note [EtaAppCo] in OptCoercion to another case) is responsible for this regression.

comment:2 Changed 5 months ago by simonpj

Owner: set to goldfire

OK, Richard, that's your patch... you're up :-).

comment:3 Changed 5 months ago by RyanGlScott

Amusingly enough, I think this is just a symptom of #15346. I tried applying this patch:

  • compiler/coreSyn/CoreOpt.hs

    diff --git a/compiler/coreSyn/CoreOpt.hs b/compiler/coreSyn/CoreOpt.hs
    index 8684c84..11cbd1e 100644
    a b pushCoTyArg co ty 
    979979
    980980  | isForAllTy tyL
    981981  = ASSERT2( isForAllTy tyR, ppr co $$ ppr ty )
    982     Just (ty `mkCastTy` mkSymCo co1, MCo co2)
     982    Just (ty `mkCastTy` co1, MCo co2)
    983983
    984984  | otherwise
    985985  = Nothing
    pushCoTyArg co ty 
    989989       -- tyL = forall (a1 :: k1). ty1
    990990       -- tyR = forall (a2 :: k2). ty2
    991991
    992     co1 = mkNthCo Nominal 0 co
    993        -- co1 :: k1 ~N k2
     992    co1 = mkSymCo (mkNthCo Nominal 0 co)
     993       -- co1 :: k2 ~N k1
    994994       -- Note that NthCo can extract a Nominal equality between the
    995995       -- kinds of the types related by a coercion between forall-types.
    996996       -- See the NthCo case in CoreLint.
  • compiler/types/Coercion.hs

    diff --git a/compiler/types/Coercion.hs b/compiler/types/Coercion.hs
    index 2ca5151..1557ce0 100644
    a b liftCoSubstVarBndrUsing fun lc@(LC subst cenv) old_var 
    18121812    Pair k1 _    = coercionKind eta
    18131813    new_var      = uniqAway (getTCvInScope subst) (setVarType old_var k1)
    18141814
    1815     lifted   = Refl (TyVarTy new_var)
     1815    lifted   = GRefl Nominal (TyVarTy new_var) (MCo eta)
    18161816    new_cenv = extendVarEnv cenv old_var lifted
    18171817
    18181818-- | Is a var in the domain of a lifting context?

And with that, the program in this ticket no longer panics.

Richard, you're currently validating this patch, yes? Would you mind adding this as a regression test?

Last edited 5 months ago by RyanGlScott (previous) (diff)

comment:4 Changed 5 months ago by monoidal

I've tried to simplify the original bug report, but it's still long:

{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE UndecidableInstances #-}
module Bug where

import Data.Kind

data Prod a b
data Proxy p = Proxy

-----

data family Sing :: forall k. k -> Type
data instance Sing x = STuple

-----

type family Rep1 (f :: k -> Type) :: k -> Type
type instance Rep1 ((,) a) = Prod a

type family From1 (f :: Type -> Type) a (z :: f a) :: Rep1 f a
type family To1 (f :: Type -> Type) a (z :: Rep1 f a) :: f a

class Generic1 (f :: Type -> Type) where
  sFrom1 :: forall (a :: Type) (z :: f a).      Proxy z -> Sing (From1 f a z)
  sTo1   :: forall (a :: Type) (r :: Rep1 f a). Proxy r -> Proxy (To1 f a r :: f a)

instance Generic1 ((,) a) where
  sFrom1 Proxy = undefined
  sTo1   Proxy = undefined

-----

type family Fmap (g :: b) (x :: f a) :: f b
type instance Fmap (g :: b) (x :: (u, a)) = To1 ((,) u) b (Fmap g (From1 ((,) u) a x))

class PFunctor (f :: Type -> Type) where
  sFmap         :: forall a b (g :: b) (x :: f a).
                   Proxy g -> Sing x -> Proxy (Fmap g x)

instance PFunctor (Prod a) where
  sFmap _ STuple = undefined

sFmap1 :: forall (f :: Type -> Type) (u :: Type) (b :: Type) (g :: b) (x :: f u).
                 (Generic1 f,
                  PFunctor (Rep1 f),
                  Fmap g x ~ To1 f b (Fmap g (From1 f u x)) )
              => Proxy g -> Proxy x -> Proxy (Fmap g x)
sFmap1 sg sx = sTo1 (sFmap sg (sFrom1 sx))

sFmap2  :: forall (p :: Type) (a :: Type) (b :: Type) (g :: b) (x :: (p, a)).
          Proxy g -> Proxy x -> Proxy (Fmap g x)
sFmap2 = sFmap1

comment:5 Changed 5 months ago by Richard Eisenberg <rae@…>

In af624071/ghc:

Fix some casts.

This fixes #15346, and is a team effort between Ryan Scott and
myself (mostly Ryan). We discovered two errors related to FC's
"push" rules, one in the TPush rule (as implemented in pushCoTyArg)
and one in KPush rule (it shows up in liftCoSubstVarBndr).

The solution: do what the paper says, instead of whatever random
thoughts popped into my head as I was actually implementing.

Also fixes #15419, which is actually the same underlying problem.

Test case: dependent/should_compile/T{15346,15419}.

comment:6 Changed 5 months ago by goldfire

Resolution: fixed
Status: newclosed
Test Case: dependent/should_compile/T15419

Labeling this as "fixed", because I set #15346 as "merge"

Note: See TracTickets for help on using tickets.