predicate subtypes of functions not propagating predicates

[erniecohen]

Failing code

type F = f:()->bool | f() witness () => true 
method test() { assert forall f:F :: f();}

Steps to reproduce the issue

• Dafny version: 4.5.0.0
• Dafny VSCode extension version: 3.2.2

Expected behavior

should verify

Actual behavior

assertion fails

[MikaelMayer]

As a workaround until we figure it out, I've found that switching back to first-order logic for definitions often helps.

function apply(f: () -> bool): bool { f() }
type F = f:()->bool | apply(f) witness () => true 
method test2() { assert forall f:F :: f();}

[racko]

Interesting. Here's something very similar but for requires clauses: https://github.com/dafny-lang/dafny/issues/2137, https://github.com/dafny-lang/dafny/issues/5106

Probably not directly related, but maybe somebody finds the references helpful anyhow.

[racko]

As a workaround until we figure it out, I've found that switching back to first-order logic for definitions often helps.

function apply(f: () -> bool): bool { f() }
type F = f:()->bool | apply(f) witness () => true 
method test2() { assert forall f:F :: f();}

@MikaelMayer, could you explain what you are doing there? I only see that you are introducing an indirection (apply), but I don't see how this is "switching back to first-order logic" or why it helps the verifier :disappointed_relieved: