Я кое-как написал такую вот жуткую функцию: setByte :: forall (ix

Question

Я кое-как написал такую вот жуткую функцию: setByte :: forall (ix

:: Nat) (width :: Nat). (9 <= width, ix + 1 <= width `Div` 8, KnownNat ix, KnownNat width) => NatRepr ix -> BV 8 -> BV width -> BV width
setByte ix val bv = Data.BitVector.Sized.or bv shifted
where extendedVal = zext (knownNat @width) val
shifted = shl (knownNat @width) extendedVal $ natVal (Proxy @ix) * 8
И у меня конпелятор ругается что первый аргумент (ix) - не используется.
В доке к NatRepr написано, что это A runtime presentation of a type-level Nat..
В теле функции ix как значение тоже не используется, насколько я понимаю, т.е. runtime presentation здесь действительно не нужен.
Одна если я просто уберу этот аргумент, то ругается could not deduce KnownNat ix0
Кто-нибудь может объяснить как можно убрать NatRepr ix из аргументов или я ошибаюсь в его ненужности?

#haskell #programming #russian

0

16.05.2021