Why can't Haskell deduce that this type is correct?

Question

I have a simple definition for a Nat and a definition for types indexed by Nat's, Natty.

data Nat :: * where 
    Zero :: Nat
    Suc  :: Nat -> Nat

data Natty :: Nat -> * where
    Zy :: Natty Zero
    Sy :: Natty n -> Natty (Suc n)

My goal is to create a function that, given a type indexed by Nat n and a type indexed by Nat m, will produce a type indexed by type Nat n + m.

For example, foo (Sy Zy) (Sy $ Sy Zy) = Sy $ Sy $ Sy Zy

Nat addition is simple and is defined as such:

nAdd :: Nat -> Nat -> Nat
nAdd x  Zero    = x
nAdd x (Suc y)  = Suc $ nAdd x y

I had thought that foo would be defined similarly in the following way:

foo :: Natty n -> Natty m -> Natty (nAdd n m)
foo x  Zy    = x
foo x (Sy y) = Sy $ foo x y

But this leads to an interesting error:

Could not deduce: n ~ nAdd n 'Zero
from the context: m ~ 'Zero

Why can't haskell deduce that n ~ nAdd n 'Zero? Is there a simple way to fix this or will a different approach be needed?

Thanks, any input would be greatly appreciated. The following extensions are also used.

{-# LANGUAGE DataKinds, KindSignatures, GADTs #-}

Haskell is not (currently) dependently typed. You cannot use the value-level function nAdd in a type signature. Natty (nAdd n m) just treats nAdd as a unique, curiously-named type variable. Perhaps you want to use a closed type family instead? Alternatively, the singletons library can promote the function to a type family for you. — Alexis King

K. A. Buhr K. A. Buhr · Accepted Answer · 2018-02-10T06:32:13

As @AlexisKing notes, the nAdd in the type signature for foo is just treated as another type variable (like m or n) and Haskell doesn't tie it back to the definition of the function nAdd.

In Haskell, you can't apply term-level functions (like nAdd) to types. Instead, you need to use type families. If you define a type-level "function" NAdd as a type family:

type family NAdd (a :: Nat) (b :: Nat) :: Nat
type instance NAdd n Zero = n
type instance NAdd n (Suc m) = Suc (NAdd n m)

then you can use this function in your foo signature:

foo :: Natty n -> Natty m -> Natty (NAdd n m)
foo x  Zy    = x
foo x (Sy y) = Sy $ foo x y

This requires a number of additional extensions to work, and the complete working example (running under GHC 8.2.2) looks like this:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}

import Data.Kind

data Nat :: * where 
    Zero :: Nat
    Suc  :: Nat -> Nat

data Natty :: Nat -> * where
    Zy :: Natty Zero
    Sy :: Natty n -> Natty (Suc n)

type family NAdd (a :: Nat) (b :: Nat) :: Nat
type instance NAdd n Zero = n
type instance NAdd n (Suc m) = Suc (NAdd n m)

nAdd :: Nat -> Nat -> Nat
nAdd x  Zero    = x
nAdd x (Suc y)  = Suc $ nAdd x y

foo :: Natty n -> Natty m -> Natty (NAdd n m)
foo x  Zy    = x
foo x (Sy y) = Sy $ foo x y 

test1 = foo (Sy Zy) (Sy $ Sy Zy)
test2 = Sy $ Sy $ Sy Zy

Why can't Haskell deduce that this type is correct?

1 Answers