Types of dimension-indexed matrices in Haskell.

Matrix.hs

{-# LANGUAGE UnicodeSyntax, NoStarIsType #-}
{-# LANGUAGE GADTs, DataKinds, PolyKinds, PatternSynonyms, ViewPatterns, TypeApplications #-}

module Data.Matrix where

import Data.Kind

-- The usual definitions of Nat and Vec:
data Nat = Z | S Nat

data Vec :: Nat -> Type -> Type where
  VNil :: Vec 'Z a
  (:>) :: a -> Vec n a -> Vec ('S n) a

-- | A matrix is a vector of /column/ vectors.
type Matrix m n a = Vec n (Vec m a)

-- | The 0×0 empty matrix. (Not sure yet how best to deal with the m×0 and 0×n cases...)
pattern MZero :: Matrix 'Z 'Z a
pattern MZero <- VNil where MZero = VNil

-- Why doesn't this work? Shouldn't a `Matrix 'Z 'Z` be perfectly valid when
-- it's expecting a `Matrix m n`?
test :: Matrix m n a -> ()
test MZero = ()
test _ = undefined
{-^
Data/Matrix.hs:33:6: error:
    • Couldn't match type ‘n’ with ‘'Z’
      ‘n’ is a rigid type variable bound by
        the type signature for:
          test :: forall (m :: Nat) (n :: Nat) a. Matrix m n a -> ()
        at Data/Matrix.hs:32:1-24
      Expected type: Matrix m n a
        Actual type: Matrix 'Z 'Z a
    • In the pattern: MZero
      In an equation for ‘test’: test MZero = ()
    • Relevant bindings include
        test :: Matrix m n a -> ()
          (bound at Data/Matrix.hs:33:1)
   |
25 | test MZero = ()
   |      ^^^^^
-}