Type Naturals cause Type Errors depending on addition/subtraction

Learn
1

I tried using DataKinds with TypeNats for the first time: building a type-level length-indexed vector.
What I produced was this:

Vector code

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE StandaloneDeriving #-}
module Numeric.Vector
(Vector(..))
where

import GHC.TypeLits (Nat, type (+))

data Vector (n :: Nat) e where
  VectorNil  :: Vector 0 e
  VectorCons :: e -> Vector n e -> Vector (n+1 :: Nat) e

deriving

but when deriving an instance

deriving instance (Eq e) => Eq (Vector n e)

I am greeted with a lengthy type-error which originates from generated code.

lengthy type error 
   • Could not deduce ‘n2 ~ n1’
     from the context: n ~ (n1 + 1)
       bound by a pattern with constructor:
                  VectorCons :: forall e (n :: GHC.Num.Natural.Natural).
                                e -> Vector n e -> Vector (n + 1) e,
                in a case alternative
       at /home/vego/Documents/Studium/SS25/Einführung in die Computergraphik/transformations/src/Numeric/Vector.broken.hs:16:1-43
     or from: n ~ (n2 + 1)
       bound by a pattern with constructor:
                  VectorCons :: forall e (n :: GHC.Num.Natural.Natural).
                                e -> Vector n e -> Vector (n + 1) e,
                in a case alternative
       at /home/vego/Documents/Studium/SS25/Einführung in die Computergraphik/transformations/src/Numeric/Vector.broken.hs:16:1-43
     Expected: Vector n1 e
       Actual: Vector n2 e
     ‘n2’ is a rigid type variable bound by
       a pattern with constructor:
         VectorCons :: forall e (n :: GHC.Num.Natural.Natural).
                       e -> Vector n e -> Vector (n + 1) e,
       in a case alternative
       at /home/vego/Documents/Studium/SS25/Einführung in die Computergraphik/transformations/src/Numeric/Vector.broken.hs:16:1-43
     ‘n1’ is a rigid type variable bound by
       a pattern with constructor:
         VectorCons :: forall e (n :: GHC.Num.Natural.Natural).
                       e -> Vector n e -> Vector (n + 1) e,
       in a case alternative
       at /home/vego/Documents/Studium/SS25/Einführung in die Computergraphik/transformations/src/Numeric/Vector.broken.hs:16:1-43
   • In the second argument of ‘(==)’, namely ‘b2’
     In the second argument of ‘(&&)’, namely ‘((a2 == b2))’
     In the expression: ((a1 == b1)) && ((a2 == b2))
     When typechecking the code for ‘==’
       in a derived instance for ‘Eq (Vector n e)’:
       To see the code I am typechecking, use -ddump-deriv
   • Relevant bindings include
       b2 :: Vector n2 e
         (bound at /home/vego/Documents/Studium/SS25/Einführung in die Computergraphik/transformations/src/Numeric/Vector.broken.hs:16:1)
       a2 :: Vector n1 e
         (bound at /home/vego/Documents/Studium/SS25/Einführung in die Computergraphik/transformations/src/Numeric/Vector.broken.hs:16:1) [GHC-25897]

handwritten

I then tried writing my own instance like so:

instance Eq e => Eq (Vector n e) where
  (==) :: Vector n e -> Vector n e -> Bool
  (==) VectorNil           VectorNil         = True
  (==) (VectorCons le lv) (VectorCons re rv) = (le == re) && (lv == rv)
  (==) _                   _                 = False

and it produces exactly the same type error as above.

As I understand it, can’t conclude that the lengths of lv and rv are the same.

alternative defintion

Using this definition, where I use type (-) instead of type (+), everything works fine:

data Vector (n :: Nat) e where
  VectorNil  :: Vector 0 e
  VectorCons :: e -> Vector (n-1) e -> Vector n e

This was the last thing I tried, but I tried it only because I know that it had to be possible somehow.

Did I overlook something, an easy-to-catch mistake? Is this a limitation of the type-checking system. Can I follow some rule of thumb to avoid such mistakes in the future?

2

Quick answer while someone more knowledgeable doesn’t chime in. GHC’s built-in type naturals are not very useful for stuff that requires proving stuff. They are not structural, therefore stuff like knowing that n + 1 = m + 1 will not give you that n = m. For structural type naturals you should use data Nat = Zero | Succ Nat (and build everything from there).

3

That’s right, GHC doesn’t implement much reasoning about arithmetic. You can use the plugin ghc-typelits-presburger to solve this. Another similar plugin is ghc-typelits-natnormalise but it might be too limited to know about injectivity of +.

2 Likes