You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
We don't always specify all constraints that could be specified on Nat in our functions. For instance, riseEvery requires an SNat larger than zero, but it also accepts zero, which causes a runtime error. Usually it's not a problem because we can pass a more-constrained argument to a less-constrained function.
But when we're talking about the argument of a higher-order function (using higher-rank type), the reverse is true. We have
smap :: forall k a b. KnownNat k => (forall l. SNat l -> a -> b) -> Vec k a -> Vec k b
(same for dfold, dtfold, vfold). This precludes using functions that restrict l (ell) to be smaller than k, like at, take, drop, select, splitAt, etc. These all require l be smaller than k, and GHC/CλaSH can't prove that this is the case.
We don't always specify all constraints that could be specified on
Nat
in our functions. For instance,riseEvery
requires anSNat
larger than zero, but it also accepts zero, which causes a runtime error. Usually it's not a problem because we can pass a more-constrained argument to a less-constrained function.But when we're talking about the argument of a higher-order function (using higher-rank type), the reverse is true. We have
(same for
dfold
,dtfold
,vfold
). This precludes using functions that restrictl
(ell) to be smaller thank
, likeat
,take
,drop
,select
,splitAt
, etc. These all requirel
be smaller thank
, and GHC/CλaSH can't prove that this is the case.This lead to this Google Group thread.
We should add constraints on these function arguments to allow using constrained functions.
The text was updated successfully, but these errors were encountered: