Regression: Could not deduce ‘((n * 3) + b0) ~ ((3 * (n - 1)) + 1)’

[rowanG077]

Basically the same symptom as #124 (also from bittide):

zeroExtendTimesThree :: forall n. (1 <= n, KnownNat n) => Index n -> Index (n * 3)
zeroExtendTimesThree = truncateB . mul (3 :: Index 4)

Leads to:

src/Bittide/SwitchDemoProcessingElement.hs:24:36: error: [GHC-05617]
    • Could not deduce ‘((n * 3) + b0) ~ ((3 * (n - 1)) + 1)’
      from the context: (1 <= n, KnownNat n)
        bound by the type signature for:
                   zeroExtendTimesThree :: forall (n :: Natural).
                                           (1 <= n, KnownNat n) =>
                                           Index n -> Index (n * 3)
        at src/Bittide/SwitchDemoProcessingElement.hs:23:1-82
      Expected: Index n -> Index ((n * 3) + b0)
        Actual: Index n -> MResult (Index 4) (Index n)
      NB: ‘+’ is a non-injective type family
      The type variable ‘b0’ is ambiguous
    • In the second argument of ‘(.)’, namely ‘mul (3 :: Index 4)’
      In the expression: truncateB . mul (3 :: Index 4)
      In an equation for ‘zeroExtendTimesThree’:
          zeroExtendTimesThree = truncateB . mul (3 :: Index 4)
    • Relevant bindings include
        zeroExtendTimesThree :: Index n -> Index (n * 3)
          (bound at src/Bittide/SwitchDemoProcessingElement.hs:24:1)
   |
24 | zeroExtendTimesThree = truncateB . mul (3 :: Index 4)

[rowanG077]

Unfortunately #125 does not solve this one.

[christiaanb]

So on version 0.7.12 of the plugin I see:

unifyNats
  [W] hole{co_aTb} {0}:: ((n_aS0[sk:1] * 3) + b_aSe[tau:1])
                         GHC.Prim.~# ((3 * (n_aS0[sk:1] - 1)) + 1) (CNonCanonical)
  b_aSe[tau:1] + 3 * n_aS0[sk:1]
  -2 + 3 * n_aS0[sk:1]
unifyNats result Draw [b_aSe[tau:1]  :=  -2]

while on version 0.9.3 of the plugin i see:

unifyNats
  [W] hole{co_aTW} {0}:: ((n_aSL[sk:1] * 3) + b_aSZ[tau:1])
                         GHC.Prim.~# ((3 * (n_aSL[sk:1] - 1)) + 1) (CNonCanonical)
  b_aSZ[tau:1] + 3 * n_aSL[sk:1]
  -2 + 3 * n_aSL[sk:1]
unifyNats result Draw []

[christiaanb]

I think the old version of the plugin was wrong to ask a type variable of type Nat to take on the value -2 (by probably emitting a [W] b ~ (0-2) constraint).
In the context of the reported error, it also feels wrong to "truncate" a value by -2 bits.
The new version of the plugin rightfully rejects this.

The original reproducer should be rewritten to:

zeroExtendTimesThree :: forall n. (1 <= n, KnownNat n) => Index n -> Index (n * 3)
zeroExtendTimesThree = zeroExtend . mul (3 :: Index 4)

in which case we see the following constraint:

unifyNats
  [W] hole{co_a14t} {0}:: (b_a145[tau:1]
                           + ((3 * (n_a13R[sk:1] - 1)) + 1))
                          GHC.Prim.~# (n_a13R[sk:1] * 3) (CNonCanonical)
  -2 + b_a145[tau:1] + 3 * n_a13R[sk:1]
  3 * n_a13R[sk:1]
unifyNats result Draw [b_a145[tau:1]  :=  2]

And we basically see that the value is "extended" by 2 bits.

[martijnbastiaan]

OK that's good to know @christiaanb, thank you!

Not sure how to say this without coming across as crass / trying to sit on the maintainer's seat, but perhaps this issue could be left over until it is added to the should-fail test suite.

[christiaanb]

Yeah, fair.