very confused, as usual

gistfile1.idr

import Data.Bits

trim : Bits (1 + n) -> Bits n
trim b = truncate b

BoundedInt : Integer -> Nat -> Type
BoundedInt min max = (x : Integer ** so (min <= x && x < toIntegerNat max))

postulate bounds : (x : Integer) -> so (lower <= x && x < toIntegerNat upper) -> so (lower <= x && 1+2*x < pow 2 upper)

bitsToBI : Bits n -> BoundedInt 0 (pow 2 n)
bitsToBI {n=Z}   _ = (0 ** oh)
bitsToBI {n=S _} b = let (x ** meh) = bitsToBI (trim b)
                     in if (b `and` (intToBits 1)) /= (intToBits 0)
                        then (1 + 2 * x ** flip bounds meh)
                        else (2 * x ** flip bounds meh)

-- 16:45
-- When elaborating right hand side of Main.case block in bitsToBI:
-- When elaborating an application of function Prelude.Basics.flip:
--         Can't unify
--                 (\\x1 => so (Prelude.Classes.Integer instance of Prelude.Classes.Ord, method < (boolElim (intToBool (prim__eqBigInt 0 x1)) (Delay EQ) (Delay (boolElim (intToBool (prim__sltBigInt 0 x1)) (Delay LT) (Delay GT)))) 0 x1 || (intToBool (prim__eqBigInt 0 x1)) && (Prelude.Classes.Integer instance of Prelude.Classes.Ord, method < (boolElim (intToBool (prim__eqBigInt x1 (toIntegerNat (pow 2 _t)))) (Delay EQ) (Delay (boolElim (intToBool (prim__sltBigInt x1 (toIntegerNat (pow 2 _t)))) (Delay LT) (Delay GT)))) x1 (toIntegerNat (pow 2 _t))))) x
--         with
--                 (\\__pi_arg => so (Prelude.Classes.Integer instance of Prelude.Classes.Ord, method < (boolElim (intToBool (prim__eqBigInt lower __pi_arg)) (Delay EQ) (Delay (boolElim (intToBool (prim__sltBigInt lower __pi_arg)) (Delay LT) (Delay GT)))) lower __pi_arg || (intToBool (prim__eqBigInt lower __pi_arg)) && (Prelude.Classes.Integer instance of Prelude.Classes.Ord, method < (boolElim (intToBool (prim__eqBigInt __pi_arg (toIntegerNat upper))) (Delay EQ) (Delay (boolElim (intToBool (prim__sltBigInt __pi_arg (toIntegerNat upper))) (Delay LT) (Delay GT)))) __pi_arg (toIntegerNat upper)))) x1
        
--         Specifically:
--                 Can't unify
--                         Prelude.Classes.Integer instance of Prelude.Classes.Ord, method < (boolElim (intToBool (prim__eqBigInt 0 x)) (Delay EQ) (Delay (boolElim (intToBool (prim__sltBigInt 0 x)) (Delay LT) (Delay GT)))) 0 x || (intToBool (prim__eqBigInt 0 x)) && (Prelude.Classes.Integer instance of Prelude.Classes.Ord, method < (boolElim (intToBool (prim__eqBigInt x (toIntegerNat (pow 2 _t)))) (Delay EQ) (Delay (boolElim (intToBool (prim__sltBigInt x (toIntegerNat (pow 2 _t)))) (Delay LT) (Delay GT)))) x (toIntegerNat (pow 2 _t)))
--                 with
--                         Prelude.Classes.Integer instance of Prelude.Classes.Ord, method < (boolElim (intToBool (prim__eqBigInt lower x1)) (Delay EQ) (Delay (boolElim (intToBool (prim__sltBigInt lower x1)) (Delay LT) (Delay GT)))) lower x1 || (intToBool (prim__eqBigInt lower x1)) && (Prelude.Classes.Integer instance of Prelude.Classes.Ord, method < (boolElim (intToBool (prim__eqBigInt x1 (toIntegerNat upper))) (Delay EQ) (Delay (boolElim (intToBool (prim__sltBigInt x1 (toIntegerNat upper))) (Delay LT) (Delay GT)))) x1 (toIntegerNat upper))