<p dir="ltr">I would think the provided equalities could be constructed in a view pattern, possibly using unsafeCoerce. Dictionaries are harder to come by, but reflection might be an option. My two biggest gripes about pattern synonyms are really</p>
<p dir="ltr">1. The constraints for "constructor" application are forced to be much tighter than necessary. This is very sad because there doesn't seem to be anything inherently difficult about fixing it--just allow the user to specify the desired type signature for the synonym used as a constructor.<br>
2. The exhaustivity check doesn't work yet.</p>
<div class="gmail_quote">On Jun 18, 2016 10:07 PM, "Matthew Pickering" <<a href="mailto:matthewtpickering@gmail.com">matthewtpickering@gmail.com</a>> wrote:<br type="attribution"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">David, Carter,<br>
<br>
It would be nice to use pattern synonyms for this task but they do not<br>
work quite as expected as they don't cause type refinement.<br>
<br>
I quickly assembled this note to explain why.<br>
<br>
<a href="http://mpickering.github.io/posts/2016-06-18-why-no-refinement.html" rel="noreferrer" target="_blank">http://mpickering.github.io/posts/2016-06-18-why-no-refinement.html</a><br>
<br>
Matt<br>
<br>
On Fri, May 27, 2016 at 4:50 AM, David Feuer <<a href="mailto:david.feuer@gmail.com">david.feuer@gmail.com</a>> wrote:<br>
> Scratch that. I think you might be right.<br>
><br>
> On May 25, 2016 8:40 PM, "David Feuer" <<a href="mailto:david.feuer@gmail.com">david.feuer@gmail.com</a>> wrote:<br>
>><br>
>> Partially. Unfortunately, bidirectional pattern synonyms tie the types of<br>
>> the pattern synonyms to the types of the smart constructors for no good<br>
>> reason, making them (currently) inappropriate. But fixing that problem would<br>
>> offer one way to this optimization, I think.<br>
>><br>
>> On May 25, 2016 8:37 PM, "Carter Schonwald" <<a href="mailto:carter.schonwald@gmail.com">carter.schonwald@gmail.com</a>><br>
>> wrote:<br>
>><br>
>> could this be simulated/modeled with pattern synonyms?<br>
>><br>
>> On Wed, May 25, 2016 at 7:51 PM, David Feuer <<a href="mailto:david.feuer@gmail.com">david.feuer@gmail.com</a>><br>
>> wrote:<br>
>>><br>
>>> I've started a wiki page,<br>
>>> <a href="https://ghc.haskell.org/trac/ghc/wiki/OptimizeCountingGADTs" rel="noreferrer" target="_blank">https://ghc.haskell.org/trac/ghc/wiki/OptimizeCountingGADTs</a> , to consider<br>
>>> optimizing GADTs that look like natural numbers but that possibly have<br>
>>> "heavy zeros". Please take a look.<br>
>>><br>
>>><br>
>>> _______________________________________________<br>
>>> ghc-devs mailing list<br>
>>> <a href="mailto:ghc-devs@haskell.org">ghc-devs@haskell.org</a><br>
>>> <a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs</a><br>
>>><br>
>><br>
><br>
> _______________________________________________<br>
> ghc-devs mailing list<br>
> <a href="mailto:ghc-devs@haskell.org">ghc-devs@haskell.org</a><br>
> <a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs</a><br>
><br>
</blockquote></div>