On Sat, Nov 29, 2014, at 04:35 PM, Gautier DI FOLCO wrote:
Hello all,
 
I have the following code:
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
 
data Branch = Left | Right
 
type family Product (v :: Branch) (a :: k) (b :: k) :: k where
  Product Left  l r = l
  Product Right l r = r
 
He is doing what I expect it to do and Product has the right Kind:
*Main> :kind Product
Product :: Branch -> k -> k -> k
 
But when I change the Kind signature syntax, its Kind changes:
type family Product v a b :: Branch -> k -> k -> k where
Its Kind become:
*Main> :kind Product
Product :: Branch
           -> (Branch -> k -> k -> k)
           -> (Branch -> k1 -> k1 -> k1)
           -> Branch
           -> k2
           -> k2
           -> k2
 
In a type family declaration, the signature to the right of the top-level "::" is always the kind of the result. When you drop the kind signatures from the parameter declarations, the kinds of those parameters become inferred rather than explicit, but that doesn't change the interpretation of the top-level signature - it is still just the kind of the result.
 
-Karl