BlockstreamResearch / rust-simplicity

Creative Commons Zero v1.0 Universal
58 stars 12 forks source link

Failed type inference should not pollute type bounds #226

Open apoelstra opened 2 months ago

apoelstra commented 2 months ago

Consider the following unit test

    #[test]
    fn inference_failure_type_pollution() {
        let unit1 = Arc::<ConstructNode<Core>>::unit(); // A -> 1a
        let unit2 = Arc::<ConstructNode<Core>>::unit(); // B -> 1b
        // Constructing a disconnect operator will bind A to 2^256 x B (which
        // will succeed) and then bind 1a to B x 1b (which will fail), so the
        // construction of the disconnect operator should fail.
        Arc::<ConstructNode<Core>>::disconnect(&unit1, &Some(Arc::clone(&unit2))).unwrap_err();
        // But because the construction of the disconnect node failed, it shouldn't
        // pollute the unit; it SHOULD NOT leave A with a product bound.
        assert_eq!(
            unit1.arrow().source.finalize().unwrap(),
            types::Final::unit(),
        );  
    }   

This fails currently, because type inference works by applying bounds one after the other. In the case of combinators like disconnect, it may happen that one bound succeeds while the following one fails, leaving the types of the program in an inconsistent state.

This isn't a super high priority because under "normal" usage once a type inference step fails you should throw the whole program away and restart, and because I have a set of huge PRs coming in that'll reorganize the type checker to no longer leak memory, but it is causing my fuzzer to slow down.