On Sat, Oct 12, 2013 at 1:29 AM, Iavor Diatchki wrote:

Hello,

I am not sure what version of GHC.TypeLits you looked at, but as of the other day the code in there is almost the same as what you propose (except for the use of different classes).

My copy of the code was a couple of days out of date, from when I started the patch. On Fri, Oct 11, 2013 at 12:54 PM, Edward Kmett wrote:

...

They are currently impossible to implement without using very deep voodoo. See the magicSingIId note.

The `magicSingI` has been redone and is quite a bit simpler now. Note [magicDictId magic] describes the current approach. Still, if we can think of a way to get rid of it, I'm strongly in support.

...

If we bring in GHC.Reflection. (I've almost finished a patch for it, my only remaining hangups are in the wiredIn itself) then the code in GHC.TypeLits for KnownNat and KnownSymbol can go away, and those two definitions can use reflection internally.

`KnowNat` and `KnownSymbol` are the basic classes that provide the built-in instances for type-level literals (SingI is gone). I don't see any way around having some built-in code like that.

Indeend, `natVal` is implemented almost exactly like this. It'd be trivial

to provide an instance for the `Reify` class if we needed to:

instance KnowNat n => Reifying (n :: Nat) where type Reified n = Integer; reflect# = natVal

If those are the classes being generated now, then I can use that to generate the instances for Reifying at those kinds.

Those classes can melt away and disappear

...

Do you mean by providing built-in instances for `Reify` instead? If so, this is mostly a renaming, and I am not so keen on making the change as I like the simplicity of `KnownSym` and `KnownNat`. Also---and this is an implementation detail---their dictionaries are simpler than the one for `Reify`: they just carry around the actual value, integer or string, while the dictionaries for `Reify` have to store a whole function. I think this matters when you package them in existentials, no?

The instance for Reifying holds a function from Proxy# a which is of unlifted kind and has no representation. Behind the scenes they should look substantially identical. Using something like the Tagged newtype could make them definitely identical behind the scenes. I'm okay with leaving them as it is. I mostly was noting that if we did consolidate then we'd get a slight code reduction.

and internally the implementation of someNatVal, and someSymbolValbecome much less horrific:

...

-- | This type represents unknown type-level natural numbers. data SomeNat = forall (n :: Nat). Reifying n => SomeNat (Proxy# n)

-- | Convert an integer into an unknown type-level natural. someNatVal :: Integer -> Maybe SomeNat someNatVal n | n >= 0 = Just (reify# n SomeNat) | otherwise = Nothing

Well, the current implementation is almost exactly this! I don't really know how `reify#` is supposed to work, but it certainly seems to do something very similar to what `magicDict` does, so we should probably make sure that there is only one implementation. I would guess that you can use `magicDict` to implement `reify#`. The other way around would also be OK with me as long as I don't have to use the `Reify` class, and can use directly the simpler (no type functions, no kind polymorphism) `KnownSymbol` and `KnownNat` classes.

In core, stripping away the newtypes and coercions reify# winds up looking like reify a k = k (\_ -> a) proxy# The lambda there is ignoring a Proxy#, which is an unlifted argument without representation, and the proxy# argument at the end is similar. Also, doesn't `reify#` introduce a coherence issue? `someNatVal` and the

instances for `KnownNat` are carefully engineered to provide a consistent view to the programmer, but as far as understand, this is not the case with `Reifying`. For example, consider the following code:

data {- kind -} K

instance Reifying (a :: K) where type Reified a = Integer reflect# _ = 5

getK :: Reifying a => Proxy (a :: K) -> Integer getK = reflect#

test :: Integer test = reify# 6 getK

It is not at all obvious if `test` should evaluate 5 (using the global instance) or 6 (using the locally supplied evidence), and the choice seems highly dependent on the mood of the constraint solver.

Fair point. I was attempting to generalize reify# to allow it to instantiate at kinds other than *, to enable it to subsume your existing usecase. When restricted to * there isn't a coherence issue, as there is no such overarching instance, but also simply by providing any concrete instance of Reifying under kind * means that any attempt by the user to define such an instance Reifying (a :: *) would overlap, preventing this conflict. I'll go back to the simpler version of reify#, which doesn't attempt to let you reify at other kinds, and leave TypeLits alone. This simplifies my task considerably. -Edward