GHC panic (tcInvisibleTyBinder) when using constraint in a kind
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 UserTypeCtxt
s 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)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^