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

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 http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.