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

[chris done]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20200627/83e0bbef/attachment.html>