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