Oleg Grenrus oleg.grenrus at iki.fi
Sat Jun 18 20:18:31 UTC 2022

```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

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.
>
> {-# LANGUAGE UnicodeSyntax #-}
> {-# LANGUAGE TypeOperators #-}
> {-# LANGUAGE DataKinds #-}
> {-# 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?
> _______________________________________________