Unless there's some issues I'm missing, all of the `liftEq` functions could be replaced by just one:

    apply :: (f :~: g) -> (a :~: b) -> (f a :~: g b)

`lower` could be generalized:

    inner :: (f a :~: g b) -> (a :~: b)

and this could be added:

    outer :: (f a :~: g b) -> (f :~: g)


On Mon, Oct 21, 2013 at 6:04 AM, Richard Eisenberg <eir@cis.upenn.edu> wrote:
- There is a new function (in Data.Type.Equality) gcastWith :: (a :~: b) -> ((a ~ b) => r) -> r. Type inference for this function works well.

In my experience, for partial application it's convenient to have the arguments the other way around.
 
- I've renamed EqualityT and CoercionT to EqualityType and CoercionType. The T's at the ends of the old names made me think of monad transformers. I don't like the new names, though.

No radically better ideas, but perhaps marginally: `TypeEq` and `TypeReprEq`? Or `TestEquality` and `TestCoercible`?
 
- EqualityType's method is now maybeEquality (instead of equalsT). CoercionType's method is now maybeCoercion (instead of coercionT).

These seem alright. I suppose they might change to track the class names, if those change.
 
- An earlier version of TypeLits had Nat1 as a canonical unary natural number type and conversions to and from. I expect this will be a popular addition, so I restored it. I also added instances of Eq, Ord, Data, Typeable, Read, Show, Num, Integral, Real, Enum, and Ix, in case someone wants to use Nat1 at the term level.

It seems GHC is on a mission to obsolete my packages :-). First type-eq, now data-nat. But that's good, these things should exist in a central place.

The name `Nat1` seems a bit unfortunate. If we ever get a term-level `Natural` type to complement `Integer`, will that and the current `Nat` be different concepts (in which case with `Nat1`, there would be 3)? If they would be the same, i.e. only 2 different types, I think calling one of them `Nat` and the other `Natural` would be nice. If all 3 would be different things then I don't have better ideas.

There's a few useful auxiliary definitions (`nat`, `foldNat`, `unfoldNat`, `infinity`, `diff`) in my version which might be worth lifting:

http://hackage.haskell.org/package/data-nat-0.1.2/docs/Data-Nat.html

I also have a `Bounded` instance with `maxBound = infinity`, which I added mostly for kicks, and I'm genuinely not sure whether it meets the implicit expectations for a `Bounded` instance. `n < infinity` will be `True` for any `n` that's not `infinity`, and similarly `[n..infinity]` will be an infinite list (which seems reasonable), but any comparison involving two infinities will be bottom.


--
Your ship was destroyed in a monadic eruption.