One thing that does work nicely is record wild cards. I can write f X{..}=X{..}. So for a product type I’m pretty much set. I can also optionally manually update one or more fields if needed. If there was an equivalent of record wild cards for sum types, that would be swell. E.g. f = \case X a -> ... .. -> .. To have GHC fill out the remainder constructors with a simple verbatim restating of “lhs -> lhs”. But it doesn't exactly match up with GHC's normal exhaustiveness checker which goes deeper than the top constructor. It's fine, though, this doesn't happen _that_ often in my code. Cheers, Chris On Sun, Jun 28, 2020, at 11:51 AM, Richard Eisenberg wrote:

I think the general answer to your question is: no, you can't avoid this pattern match. In your particular case, the domain (Global Renamed) is a subset of the range (Global Generated), and so we can imagine a function that just changes the type without any fuss. This would, I'm pretty sure, be safe. But GHC has no notion of this kind of one-way transformation, so you're stuck just doing it via a manual pattern-match.

I hope this helps! Richard

...

On Jun 27, 2020, at 3:23 PM, chris done wrote:

Hi all,

I have stages in my compiler that convert e.g. Global Renamed -> Global Generated, etc. where certain constructors are available in certain stages.

data GlobalRef s where FromIntegerGlobal :: GlobalRef s FromDecimalGlobal :: GlobalRef s InstanceGlobal :: !InstanceName -> GlobalRef Resolved

E.g. after type class resolution is done, the InstanceGlobal constructor is available. But instances can't appear in the AST at other stages.

In three stages, I've had to copy/paste this code:

+ refl = + case name of + FromIntegerGlobal -> FromIntegerGlobal + FromDecimalGlobal -> FromDecimalGlobal

Because if I just put `name` then GHC will complain that the types are different, which is correct. But a straight-forward pattern match gives GHC the proof that they can be converted.

Is there a handy way already implemented that could derive either this code or this proof for me?

Cheers,

Chris _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.