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,255
    • Issues 5,255
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 562
    • Merge requests 562
  • 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
  • #16391
Closed
Open
Issue created Mar 05, 2019 by Ryan Scott@RyanGlScottMaintainer

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