Opened 3 months ago

Closed 3 months ago

#15343 closed bug (fixed)

Implicitly quantifying a kind variable causes GHC 8.6 to panic (coercionKind)

Reported by: RyanGlScott Owned by:
Priority: high 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_fail/T15343
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

The following program panics on GHC 8.6 and later:

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Bug where

import Data.Kind
import Data.Type.Equality

data family Sing :: forall k. k -> Type
data SomeSing :: Type -> Type where
  SomeSing :: Sing (a :: k) -> SomeSing k

class SingKind k where
  type Demote k :: Type
  fromSing :: Sing (a :: k) -> Demote k
  toSing   :: Demote k -> SomeSing k

data instance Sing (z :: a :~~: b) where
  SHRefl :: Sing HRefl

instance SingKind (a :~~: b) where
  type Demote (a :~~: b) = a :~~: b
  fromSing SHRefl = HRefl
  toSing HRefl    = SomeSing SHRefl

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

(~>:~~:) :: forall (j :: Type) (k :: Type) (a :: j) (b :: k)
                   (p :: forall (z :: Type) (y :: z). (a :~~: y) ~> Type)
                   (r :: a :~~: b).
            Sing r
         -> Apply p HRefl
         -> Apply p r
(~>:~~:) SHRefl pHRefl = pHRefl

type family Why (a :: j) (e :: a :~~: (y :: z)) :: Type where
  Why a (_ :: a :~~: y)  = y :~~: a

data    WhySym (a :: j) :: forall   (y :: z). (a :~~: y) ~> Type
-- data WhySym (a :: j) :: forall z (y :: z). (a :~~: y) ~> Type
-- The version above does NOT panic
type instance Apply (WhySym a) e = Why a e

hsym :: forall (j :: Type) (k :: Type) (a :: j) (b :: k).
        a :~~: b -> b :~~: a
hsym eq = case toSing eq of
            SomeSing (singEq :: Sing r) ->
              (~>:~~:) @j @k @a @b @(WhySym a) @r singEq HRefl
$ /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.20180627 for x86_64-unknown-linux):
        coercionKind
  Nth:3
      (Inst {co_a1jI} (Coh <k_a1js[sk:1]>_N (Nth:0 (Sym {co_a1jI}))))
  Call stack:
      CallStack (from HasCallStack):
        callStackDoc, called at compiler/utils/Outputable.hs:1164:37 in ghc:Outputable
        pprPanic, called at compiler/types/Coercion.hs:1887:9 in ghc:Coercion

As noted in the comments, replacing WhySym with a version that explicitly quantifies z avoids the panic.

This is a regression from GHC 8.4.3, in which the program simply errored:

$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:56:38: error:
    • Expected kind ‘forall z (y :: z). (a1 :~~: y) ~> *’,
        but ‘WhySym a’ has kind ‘forall (y :: z0).
                                 TyFun (a1 :~~: y) * -> *’
    • In the type ‘(WhySym a)’
      In the expression: (~>:~~:) @j @k @a @b @(WhySym a) @r singEq HRefl
      In a case alternative:
          SomeSing (singEq :: Sing r)
            -> (~>:~~:) @j @k @a @b @(WhySym a) @r singEq HRefl
    • Relevant bindings include
        singEq :: Sing a2 (bound at Bug.hs:55:23)
        eq :: a1 :~~: b (bound at Bug.hs:54:6)
        hsym :: (a1 :~~: b) -> b :~~: a1 (bound at Bug.hs:54:1)
   |
56 |               (~>:~~:) @j @k @a @b @(WhySym a) @r singEq HRefl
   |                                      ^^^^^^^^

Change History (8)

comment:1 Changed 3 months ago by RyanGlScott

Here's a smaller example:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeInType #-}
module Bug where

import Data.Kind

data HEq :: forall j k. j -> k -> Type where
  HRefl :: HEq a a

data Sing :: forall j k (a :: j) (b :: k).
             HEq a b -> Type where
  SHRefl :: Sing HRefl

elimSing :: forall (j :: Type) (k :: Type) (a :: j) (b :: k)
                   (p :: forall (z :: Type) (y :: z). HEq a y -> Type)
                   (r :: HEq a b).
            Sing r
         -> p HRefl
         -> p r
elimSing SHRefl pHRefl = pHRefl

data    WhySym (a :: j) :: forall   (y :: z). HEq a y -> Type
-- data WhySym (a :: j) :: forall z (y :: z). (a :~~: y) ~> Type
-- The version above does NOT panic

hsym :: forall (j :: Type) (k :: Type) (a :: j) (b :: k) (r :: HEq a b).
        Sing r -> WhySym a r
hsym singEq = elimSing @j @k @a @b @(WhySym a) @r singEq undefined

comment:2 Changed 3 months ago by RyanGlScott

Cc: goldfire added

This started panicking in commit e3dbb44f53b2f9403d20d84e27f187062755a089 (Fix #12919 by making the flattener homegeneous.)

comment:3 Changed 3 months ago by monoidal

Simplification:

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeInType #-}
module Bug where

import Data.Kind

elimSing :: forall (p :: forall z. z). p
elimSing = undefined

data WhySym :: Type -> Type

hsym = elimSing @WhySym

comment:4 Changed 3 months ago by simonpj

I'm on this. It turns out to be a very dark corner.

comment:5 Changed 3 months ago by Simon Peyton Jones <simonpj@…>

In aedbf7f1/ghc:

Fix decompsePiCos and visible type application

Trac #15343 was caused by two things

First, in TcHsType.tcHsTypeApp, which deals with the type argment
in visible type application, we were failing to call
solveLocalEqualities. But the type argument is like a user type
signature so it's at least inconsitent not to do so.

I thought that would nail it.  But it didn't. It turned out that we
were ended up calling decomposePiCos on a type looking like this
    (f |> co) Int

where co :: (forall a. ty) ~ (t1 -> t2)

Now, 'co' is insoluble, and we'll report that later.  But meanwhile
we don't want to crash in decomposePiCos.

My fix involves keeping track of the type on both sides of the
coercion, and ensuring that the outer shape matches before
decomposing.  I wish there was a simpler way to do this. But
I think this one is at least robust.

I suppose it is possible that the decomposePiCos fix would
have cured the original report, but I'm leaving the one-line
tcHsTypeApp fix in too because it just seems more consistent.

comment:6 Changed 3 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.

comment:7 Changed 3 months ago by simonpj

Status: newmerge
Test Case: dependent/should_fail/T15343

I'd like Richard to check these patches, if he has time, but they are outright bugs and should probably move to the branch

comment:8 Changed 3 months ago by bgamari

Resolution: fixed
Status: mergeclosed
Note: See TracTickets for help on using tickets.