GHC panic (No skolem info) with RankNTypes and strange scoping

The following program panics with GHC 8.6.3 and HEAD:

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE QuantifiedConstraints #-}
module Bug where

import Data.Kind

type Const a b = a
type SameKind (a :: k) (b :: k) = (() :: Constraint)
class (forall (b :: k). SameKind a b) => C (k :: Const Type a)

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

Bug.hs:11:36: error:ghc: panic! (the 'impossible' happened)
  (GHC version 8.6.3 for x86_64-unknown-linux):
        No skolem info:
  [k1_a1X4[sk:1]]
  Call stack:
      CallStack (from HasCallStack):
        callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable
        pprPanic, called at compiler/typecheck/TcErrors.hs:2891:5 in ghc:TcErrors

As with #16244 (closed), I imagine that the real culprit is that SameKind a b would force a :: k, which would be ill-scoped.

Trac metadata

Trac field	Value
Version	8.6.3
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

changed weight to 5

added Tbug Trac import typechecker labels

changed milestone to %8.10.1

added TypeInType + 1 deleted label

added compiler crash label

added QuantifiedConstraints label

Actually, this isn't really a QuantifiedConstraints bug, but rather a general rank-n types bug. This program also exhibits the same panic:

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

import Data.Kind

type Const a b = a
data SameKind :: k -> k -> Type

newtype T (k :: Const Type a) = MkT (forall (b :: k). SameKind a b)

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

Bug.hs:10:66: error:ghc: panic! (the 'impossible' happened)
  (GHC version 8.6.5 for x86_64-unknown-linux):
        No skolem info:
  [k1_aWg[sk:1]]
  Call stack:
      CallStack (from HasCallStack):
        callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable
        pprPanic, called at compiler/typecheck/TcErrors.hs:2891:5 in ghc:TcErrors

If you compile this program with GHC 8.2 or 8.4, then it simply goes into an infinite loop.

added RankNTypes label

changed title from GHC panic (No skolem info) with QuantifiedConstraints and strange scoping to GHC panic (No skolem info) with RankNTypes and strange scoping

It gets worse. This one simply goes into an infinite loop, apparently

type T (k :: Const Type a) = forall (b :: k). SameKind a b

added Pnormal label

removed milestone

mentioned in issue #17841 (closed)

Commit e3c374cc ended up fixing the original program in this issue, as GHC now throws an error message instead of panicking:

[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:11:36: error:
    • Couldn't match kind ‘k1’ with ‘k’
      ‘k1’ is a rigid type variable bound by
        the class declaration for ‘C’
        at Bug.hs:11:45
      ‘k’ is a rigid type variable bound by
        the class declaration for ‘C’
        at Bug.hs:11:1-62
    • In the second argument of ‘SameKind’, namely ‘b’
      In the class declaration for ‘C’
   |
11 | class (forall (b :: k). SameKind a b) => C (k :: Const Type a)
   |                                    ^

I'll add a regression test to !3200 (closed), since it's in very similar territory.

Alas, the program in #16245 (comment 211369) still panics, and the program in #16245 (comment 211400) still loops infinitely.

mentioned in commit 01dd8c76

mentioned in merge request !3200 (closed)

mentioned in commit df995a3d

mentioned in commit 2420c555

Commit 2420c555 adds a regression test (polykinds/T16245) for the original program in this issue, which no longer compiles. However, since the program in #16245 (comment 211369) still panics, and the program in #16245 (comment 211400) still loops infinitely, I'll keep this issue open.

mentioned in issue #18451 (closed)

Note that the program from #16245 (comment 211400) now has its own issue: #18451 (closed).

mentioned in commit 30e875f4

mentioned in commit ca6505d4

mentioned in commit 336abb3b

mentioned in commit 69f79f77

mentioned in commit b18c7f3b

mentioned in commit e11af031

mentioned in commit c846d4a0

mentioned in commit 8cf7b275

mentioned in commit 91c68504

mentioned in commit 29962b14

mentioned in commit 24089329

mentioned in commit 675d82eb

mentioned in commit 0b2e16b2

mentioned in commit 710aad27

mentioned in commit 862cb017

mentioned in commit b544bb03

mentioned in commit c87c7331

mentioned in commit be4e8e8c

mentioned in commit ea097e5f

mentioned in commit 94d7e377

mentioned in commit c2214738

mentioned in commit d297b1b5

mentioned in commit f4f40866

mentioned in commit 68577cea

mentioned in commit 552b267b

mentioned in commit bff82032

mentioned in commit 92548dd6

mentioned in commit cca982e8

Same or different issue ?

PolyKinds is weird

{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE PolyKinds #-}
import Data.Kind
import Control.Category

class Category hom => HasProduct (hom :: k -> k -> Type) where
   generic :: (forall (i :: a). hom i b) -> hom a b

It might be the issue that caused the original program in this issue to panic, but I don't think it's the same issue that causes the program in #16245 (comment 211369) to panic. The difference is that the former has been fixed, but the latter still panics on GHC 9.0 or later. Your program appears to be of the former variety, since it no longer panics on 9.0 or later:

$ ~/Software/ghc-9.0/bin/ghc Bug.hs
[1 of 1] Compiling Main             ( Bug.hs, Bug.o )

Bug.hs:8:29: error:
    • Expected a type, but ‘a’ has kind ‘k1’
      ‘k1’ is a rigid type variable bound by
        the class declaration for ‘HasProduct’
        at Bug.hs:7:35-55
    • In the kind ‘a’
      In the type signature:
        generic :: (forall (i :: a). hom i b) -> hom a b
      In the class declaration for ‘HasProduct’
  |
8 |    generic :: (forall (i :: a). hom i b) -> hom a b
  |                             ^

Happily all this is fixed in !3220 (closed), which should land soon.

mentioned in commit 039be784

mentioned in commit 2ef18ab4

mentioned in commit 89831ac8

mentioned in commit 00080feb

closed via commit 9fa26aa1

mentioned in commit 9fa26aa1

Fixed by

commit 89831ac862914568a77fbdcb82b616af49e1b994 (HEAD -> wip/T18126, origin/wip/T18126)
Author: Simon Peyton Jones <simonpj@microsoft.com>
Date:   Thu Jul 16 14:35:42 2020 +0100

    Improve kind generalisation, error messages

Test for #16245 (comment 211369) is polykinds/T16245a

There is also the existing polykinds/T16335 for the program in the Description

marked #19140 (closed) as a duplicate of this issue

marked this issue as related to #19140 (closed)

mentioned in issue #19140 (closed)