[GHC] #11113: Type family If is too strict

[GHC]

#11113: Type family If is too strict
-------------------------------------+-------------------------------------
        Reporter:  olshanskydr       |                Owner:
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  7.10.2
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Description changed by olshanskydr:

Old description:

> This code
> {{{#!hs
> 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
> {{{#!hs
> 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

New description:

 This code
 {{{#!hs
 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
 {{{#!hs
 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
 {{{#!hs
 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)
 }}}

--

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11113#comment:1>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler