Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
  • Sign in / Register
  • GHC GHC
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Locked Files
  • Issues 5,243
    • Issues 5,243
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 567
    • Merge requests 567
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
    • Test Cases
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Code review
    • Insights
    • Issue
    • Repository
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Glasgow Haskell CompilerGlasgow Haskell Compiler
  • GHCGHC
  • Issues
  • #18714
Closed
Open
Issue created Sep 18, 2020 by Ryan Scott@RyanGlScottMaintainer

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 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)
   |              ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking