`(:>)` vs. `Cons`

[kleinreact]

I recognized that

mymap :: (a -> b) -> Vec n a -> Vec n b
mymap _ Nil           = Nil
mymap f (x `Cons` xr) = f x `Cons` mymap f xr

type-checks, but

mymap' :: (a -> b) -> Vec n a -> Vec n b
mymap' _ Nil       = Nil
mymap' f (x :> xr) = f x :> mymap' f xr

does not (GHC 9.10):

<interactive>:4:11: error: [GHC-25897]
    • Couldn't match type ‘n’ with ‘n0 + 1’
      Expected: Vec n a
        Actual: Vec (n0 + 1) a
      ‘n’ is a rigid type variable bound by
        the type signature for:
          mymap' :: forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
        at <interactive>:2:1-40
    • In the pattern: x :> xr
      In an equation for ‘mymap'’:
          mymap' f (x :> xr) = f x :> mymap' f xr
    • Relevant bindings include
        mymap' :: (a -> b) -> Vec n a -> Vec n b
          (bound at <interactive>:3:1)

This is kind of annoying, as up to my knowledge most people use (:>) and are not much aware about Cons. A little research revealed that there already was a discussion about this in the past (#170, #966, #867, #943), but that discussion was within the scope of some old GHC (we don't even support any more). Thus, it might be that these past considerations need some re-evaluation first.

My primary question would be: "Do we still need both: Cons and (:>) these days?"

---

A possible solution would be to update the (:>) synonym to

pattern (:>) ::
  forall n a. () =>
  forall m. n ~ m + 1 =>
  a -> Vec m a -> Vec n a
pattern (:>) x xs = Cons x xs

which elides the aforementioned type-mismatch (and yes, the explicit quantifier split is necessary here). However, this change also introduces a different quantifier alternation than Cons, which might be non-desirable.

Another solution (my favorite) would be to just rename Cons to (:>) and to drop Cons, as I could not find any counterexample, where this solution would cause any trouble, i.e., where using the constructor directly breaks things.

[DigitalBrains1]

Relevant: #2716

[martijnbastiaan]

So after reading the history I think there are three open questions:

While it improves type inference in some cases (see issue #867), it worsens it in others. (See testsuite changes in
#943.)

I wonder if this comment was on:

middleL :: Vec (n + 2) a -> Vec n a
middleL ((_ :> xs) :< _) = xs
+ middleL _ = error "middleL: unreachable"

middleR :: Vec (n + 2) a -> Vec n a
middleR (_ :> (xs :< _)) = xs
+ middleR _ = error "middleR: unreachable"

And whether it is fixed by #2716? It also wouldn't really make it a question of type inference, but exhaustiveness checking.

GADT don't permit lazy patterns, which seems to be widely used in existing code bases.

Note that these "existing code bases" were client ones. This one probably remains unsolved?

Using the Vec constructor can trigger a bug in GHC stochastically making compilation super slow. Having it as a default is therefore not ideal for now.

This one is a real hoot.. If we can't find any evidence for it in clash-testsuite/bittide/other important projects I think we can mark this "solved".

[kleinreact]

I wonder if this comment was on:

middleL :: Vec (n + 2) a -> Vec n a
middleL ((_ :> xs) :< _) = xs
+ middleL _ = error "middleL: unreachable"

middleR :: Vec (n + 2) a -> Vec n a
middleR (_ :> (xs :< _)) = xs
+ middleR _ = error "middleR: unreachable"

And whether it is fixed by #2716? It also wouldn't really make it a question of type inference, but exhaustiveness checking.

#2716 is a definite improvement, as mymap' would be marked as incomplete without the pragma.

The middleL and middleR examples confuse me, as they are either both incomplete (without the error case) or complete (with the error case). Up to my knowledge, GHC cannot exclude the unreachable cases when using equality constraints over type level naturals. We'd either need to use inequality constraints or peano numbers (like in the vec package, if we wanna different behavior in that regard.

I don't see an issue with the completeness here any more, but type inference not being able to resolve the type family application properly.

Fortunately, I figured that we can enforce the same quantifier order as for Cons, if we hide the n parameter above, e.g.,

pattern (:>) ::
  forall {n} a. () =>
  forall m. n ~ m + 1 =>
  a -> Vec m a -> Vec n a
pattern (:>) x xs = Cons x xs

I'll give this a shot in #2914. Let's see what it breaks.

[martijnbastiaan]

The middleL and middleR examples confuse me, as they are either both incomplete (without the error case) or complete (with the error case). Up to my knowledge, GHC cannot exclude the unreachable cases when using equality constraints over type level naturals. We'd either need to use inequality constraints or peano numbers (like in the vec package, if we wanna different behavior in that regard.

I think what's happening here is that the pattern is implemented in terms of head and tail, which have the nice property of "always succeeding", as long as you supply it the right types. So either you get a type error or it is complete. In this case the type checker plugins step in and figure out that n+2 ~ (n+1)+1.

[kleinreact]

I think what's happening here is that the pattern is implemented in terms of head and tail, which have the nice property of "always succeeding", as long as you supply it the right types. So either you get a type error or it is complete. In this case the type checker plugins step in and figure out that n+2 ~ (n+1)+1.

Sry, but I don't get your point 🤔.

middleL :: Vec (n + 2) a -> Vec n a
middleL ((_ :> xs) :< _) = xs

gives me on <clashi, 1.8.2, GHC 9.10, not containing #2716 (as far as I can see)>

    Pattern match(es) are non-exhaustive
    In an equation for ‘middleL’:
        Patterns of type ‘Vec (n + 2) a’ not matched:
            Nil
            Cons _ _
            :< Nil _
            :< (Cons _ _) _
   |
27 | middleL ((_ :> xs) :< _) = xs
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

and <clashi, master, GHC 9.10> produces

    Pattern match(es) are non-exhaustive
    In an equation for ‘middleL’:
        Patterns of type ‘Vec (n + 2) a’ not matched:
            Nil
            Cons _ _
            :< Nil _
   |
27 | middleL ((_ :> xs) :< _) = xs
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

while

middleL :: Vec (n + 2) a -> Vec n a
middleL ((_ :> xs) :< _) = xs
middleL _ = error "middleL: unreachable"

is complete by definition due to the any-pattern matching _-case (hence, clearly there won't be any warnings).

middleL :: Vec (n + 2) a -> Vec n a
middleL ((_ `Cons` xs) :< _) = xs

also leads to

    Pattern match(es) are non-exhaustive
    In an equation for ‘middleL’:
        Patterns of type ‘Vec (n + 2) a’ not matched:
            Nil
            Cons _ _
            :< Nil _
   |
27 | middleL ((_ `Cons` xs) :< _) = xs
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

So yes, the pragma improves the situation here, but middleL is kind of a strange example, because it still comes with some missing patterns without the _-case. Maybe I am just confused by that.

The plugin should deduce exactly the same in all of those cases, so I don't see any improvement there either.

[martijnbastiaan]

Yeah, scrap my comment. I didn't realize we used {-# OPTIONS_GHC -fno-warn-incomplete-patterns -#}. In that case, I still don't know what I meant with:

While it improves type inference in some cases (see issue #867), it worsens it in others. (See testsuite changes in #943.)

[kleinreact]

clash-compiler/clash-prelude/src/Clash/Sized/Vector.hs

Line 678 in 952fd85

-- >>> let g (a :> b :> (_ :< y :< x)) = a + b + x + y

seems to be a good hint, as

clashi> g (a :> b :> (_ :< y :< x)) = a + b + x + y

is accepted, while

clashi> g (Cons a (Cons b (_ :< y :< x))) = a + b + x + y

is not:

<interactive>:5:38: error: [GHC-25897]
    • Could not deduce ‘b ~ p’
      from the context: a ~ (n + 1)
        bound by a pattern with constructor:
                   Cons :: forall b (n :: Natural). b -> Vec n b -> Vec (n + 1) b,
                 in an equation for ‘g’
        at <interactive>:5:5-33
      or from: n ~ (n1 + 1)
        bound by a pattern with constructor:
                   Cons :: forall b (n :: Natural). b -> Vec n b -> Vec (n + 1) b,
                 in an equation for ‘g’
        at <interactive>:5:13-32
      ‘b’ is a rigid type variable bound by
        the inferred type of g :: Num b => Vec a b -> p
        at <interactive>:5:2-50
      ‘p’ is a rigid type variable bound by
        the inferred type of g :: Num b => Vec a b -> p
        at <interactive>:5:2-50
    • In the expression: a + b + x + y
      In an equation for ‘g’:
          g (Cons a (Cons b (_ :< y :< x))) = a + b + x + y
    • Relevant bindings include
        x :: b (bound at <interactive>:5:31)
        y :: b (bound at <interactive>:5:26)
        b :: b (bound at <interactive>:5:18)
        a :: b (bound at <interactive>:5:10)
        g :: Vec a b -> p (bound at <interactive>:5:2)
    Suggested fix: Consider giving ‘g’ a type signature

I'll have to give it a closer look to understand what's going on here.

[kleinreact]

Alright, I got some simplified insights on this.

The following type-checks for cop = Cons, but not for cop = (:>):

vid0 :: forall n a. Vec n a -> Vec n a
vid0 Nil        = Nil
vid0 (cop x xr) = Cons x (vid0 xr)

However, in converse, the following type-checks for cop = (:>), but not for cop = Cons:

vid1 :: forall n m a. (m ~ (n - 1), 1 <= n) => Vec n a -> Vec n a
vid1 (Cons t Nil) = Cons t Nil
vid1 (cop t xs)  = Cons t (vid1 @(n - 1) xs)

The latter example is a bit strange though, because it neither type checks for Cons nor (:>), if dropping the non-utilized (m ~ (n - 1) constraint. It looks to me like the plugin just somehow gets lucky here to make this work, but it'd be fine if we wouldn't rely on that.

This is the only limitation we currently run into with #2914.

[kleinreact]

It turns out that the currently used type signature and definition of the pattern synonym only leads to some code passing the type check without some type annotations or explicit constructor pattern matches, which is very dependent on the particular setup of use. Hence, using the pattern (as it is defined currently) is more designated to lead to unexpected behavior than using the constructor directly.

I opened #2914, which proposes the enhancement to resolve the situation by aligning both signatures and preparing the code for getting rid of the Cons name eventually.

Please let me now, if there is still more infoneeded at this point.