Can't create simple binary data structure with IdrisNet2

Question

I am trying to use the IdrisNet2 library to define some binary data structures. I am using Idris 0.9.17.1 and commit 262b746c9a2405e43d1de6a48de44cac2fd19932 of IdrisNet2. I am defining a packet with one 16 bit field:

module Main
import IdrisNet.PacketLang
import Data.So

myPacket : PacketLang
myPacket = with PacketLang do
    bits 16

main : IO ()
main = putStrLn "hello"

I get the compiler error:

 Can't solve goal 
       So (fromInteger 16 > fromInteger 0)

What exactly is the problem and how can I fix it? I am guessing that I need to prove to the compiler that 16 is greater than 0, but I'm not sure how to do this in Idris or why this is necessary.

Answer 1

Sorry about that. A while back we decided to standardize on uppercase for all the types and their constructors; that meant oh and so got renamed to Oh and So. So there was an update to this lib to get it to compile, but it looks like an oh in the default tactics to solve an implicit param got overlooked: https://github.com/SimonJF/IdrisNet2/blob/master/src/IdrisNet/PacketLang.idr#L149 So that tactic would always fail (oh is an undefined reference). You could explicitly pass the value of p there, and that would work: bits 16 {p = Oh}.

But I've submitted a pull request to fix that issue in the lib: https://github.com/SimonJF/IdrisNet2/pull/11