idris - IdrisNet2 で単純なバイナリ データ構造を作成できない

Question

IdrisNet2ライブラリを使用して、いくつかのバイナリ データ構造を定義しようとしています。Idris 0.9.17.1 を使用しており、IdrisNet2 の 262b746c9a2405e43d1de6a48de44cac2fd19932 をコミットしています。1 つの 16 ビット フィールドでパケットを定義しています。

module Main
import IdrisNet.PacketLang
import Data.So

myPacket : PacketLang
myPacket = with PacketLang do
    bits 16

main : IO ()
main = putStrLn "hello"

コンパイラ エラーが発生します。

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

正確には何が問題で、どうすれば修正できますか? 16 が 0 より大きいことをコンパイラに証明する必要があると推測していますが、Idris でこれを行う方法や、なぜこれが必要なのかがわかりません。