
On Mon, Oct 21, 2013 at 6:04 AM, Richard Eisenberg
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'd be worried about type inference with partial application and reversed parameters. The values of a and b can only be gleaned from the equality witness, so I would think that delaying that parameter would cause some havoc. Is that not what you've seen?
I use the alternate order in (\\) for the constraints package and have had no issues with it after "using it in anger" for a couple of years now. - 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`?
Out of those alternatives I rather prefer TestEquality and TestCoercible over randomly introducing unrelated abbreviations. =/ -Edward