Issues Board

## clash-lang/clash-compiler

• #867
(This is all with Clash 1.0.0) I think the following program should typecheck: ``` import Clash.Prelude foo :: (1 <= n, KnownNat n) => Vec n a -> Vec n a foo = id bar :: (KnownNat n) => Vec n a -> Vec n a bar Nil = Nil bar xs@(_ :> _) = foo xs ``` but it doesn't, because: ``` /tmp/a.hs:16:10: error: • Couldn't match type ‘n’ with ‘n0 + 1’ ‘n’ is a rigid type variable bound by the type signature for: bar :: forall (n :: Nat) a. KnownNat n => Vec n a -> Vec n a at /tmp/a.hs:14:1-42 Expected type: Vec n a Actual type: Vec (n0 + 1) a • In the pattern: _ :> _ In an equation for ‘bar2’: bar2 xs@(_ :> _) = foo xs /tmp/a.hs:16:20: error: • Couldn't match type ‘1 <=? n’ with ‘'True’ arising from a use of ‘foo’ • In the expression: foo xs In an equation for ‘bar’: bar xs@(_ :> _) = foo xs ``` The same code works when using `Cons` directly: ``` bar1 :: (KnownNat n) => Vec n a -> Vec n a bar1 Nil = Nil bar1 xs@Cons{} = foo xs ``` and moreover, it works if I define a `(:>)`-like pattern synonym, but using `Cons` directly instead of `head` and `tail`: ``` pattern x ::> xs = Cons x xs bar2 :: (KnownNat n) => Vec n a -> Vec n a bar2 Nil = Nil bar2 xs@(_ ::> _) = foo xs ```