I assume you want to have a complete pattern synonym for non-zero Vektors? The problem is the same as if you would try to write a matching function: match :: Vektor (1 + length) value -> (value, Vektor length value) match (Sektor x xs) = (x, xs) It fails similarly Foo.hs:22:27: error:     • Could not deduce: length1 ~ length       from the context: (1 + length) ~ (1 + length1)         bound by a pattern with constructor:                    Sektor :: forall value (length :: Natural).                              value -> Vektor length value -> Vektor (1 + length) value,                  in an equation for ‘match’         at Foo.hs:22:8-18       Expected: Vektor length value         Actual: Vektor length1 value       ‘length1’ is a rigid type variable bound by         a pattern with constructor:           Sektor :: forall value (length :: Natural).                     value -> Vektor length value -> Vektor (1 + length) value,         in an equation for ‘match’         at Foo.hs:22:8-18       ‘length’ is a rigid type variable bound by         the type signature for:           match :: forall (length :: Natural) value.                    Vektor (1 + length) value -> (value, Vektor length value)         at Foo.hs:21:1-66     • In the expression: xs       In the expression: (x, xs)       In an equation for ‘match’: match (Sektor x xs) = (x, xs)     • Relevant bindings include         xs :: Vektor length1 value (bound at Foo.hs:22:17)         match :: Vektor (1 + length) value -> (value, Vektor length value)           (bound at Foo.hs:22:1) And the reason is that GHC doesn't know that partially applied `+` is injective. It's type family (m :: Nat) + (n :: Nat) :: Nat not type family (m :: Nat) + (n :: Nat) = (p :: Nat) | p m -> n, p n -> m https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/type_families.html#i... But maybe it could, as it's a magic type-family after all. - Oleg On 18.6.2022 22.55, Ignat Insarov wrote:

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? _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.