"Quantified type's kind mentions quantified type variable" error with fancy-kinded GADT

Given the following:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}

import Data.Kind

type Const (a :: Type) (b :: Type) = a

GHC happily accepts these definitions:

type family F :: Const Type a where
  F = Int
type TS = (Int :: Const Type a)

However, the situation becomes murkier with data types. For some reason, GHC //rejects// this definition:

data T :: Const Type a where
  MkT :: T

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

Bug.hs:14:3: error:
    • Quantified type's kind mentions quantified type variable
      (skolem escape)
           type: forall a1. T
        of kind: Const * a
    • In the definition of data constructor ‘MkT’
      In the data type declaration for ‘T’
   |
14 |   MkT :: T
   |   ^^^^^^^^

I'm not quite sure how to interpret that error message, but it seems fishy to me. Even fishier is the fact that GHC //accepts// this slight modification of T:

data T2 :: Const Type a -> Type where
  MkT2 :: T2 b

Quite mysterious.

---

I briefly looked into where this error message is being thrown from. It turns out if you make this one-line change to GHC:

diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs
index 218f539c68..c7925767f9 100644
--- a/compiler/typecheck/TcValidity.hs
+++ b/compiler/typecheck/TcValidity.hs
@@ -635,7 +635,7 @@ check_type ve@(ValidityEnv{ ve_tidy_env = env, ve_ctxt = ctxt
         ; check_type (ve{ve_tidy_env = env'}) tau
                 -- Allow foralls to right of arrow

-        ; checkTcM (not (any (`elemVarSet` tyCoVarsOfType phi_kind) tvs))
+        ; checkTcM (not (any (`elemVarSet` exactTyCoVarsOfType phi_kind) tvs))
                    (forAllEscapeErr env' ty tau_kind)
         }
   where

Then GHC will accept T. Whether this change is the right choice to make, I don't think I'm qualified to say.

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