#12081 closed bug (fixed)

TypeInType Compile-time Panic

Reported by: MichaelK Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.0.1-rc4
Keywords: TypeInType Cc: jstolarek
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Compile-time crash Test Case: dependent/should_fail/T12081
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

I've been playing around with GHC 8.0.1-rc4 release and got a panic from the following (stripped down) code:

{-# LANGUAGE TypeInType #-}

data Nat = Z | S Nat

class C (n :: Nat) where
  type T n :: Nat
  f :: (a :: T n)
ghc: panic! (the 'impossible' happened)
  (GHC version 8.0.0.20160421 for x86_64-apple-darwin):
	isInjectiveTyCon sees a TcTyCon T

Change History (6)

comment:1 Changed 16 months ago by goldfire

Keywords: TypeInType added

GHC should never panic, so this is certainly a bug.

However, your program is not type-correct: any type that classifies a runtime value must have kind Type (same as *). The type of f is given as (a :: T n), which has kind T n, not Type. I'm not sure what your goal is here, but even without the panic, this program would be rejected by GHC.

Thanks for reporting!

comment:2 Changed 16 months ago by MichaelK

goldfire,

Thanks for the explanation. For background, I've been trying to make a 'good' wrapper type for Natural whose type is effectively Nat.

comment:3 Changed 15 months ago by MitchellSalad

I happened to hit this same panic with a simpler example:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeInType #-}

data Foo = forall (x :: Foo). Bar x

fails with:

ghc: panic! (the 'impossible' happened)
  (GHC version 8.0.1 for x86_64-unknown-linux):
	isInjectiveTyCon sees a TcTyCon Foo

Without -XTypeInType, it fails with:

foo.hs:5:25: error:
    • Type constructor ‘Foo’ cannot be used here
        (Perhaps you intended to use TypeInType)
    • In the kind ‘Foo’
      In the definition of data constructor ‘Bar’
      In the data declaration for ‘Foo’

And without the x in Bar x, it compiles fine.

Last edited 15 months ago by MitchellSalad (previous) (diff)

comment:4 Changed 15 months ago by jstolarek

Cc: jstolarek added

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

In 853cdaea/ghc:

Test Trac #12081

comment:6 Changed 11 months ago by simonpj

Resolution: fixed
Status: newclosed
Test Case: dependent/should_fail/T12081
Note: See TracTickets for help on using tickets.