Type family If is too strict

This code

type family Div (k::Nat) (n::Nat) where
    Div k n = If (CmpNat k n == LT) 0 (1 + Div (k-n) n)

is not working. When I try

ghci> :t (Proxy :: Proxy (Div 100 9))

it hangs on. Probably ghci is trying to calculate both If branches.

If I rewrite it this way

type family Div (k::Nat) (n::Nat) where
    Div k n = Div' k n (CmpNat k n)

type family Div' (k::Nat) (n::Nat) (b::Ordering) where
    Div' k n LT = 0
    Div' k n EQ = 1
    Div' k n GT = 1 + Div (k-n) n

it works well.

This code also not working

type family Div (k::Nat) (n::Nat) where
    Div k n = Div'' k n (CmpNat k n == LT)

type family Div'' (k::Nat) (n::Nat) (b::Bool) where
    Div'' k n b = If b 0 (1 + Div (k-n) n)