#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 (Type | Version: 8.6.3 checker) | Resolution: | 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: | -------------------------------------+------------------------------------- Comment (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? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16391#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler