Opened 9 months ago

Closed 8 months ago

Last modified 6 months ago

#14904 closed bug (fixed)

Compiler panic (piResultTy)

Reported by: kcsongor Owned by:
Priority: normal Milestone: 8.6.1
Component: Compiler (Type checker) Version: 8.2.2
Keywords: TypeInType Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: typecheck/should_fail/T14904a, typecheck/should_fail/T14904b, indexed-types/should_fail/T14904
Blocked By: Blocking:
Related Tickets: #14873 Differential Rev(s):
Wiki Page:

Description

Type-checking the following type family

type family F (f :: forall a. g a) :: Type where
  F (f :: forall a. g a) = Int

panics with the message:

ghc: panic! (the 'impossible' happened)
  (GHC version 8.4.0.20180118 for x86_64-apple-darwin):
        piResultTy
  k_aVM[tau:1]
  a_aVF[sk:1]
  Call stack:
      CallStack (from HasCallStack):
        callStackDoc, called at compiler/utils/Outputable.hs:1150:37 in ghc:Outputable
        pprPanic, called at compiler/types/Type.hs:950:35 in ghc:Type

The panic happens with HEAD, 8.4 and 8.2. 8.0 rejects the program with an error message, but even it panics on the following version:

type family F f :: Type where
  F ((f :: forall a. g a) :: forall a. g a) = Int

#14873 seemed somewhat related, so I tried with the patch implemented in 3d252037234ce48f9bdada7d5c9b1d8eba470829, but that fails with the same panic too.

Attachments (1)

Bug.hs (324 bytes) - added by kcsongor 9 months ago.

Download all attachments as: .zip

Change History (11)

Changed 9 months ago by kcsongor

Attachment: Bug.hs added

comment:1 Changed 9 months ago by goldfire

Keywords: TypeInType added

This is clearly in my wheelhouse...

comment:2 Changed 8 months ago by RyanGlScott

It looks like commit faec8d358985e5d0bf363bd96f23fe76c9e281f7 (Track type variable scope more carefully.) nabbed this one. After that commit, I get error messages instead of panics on each program in the ticket.

For the first program:

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

import Data.Kind

type family F (f :: forall a. g a) :: Type where
  F (f :: forall a. g a) = Int
$ ghc/inplace/bin/ghc-stage2 Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:8:1: error:
    You have written a *complete user-suppled kind signature*,
    but the following variable is undetermined: k0 :: *
    Perhaps add a kind signature.
    Inferred kinds of user-written variables:
      g :: k0 -> *
      f :: forall (a :: k0). g a
  |
8 | type family F (f :: forall a. g a) :: Type where
  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

For the second program:

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module Bug2 where

import Data.Kind

type family F f :: Type where
  F ((f :: forall a. g a) :: forall a. g a) = Int
$ ghc/inplace/bin/ghc-stage2 Bug2.hs
[1 of 1] Compiling Bug2             ( Bug2.hs, Bug2.o )

Bug2.hs:9:7: error:
    • Expected kind ‘forall (a :: k1). g a’, but ‘f’ has kind ‘k0’
    • In the first argument of ‘F’, namely
        ‘((f :: forall a. g a) :: forall a. g a)’
      In the type family declaration for ‘F’
  |
9 |   F ((f :: forall a. g a) :: forall a. g a) = Int
  |       ^

I'll add regression tests and close this.

comment:3 Changed 8 months ago by kcsongor

Thanks!

comment:4 Changed 8 months ago by Ryan Scott <ryan.gl.scott@…>

In 5de0be8/ghc:

Add regression tests for #14904

Trac #14904 was fixed in commit
faec8d358985e5d0bf363bd96f23fe76c9e281f7. Let's add some tests to
ensure that it stays fixed.

comment:5 Changed 8 months ago by RyanGlScott

Milestone: 8.6.1
Resolution: fixed
Status: newclosed
Test Case: typecheck/should_fail/T14904a, typecheck/should_fail/T14904b

comment:6 Changed 8 months ago by goldfire

Hooray for RyanGlScott! :)

comment:7 Changed 6 months ago by sighingnow

For ASSERT-enabled ghc-stage2, the testcase T14904b still raises an "ASSERT failed!" panic. Not sure if it's worth further fix.

T14904b.hs:

import Data.Kind

type family F f :: Type where
  F ((f :: forall a. g a) :: forall a. g a) = Int

The panic error message:

λ ginplace\bin\ghc-stage2.exe--make T.hs
[1 of 1] Compiling T14904b          ( T.hs, T.o )
ghc-stage2.exe: panic! (the 'impossible' happened)
  (GHC version 8.5.20180608 for x86_64-unknown-mingw32):
        ASSERT failed!
  1
  0
  k_aWM[tau:0]
  (g_aWI[sig:0] |> {co_aWV}) a_aX4[tau:0]
  Call stack:
      CallStack (from HasCallStack):
        callStackDoc, called at compiler\utils\Outputable.hs:1161:37 in ghc:Outputable
        pprPanic, called at compiler\utils\Outputable.hs:1220:5 in ghc:Outputable
        assertPprPanic, called at compiler\\typecheck\\TcMType.hs:745:54 in ghc:TcMType
CallStack (from -prof):
  TcRnDriver.tc_rn_src_decls (compiler\typecheck\TcRnDriver.hs:(496,4)-(560,7))
  TcRnDriver.tcRnSrcDecls (compiler\typecheck\TcRnDriver.hs:259:25-65)

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

In 30b029be/ghc:

Fix typechecking of kind signatures

When typechecking a type like
   Maybe (a :: <kind-sig>)
with a kind signature, we were using tc_lhs_kind to
typecheck the signature.  But that's utterly wrong; we
need the signature to be fully solid (non unresolved
equalities) before using it.  In the case of Trac #14904
we went on to instantiate the kind signature, when it
still had embedded unsolved constraints.  This tripped
the level-checking assertion when unifying a variable.

The fix looks pretty easy to me: just call tcLHsKind
instead.  I had to add KindSigCtxt to

comment:9 Changed 6 months ago by simonpj

Test Case: typecheck/should_fail/T14904a, typecheck/should_fail/T14904btypecheck/should_fail/T14904a, typecheck/should_fail/T14904b, indexed-types/should_fail/T14904

I can't predict all the consequences of this bug, so even though it doesn't seem to cause problems in a non-DEBUG-enabled compiler, I suggest merging to 8.6.

Again, Richard might you check my work?

comment:10 Changed 6 months ago by goldfire

Checked. Looks good, except for the typo fix I pushed. Yes, this was an oversight.

Note: See TracTickets for help on using tickets.