idris is it possible to restrict function output by interface?

It might be possible to use auto and %hint to reduce boilerplate.

interface Convertible c where
    target : c -> Type
    p : (item : c) -> Convertible (target item)
    convert: (item: c) -> target item

implementation Convertible () where
    -- This is allowed, since we're implementing Convertible for unit type right now.
    target _ = ()
    convert _ = ()
    p _ = %implementation

implementation Convertible String where
    -- This is allowed, since Convertible is already implemented for unit type.
    target _ = ()
    convert _ = ()
    p _ = %implementation


data Wrapper : Type -> Type where
    -- The type should be restricted here, otherwise we'll have signature clashes
    -- fromInteger here is only as an example, but the real-life case is similar
    fromInteger : (Convertible c) => c -> Wrapper c
    -- This works, but is extremely unergonomic, so I'd like to avoid it:
    -- fromInteger : c -> Wrapper c

-- ...but with the restriction on data type, we can't implement this:
implementation (Convertible c) => Convertible (Wrapper c) where
    target (fromInteger inner) = Wrapper (target inner)
    convert (fromInteger inner) = let _ = p inner in fromInteger (convert inner)
    p (fromInteger inner) = let _ = p inner in %implementation

implementation Convertible Double where
    -- This doesn't make sense, since Integer isn't Convertible.
    target _ = Integer
    convert item = cast $ floor item
    p _ = %implementation

fails with Can't find implementation for Convertible Integer