Closed axman6 closed 3 months ago
It looks like the tests are failing, but as far as I can tell the errors have nothing to do with my changes.
Can you rebase @axman6? The CI failures are caused by https://github.com/haskell-actions/setup/issues/77, and has been worked around in master
.
Hmm, I had hoped that I could rebase in github, but apparently it just merges the target branch in - hopefully this is still fine.
Ok, I've rebased properly now, we'll see how this goes (though merging in master also didn't pass which is odd).
I've rebased again.. Hopefully the CI errors are now gone. @christiaanb could you give this a look to? To me this looks "obviously correct", but we had some subtleties creeping in with Vec
's patterns before.
https://github.com/clash-lang/clash-compiler/blob/0fe5d49b113e21bb4d35fecd58cc049e668344f8/clash-lib/src/Clash/Normalize/Transformations/Case.hs#L688 will likely not fire on the pattern synonym, meaning Clash won’t be able to unroll recursive functions defined in terms of Nil
and :>
. From that perspective I’d rather the compiler suggests you use Cons
.
Sure, that would be a good reason to remove the patterns entirely, but we've tried before and couldn't for various reasons. So while we're stuck with them, isn't the correct thing to do is add a complete pragma? Or are you saying that that makes things worse somehow?
Or are you saying that that makes things worse somehow?
I guess we're fine, I cannot even get a recursive function to type-check:
module Test where
import Clash.Prelude
myMap :: forall n a b . (a -> b) -> Vec n a -> Vec n b
myMap _ Nil = Nil
myMap f (x :> (xs :: Vec m a)) = f x :> myMap f xs
topEntity :: Vec 3 Int -> Vec 3 Int
topEntity = myMap (+1)
gives:
Test.hs:8:10: error:
• Couldn't match type ‘n’ with ‘m + 1’
Expected: Vec n a
Actual: Vec (m + 1) a
‘n’ is a rigid type variable bound by
the type signature for:
myMap :: forall (n :: Nat) a b. (a -> b) -> Vec n a -> Vec n b
at Test.hs:6:1-54
• When checking that the pattern signature: Vec (m + 1) a
fits the type of its context: Vec n a
In the pattern: (x :> (xs :: Vec m a)) :: Vec (m + 1) a
In an equation for ‘myMap’:
myMap f ((x :> (xs :: Vec m a)) :: Vec (m + 1) a)
= f x :> myMap f xs
• Relevant bindings include
myMap :: (a -> b) -> Vec n a -> Vec n b (bound at Test.hs:7:1)
|
8 | myMap f ((x :> (xs :: Vec m a)) :: Vec (m+1) a) = f x :> myMap f xs
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
So I guess I don't have to worry that Clash won't be able to unroll the recursion.
Thanks for the comment @christiaanb, thanks for the CI fixes @DigitalBrains1. I think we can merge this one.
@kloonbot run_ci 3f4f65a
I was banging my head against some type errors for hours until I decided to use the
Cons
constructor instead of the:>
pattern - hopefully this will save someone else the same pain.Still TODO: