But it seems to me like the whole point of using "newtype" is because you *don't* want your new type to be used everywhere that the old type can be used; otherwise you would just use "type" to create an alias. The only convincing exception I have heard to this (as you helpfully explained to me) is that one might be forced to use newtype to make a piece of code use a different instance declaration for a type. In particular, I am not sure what you are getting at with your example, since one :: Integer one = 1 works just as well. Why did you want to define a new type? Cheers, Greg On Dec 2, 2009, at 6:40 PM, Greg Fitzgerald wrote:
That suggests that the feature we'd really like is a way to declare that we want a type in a context to act as if it had a different instance declaration for a given typeclass, without having to go through newtype.
I'd want implicit type coercion from subtypes, so that you wouldn't need an infinite hierarchy of nested typeclasses to implement the following for all integers:
data One = One
-- Somehow tell GHC that One is a subset of Integer (without implementing Num) oneToInteger :: One -> Integer oneToInteger One = 1
One + One == (2 :: Integer)
Seems like something Agda could handle.
-Greg