<div dir="ltr"><div><div class="gmail_extra"><div class="gmail_quote">On Tue, Mar 15, 2016 at 1:23 PM, Dmitriy Matrosov <span dir="ltr"><<a href="mailto:sgf.dma@gmail.com" target="_blank">sgf.dma@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr">> {-# LANGUAGE DataKinds, KindSignatures, TypeFamilies, UndecidableInstances #-}<br><br>Hi.<br><br>I've reading "Part I: Dependent Types in Haskell" by Hiromi ISHII at<br>schoolofhaskell [1] and i can't understand why my multiplication for<br>singletons (that was exercise) does not not work:<br><br>> data Nat = Z | S Nat<br>><br>> type family Plus (a :: Nat) (b :: Nat) :: Nat where<br>>     Plus 'Z      b  = b<br>>     Plus ('S a1) b  = 'S (Plus a1 b)<br>><br>> type family Mult (a :: Nat) (b :: Nat) :: Nat where<br>>     Mult 'Z      b  = 'Z<br>>     Mult ('S 'Z) b  = b<br>>     Mult ('S a1) b  = Plus (Mult a1 b) b<br>><br>> data SNat :: Nat -> * where<br>>     SZ :: SNat 'Z<br>>     SN :: SNat n -> SNat ('S n)<br>><br>> plusN :: SNat n -> SNat m -> SNat (Plus n m)<br>> plusN SZ     y      = y<br>> plusN (SN x) y      = SN (plusN x y)<br>><br>> multN :: SNat n -> SNat m -> SNat (Mult n m)<br>> multN SZ      y     = SZ<br>> multN (SN SZ) y     = y<br>> multN (SN x)  y     = plusN (multN x y) y<br><br>The last line (multN) does not type-check with error:<br><br>1.lhs:31:25:<br>    Could not deduce (Mult ('S n1) m ~ Plus (Mult n1 m) m)<br>    from the context (n ~ 'S n1)<br>      bound by a pattern with constructor<br>                 SN :: forall (n :: Nat). SNat n -> SNat ('S n),<br>               in an equation for ‘multN’<br>      at 1.lhs:31:10-13<br>    Expected type: SNat (Mult n m)<br>      Actual type: SNat (Plus (Mult n1 m) m)<br>    Relevant bindings include<br>      y :: SNat m (bound at 1.lhs:31:17)<br>      x :: SNat n1 (bound at 1.lhs:31:13)<br>      multN :: SNat n -> SNat m -> SNat (Mult n m) (bound at 1.lhs:29:3)<br>    In the expression: plusN (multN x y) y<br>    In an equation for ‘multN’: multN (SN x) y = plusN (multN x y) y<br><br>Though, when (n ~ 'S n1) i get `SNat (Mult ('S n1) m)` and by definition of<br>Mult this is `SNat (Plus (Mult n1 m) m)` . On the other hand, when i check the<br>type of expression, i get `SNat (Plus (Mult n1 m) m)` by definition of plusN.<br>I.e. exactly the same type.<br><br><br>[1]: <a href="https://www.schoolofhaskell.com/user/konn/prove-your-haskell-for-great-safety/dependent-types-in-haskell" target="_blank">https://www.schoolofhaskell.com/user/konn/prove-your-haskell-for-great-safety/dependent-types-in-haskell</a><br><br></div>
</blockquote></div><br>Aah, it seems, the reason is wrong (my) definition of Mult: 2nd and 3rd 
type family branches are not compatible: `Mult ('S 'Z) b` and `Mult ('S 
a1) b` are not apart (hm.. probably; not sure what "arbitrary 
type-family simplifications" means in [2], 6.2.1) and their RHS-es are 
not the same "under the substitution induced by the unification" ([2], 
6.2.1). And because 2nd branch is not needed at all, all works fine with
 such Mult:<br><br>> type family Mult (a :: Nat) (b :: Nat) :: Nat where<br>>     Mult 'Z      b  = 'Z<br>>     Mult ('S a1) b  = Plus (Mult a1 b) b<br><br>[2]: <a href="https://wiki.haskell.org/GHC/Type_families#Closed_family_simplification">https://wiki.haskell.org/GHC/Type_families#Closed_family_simplification</a><br></div></div></div>