{-# 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-safet...