feat: collect effect constraints to be unified together

[mlutze]

fixes #7503

[magnus-madsen]

@mlutze This should stay open, right?

[mlutze]

@mlutze This should stay open, right?

Yes

[magnus-madsen]

@mlutze This seems very close to working. Do you need help with debugging? It seems Datalog related. So maybe lowering or something with free variables? I am kind of unsure how you can get those errors we are getting though.

[magnus-madsen]

Ah- its not calling the new solver yet, right?

[mlutze]

@mlutze This seems very close to working. Do you need help with debugging? It seems Datalog related. So maybe lowering or something with free variables? I am kind of unsure how you can get those errors we are getting though.

Yes, please! I'm thinking maybe I lose part of the substitution somewhere so we end up with free variables that should have been substituted, but I haven't identified the problem yet.

Ah- its not calling the new solver yet, right?

It should be (?)

[magnus-madsen]

Bug is non-deterministic, but this reproduces it always with threads = 1:

@test
def main(): Bool =
    let p = #{
        A(1, 2, 3).
        R(x, y, z) :- A(x, y, z).
    };
    let r = query p select (x, y, z) from R(x, y, z);
    Vector.memberOf((1, 2, 3), r)

[magnus-madsen]

Removing Graph.flix from std lib fixes the problem-- which is super strange.

[magnus-madsen]

@mlutze @JonathanStarup I have isolated the bug. It has to do with UncheckedMaskingCast.

If I remove:

Interpreter.flix:32:    masked_cast(Fixpoint.Debugging.notifyPreInterpret(stmt));
Solver.flix:47:   masked_cast(Fixpoint.Debugging.notifyPreSolve(d, stf));
Solver.flix:64:    masked_cast(Fixpoint.Debugging.notifyPostSolve(model))

All tests (except one unrelated) run.

[magnus-madsen]

I suspect it has to do with UncheckedMaskingCast being erased and then later the inliner making changes which gives rise to inconsistent effects.

@JonathanStarup Does the verifier not check for effect consistency? E.g. if a sub-expression is control-impure presumable the expression itself must also be control-impure.

[magnus-madsen]

I have a workaround here #7659

It solves nothing, but at least it makes the problem go-away.

[magnus-madsen]

I think now there is just Type.Error left to deal with.

[mlutze]

I think now there is just Type.Error left to deal with.

I think ideally we could treat every Type.Error as a free var. Then any type errors we get out will only be ones we would have no matter what the real value of Type.Error is. What do you think?

[magnus-madsen]

I think now there is just Type.Error left to deal with.

I think ideally we could treat every Type.Error as a free var. Then any type errors we get out will only be ones we would have no matter what the real value of Type.Error is. What do you think?

I was thinking constant?

[magnus-madsen]

I think now there is just Type.Error left to deal with.

I think ideally we could treat every Type.Error as a free var. Then any type errors we get out will only be ones we would have no matter what the real value of Type.Error is. What do you think?

I was thinking constant?

Ill let you experiment/decide. I don't think the choice right now is important.

[mlutze]

