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: [email protected] [mailto:[email protected]] On
Behalf Of Iavor Diatchki
Sent: 21 May 2013 02:55
To: [email protected]
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
_______________________________________________
ghc-devs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/ghc-devs
