[GHC] #12928: Too easy to trigger CUSK condition using TH

[GHC]

#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