charon icon indicating copy to clipboard operation
charon copied to clipboard

Bug: Types cannot convert to pattern

Open ssyram opened this issue 2 months ago • 1 comments

Now in file charon-ml/src/NameMatcher.ml, the function ty_to_pattern_aux, the conversion from ty to the pattern expr is PARTIAL and may lead to failure in Eurydice.

Specifically, the problem is caused by missing the TNever, TDynTrait, TFnDef and TPtrMetadata patterns.

ssyram avatar Oct 31 '25 09:10 ssyram

Easy fix would be to translate them to the _ pattern. This would make the output pattern too general, but I also don't want the name matcher to be able to handle this level of type precision unless we have a real use for that.

Nadrieril avatar Nov 03 '25 15:11 Nadrieril