Skip to content

Failed type inference should not pollute type bounds #226

Open
@apoelstra

Description

@apoelstra

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.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions