On Wed, Sep 19, 2012 at 1:51 PM, Richard Eisenberg
As for recovering "kind classes" and such once Any is made into a type family: I'm in favor of finding some way to do explicit kind instantiation, making the Any trick obsolete. I'm happy to leave it to others to decide the best concrete syntax.
I'll admit I haven't parsed this entire email thread, but I read enough of it early on that I wanted to avoid Any recently. Returning to find this quote from Richard, perhaps the trick I came up is the one you're after. (Also — what's the general status on this initiative? Has much happened in about a month?) The to my trick key is to use the promotion of this data type.
data KindProxy (k :: *) = KindProxy
I needed it in order to define this family, which counts the number of arguments a kind has.
type family CountArgs (kp :: KindProxy k) :: Nat type instance CountArgs (kp :: *) = Z type instance CountArgs (kp :: kD -> kR) = S (CountArgs ('KindProxy :: KindProxy kR))
The proxy is necessary on the RHS of the second instance, in which I need a type of kind kR, but I wouldn't have any means to build one (without Any) were CountArgs simply of kind (k -> Nat). This usage is comparable to Richard's usage in the singletons library, insomuch as I understand from the Haskell 2012 paper. I'm less familiar with the usage in GHC.TypeLits. At a quick glance, I believe I'd change SingE like so
class SingE (kparam :: KindProxy k) rep | kparam -> rep where fromSing :: Sing (a :: k) -> rep
instance SingE (kparam :: KindProxy Nat) Integer where fromSing (SNat n) = n
instance SingE (kparam :: KindProxy Symbol) String where fromSing (SSym s) = s
However, looking through the rest of that module, I see no point where a proxy is actually required (as it is required in the second case of CountArgs). Maybe I'm just missing it, or maybe Iavor is just interested in *enforcing* the fact that the type is not of consequence? Along those same lines… Iavor had SingE instances declared for (Any :: KindProxy Nat) and (Any :: KindProxy Symbol). I'm not sure why he didn't leave the type polymorphic, as I have. Perhaps it matters for various uses of SingE? I haven't tried using my code with examples, so maybe that's where issues would show up. If it were necessary, the instances could instead be as follows.
instance SingE ('KindProxy :: KindProxy Nat) Integer where fromSing (SNat n) = n
instance SingE ('KindProxy :: KindProxy Symbol) String where fromSing (SSym s) = s
Is this the kind of trick you were after, Richard? It might pollute the code base and interface a bit with KindProxy wrappers, but I've not found that insurmountable. Hopefully that isn't a show stopper for you. HTH