`CLog n k` gets stuck even if `n` and `k` are known

[gergoerdi]

{-# LANGUAGE GADTs, DataKinds, TypeApplications, TypeOperators, KindSignatures #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver #-}

import GHC.TypeLits
import GHC.TypeLits.Extra

data SNat (n :: Nat) where
    SNat :: KnownNat n => SNat n

foo :: (1 <= n) => SNat n -> SNat (CLog 2 n)
foo SNat = undefined

mask
    :: (KnownNat k, KnownNat n)
    => SNat (n + k)
    -> SNat k
    -> SNat (n + k)
mask = undefined

main :: IO ()
main = undefined $ mask (SNat @16) $ foo (SNat @0x1000)

This results in the following error message:

      Expected type: SNat (n0 + CLog 2 4096)
        Actual type: SNat 16
      The type variable ‘n0’ is ambiguous

I see no reason this shouldn't simplify to SNat (n0 + 12) ~ SNat 16 which could then be solved as n0 ~ 4 .

[christiaanb]

I've been unable to reproduce this bug locally. The error that I get is:

christiaan@DESKTOP-O5QKI8I:~/ghc-typelits-extra$ ghci Test.hs
GHCi, version 8.10.1: https://www.haskell.org/ghc/  :? for help
Loaded package environment from /home/christiaan/ghc-typelits-extra/.ghc.environment.x86_64-linux-8.10.1
[1 of 1] Compiling Main             ( Test.hs, interpreted )

Test.hs:22:20: error:
    • No instance for (KnownNat (CLog 2 4096))
        arising from a use of ‘mask’
    • In the expression: mask (SNat @16)
      In the second argument of ‘($)’, namely
        ‘mask (SNat @16) $ foo (SNat @4096)’
      In the expression: undefined $ mask (SNat @16) $ foo (SNat @4096)
   |
22 | main = undefined $ mask (SNat @16) $ foo (SNat @0x1000)
   |   

As you can see, I simply copied the content into Test.hs and run ghci Test.hs (with a .ghc.environment file from cabal build --write-ghc-environment-files=always). These are the versions of the plugins in scope:

package-id ghc-typelits-knownnat-0.7.3-105b9862419288e16d8e91c03e49650fbdd869ee7fee2f625cd66c0dcf197b67
package-id ghc-typelits-natnormalise-0.7.2-3feb4a64edd6c3b07cbd78c52b624e63354bead677f7ae9fa29dd8200baf82c3
package-id ghc-typelits-extra-0.4.1-inplace

And I can get it to compile by simply adding;

{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}

I've tested with GHC 8.6, 8.8 and 8.10

Could you give some more details on your environment which would help me reproduce the bug?

[christiaanb]

I think this might be solved by https://github.com/clash-lang/ghc-typelits-extra/commit/9e7eb8a265e888f832da6af9ab121864205432ed

Which is included in the 0.4 release of ghc-typelits-extra. This assumption is based on the fact that I got the same error as reported in an environment with the 0.3.3 release of ghc-typelits-extra.

[gergoerdi]

I'm using 0.4. I've just tried with both 0.4 and 0.4.1, and it seems the fix was somewhere in between: 0.4 gives the above error, whereas 0.4.1 doesn't (and then, as you say, needs the KnownNat solver but that's not a problem, that's an artifact of making my test case as small as possible).

[gergoerdi]

So I guess this can be solved as fixed by 0.4.1.