[Haskell-cafe] A pattern does not admit a type signature.

[Ignat Insarov]

Hello Café!

I cannot understand why the following code does not compile.

```Haskell
{-# LANGUAGE UnicodeSyntax #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternSynonyms #-}

module Arity where

import GHC.TypeNats

data Vektor length value where
  Sektor ∷ value → Vektor length value → Vektor (1 + length) value
  Mektor ∷ Vektor 0 value

pattern (:>) ∷ value → Vektor length value → Vektor (1 + length) value
pattern value :> values = Sektor value values
infixr 5 :>
```

The error:

```
    • Could not deduce: length1 ~ length
      from the context: (1 + length) ~ (1 + length1)
        bound by a pattern with constructor:
                   Sector :: forall value (length :: Natural).
                             value -> Vector length value -> Vector (1
+ length) value,
                 in a pattern synonym declaration
        at Arity.hs:16:27-45
      Expected: Vector length value
        Actual: Vector length1 value
      ‘length1’ is a rigid type variable bound by
        a pattern with constructor:
          Sector :: forall value (length :: Natural).
                    value -> Vector length value -> Vector (1 + length) value,
        in a pattern synonym declaration
        at Arity.hs:16:27-45
      ‘length’ is a rigid type variable bound by
        the signature for pattern synonym ‘:>’
        at Arity.hs:15:16-70
    • In the declaration for pattern synonym ‘:>’
    • Relevant bindings include
        values :: Vector length1 value (bound at Arity.hs:16:40)
   |
16 | pattern value :> values = Sector value values
   |                                        ^^^^^^
```

If I omit the pattern's type signature, the code compiles. What is going on?