#11203: Kind inference with SigTvs is wrong -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Consider {{{#!hs data SameKind :: k -> k -> * data Q (a :: k1) (b :: k2) c = MkQ (SameKind a b) }}} This code should be rejected. Yet it is accepted. The problem is that, when kind-checking a datatype declaration without a CUSK, GHC uses `SigTv`s for user-written kind variables. `SigTv`s are allowed to unify with other `SigTv`s, leading to incorrect behavior here. The motivating scenario is this: {{{#!hs data T (a :: k1) x = MkT (S a ()) data S (b :: k2) y = MkS (T b ()) }}} This program should be accepted. Neither type has a CUSK and therefore is not generalized before kind-checking the group. GHC must then unify `k1` and `k2`. If they were skolems, this unification would fail and this pair of definitions would be rejected. This ticket is identical in spirit to #9201, but that example has a CUSK and thus works. The bug can happen only when there is no CUSK. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11203 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler