[Haskell-cafe] Is there a handy refl or refl generator for converting GADT types?

[chris done]

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 <haskell-cafe at chrisdone.com> 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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20200702/7f3b1497/attachment.html>