[Haskell-beginners] Multiplicaton of singletons

[Dmitriy Matrosov]

> {-# LANGUAGE DataKinds, KindSignatures, TypeFamilies,
UndecidableInstances #-}

Hi.

I've reading "Part I: Dependent Types in Haskell" by Hiromi ISHII at
schoolofhaskell [1] and i can't understand why my multiplication for
singletons (that was exercise) does not not work:

> data Nat = Z | S Nat
>
> type family Plus (a :: Nat) (b :: Nat) :: Nat where
>     Plus 'Z      b  = b
>     Plus ('S a1) b  = 'S (Plus a1 b)
>
> type family Mult (a :: Nat) (b :: Nat) :: Nat where
>     Mult 'Z      b  = 'Z
>     Mult ('S 'Z) b  = b
>     Mult ('S a1) b  = Plus (Mult a1 b) b
>
> data SNat :: Nat -> * where
>     SZ :: SNat 'Z
>     SN :: SNat n -> SNat ('S n)
>
> plusN :: SNat n -> SNat m -> SNat (Plus n m)
> plusN SZ     y      = y
> plusN (SN x) y      = SN (plusN x y)
>
> multN :: SNat n -> SNat m -> SNat (Mult n m)
> multN SZ      y     = SZ
> multN (SN SZ) y     = y
> multN (SN x)  y     = plusN (multN x y) y

The last line (multN) does not type-check with error:

1.lhs:31:25:
    Could not deduce (Mult ('S n1) m ~ Plus (Mult n1 m) m)
    from the context (n ~ 'S n1)
      bound by a pattern with constructor
                 SN :: forall (n :: Nat). SNat n -> SNat ('S n),
               in an equation for ‘multN’
      at 1.lhs:31:10-13
    Expected type: SNat (Mult n m)
      Actual type: SNat (Plus (Mult n1 m) m)
    Relevant bindings include
      y :: SNat m (bound at 1.lhs:31:17)
      x :: SNat n1 (bound at 1.lhs:31:13)
      multN :: SNat n -> SNat m -> SNat (Mult n m) (bound at 1.lhs:29:3)
    In the expression: plusN (multN x y) y
    In an equation for ‘multN’: multN (SN x) y = plusN (multN x y) y

Though, when (n ~ 'S n1) i get `SNat (Mult ('S n1) m)` and by definition of
Mult this is `SNat (Plus (Mult n1 m) m)` . On the other hand, when i check
the
type of expression, i get `SNat (Plus (Mult n1 m) m)` by definition of
plusN.
I.e. exactly the same type.


[1]:
https://www.schoolofhaskell.com/user/konn/prove-your-haskell-for-great-safety/dependent-types-in-haskell
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/beginners/attachments/20160315/8695d8a9/attachment.html>