I've made the changes that I see fit, regarding http://ghc.haskell.org/trac/ghc/wiki/TypeLevelNamingIssues As I wanted a little feedback before pushing, the changes are at my fork of the base repo, at https://github.com/goldfirere/packages-base Here is what I've done: - The function with type (a :~: b) -> a -> b is now named castWith. - There is a new function (in Data.Type.Equality) gcastWith :: (a :~: b) -> ((a ~ b) => r) -> r. Type inference for this function works well. - 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. - EqualityType's method is now maybeEquality (instead of equalsT). CoercionType's method is now maybeCoercion (instead of coercionT). - I've added (==) as type-level Boolean equality to Data.Type.Equality. Instead of the fully-general poly-kinded definition, my experience has shown that a recursive definition of Boolean equality over algebraic types is superior to the general poly-kinded one. So, (==) is an open type family, with many closed type family specializations over certain types (including * and (k1 -> k2), as well as promoted versions of the base datatypes). - 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. Questions for you all: - Better name ideas for EqualityType/maybeEquality and CoercionType/maybeCoercion? I'm very unsatisfied. - OK to add (==)? There is a naming tension with the (<=) and (<=?) operators in TypeLits. Following the convention of appending ? for Boolean operators, (==) should be spelled (~?). But, I don't like that terribly much, for aesthetic more than practical reasons. Please disagree with me or suggest a more unified structure. (Maybe the constraint (<=) should really be (<~)... but I think that's *very* confusing, as it looks like an arrow!) - OK to add Nat1? Comments on the instances? Thanks, Richard