"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 |