onsidere esta definición dezip para la longitud de los vectores habituales indexados por números de Peano:

{-# language DataKinds          #-}
{-# language KindSignatures     #-}
{-# language GADTs              #-}
{-# language TypeOperators      #-}
{-# language StandaloneDeriving #-}
{-# language FlexibleInstances  #-}
{-# language FlexibleContexts   #-}

module Vector
  where

import Prelude hiding (zip)

data N
  where
    Z :: N
    S :: N -> N

data Vector (n :: N) a
  where
    VZ :: Vector Z a
    (:::) :: a -> Vector n a -> Vector (S n) a

infixr 1 :::

deriving instance Show a => Show (Vector n a)

class Zip z
  where
    zip :: z a -> z b -> z (a, b)

instance Zip (Vector n) => Zip (Vector (S n))
  where
    zip (x ::: xs) (y ::: ys) = (x, y) ::: zip xs ys

instance Zip (Vector Z)
  where
    zip _ _ = VZ

-- ^
-- λ :t zip (1 ::: 2 ::: 3 ::: VZ) (4 ::: 5 ::: 6 ::: VZ)
-- zip (1 ::: 2 ::: 3 ::: VZ) (4 ::: 5 ::: 6 ::: VZ)
--   :: (Num a, Num b) => Vector ('S ('S ('S 'Z))) (a, b)
-- λ zip (1 ::: 2 ::: 3 ::: VZ) (4 ::: 5 ::: 6 ::: VZ)
-- (1,4) ::: ((2,5) ::: ((3,6) ::: VZ))

Escribir en números unarios es agotador (aunque tengo una macro para eso). Afortunadamente, hayGHC.TypeLits. Vamos a usarlo:

module Vector
  where

import Prelude hiding (zip)
import GHC.TypeLits

data Vector (n :: Nat) a
  where
    VZ :: Vector 0 a
    (:::) :: a -> Vector n a -> Vector (n + 1) a

infixr 1 :::

deriving instance Show a => Show (Vector n a)

class Zip z
  where
    zip :: z a -> z b -> z (a, b)

instance Zip (Vector n) => Zip (Vector (n + 1))
  where
    zip (x ::: xs) (y ::: ys) = (x, y) ::: zip xs ys

instance Zip (Vector 0)
  where
    zip _ _ = VZ

- Pero no

    • Illegal type synonym family application in instance:
        Vector (n + 1)
    • In the instance declaration for ‘Zip (Vector (n + 1))’
   |
28 | instance Zip (Vector n) => Zip (Vector (n + 1))
   |                            ^^^^^^^^^^^^^^^^^^^^

Así que reemplazo la clase con una función ordinaria:

zip :: Vector n a -> Vector n b -> Vector n (a, b)
zip (x ::: xs) (y ::: ys) = (x, y) ::: zip xs ys
zip VZ VZ = VZ

- Pero ahora ya no puedo usar el razonamiento inductivo:

Vector.hs:25:47: error:
    • Could not deduce: n2 ~ n1
      from the context: n ~ (n1 + 1)
        bound by a pattern with constructor:
                   ::: :: forall a (n :: Nat). a -> Vector n a -> Vector (n + 1) a,
                 in an equation for ‘zip’
        at Vector.hs:25:6-13
      or from: n ~ (n2 + 1)
        bound by a pattern with constructor:
                   ::: :: forall a (n :: Nat). a -> Vector n a -> Vector (n + 1) a,
                 in an equation for ‘zip’
        at Vector.hs:25:17-24
      ‘n2’ is a rigid type variable bound by
        a pattern with constructor:
          ::: :: forall a (n :: Nat). a -> Vector n a -> Vector (n + 1) a,
        in an equation for ‘zip’
        at Vector.hs:25:17-24
      ‘n1’ is a rigid type variable bound by
        a pattern with constructor:
          ::: :: forall a (n :: Nat). a -> Vector n a -> Vector (n + 1) a,
        in an equation for ‘zip’
        at Vector.hs:25:6-13
      Expected type: Vector n1 b
        Actual type: Vector n2 b
    • In the second argument of ‘zip’, namely ‘ys’
      In the second argument of ‘(:::)’, namely ‘zip xs ys’
      In the expression: (x, y) ::: zip xs ys
    • Relevant bindings include
        ys :: Vector n2 b (bound at Vector.hs:25:23)
        xs :: Vector n1 a (bound at Vector.hs:25:12)
   |
25 | zip (x ::: xs) (y ::: ys) = (x, y) ::: zip xs ys
   |                                               ^^

¿Estoy fallando en observar algo obvio? EstasTypeLits no puede ser inútil? .. ¿Cómo se supone que funciona?