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 kcHsTyVarBndrs
function:
-- 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 base
.
Trac metadata
Trac field | Value |
---|---|
Version | 8.0.1 |
Type | FeatureRequest |
TypeOfFailure | OtherFailure |
Priority | high |
Resolution | Unresolved |
Component | Compiler (Type checker) |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |