#11648: assertPprPanic, called at compiler/types/TyCoRep.hs:1932 -------------------------------------+------------------------------------- Reporter: thomie | Owner: goldfire Type: bug | Status: new Priority: highest | Milestone: 8.0.1 Component: Compiler | Version: 8.1 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): This is making yet more sense. And it seems that you are proposing: * INVARIANT: The kind of a quantified type variable has no meta-tyvars. We already had that the quantified type variable itself must not be a meta-tyvar. But this invariant goes one step further, in that the set of variables reachable from a quantified tyvar must be devoid of meta-tyvars. Do you agree with this invariant? And, as for design, it seems you are proposing (forgetting about associated types for the moment): * Keep the syntactic definition of CUSK as it is (Note [Complete user- supplied kind signatures] in HsDecls). * When a declaration has a CUSK, default any remaining meta-tyvars after `getInitialKind`. * If a meta-tyvar is not defaultable, the program is erroneous. I'm quite dubious of this design for several reasons. First, this seems strange to users. For example: {{{ data T1 (a :: Proxy k) data T2 (a :: Proxy k) b }}} `T1` has a CUSK, according to our definition. Thus its `k` will be defaulted to kind `*`. `T2`, though, does not have a CUSK, and so `k` is not defaulted and has kind `k2`. Second, the design seems hard to implement without annoying users. For example: {{{ data T3 (x :: * -> *) data T4 (a :: T3 k) }}} `T4` has a CUSK, and `k` should clearly have kind `* -> *`. But we can't discover that until `kcTyClDecl`, which is too late. According to the last bullet above, we'll fail at defaulting `T4`'s `k`'s kind and issue an error, even though it's quite obvious what we should do. So, I must ask: why is it so necessary to have the INVARIANT at the top? I understand this requires expanding the in-scope set for the substitution at hand, but why is that problematic? I don't see what's so bad about a meta-tyvar in a quantified variable's kind. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11648#comment:16 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler