There's something really wonky going on with closed type families.

Wonky.hs

{-# LANGUAGE DataKinds    #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE RankNTypes   #-}

module Lib where

data Nat = Z
         | S Nat

-- There's something really wonky going on with closed type families: if both
-- arguments of Min have type variables in them, then it seems that only the
-- first rule of a closed type family is ever tried. For instance, below we have
-- a version of Min which matches 'Min m m' and, as an optimisation, 'Min m (S m)':

type family Min1 (m :: Nat) (n :: Nat) :: Nat where
  Min1 m      m      = m
  Min1 m      ('S m) = m
  Min1 'Z     n      = 'Z
  Min1 m      'Z     = 'Z
  Min1 ('S m) ('S n) = 'S (Min1 m n)

-- However, the second rule never seems to fire:

-- ghci> :k! forall n. Min1 n n
-- = n
-- ghci> :k! forall n. Min1 n (S n)
-- = Min1 n ('S n)
-- ghci> :k! forall n. Min1 Z (S Z)
-- = 'Z

-- If we swap the first two rules, then the result is swapped as well:

type family Min2 (m :: Nat) (n :: Nat) :: Nat where
  Min2 m      ('S m) = m
  Min2 m      m      = m
  Min2 'Z     n      = 'Z
  Min2 m      'Z     = 'Z
  Min2 ('S m) ('S n) = 'S (Min2 m n)

-- ghci> :k! forall n. Min2 n n
-- = Min2 n n
-- ghci> :k! forall n. Min2 n (S n)
-- = n
-- ghci> :k! forall n. Min2 Z (S Z)
-- = 'Z

-- And if we put both rules at the very end, it seems that neither ever fires:

type family Min3 (m :: Nat) (n :: Nat) :: Nat where
  Min3 'Z     n      = 'Z
  Min3 m      'Z     = 'Z
  Min3 ('S m) ('S n) = 'S (Min3 m n)
  Min3 m      m      = m
  Min3 m      ('S m) = m

-- ghci> :k! forall n. Min3 n n
-- = Min3 n n
-- ghci> :k! forall n. Min3 n (S n)
-- = Min3 n ('S n)
-- ghci> :k! forall n. Min3 Z (S Z)
-- = 'Z