typechecker: check exhaustiveness against refined args

[berbiche]

This PR changes the logic in the exhaustiveness check to check for refinability of the refined args instead of the non-refined args.

This was suggested in a different issue here: https://github.com/josefs/Gradualizer/issues/339#issuecomment-895786061 The change resolves an issue I encounter where the type checked for exhaustiveness is accepted but the refined type fails with a badargs in pick_value.

As far as I understand, the refinable3/ function also acts as a gatekeeper for pick_value/2.

edit: Fixes #414

[berbiche]

One issue with checking refinement against the refined args is that pick_value is called against the refined type instead of the non refined type.

For instance, the refined type of a char is an integer range. The information is more exact but loses meaning for the user (IMO).

[zuiderkwast]

the refined type of a char is an integer range

Can we turn it into a char range? Or is it normalized here?

IIRC, normalize turns chars into integers, but in some cases (like this) it'd be good to keep them as chars. OTOH in other cases it's good to have a unique representation to pattern match on.

The information is more exact but loses meaning for the user (IMO).

I agree, but maybe we can live with a more obscure message if we get better exactness?

[berbiche]

the refined type of a char is an integer range

Can we turn it into a char range? Or is it normalized here?

IIRC, normalize turns chars into integers, but in some cases (like this) it'd be good to keep them as chars. OTOH in other cases it's good to have a unique representation to pattern match on.

Yes char() is normalized to an integer range. https://github.com/josefs/Gradualizer/blob/9e629ade733780113973fe672a51d9650ed0cd86/src/typechecker.erl#L826-L827

I think it could be possible to extend the range type to use chars like type(range, [type(char), type(char)])?

The information is more exact but loses meaning for the user (IMO).

I agree, but maybe we can live with a more obscure message if we get better exactness?

Right, like you've said it's a trade-off between correctness and UX. I would prefer to be showed a char that isn't matched than a random integer.

[berbiche]

Closing my PR as recent changes (and new issues) have invalidated the need for this change.