Boogie crash: Error: invalid argument types (Box and DatatypeType) to binary operator ==

[selig]

Dafny version

4.4.0

Code to produce this issue

trait Foo {}
datatype Bar extends Foo = Bar

function getFoo() : Foo { Bar }

Command to run and resulting output

dafny verify --type-system-refresh --general-traits:datatype

tmpg7YYPr.tmp.dfy(4,9): Error: invalid argument types (Box and DatatypeType) to binary operator ==
tmpg7YYPr.tmp.dfy(4,9): Error: invalid argument types (Box and DatatypeType) to binary operator ==
2 type checking errors detected in /tmp/tmpg7YYPr.tmp__module.bpl

*** Encountered internal translation error - re-running Boogie to get better debug information

/tmp/tmpg7YYPr.tmp__module.bpl(2838,34): Error: invalid argument types (Box and DatatypeType) to binary operator ==
/tmp/tmpg7YYPr.tmp__module.bpl(2843,34): Error: invalid argument types (Box and DatatypeType) to binary operator ==
2 type checking errors detected in /tmp/tmpg7YYPr.tmp__module.bpl

What happened?

Expected it to verify; it crashed.

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

Other