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

[Richard Eisenberg]

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 <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/20200628/c5513866/attachment.html>