regression in datatype instance containing itself being ruled out?

[namin]

Dafny version

4.10.1+f5ca47b85f9af29721646ea517b69088c52bd385

Code to produce this issue

This code verifies in 4.10.0 but not in master.


datatype ty =  TBase                             // (opaque base type)
            |  TArrow(T1: ty, T2: ty)            // T1 => T2

lemma ex(t: ty)
requires t.TArrow?
ensures t.T1 != t
{
}

This is a minimized example, adapted from https://github.com/namin/dafny-sandbox/blob/master/Stlc.dfy where the example of ensuring self application does NOT typecheck no longer holds (nonexample_typing_3).

Command to run and resulting output

% ~/Downloads/dafny/dafny mini.dfy 
Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format
mini.dfy(7,0): Error: a postcondition could not be proved on this return path
mini.dfy(6,13): Related location: this is the postcondition that could not be proved

Dafny program verifier finished with 1 verified, 1 error
(base) namin@black dafny-sandbox % dafny --version
4.10.0
(base) namin@black dafny-sandbox % dafny mini.dfy
Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format

Dafny program verifier finished with 2 verified, 0 errors
Compiled assembly into mini.dll

What happened?

Somehow, it's no longer straightforward to reason that a datatype instance does not contain itself?

What type of operating system are you experiencing the problem on?

Mac