Using intermediate type variables prevents deducing (1 <= 2^n)
lmbollen opened this issue · 2 comments
lmbollen commented
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 commented
@lmbollen I will take a look at this tonight. Probably somewhere a substitution is missing.
martijnbastiaan commented
Partially fixes, mr. GitHub :-)