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.