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 )
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
Description: | modified (diff) |
---|
comment:2 Changed 4 years ago by
comment:3 Changed 4 years ago by
Keywords: | TypeFamilies added |
---|
comment:4 Changed 21 months ago by
Cc: | echo@… added |
---|
Note: See
TracTickets for help on using
tickets.
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.