Could not deduce: `CLog 2 (n * 2)` ~ `CLog 2 n + 1`

[martijnbastiaan]

This should hold for all n*, but the plugin doesn't infer it.

*For n ~ 0 the answer is undefined in both cases

[martijnbastiaan]

A workaround would be to define:

import Data.Type.Equality ((:~:)(Refl))
import Unsafe.Coerce (unsafeCoerce)

clog2axiom :: (CLog 2 (n * 2)) :~: ((CLog 2 n) + 1)
clog2axiom = unsafeCoerce Refl

And use it like:

coerceIndices :: forall n. (KnownNat n, 1 <= n) => Index (n*2) -> (Index n, Bool)
coerceIndices = case clog2axiom @n of Refl -> bitCoerce

[martijnbastiaan]

@rowanG077 mentioned that we should be able to add this derivation by patching:

ghc-typelits-extra/src/GHC/TypeLits/Extra/Solver/Operations.hs

Line 191 in fe80881

mergeCLog :: ExtraOp -> ExtraOp -> Maybe NormaliseResult

[martijnbastiaan]

Finally, some "proof" that this equation holds:

>>> import Clash.Util (clogBase)
>>> import Test.QuickCheck (quickCheck, withMaxSuccess)
>>> clog2 = clogBase 2
>>> prop_eq n = (clog2 (n*2)) == (succ <$> clog2 n)
>>> quickCheck (withMaxSuccess 1000000 prop_eq)
+++ OK, passed 1000000 tests.