unable to resolve types in Div constructs

[mikesteele81]

I'm unable to turn Div constructs into integrals:

> toNum (d2 `Data.TypeLevel.div` d1)

<interactive>:16:1:
    No instance for (Data.TypeLevel.Num.Sets.NatI
                       (Data.TypeLevel.Num.Ops.Div' D2 D1 GT))
      arising from a use of `toNum'
    Possible fix:
      add an instance declaration for
      (Data.TypeLevel.Num.Sets.NatI
         (Data.TypeLevel.Num.Ops.Div' D2 D1 GT))
    In the expression: toNum (d2 `Data.TypeLevel.div` d1)
    In an equation for `it': it = toNum (d2 `Data.TypeLevel.div` d1)
>

It looks like the problem is in Data.TypeLevel.Num.Ops:

type family Div' x y x_gt_y
type instance Div' x y False = D0
type instance Div' x y True = Succ (Div' (Sub x y) y ((Sub x y) :>=: y))  
type family Div x y
type instance Div x y = Div' x y (Trich x y)

I think I could get some output with type instance Div x y = Div' x y (x :>=: y) (I have not tried this), but that would create invalid instances. Should I expect this type-level function to mirror the behavior of Prelude's div?

Are my expectations wrong? I'm still trying to wrap my head around type-level arithmetic.

[coreyoconnor]

I have not tried the div instances actually. I will have to investigate.
On Oct 4, 2012 2:18 PM, "Michael Steele" notifications@github.com wrote:

I'm unable to turn Div constructs into integrals:

toNum (d2 Data.TypeLevel.div d1)

:16:1:
No instance for (Data.TypeLevel.Num.Sets.NatI
(Data.TypeLevel.Num.Ops.Div' D2 D1 GT))
arising from a use of toNum' Possible fix: add an instance declaration for (Data.TypeLevel.Num.Sets.NatI (Data.TypeLevel.Num.Ops.Div' D2 D1 GT)) In the expression: toNum (d2Data.TypeLevel.divd1) In an equation forit': it = toNum (d2 Data.TypeLevel.div d1)

It looks like the problem is in Data.TypeLevel.Num.Ops:

type family Div' x y x_gt_y
type instance Div' x y False = D0
type instance Div' x y True = Succ (Div' (Sub x y) y ((Sub x y) :>=: y))
type family Div x y
type instance Div x y = Div' x y (Trich x y)

I think I could get some output with type instance Div x y = Div' x y (x
:>=: y) (I have not tried this), but that would create invalid instances.
Should I expect this type-level function to mirror the behavior of
Prelude's div?

Are my expectations wrong? I'm still trying to wrap my head around
type-level arithmetic.

—
Reply to this email directly or view it on GitHubhttps://github.com//issues/1.