#15142: GHC HEAD regression: tcTyVarDetails -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: goldfire Type: bug | Status: closed Priority: highest | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Keywords: TypeInType, Resolution: fixed | TypeFamilies, CUSKs Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Compile-time | Test Case: indexed- crash or panic | types/should_compile/T15142 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Richard, I have augmented the Note as below. Do you agree with it? On the last point, we say that this does not have a CUSK (taken from `dependent/should_compile/kind_levels`): {{{ data C :: B a -> * }}} But why not? The lexical-forall rule means that it's equivalent to {{{ data C :: forall a. B a -> * }}} which now does have a CUSK. Either the rule needs more justification, or its over-restrictive. Here's the new Note: {{{ {- Note [CUSKs: complete user-supplied kind signatures] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ We kind-check declarations differently if they have a complete, user- supplied kind signature (CUSK). This is because we can safely generalise a CUSKed declaration before checking all of the others, supporting polymorphic recursion. See ghc.haskell.org/trac/ghc/wiki/GhcKinds/KindInference#Proposednewstrategy and #9200 for lots of discussion of how we got here. PRINCIPLE: a type declaration has a CUSK iff we could produce a separate kind signature for it, just like a type signature for a function, looking only at the header of the declaration. Examples: * data T1 (a :: *->*) (b :: *) = .... -- Has CUSK; equivalant to T1 :: (*->*) -> * -> * * data T2 a b = ... -- No CUSK; we do not want to guess T2 :: * -> * -> * -- becuase the full decl might be data T a b = MkT (a b) * data T3 (a :: k -> *) (b :: *) = ... -- CUSK; equivalent to T3 :: (k -> *) -> * -> * -- We lexically generalise over k to get -- T3 :: forall k. (k -> *) -> * -> * -- The generalisation is here is purely lexical, just like -- f3 :: a -> a -- means -- f3 :: forall a. a -> a * data T4 (a :: j k) = ... -- CUSK; equivalent to T4 :: j k -> * -- which we lexically generalise to T4 :: forall j k. j k -> * -- and then, if PolyKinds is on, we further generalise to -- T4 :: forall kk (j :: kk -> *) (k :: kk). j k -> * -- Again this is exactly like what happens as the term level -- when you write -- f4 :: forall a b. a b -> Int NOTE THAT * A CUSK does /not/ mean that everything about the kind signature is fully specified by the user. Look at T4 and f4: we had do do kind inference to figure out the kind-quantification. But in both cases (T4 and f4) that inference is done looking /only/ at the header of T4 (or signature for f4), not at the definition thereof. * The CUSK completely fixes the kind of the type constructor, forever. * The precise rules, for each declaration form, for whethher a declaration has a CUSK are given in the user manual section "Complete user- supplied kind signatures and polymorphic recursion". BUt they simply implement PRINCIPLE above. * Open type families are interesting: type family T5 a b :: * There simply /is/ no accompanying declaration, so that info is all we'll ever get. So we it has a CUSK by definition, and we default any un-fixed kind variables to *. * Associated types are a bit tricker: class C6 a where type family T6 a b :: * op :: a Int -> Int Here C6 does not have a CUSK (in fact we ultimately discover that a :: * -> *). And hence neither does T6, the associated family, because we can't fix its kind until we have settled C6. Another way to say it: unlike a top-level, we /may/ discover more about a's kind from C6's definition. * A data definition with a top-level :: must explicitly bind all kind variables to the right of the ::. See test dependent/should_compile/KindLevels, which requires this case. (Naturally, any kind variable mentioned before the :: should not be bound after it.) }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15142#comment:20 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler