Question about wired-in class TyCons

[Simon Peyton-Jones]

Good question, and I’m afraid it’s quite awkward.

Stuff that is wired in to the compiler indeed avoids mentioning classes (or even complicated TyCons) precisely because they are complicated structures.  It would not be impossible to wire them in too, but I’d prefer not to.

My guess is that the unfolding you desire also mentions hard-to-wire-in classes or types.

So here’s an alternative.

·      In MkId add a new wired-in Id  magicNatSingI :: forall a. a

·      In your Sing module define
    natSingI :: Sing a -> (Sing I a => b) -> b
    natSingI = magicNatSingI

·      In prelude/PrelRules you’ll find ‘builtinRules’ which gives RULES that can’t be expressed in Haskell.   Add a RULE for magicNatSingI that rewrites (natSingI tau) to the right Core.  The tau you’ll get is precisely the type of natSingI.

So in effect magicNatSingI is a place-holder for the Core.

Not beautiful, but I think it’s a recipe that should work.

Simon

From: ghc-devs-bounces at haskell.org [mailto:ghc-devs-bounces at haskell.org] On Behalf Of Iavor Diatchki
Sent: 21 May 2013 02:55
To: ghc-devs at haskell.org
Subject: Question about wired-in class TyCons

Hello,

I was trying to add a new compulsory-unfoldable primitive (i.e., one like `unsafeCoerce` in `basicTypes/MkId.hs`), but I got stuck while trying to construct its type.  The primitive needs to have this type:

    natSingI :: Sing a -> (SingI a => b) -> b

`Sing` is a kind polymorphic data family.
`SingI` is a kind polymorphic class.

I am using these at kind `Nat` so, I believe, the fully-explicit type that I need to construct is actually this:

    natSingI :: forall (a :: Nat) (b :: *). Sing Nat a -> (SingI Nat a -> b) -> b

I can almost create this type, but I got stuck on making the `SingI` type constructor.  While there are many examples of making `Name`s for classes, I couldn't find one where we make a `TyCon` for a class.  In particular, it looks like to make a class `TyCon`, I need to provide a `Class` value, which contains a whole lot of information that would normally be constructed by the compiler itself (class `SingI` is an ordinary class defined in source code).

So I was wondering if there might be a way to obtain this information in some way or if, indeed, I need to define explicitly the entire class as a wired-in thing.

Any advice would be most appreciated!
-Iavor

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20130521/c0141dba/attachment-0001.htm>