z-snails / idris2-hashable Goto Github PK

It looks to me like Hashable Int etc. are all total but Idris only considers them covering. I've looked at a number of approaches to making them obviously total

In my project, my approach has been to define my own, local wrappers of these implementations. This has the problem that Hashable is in the same namespace as Hashable Int so Idris can't resolve the interface. This could be fixed by either moving the implementations into a separate module from the interface, or marking the library implementations total.

We could do this by either adding assert_total in this library, or using a little refactoring like

export
defaultHashWithSalt : (a -> Bits64) -> Bits64 -> a -> Bits64
defaultHashWithSalt hash salt x = salt `combine` hash x

export total
Hashable Bits8 where
    hash = cast
    hashWithSalt = defaultHashWithSalt hash

although I imagine Hashable a => makes for a nicer API