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?