Unable to match Haskell type

Question

I know there are lots of questions on this topic, but I feel that there is something specific about the library that I am using that is giving me the error.

module Test where

import Clash.Prelude

init' :: Vec (n + 1) a -> Vec n a
init' (_ :> Nil) = Nil
init' (x :> (xs:>ys)) = x :> (init' (xs:>ys))

The error I am getting is,

Test.hs:28:14: error:
    • Couldn't match type ‘n’ with ‘n0 + 1’
      ‘n’ is a rigid type variable bound by
        the type signature for:
          init' :: forall (n :: Nat) a. Vec (n + 1) a -> Vec n a
        at Test.hs:26:1-33
      Expected type: Vec n a
        Actual type: Vec (n0 + 1) a
    • In the pattern: xs :> ys
      In the pattern: x :> (xs :> ys)
      In an equation for ‘init'’:
          init' (x :> (xs :> ys)) = x :> (init' (xs :> ys))
    • Relevant bindings include
        init' :: Vec (n + 1) a -> Vec n a (bound at Test.hs:27:1)
   |
28 | init' (x :> (xs:>ys)) = x :> (init' (xs:>ys))
   | 

The definitions from the Clash.Prelude library are

data Vec :: Nat -> * -> * where
  Nil  :: Vec 0 a
  Cons :: a -> Vec n a -> Vec (n + 1) a

pattern (:>) :: a -> Vec n a -> Vec (n + 1) a
pattern (:>) x xs <- ((\ys -> (head ys,tail ys)) -> (x,xs))
  where
    (:>) x xs = Cons x xs

Answer 1

This is a bug/limitation in the Clash library. You'll find that you can't even define something straightforward like:

safeHead :: Vec n a -> Maybe a
safeHead Nil = Nothing
safeHead (x :> _) = Just x

The problem is the definition of the (:>) pattern:

pattern (:>) :: a -> Vec n a -> Vec (n + 1) a
pattern (:>) x xs <- ((\ys -> (head ys,tail ys)) -> (x,xs))
  where
    (:>) x xs = Cons x xs

Despite first appearances, its signature is wrong! Had it instead been given the much simpler (and essentially equivalent) definition:

pattern (:>) x xs = Cons x xs

the inferred type signature would have been:

pattern (:>) :: () => (n ~ n1 + 1) => a -> Vec n1 a -> Vec n a

(which could have been given explicitly, too), and your code would have worked fine (as it would if you were able to use Cons directly in place of (:>).

The unusual form of this signature, with two sets of constraints, is specific to pattern synonyms. The first set of constraints gives a set of "required" constraints, those that are required to be satisfied in order to consider the code using the pattern to be type correct. The second gives the set of "provided" constraints, those that are brought into scope in a case-branch by actually matching the pattern at runtime. You can read more about this in Typing of Pattern Synonyms in the GHC docs.

Unfortunately, the explicit signature used in the library:

pattern (:>) :: a -> Vec n a -> Vec (n + 1) a

is equivalent to:

pattern (:>) :: (n ~ n1 + 1) => () => Vec n1 a -> Vec n a

where the constraint on n and n1 appears in the "required" instead of the "provided" constraint set. This is a big problem!

In this part of the definition of init':

init' (x :> (xs:>ys)) = x :> (init' (xs:>ys))

the first :> requires that the argument being matched by the whole expression x :> (xs :> ys) be a Vec (n + 1) a for some n. Fortunately, it is because of the type signature of init'. Unfortunately, the second :> requires that the argument (which is known to be of type Vec n a) be a Vec (m + 1) a for some m in order to type check. No such constraint is available! It would be the matching by this second :> (as opposed to matching by Nil, as in the previous line) that would PROVIDE such a constraint.

Ultimately, we're stuck in a kind of constraint loop where in order to provide n ~ m + 1 for some m, we need to already have n ~ m + 1 for some m.

So, what can you do? It's hard to say. According to the CHANGELOG for Clash, this bizarre pattern definition was intentionally added so that "pattern matching on :> is now synthesisable by the CLaSH compiler". I don't know what this means, but the Clash maintainer probably does. I would send an email to him or her, point out that the pattern definition for (:>) prevents you from doing simple things like defining safeHead or init', and see if he or she can rewrite the pattern to both allow proper pattern matching and also keep this "synthesisable" business working.