[Haskell-cafe] Implicit newtype unwrapping

[Greg Fitzgerald]

> 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