VarEq bug in normalize

[wrengr]

Email from @zaxtax:

When I call normalize on the following program:

bet <~ beta(5,3)
x1 <~ factor(bet)
if bet > 0.7: return true else: return false

I get the following error:

[zv@t420 hakaru (master)]% normalize t.hk
normalize: VarEqTypeError (Variable "x1" (Nat 1) (SData (STyCon (SingSymbol Proxy :: Sing "Unit")) (SPlus SDone SVoid))) (Variable "" (Nat 1) SProb)

Note this happens after expect is called, as if I print out the AST for the program, every Variable has a unique ID:

syn (MBind :$ ((syn ((MeasureOp_ Beta) :$ ((syn ((CoerceTo_ (CCons (Continuous HContinuous_Prob) CNil)) :$ ((syn (Literal_ (LNat 5))) :* End))) :* ((syn ((CoerceTo_ (CCons (Continuous HContinuous_Prob) CNil)) :$ ((syn (Literal_ (LNat 3))) :* End))) :* End)))) :* ((bind (Variable "bet" (Nat 0) SProb) (syn (MBind :$ ((syn (Superpose_ [(var (Variable "bet" (Nat 0) SProb),syn (Dirac :$ ((syn (Datum_ (Datum "unit" (Inl Done)))) :* End)))])) :* ((bind (Variable "x1" (Nat 1) (SData (STyCon (SingSymbol Proxy :: Sing "Unit")) (SPlus SDone SVoid))) (syn (Case_ (syn ((PrimOp_ (Less HOrd_Prob)) :$ ((syn (Literal_ (LProb (7 % 10)))) :* ((var (Variable "bet" (Nat 0) SProb)) :* End)))) [Branch (PDatum "true" (PInl PDone)) (syn (Dirac :$ ((syn (Datum_ (Datum "true" (Inl Done)))) :* End))),Branch (PDatum "false" (PInr (PInl PDone))) (syn (Dirac :$ ((syn (Datum_ (Datum "false" (Inr (Inl Done))))) :* End)))]))) :* End))))) :* End)))

Any ideas?

[wrengr]

The problem is that runExpect was initializing its nextFreshNat to the nextFree which apparently is insufficiently fresh. I fixed this by switching to the newly defined nextFreeOrBind in patch c9641a9

$> cat bug15.hk
bet <~ beta(5,3)
x1 <~ factor(bet)
if bet > 0.7:
    return true
else:
    return false

$> cat bug15.hk | ./dist/build/normalize/normalize
weight(recip(integrate x2 from 0.0 to 1.0:
              x3 = unsafeProb(x2)
              ((x3 ** 4.0) *
               (unsafeProb((1.0 + negate(fromProb(x3)))) ** 2.0) *
               recip(betaFunc(5.0, 3.0)) *
               x3 *
               expect x5 match (0.7 < x3):
                          true: return true
                          false: return false:
                1.0)),
       bet <~ beta(5.0, 3.0)
       x1 <~ weight(bet, return ())
       match (0.7 < bet):
        true: return true
        false: return false)

[zaxtax]

:+1: