[GHC] #16391: "Quantified type's kind mentions quantified type variable" error with fancy-kinded GADT

[GHC]

#16391: "Quantified type's kind mentions quantified type variable" error with
fancy-kinded GADT
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.6.3
  (Type checker)                     |
           Keywords:  TypeInType     |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  GHC rejects
  Unknown/Multiple                   |  valid program
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Given the following:

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

 import Data.Kind

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

 GHC happily accepts these definitions:

 {{{#!hs
 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:

 {{{#!hs
 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`:

 {{{#!hs
 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
 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.

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16391>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler