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

[Oleg Grenrus]

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#injective-type-families

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.