Code Contracts: Why are some invariants not considered outside the class?

Consider this immutable type:

public class Settings
{
    public string Path { get; private set; }

    [ContractInvariantMethod]
    private void ObjectInvariants()
    {
        Contract.Invariant(Path != null);
    }

    public Settings(string path)
    {
        Contract.Requires(path != null);
        Path = path;
    }
}

Two things to notice here:

• There is a contract invariant which ensures the Path property can never be null
• The constructor checks the path argument value to respect the previous contract invariant

At this point, a Setting instance can never have a null Path property.

Now, look at this type:

public class Program
{
    private readonly string _path;

    [ContractInvariantMethod]
    private void ObjectInvariants()
    {
        Contract.Invariant(_path != null);
    }

    public Program(Settings settings)
    {
        Contract.Requires(settings != null);
        _path = settings.Path;
    } // <------ "CodeContracts: invariant unproven: _path != null"
}

Basically, it has its own contract invariant (on _path field) that can't be satisfied during static checking (cf. comment above). That sounds a bit weird to me, since it's easy to prove it:

• settings is immutable
• settings.Path can't be null (because Settings has the corresponding contract invariant)
• so by assigning settings.Path to _path, _path can't be null

Did I miss something here?