Opened 7 months ago

Closed 7 months ago

Last modified 7 months ago

#16391 closed bug (fixed)

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

Reported by: RyanGlScott Owned by:
Priority: normal Milestone: 8.10.1
Component: Compiler (Type checker) Version: 8.6.3
Keywords: TypeInType Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case: dependent/should_compile/T16391a, dependent/should_fail/T16391b
Blocked By: Blocking:
Related Tickets: Differential Rev(s): https://gitlab.haskell.org/ghc/ghc/merge_requests/503
Wiki Page:

Description

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:

  • compiler/typecheck/TcValidity.hs

    diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs
    index 218f539c68..c7925767f9 100644
    a b check_type ve@(ValidityEnv{ ve_tidy_env = env, ve_ctxt = ctxt 
    635635        ; check_type (ve{ve_tidy_env = env'}) tau
    636636                -- Allow foralls to right of arrow
    637637
    638         ; checkTcM (not (any (`elemVarSet` tyCoVarsOfType phi_kind) tvs))
     638        ; checkTcM (not (any (`elemVarSet` exactTyCoVarsOfType phi_kind) tvs))
    639639                   (forAllEscapeErr env' ty tau_kind)
    640640        }
    641641  where

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

Change History (6)

comment:1 Changed 7 months ago by simonpj

Two things here. First, could you add this note in module Type

Note [Phantom type variables in kinds]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider

  type K (r :: RuntimeRep) = Type   -- Note 'r' is unused
  data T r :: K r                   -- T :: forall r -> K r
  foo :: forall r. T r

The body of the forall in foo's type has kind (K r), and
normally it would make no sense to have
   forall r. (ty :: K r)
because the kind of the forall would escape the binding
of 'r'.  But in this case it's fine because (K r) exapands
to Type, so we expliclity /permit/ the type
   forall r. T r

To accommodate such a type, in typeKind (forall a.ty) we use
occCheckExpand to expand any type synonyms in the kind of 'ty' 
to eliminate 'a'.  See kinding rule (FORALL) in 
Note [Kinding rules for types]

And in TcValidity.checkEscapingKind, we use also use
occCheckExpand, for the same reason.

just after Note [Kinding rules for types]. And refer to the Note from the calls to occCheckExpand in typeKind and tcTypeKind.

Then, in TcValidity, perhpas pull that entire check out intoa named function checkEscapingKind, and refer again to the same Note. And I think it'd be simpler to use occCheckExpand there too. (Your suggestion of exactTyCoVarsOfType is equivalent, but using the same function in all three places seems better.)

Does that make sense?

comment:2 Changed 7 months ago by simonpj

The other bad thing is that the error message is a mess, becuase it mentions 'a' in one place and 'a1' in the other. Very confusing.

Reason:

                   (forAllEscapeErr env' ty tau_kind)

we pass env' (the result of tidying tvs) to forAllEscapeErr, which then prints ty in this tidy-env, thereby tidying the same tyvars again. This would not be hard to clear up, perhpas not by printing ty afresh, but by passing tvs' and phi to forAllEscapeErr, and printing the foralls manually, as it were.

Does that make sense? Also I wonder if if might be easier to understand if we said

   • Quantified type's kind mentions quantified type variable
           type: forall a1. T
     where the body of the forall has this kind
           T :: Const * a

comment:3 Changed 7 months ago by simonpj

PS: here is a test caes that is rightly rejected by the test in TcFValidity.

type family T (r :: RuntimeRep) :: TYPE r

foo :: T r
foo = foo

It'd be good to add a note to TcValidity to show this example of how the test does something useful.

comment:4 Changed 7 months ago by RyanGlScott

Differential Rev(s): https://gitlab.haskell.org/ghc/ghc/merge_requests/503
Status: newpatch

comment:5 Changed 7 months ago by RyanGlScott

Milestone: 8.10.1
Resolution: fixed
Status: patchclosed
Test Case: dependent/should_compile/T16391a, dependent/should_fail/T16391b

Landed in 068b7e98.

comment:6 Changed 7 months ago by Marge Bot <ben+marge-bot@…>

In 068b7e98/ghc:

Fix #16391 by using occCheckExpand in TcValidity

The type-variables-escaping-their-scope-via-kinds check in
`TcValidity` was failing to properly expand type synonyms, which led
to #16391. This is easily fixed by using `occCheckExpand` before
performing the validity check.

Along the way, I refactored this check out into its own function,
and sprinkled references to Notes to better explain all of the moving
parts. Many thanks to @simonpj for the suggestions.

Bumps the haddock submodule.
Note: See TracTickets for help on using tickets.