Error with Div/CLog Expression

[paddytheplaster]

Howsagoin,

I'd like to report a bug and ask for some advice.

First the bug. The type checker on my real implementation is working like mad as it needs lots of time (90 sec for one module) and needs so much CPU time that the fan is making over time. I suspect this is triggered by the following bug.

 module Bug where

 import Clash.Prelude

 type K i = ((Div (3^((CLog 3 i) - 1) - 3) 2) * 2 + 3)

 bug :: forall (i :: Nat) (l :: Nat) . (KnownNat i,KnownNat l,l~(K i),l+1<= i) => SNat i -> ( SNat l,SNat i)
 bug i = (SNat,SNat)

 grand :: forall (i :: Nat) (l :: Nat) . (KnownNat i,KnownNat l,l~(K i)) => SNat i -> ( SNat l,SNat i)
 grand i = (SNat,SNat)
 >>> bug d4
* Couldn't match type `(((Div ((3 ^ (CLog 3 4 - 1)) - 3) 2 * 2)
                         + 3)
                        + 1)
                       <=? 4'
                 with 'True
    arising from a use of `bug'

Notice that

   (((Div ((3 ^ (CLog 3 4 - 1)) - 3) 2 * 2) + 3) + 1)
  ~(((Div ((3 ^ (2 - 1)) - 3) 2 * 2) + 3) + 1)
  ~(((Div ((3 ^ 1) - 3) 2 * 2) + 3) + 1)
  ~(((Div (3 - 3) 2 * 2) + 3) + 1)
  ~(((Div 0 2 * 2) + 3) + 1)
  ~(((0 * 2) + 3) + 1)
  ~((0 + 3) + 1)
  ~(3+1)
  ~4 <= 4

Interestingly, we have

>>>grand d4
(d3,d4)

which is the correct equivalent of (l,i) and which satisfies the omitted constraint l+1<=i. I may very well be that the simplifier on its own works properly.

The advice I'm looking for is triggered by the need for a proper build environment, which only recompiles files if they or their dependants have changed.

If anybody can give some pointer to a simple Haskell build tool, which doesn't need hours to install/configure, and can be used out of the box then that'd be much appreciated.

Regards/TIA,

Paddy

[alex-mckenna]

I'm not sure what you use to build currently, most Haskell users tend to use cabal or stack which only recompile files when necessary. Of the two I would recommend cabal if you're not on Windows, stack if you are (YMMV).

As for the bug, I think maybe someone who knows more about TC plugins is needed (paging @martijnbastiaan)

[martijnbastiaan]

Nice one @paddytheplaster . I've managed to reduce it to:

module Bug where

import Clash.Prelude

bug ::
  ( ((CLog 3 1) + 1) <= 1 ) =>
  ()
bug = ()

x :: ()
x = bug

edit: slightly smaller example

Let's see what the type checkers think..

Edit: interestingly, trying it with CLog 2 1 does make it pass! Even though:

Prelude> ceiling (logBase 3 1)
0
Prelude> ceiling (logBase 2 1)
0

[rowanG077]

@martijnbastiaan The problem is that ghc-typelits-natnormalise reports the constraint as unsolveable.

tcPluginSolve start ghc-typelits-natnormalise
  given   = []
  derived = []
  wanted  = [[WD] hole{co_aioq} {2}:: ((CLog 3 1 + 1) <=? 1)
                                      GHC.Prim.~# 'True (CNonCanonical)]
simplifyNats
  [(Right ([WD] hole{co_aioq} {2}:: ((CLog 3 1 + 1) <=? 1)
                                    GHC.Prim.~# 'True (CNonCanonical),
           (1 + CLog 3 1, 1, True)),
    [])]
unifyNats(ineq) results
  ([WD] hole{co_aioq} {2}:: ((CLog 3 1 + 1) <=? 1)
                            GHC.Prim.~# 'True (CNonCanonical),
   (1 + CLog 3 1, 1, True),
   -1 * CLog 3 1,
   [])
normalised
  Impossible Right ([WD] hole{co_aioq} {2}:: ((CLog 3 1 + 1) <=? 1)
                                             GHC.Prim.~# 'True (CNonCanonical),
                    (1 + CLog 3 1, 1, True))
tcPluginSolve contradiction ghc-typelits-natnormalise
  bad = [[WD] hole{co_aioq} {2}:: ((CLog 3 1 + 1) <=? 1)
                                  GHC.Prim.~# 'True (CNonCanonical)]

[martijnbastiaan]

Yeah.. I wonder what's up with that -1?

[rowanG077]

I can take a look why this is tonight if you want to @martijnbastiaan.

[christiaanb]

There's a subtraction in the original expression, and we represent that by multiplying with -1.

[martijnbastiaan]

I don't think that's it. I see it for

bug :: (((CLog 3 1) + 1) <= 1) => ()
bug = ()

too

[martijnbastiaan]

@rowanG077 Sure :). Thanks!

[christiaanb]

Ah... we check whether a <= b by checking whether 0 <= b - a

[paddytheplaster]

I'm not sure what you use to build currently, most Haskell users tend to use cabal or stack which only recompile files when necessary. Of the two I would recommend cabal if you're not on Windows, stack if you are (YMMV).

As for the bug, I think maybe someone who knows more about TC plugins is needed (paging @martijnbastiaan) Hi Alex,

For type-check compiling (no object file creation, no synthesis)I have a source directory, './src', which contains all my source files. I then compile with a script which basically sets some project specific flags and compiles a source file. The compilation basically uses the following

 #!/bin/bash
 OPT="-O0"
 SRC=./src
 if [ ${#} -ne 1 ]; then
     exit 1
 else
     SOURCE=${1}
 fi
 clash -i${SRC} -fno-code -fclash-no-cache ${OPT} ${SOURCE}

I'll have a look at 'cabal' when I have some more time.

Thanks again,

Paddy

[paddytheplaster]

@martijnbastiaan The problem is that ghc-typelits-natnormalise reports the constraint as unsolveable.

tcPluginSolve start ghc-typelits-natnormalise
  given   = []
  derived = []
  wanted  = [[WD] hole{co_aioq} {2}:: ((CLog 3 1 + 1) <=? 1)
                                      GHC.Prim.~# 'True (CNonCanonical)]
simplifyNats
  [(Right ([WD] hole{co_aioq} {2}:: ((CLog 3 1 + 1) <=? 1)
                                    GHC.Prim.~# 'True (CNonCanonical),
           (1 + CLog 3 1, 1, True)),
    [])]
unifyNats(ineq) results
  ([WD] hole{co_aioq} {2}:: ((CLog 3 1 + 1) <=? 1)
                            GHC.Prim.~# 'True (CNonCanonical),
   (1 + CLog 3 1, 1, True),
   -1 * CLog 3 1,
   [])
normalised
  Impossible Right ([WD] hole{co_aioq} {2}:: ((CLog 3 1 + 1) <=? 1)
                                             GHC.Prim.~# 'True (CNonCanonical),
                    (1 + CLog 3 1, 1, True))
tcPluginSolve contradiction ghc-typelits-natnormalise
  bad = [[WD] hole{co_aioq} {2}:: ((CLog 3 1 + 1) <=? 1)
                                  GHC.Prim.~# 'True (CNonCanonical)]

Thanks Rowan.

Could you say a bit more about the tool you're using, please? If not, no worries.

Regards,

Paddy

[rowanG077]

@paddytheplaster Sure it's a GHC flag that enables tracing of the type checker. You can enable it with the -ddump-tc-trace flag.

[paddytheplaster]

@paddytheplaster Sure it's a GHC flag that enables tracing of the type checker. You can enable it with the -ddump-tc-trace flag.

Many thanks.

[alex-mckenna]

@paddytheplaster A no-fuss way to manage GHC / cabal installations is ghcup. We also have the clash starter project which is a useful starting point for making clash projects with cabal or stack

[paddytheplaster]

Does anybody have an idea how long it is going to take (approximately) for the pull request to be merged?

(I'm stuck...)

[basile-henry]

@paddytheplaster I think one issue that you're having is the clash or even the type checker plugins can't actually solve the CLog for you. But you can help it, if you just add the constraint CLog 3 4 ~ 2 then it'll be able to solve it:

> :set -XPartialTypeSignatures
> bug d4 :: (CLog 3 4 ~ 2) => _

<interactive>:34:29: warning: [-Wpartial-type-signatures]
    • Found type wildcard ‘_’ standing for ‘(SNat 3, SNat 4)’
    • In an expression type signature: (CLog 3 4 ~ 2) => _
      In the expression: bug d4 :: (CLog 3 4 ~ 2) => _
      In an equation for ‘it’: it = bug d4 :: (CLog 3 4 ~ 2) => _
    • Relevant bindings include
        it :: (SNat 3, SNat 4) (bound at <interactive>:34:1)

<interactive>:34:29: warning: [-Wpartial-type-signatures]
    • Found type wildcard ‘_’ standing for ‘(SNat 3, SNat 4)’
    • In an expression type signature: (CLog 3 4 ~ 2) => _
      In the expression: bug d4 :: (CLog 3 4 ~ 2) => _
      In an equation for ‘it’: it = bug d4 :: (CLog 3 4 ~ 2) => _
    • Relevant bindings include
        it :: (SNat 3, SNat 4) (bound at <interactive>:34:1)
(d3,d4)

Providing these extra redundant constraint is not always easy to do in complicated expressions. But you can use something like withDict to make it a bit easier.

Hope that helps! :smile:

[paddytheplaster]

CLog 3 4 ~ 2

Thanks Basile.

It's a good idea. I'm testing the relevant part of the code and I'm changing the constants all the time. Also my code is a bit more complex. I must now have a look at withDict.

Regards,

Paddy

[basile-henry]

@paddytheplaster You can write several constraints like this even if they don't end up being used: (CLog 3 4 ~ 2, CLog 2 64 ~ 6).

I'm changing the constants all the time

Surely there is one place towards the top of the project where types are given monomorphic values? That would be the best place to put these constraints to help the type checker. Make sure you're doing the correct maths though, otherwise type errors will get confusing really quickly! :sweat_smile:

[paddytheplaster]

@paddytheplaster You can write several constraints like this even if they don't end up being used: (CLog 3 4 ~ 2, CLog 2 64 ~ 6).

I'm changing the constants all the time

Surely there is one place towards the top of the project where types are given monomorphic values? That would be the best place to put these constraints to help the type checker. Make sure you're doing the correct maths though, otherwise type errors will get confusing really quickly!

Thanks. That worked, which means I can do some more testing. Unfortunately, I now have to add constraints like ((k-1)+1)~k.

For the moment this is fine but it may indicate something else is wrong.

Regards,

Paddy

[christiaanb]

((k-1)+1) ~ k is only valid for natural numbers when 1 <= k

[paddytheplaster]

((k-1)+1) ~ k is only valid for natural numbers when 1 <= k

I know. I have '2 <= k' among the constraints. I then transform the constraints to eliminate the subtraction.

Regards,

Paddy