#12928: Too easy to trigger CUSK condition using TH -------------------------------------+------------------------------------- Reporter: int-index | Owner: Type: feature request | Status: new Priority: high | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: 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 goldfire): ezyang is right -- it would be sound. But it would defeat the purpose of CUSKs. The idea with CUSKs is that they allow a user to specify when everything about the kind of a type-level definition (datatype, newtype, class, family, type synonym) is known, without any inference. When a CUSK is available, GHC can then use polymorphic recursion and other fancy features while checking the type. Without a CUSK, though, inference with polymorphic recursion is impossible. Here is an example: {{{ type family F (a :: k) where F Int = Bool }}} What's the kind of `F`? There are at least two possibilities: `k -> Type` and `k -> k`. Neither is more general than the other. Instead of guessing between these (and others that use kind families!), GHC rejects the definition as lacking a CUSK. Is this an example of polymorphic recursion? Sort of. You can see it as polymorphic recursion if we consider that we're defining `F` but the occurrence of `F` in the equation is specialized to operate at kind `Type`. So it falls under this whole umbrella. Getting back to the original question: we ''could'' generalize here. But then type inference would become unpredictable. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12928#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler