CODEWITHSUNDEEP
idris
joel
joel

Reputation: 7867

Can't resolve indirect interface

I'm having difficulty with indirect interface resolution. I have a set of backend (custom C++) types (e.g. float64) that I capture in Idris with empty types (e.g. F64), and which correspond to Idris builtin types (e.g. Double). I capture the ability to read and write from the backend with an interface

interface BackendRW cpp idr where

For example, I have the implementation

BackendRW F64 Double where

I use this interface to constrain operations on backend types by properties on the Idris types. For example

negate : (Neg idr, BackendRW cpp idr) => cpp -> cpp

But at usage site I'm finding Idris can't resolve ?idr in negate in

x : F64

y : F64
y = -x

There are no other implementations for F64 than that shown above. I get

Can't find an implementation for (Neg ?idr, BackendRW F64 ?idr)

It works if I specify {idr=Double} but that's not practical. I tried to fix this by saying each C++ type corresponds to only one Idris type and using a determining parameter

interface BackendRW cpp idr | cpp where

but that didn't fix it.

Upvotes: 1

Views: 44

Answers (1)

joel
joel

Reputation: 7867

I can use

interface BackendRW cpp idr | cpp where

if I don't ask for both implementations at once

negate : Neg idr => BackendRW cpp idr => cpp -> cpp

which presumably means the type checker is freer to find one implementation then the other rather than both at the same time.

Upvotes: 1

Related Questions