Add COMPLETE pragma for Vec: Nil, (:>)

[axman6]

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:

• Write a changelog entry (see changelog/README.md)
• Check copyright notices are up to date in edited files

[axman6]

It looks like the tests are failing, but as far as I can tell the errors have nothing to do with my changes.

[martijnbastiaan]

Can you rebase @axman6? The CI failures are caused by haskell-actions/setup#77, and has been worked around in master.

[martijnbastiaan]

This does LGTM. Surprising we didn't have this.

[axman6]

Hmm, I had hoped that I could rebase in github, but apparently it just merges the target branch in - hopefully this is still fine.

[axman6]

Ok, I've rebased properly now, we'll see how this goes (though merging in master also didn't pass which is odd).

[martijnbastiaan]

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.

[christiaanb]

clash-compiler/clash-lib/src/Clash/Normalize/Transformations/Case.hs

Line 688 in 0fe5d49

elimExistentials :: HasCallStack => NormRewrite

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.

[martijnbastiaan]

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?

[christiaanb]

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.

[martijnbastiaan]

Thanks for the comment @christiaanb, thanks for the CI fixes @DigitalBrains1. I think we can merge this one.

[DigitalBrains1]

@kloonbot run_ci 3f4f65a