Too easy to trigger CUSK condition using TH
While trying to make
singletons class promotion work with kind-polymorphic type variables, I've encountered a problem regarding CUSKs.
Consider this class:
$(promoteOnly [d| class Cls a where fff :: Proxy a -> () |])
The generated TH (slightly simplified by hand) looks like this:
type FffSym1 (t_alvm :: Proxy a1627472612) = Fff t_alvm data FffSym0 (l_alvn :: TyFun (Proxy a1627472612) ()) type instance Apply FffSym0 l_alvn = FffSym1 l_alvn class PCls a_alve where type Fff (arg_alvl :: Proxy a_alve) :: ()
However, it fails to compile with the following error:
cusk.hs:25:1: error: You have written a *complete user-suppled kind signature*, but the following variable is undetermined: k0 :: * Perhaps add a kind signature. Inferred kinds of user-written variables: a1627472612 :: k0 l_alvn :: TyFun (Proxy a1627472612) ()
As suggested by the error message, we need to specify the kind in its entirety (write a proper CUSK). So to sidestep the issue, we can write
data FffSym0 (l_alvn :: TyFun (Proxy (a1627472612 :: k)) ())
and it'll work. However, this means that the TH code generator should perform some guesswork to modify kind annotations. It sounds like a minefield — too much can go wrong, so it'd be great to avoid doing so.
Looking at the module
TcHsType in the GHC sources, I see that the error is reported by the
-- If there are any meta-tvs left, the user has -- lied about having a CUSK. Error. ; let (meta_tvs, good_tvs) = partition isMetaTyVar qkvs ; when (not (null meta_tvs)) $ report_non_cusk_tvs (qkvs ++ tc_tvs)
However, I don't see why we can't generalize over
meta_tvs instead of reporting a failure. I asked on IRC #ghc and ezyang suggested that it should be sound.
Below I attach a self-contained example that demonstrates the issue and has no dependencies except
|Component||Compiler (Type checker)|