Idris: is it possible to restrict function output by interface?

Question

I'm trying to make an interface for values which can be (in some sense, not relevant to the question) converted into other values. Currently, it is defined as following:

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

So, when implementing this interface, one must provide both the conversion and the target type, which can possible depend on the value being converted.

In real life, it will be natural for every conversion target to be convertible too - for example:

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

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

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

Furthermore, any convertible value can be "wrapped" into provided type, which will be convertible too. However, if the conversion target is possible not convertible itself, this leads to the following problem:

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) = fromInteger (convert inner)

Error:

test.idr:32:35-61:
   |
32 |     convert (fromInteger inner) = fromInteger (convert inner)
   |                                   ~~~~~~~~~~~~~~~~~~~~~~~~~~~
When checking right hand side of Main.Main.Wrapper c implementation of Main.Convertible, method convert with expected type
        Main.Wrapper c implementation of Main.Convertible, method target c constraint (fromInteger inner)

Can't find implementation for Convertible (target inner)

So, is it possible to make Idris understand (and check), that target c is always Convertible, as long as c is Convertible?

Answer 1

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