Opened 4 years ago

Last modified 21 months ago

#11113 new bug

Type family If is too strict

Reported by: olshanskydr Owned by:
Priority: normal Milestone:
Component: Compiler Version: 7.10.2
Keywords: TypeFamilies Cc: echo@…
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 (last modified by olshanskydr)

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)

Change History (4)

comment:1 Changed 4 years ago by olshanskydr

Description: modified (diff)

comment:2 Changed 4 years ago by goldfire

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.

comment:3 Changed 4 years ago by thomie

Keywords: TypeFamilies added

comment:4 Changed 21 months ago by enolan

Cc: echo@… added
Note: See TracTickets for help on using tickets.