2 Dec
2009
2 Dec
'09
9:40 p.m.
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