Using intermediate type variables prevents deducing (1 <= 2^n)

[lmbollen]

Using an intermediate type variable in your function and binding it to 2^n prevents the deduction that it is greater or equal to 1.

This reproducer:

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}

module Example.Project where

import Clash.Prelude

works :: forall n . SNat n -> SNat (CLog 2 (2^n))
works SNat = SNat @(CLog 2 (2^n))

fails :: forall a b  . (b ~ (2^a)) => SNat a -> SNat (CLog 2 b)
fails SNat = SNat @(CLog 2 b)

produces the following error:

[1 of 1] Compiling Example.Project  ( src/Example/Project.hs, interpreted )

src/Example/Project.hs:12:14: error:
    Could not deduce: (1 <=? b) ~ 'True arising from a use of ‘SNat’
    from the context: b ~ (2 ^ a)
      bound by the type signature for:
                 fails :: forall (a :: Nat) (b :: Nat).
                          (b ~ (2 ^ a)) =>
                          SNat a -> SNat (CLog 2 b)
      at src/Example/Project.hs:11:1-63
   |
12 | fails SNat = SNat @(CLog 2 b)
   |              ^^^^^^^^^^^^^^^^
Failed, no modules loaded.

[rowanG077]

@lmbollen I will take a look at this tonight. Probably somewhere a substitution is missing.

[martijnbastiaan]

Partially fixes, mr. GitHub :-)