GitLab

The following program will panic when compiled with GHC 8.10 or HEAD:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
module Bug where

import GHC.Exts

type Id a = a

type F = Id (Any :: forall a. Show a => a -> a)

$ /opt/ghc/8.10.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )
ghc: panic! (the 'impossible' happened)
  (GHC version 8.10.2:
        tcInvisibleTyBinder
  Show a_avp[sk:2]
  Call stack:
      CallStack (from HasCallStack):
        callStackDoc, called at compiler/utils/Outputable.hs:1179:37 in ghc:Outputable
        pprPanic, called at compiler/typecheck/Inst.hs:460:5 in ghc:Inst

I'm a bit surprised that this happens, since GHC has a validity check intended to rule out the use of arbitrary constraints in kinds. This check is implemented by GHC.Tc.Validity.allConstraintsAllowed:

allConstraintsAllowed :: UserTypeCtxt -> Bool
-- We don't allow arbitrary constraints in kinds
allConstraintsAllowed (TyVarBndrKindCtxt {}) = False
allConstraintsAllowed (DataKindCtxt {})      = False
allConstraintsAllowed (TySynKindCtxt {})     = False
allConstraintsAllowed (TyFamResKindCtxt {})  = False
allConstraintsAllowed (StandaloneKindSigCtxt {}) = False
allConstraintsAllowed _ = True

Upon closer inspection, allConstraintsAllowed appears to be incomplete. Compare this to GHC.Tc.Validity.vdqAllowed, which must also make a distinction between types and kinds:

vdqAllowed :: UserTypeCtxt -> Bool
-- Currently allowed in the kinds of types...
vdqAllowed (KindSigCtxt {}) = True
vdqAllowed (StandaloneKindSigCtxt {}) = True
vdqAllowed (TySynCtxt {}) = True
vdqAllowed (ThBrackCtxt {}) = True
vdqAllowed (GhciCtxt {}) = True
vdqAllowed (TyVarBndrKindCtxt {}) = True
vdqAllowed (DataKindCtxt {}) = True
vdqAllowed (TySynKindCtxt {}) = True
vdqAllowed (TyFamResKindCtxt {}) = True
-- ...but not in the types of terms.
...

Note that vdqAllowed identifies more UserTypeCtxts as being kind-level positions than allConstraintsAllowed does. Crucially, allConstraintsAllowed omits a case for KindSigCtxt. If I add such as case:

diff --git a/compiler/GHC/Tc/Validity.hs b/compiler/GHC/Tc/Validity.hs
index fba45562b7..39ebc260da 100644
--- a/compiler/GHC/Tc/Validity.hs
+++ b/compiler/GHC/Tc/Validity.hs
@@ -479,6 +479,7 @@ allConstraintsAllowed (DataKindCtxt {})      = False
 allConstraintsAllowed (TySynKindCtxt {})     = False
 allConstraintsAllowed (TyFamResKindCtxt {})  = False
 allConstraintsAllowed (StandaloneKindSigCtxt {}) = False
+allConstraintsAllowed (KindSigCtxt {}) = False
 allConstraintsAllowed _ = True

 -- | Returns 'True' if the supplied 'UserTypeCtxt' is unambiguously not the

Then the program above no longer panics:

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

Bug.hs:11:14: error:
    • Illegal constraint in a kind: forall a. Show a => a -> a
    • In the first argument of ‘Id’, namely
        ‘(Any :: forall a. Show a => a -> a)’
      In the type ‘Id (Any :: forall a. Show a => a -> a)’
      In the type declaration for ‘F’
   |
11 | type F = Id (Any :: forall a. Show a => a -> a)
   |              ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^