Still transient issues :(

[magnus-madsen]

Still transient issues :(

Do you mean flaky tests? Is it only TestVector that fails?

The new solver has no state... So it seems strange. Are we still using Type.minimize?

[magnus-madsen]

I see lots of non-determinism indeed.

[magnus-madsen]

Disabling the optimizer seems to make the tests pass. But what causes the non-determinism which sometimes allows everything to go through?

[magnus-madsen]

@JonathanStarup We are going to need some help debugging this, when you have time.

[mlutze]

Disabling the optimizer seems to make the tests pass. But what causes the non-determinism which sometimes allows everything to go through?

One source is the mapping of types to Boolean terms.

[magnus-madsen]

Another source is the naming of variables which affects the solutions computed by the solver (?)

[magnus-madsen]

I think we need the Verifier to reject illegal programs w.r.t effects.

[magnus-madsen]

What's the working thesis: That we produce expressions with non-deterministic effects that are only sometimes wrong and hence only sometimes screwed up by the optimizer?

[magnus-madsen]

I have created #7672 and #7673 sadly neither seems to address the issue, but nevertheless I believe they make things safer.

[magnus-madsen]

Interestingly running Reachable.flix always fails deterministically.
So its the presence of other tests that some times make it pass.

EDIT: Add pub def main(): Bool = Reachable.Logic.test() to run it

[magnus-madsen]

In monomorpher, if I compare what source locations are made pure by the strict subst:

      case Kind.Eff =>
        // If an effect variable is free, we may assume its Pure due to the subst. lemma.
        println(tpe0.loc)
        Type.Pure

it seems that this PR has more source locations made pure, including in e.g.

MutList.flix:854:9
MutList.flix:851:17
(and several other places)

which at least suggests that more variables are free in this PR...

[magnus-madsen]

@JonathanStarup We believe the bug is in the typer, but we could really benefit from having a verifier that checks effects s.t. the backend does not generate incorrect code.

[magnus-madsen]

Did you have some success or not yet?

[mlutze]

Did you have some success or not yet?

Not yet :(

[magnus-madsen]

@mlutze Do you want to rebase?

[magnus-madsen]

RFM?

[magnus-madsen]

test failures?

[mlutze]

test failures?

please no

[magnus-madsen]

What a pain. Same issue or new issue?

[mlutze]

What a pain. Same issue or new issue?

Seems new. There's no runtime crash, but apparently a nondeterministic miscompilation. I cannot reliably reproduce.

[magnus-madsen]

What a pain. Same issue or new issue?

Seems new. There's no runtime crash, but apparently a nondeterministic miscompilation. I cannot reliably reproduce.

Try to compile one of the tests in isolation. That worked last time.

[mlutze]

What a pain. Same issue or new issue?

Seems new. There's no runtime crash, but apparently a nondeterministic miscompilation. I cannot reliably reproduce.

Try to compile one of the tests in isolation. That worked last time.

What a pain. Same issue or new issue?

Seems new. There's no runtime crash, but apparently a nondeterministic miscompilation. I cannot reliably reproduce.

Try to compile one of the tests in isolation. That worked last time.

not working for me :(

[magnus-madsen]

One in about ten run produces false:

mod Reachable.Imperative {
    pub def reachable(origin: n, edges: es): Set[n] \ Iterable.Aef[es] with Iterable[es], Order[n] where Iterable.Elm[es] ~ (n, n) =
        region rc {
            // collect edge lists
            let edgeMap = MutMap.empty(rc);
            foreach((start, end) <- edges) {
                let startEdges = MutMap.getOrElsePut!(start, MutList.empty(rc), edgeMap);
                MutList.push!(end, startEdges)
            };
            // define the reachable set
            let reachable = MutSet.empty(rc);
            // explore graph depth first by task list
            let taskList = MutDeque.empty(rc);
            taskList |> MutDeque.pushFront(origin);
            def whileLoop() = {
                MutDeque.popFront(taskList) |> Option.forEach(node -> {
                    // this node has now been reached
                    reachable |> MutSet.add!(node);
                    // add all non-reached end points to tasklist
                    let endPoints = MutMap.getWithDefault(node, MutList.empty(rc), edgeMap);
                    MutList.forEach(nextNode -> {
                        let alreadyReached = MutSet.memberOf(nextNode, reachable);
                        if (not alreadyReached)
                            taskList |> MutDeque.pushFront(nextNode)
                        else ()
                    }, endPoints);
                    whileLoop()
                })
            };
            whileLoop();
            MutSet.toSet(reachable)
        }

    @test
    pub def test(): Bool = validate(reachable)
}

pub def main(): Unit \ IO =
    validate(Reachable.Imperative.reachable) |> println

pub def graph1(): Set[(Int32, Int32)] = Set#{}

pub def graph2(): Set[(Int32, Int32)] = Set#{
    (1, 2), (2, 3), (3, 4), (4, 1)
}

pub def graph3(): Set[(Int32, Int32)] = Set#{
    (1, 2), (1, 3), (4, 5)
}

pub def graph4(): Set[(Int32, Int32)] = Set#{
    (2, 3), (3, 4)
}

pub def graph5(): Set[(Int32, Int32)] = Set#{
    (4, 5), (5, 6), (4, 3), (4, 2), (12, 13), (29, 4)
}

pub def validate(reachable: Int32 -> Set[(Int32, Int32)] -> Set[Int32]): Bool = {
    let test1 = reachable(42, graph1()) == Set#{42};
    let test2 = reachable(1, graph2()) == Set#{1, 2, 3, 4};
    let test3 = reachable(1, graph3()) == Set#{1, 2, 3};
    let test4 = reachable(1, graph4()) == Set#{1};
    let test5 = reachable(4, graph5()) == Set#{2, 3, 4, 5, 6};
    test1 and test2 and test3 and test4 and test5
}

[magnus-madsen]

Add this to TypeReconstruction.scala:

    case KindedAst.Expr.Apply(exp, exps, tvar, evar, loc) =>
      val e = visitExp(exp)
      val es = exps.map(visitExp(_))

      val applyEff = subst(evar)
      val arrowEff = e.tpe.typeArguments.headOption

      if (Some(applyEff) != arrowEff) {
        println(arrowEff.getOrElse("<None>"))
        println(applyEff)
        println(loc.format)
        println()
      }

      TypedAst.Expr.Apply(e, es, subst(tvar), applyEff, loc)

and it shows lots of:

Pure
e104501 & Aef['26648]
Foldable.flix:100:46

(e104501 & Aef['26648]) + Aef['26648]
Aef['26648]
Foldable.flix:100:9

Aef['26648]
Aef['26648]
Foldable.flix:163:9

e26689 + Aef['26648]
e26689 + Aef['26648]
Foldable.flix:56:9

Aef['26648]
Aef['26648]
Foldable.flix:258:9

Aef['26648]
Aef['26648]
Foldable.flix:128:7

e26831 + Aef['26648]
Aef['26648] + e26831
Foldable.flix:179:9

EDIT: Woops, have to be careful and remember arguments could have effects too...

[magnus-madsen]

Observation Aef['26648] and Aef['26648] are not equal if they have different source locations.

This is because Type.AssocType is a case class, but notably Type.Apply and Type.Cst ignores source locations.

[magnus-madsen]

The equality thing is bad, but not the cause.