MD5 doesn't typecheck

[sciadopitys]

When I try to build the package, this error message is displayed. I am currently using Windows 8.

Type checking .\Data\Crypto\Hash\MD5.idr
.\Data\Crypto\Hash\MD5.idr:85:15:
   |
85 | shouldMatch_a : hashMessage dummyMD5 (map (intToBits {n=8}) [97]) = intToBits 0x0cc175b9c0f1b6a831c399e269772661
   |               ^
When checking type of Data.Crypto.Hash.MD5.shouldMatch_a:
Can't find implementation for Hash phTy b outputLength

[sellout]

I get that same error message on OS X. Apologies. I’ll dig into it tomorrow.

[sellout]

Ah, it’s the old “bound as an implicit” error.

[sellout]

The quick fix is to replace dummyMD5 with Data.Crypto.Hash.MD5.dummyMD5 in all of the shouldMatch types.

Or, just comment out the shouldMatch definitions, as they’re just the tests.

But I should have a proper PR tomorrow.

[sciadopitys]

I replaced dummyMD5 with Data.Crypto.Hash.MD5.dummyMD5, but now it is stuck on "Type checking .\Data\Crypto\Hash\MD5.idr"

[sciadopitys]

Are you still working on this?

[sellout]

Sorry – this is a trickier problem – there are a number of places in idris-crypto that have hit performance issues with Fin / Vect / etc. It’ll take some dedicated time to iron out, and I don’t have any at the moment.

[galtys]

Hello,
I tried to build the crypto package but no luck. What are the performance issues with Fin / Vect / etc. Is it solvable? Thanks.