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
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@haskell.org [mailto:ghc-devs-bounces@haskell.org] On Behalf Of Iavor Diatchki Sent: 21 May 2013 02:55 To: ghc-devs@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
participants (2)
-
Iavor Diatchki -
Simon Peyton-Jones