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)

changed weight to 5

added Tbug Trac import labels

changed the description

At one point, I thought I could come up with a terrible hack that would fix this, but I don't think so anymore. What we really need is a proper (preferably lazy!) semantics for type-level reduction.

I'm afraid I can't offer any workaround better than the one you've already come up with.

added Pnormal label