charon
charon copied to clipboard
Bug: Types cannot convert to pattern
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.
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.