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