<!DOCTYPE html><html><head><title></title><style type="text/css">p.MsoNormal,p.MsoNoSpacing{margin:0}
p.MsoNormal,p.MsoNoSpacing{margin:0}</style></head><body><div>One thing that does work nicely is record wild cards. I can write f X{..}=X{..}. So for a product type I’m pretty much set. I can also optionally manually update one or more fields if needed. <br></div><div><br></div><div>If there was an equivalent of record wild cards for sum types, that would be swell. E.g.<br></div><div><br></div><div>f = \case<br></div><div> X a -> ...</div><div> .. -> ..<br></div><div><br></div><div>To have GHC fill out the remainder constructors with a simple verbatim restating of “lhs -> lhs”. But it doesn't exactly match up with GHC's normal exhaustiveness checker which goes deeper than the top constructor.<br></div><div><br></div><div>It's fine, though, this doesn't happen _that_ often in my code.<br></div><div><br></div><div>Cheers,<br></div><div><br></div><div>Chris</div><div><br></div><div>On Sun, Jun 28, 2020, at 11:51 AM, Richard Eisenberg wrote:<br></div><blockquote type="cite" id="qt" style="overflow-wrap:break-word;"><div>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.<br></div><div class="qt-"><br></div><div class="qt-">I hope this helps!<br></div><div class="qt-"><div>Richard<br></div><div><div><br></div><blockquote type="cite" class="qt-"><div class="qt-">On Jun 27, 2020, at 3:23 PM, chris done <<a href="mailto:haskell-cafe@chrisdone.com" class="qt-">haskell-cafe@chrisdone.com</a>> wrote:<br></div><div><br></div><div class="qt-"><div style="font-style:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;text-size-adjust:auto;-webkit-text-stroke-width:0px;text-decoration-line:none;text-decoration-style:initial;text-decoration-color:initial;color:rgb(31, 31, 31);font-family:"Proxima Nova", system-ui, -apple-system, "Segoe UI", Arial, sans-serif;font-size:14px;font-variant-ligatures:normal;orphans:2;widows:2;background-color:rgb(255, 255, 255);" class="qt-">Hi all,<br></div><div style="font-style:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;text-size-adjust:auto;-webkit-text-stroke-width:0px;text-decoration-line:none;text-decoration-style:initial;text-decoration-color:initial;color:rgb(31, 31, 31);font-family:"Proxima Nova", system-ui, -apple-system, "Segoe UI", Arial, sans-serif;font-size:14px;font-variant-ligatures:normal;orphans:2;widows:2;background-color:rgb(255, 255, 255);" class="qt-"><br></div><div style="font-style:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;text-size-adjust:auto;-webkit-text-stroke-width:0px;text-decoration-line:none;text-decoration-style:initial;text-decoration-color:initial;color:rgb(31, 31, 31);font-family:"Proxima Nova", system-ui, -apple-system, "Segoe UI", Arial, sans-serif;font-size:14px;font-variant-ligatures:normal;orphans:2;widows:2;background-color:rgb(255, 255, 255);" class="qt-">I have stages in my compiler that convert e.g. Global Renamed -> Global Generated, etc. where certain constructors are available in certain stages.<span class="qt-"> </span><br></div><div style="font-style:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;text-size-adjust:auto;-webkit-text-stroke-width:0px;text-decoration-line:none;text-decoration-style:initial;text-decoration-color:initial;color:rgb(31, 31, 31);font-family:"Proxima Nova", system-ui, -apple-system, "Segoe UI", Arial, sans-serif;font-size:14px;font-variant-ligatures:normal;orphans:2;widows:2;background-color:rgb(255, 255, 255);" class="qt-"><br></div><div style="font-style:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;text-size-adjust:auto;-webkit-text-stroke-width:0px;text-decoration-line:none;text-decoration-style:initial;text-decoration-color:initial;color:rgb(31, 31, 31);font-family:"Proxima Nova", system-ui, -apple-system, "Segoe UI", Arial, sans-serif;font-size:14px;font-variant-ligatures:normal;orphans:2;widows:2;background-color:rgb(255, 255, 255);" class="qt-">data GlobalRef s where<br></div><div style="font-style:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;text-size-adjust:auto;-webkit-text-stroke-width:0px;text-decoration-line:none;text-decoration-style:initial;text-decoration-color:initial;color:rgb(31, 31, 31);font-family:"Proxima Nova", system-ui, -apple-system, "Segoe UI", Arial, sans-serif;font-size:14px;font-variant-ligatures:normal;orphans:2;widows:2;background-color:rgb(255, 255, 255);" class="qt-"> FromIntegerGlobal :: GlobalRef s<br></div><div style="font-style:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;text-size-adjust:auto;-webkit-text-stroke-width:0px;text-decoration-line:none;text-decoration-style:initial;text-decoration-color:initial;color:rgb(31, 31, 31);font-family:"Proxima Nova", system-ui, -apple-system, "Segoe UI", Arial, sans-serif;font-size:14px;font-variant-ligatures:normal;orphans:2;widows:2;background-color:rgb(255, 255, 255);" class="qt-"> FromDecimalGlobal :: GlobalRef s<br></div><div style="font-style:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;text-size-adjust:auto;-webkit-text-stroke-width:0px;text-decoration-line:none;text-decoration-style:initial;text-decoration-color:initial;color:rgb(31, 31, 31);font-family:"Proxima Nova", system-ui, -apple-system, "Segoe UI", Arial, sans-serif;font-size:14px;font-variant-ligatures:normal;orphans:2;widows:2;background-color:rgb(255, 255, 255);" class="qt-"> InstanceGlobal :: !InstanceName -> GlobalRef Resolved<br></div><div style="font-style:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;text-size-adjust:auto;-webkit-text-stroke-width:0px;text-decoration-line:none;text-decoration-style:initial;text-decoration-color:initial;color:rgb(31, 31, 31);font-family:"Proxima Nova", system-ui, -apple-system, "Segoe UI", Arial, sans-serif;font-size:14px;font-variant-ligatures:normal;orphans:2;widows:2;background-color:rgb(255, 255, 255);" class="qt-"><br></div><div style="font-style:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;text-size-adjust:auto;-webkit-text-stroke-width:0px;text-decoration-line:none;text-decoration-style:initial;text-decoration-color:initial;color:rgb(31, 31, 31);font-family:"Proxima Nova", system-ui, -apple-system, "Segoe UI", Arial, sans-serif;font-size:14px;font-variant-ligatures:normal;orphans:2;widows:2;background-color:rgb(255, 255, 255);" class="qt-">E.g. after type class resolution is done, the InstanceGlobal constructor is available. But instances can't appear in the AST at other stages.<br></div><div style="font-style:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;text-size-adjust:auto;-webkit-text-stroke-width:0px;text-decoration-line:none;text-decoration-style:initial;text-decoration-color:initial;color:rgb(31, 31, 31);font-family:"Proxima Nova", system-ui, -apple-system, "Segoe UI", Arial, sans-serif;font-size:14px;font-variant-ligatures:normal;orphans:2;widows:2;background-color:rgb(255, 255, 255);" class="qt-"><br></div><div style="font-style:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;text-size-adjust:auto;-webkit-text-stroke-width:0px;text-decoration-line:none;text-decoration-style:initial;text-decoration-color:initial;color:rgb(31, 31, 31);font-family:"Proxima Nova", system-ui, -apple-system, "Segoe UI", Arial, sans-serif;font-size:14px;font-variant-ligatures:normal;orphans:2;widows:2;background-color:rgb(255, 255, 255);" class="qt-">In three stages, I've had to copy/paste this code: <br></div><div style="font-style:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;text-size-adjust:auto;-webkit-text-stroke-width:0px;text-decoration-line:none;text-decoration-style:initial;text-decoration-color:initial;color:rgb(31, 31, 31);font-family:"Proxima Nova", system-ui, -apple-system, "Segoe UI", Arial, sans-serif;font-size:14px;font-variant-ligatures:normal;orphans:2;widows:2;background-color:rgb(255, 255, 255);" class="qt-"><br></div><div style="font-style:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;text-size-adjust:auto;-webkit-text-stroke-width:0px;text-decoration-line:none;text-decoration-style:initial;text-decoration-color:initial;color:rgb(31, 31, 31);font-family:"Proxima Nova", system-ui, -apple-system, "Segoe UI", Arial, sans-serif;font-size:14px;font-variant-ligatures:normal;orphans:2;widows:2;background-color:rgb(255, 255, 255);" class="qt-">+ refl =<br></div><div style="font-style:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;text-size-adjust:auto;-webkit-text-stroke-width:0px;text-decoration-line:none;text-decoration-style:initial;text-decoration-color:initial;color:rgb(31, 31, 31);font-family:"Proxima Nova", system-ui, -apple-system, "Segoe UI", Arial, sans-serif;font-size:14px;font-variant-ligatures:normal;orphans:2;widows:2;background-color:rgb(255, 255, 255);" class="qt-">+ case name of<br></div><div style="font-style:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;text-size-adjust:auto;-webkit-text-stroke-width:0px;text-decoration-line:none;text-decoration-style:initial;text-decoration-color:initial;color:rgb(31, 31, 31);font-family:"Proxima Nova", system-ui, -apple-system, "Segoe UI", Arial, sans-serif;font-size:14px;font-variant-ligatures:normal;orphans:2;widows:2;background-color:rgb(255, 255, 255);" class="qt-">+ FromIntegerGlobal -> FromIntegerGlobal<br></div><div style="font-style:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;text-size-adjust:auto;-webkit-text-stroke-width:0px;text-decoration-line:none;text-decoration-style:initial;text-decoration-color:initial;color:rgb(31, 31, 31);font-family:"Proxima Nova", system-ui, -apple-system, "Segoe UI", Arial, sans-serif;font-size:14px;font-variant-ligatures:normal;orphans:2;widows:2;background-color:rgb(255, 255, 255);" class="qt-">+ FromDecimalGlobal -> FromDecimalGlobal<br></div><div style="font-style:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;text-size-adjust:auto;-webkit-text-stroke-width:0px;text-decoration-line:none;text-decoration-style:initial;text-decoration-color:initial;color:rgb(31, 31, 31);font-family:"Proxima Nova", system-ui, -apple-system, "Segoe UI", Arial, sans-serif;font-size:14px;font-variant-ligatures:normal;orphans:2;widows:2;background-color:rgb(255, 255, 255);" class="qt-"><br></div><div style="font-style:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;text-size-adjust:auto;-webkit-text-stroke-width:0px;text-decoration-line:none;text-decoration-style:initial;text-decoration-color:initial;color:rgb(31, 31, 31);font-family:"Proxima Nova", system-ui, -apple-system, "Segoe UI", Arial, sans-serif;font-size:14px;font-variant-ligatures:normal;orphans:2;widows:2;background-color:rgb(255, 255, 255);" class="qt-">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.<br></div><div style="font-style:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;text-size-adjust:auto;-webkit-text-stroke-width:0px;text-decoration-line:none;text-decoration-style:initial;text-decoration-color:initial;color:rgb(31, 31, 31);font-family:"Proxima Nova", system-ui, -apple-system, "Segoe UI", Arial, sans-serif;font-size:14px;font-variant-ligatures:normal;orphans:2;widows:2;background-color:rgb(255, 255, 255);" class="qt-"><br></div><div style="font-style:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;text-size-adjust:auto;-webkit-text-stroke-width:0px;text-decoration-line:none;text-decoration-style:initial;text-decoration-color:initial;color:rgb(31, 31, 31);font-family:"Proxima Nova", system-ui, -apple-system, "Segoe UI", Arial, sans-serif;font-size:14px;font-variant-ligatures:normal;orphans:2;widows:2;background-color:rgb(255, 255, 255);" class="qt-">Is there a handy way already implemented that could derive either this code or this proof for me?<br></div><div style="font-style:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;text-size-adjust:auto;-webkit-text-stroke-width:0px;text-decoration-line:none;text-decoration-style:initial;text-decoration-color:initial;color:rgb(31, 31, 31);font-family:"Proxima Nova", system-ui, -apple-system, "Segoe UI", Arial, sans-serif;font-size:14px;font-variant-ligatures:normal;orphans:2;widows:2;background-color:rgb(255, 255, 255);" class="qt-"><br></div><div style="font-style:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;text-size-adjust:auto;-webkit-text-stroke-width:0px;text-decoration-line:none;text-decoration-style:initial;text-decoration-color:initial;color:rgb(31, 31, 31);font-family:"Proxima Nova", system-ui, -apple-system, "Segoe UI", Arial, sans-serif;font-size:14px;font-variant-ligatures:normal;orphans:2;widows:2;background-color:rgb(255, 255, 255);" class="qt-">Cheers,<br></div><div style="font-style:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;text-size-adjust:auto;-webkit-text-stroke-width:0px;text-decoration-line:none;text-decoration-style:initial;text-decoration-color:initial;color:rgb(31, 31, 31);font-family:"Proxima Nova", system-ui, -apple-system, "Segoe UI", Arial, sans-serif;font-size:14px;font-variant-ligatures:normal;orphans:2;widows:2;background-color:rgb(255, 255, 255);" class="qt-"><br></div><div style="font-style:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;text-size-adjust:auto;-webkit-text-stroke-width:0px;text-decoration-line:none;text-decoration-style:initial;text-decoration-color:initial;color:rgb(31, 31, 31);font-family:"Proxima Nova", system-ui, -apple-system, "Segoe UI", Arial, sans-serif;font-size:14px;font-variant-ligatures:normal;orphans:2;widows:2;background-color:rgb(255, 255, 255);" class="qt-">Chris<br></div><div><span style="font-style:normal;font-variant-caps:normal;font-weight:normal;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;-webkit-text-stroke-width:0px;text-decoration-line:none;text-decoration-style:initial;text-decoration-color:initial;float:none;display:inline !important;" class="qt-"><span class="font" style="font-family:Helvetica;"><span class="size" style="font-size:12px;">_______________________________________________</span></span></span><br></div><div><span style="font-style:normal;font-variant-caps:normal;font-weight:normal;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;-webkit-text-stroke-width:0px;text-decoration-line:none;text-decoration-style:initial;text-decoration-color:initial;float:none;display:inline !important;" class="qt-"><span class="font" style="font-family:Helvetica;"><span class="size" style="font-size:12px;">Haskell-Cafe mailing list</span></span></span><br></div><div><span style="font-style:normal;font-variant-caps:normal;font-weight:normal;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;-webkit-text-stroke-width:0px;text-decoration-line:none;text-decoration-style:initial;text-decoration-color:initial;float:none;display:inline !important;" class="qt-"><span class="font" style="font-family:Helvetica;"><span class="size" style="font-size:12px;">To (un)subscribe, modify options or view archives go to:</span></span></span><br></div><div><a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" style="font-family:Helvetica;font-size:12px;font-style:normal;font-variant-caps:normal;font-weight:normal;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;text-size-adjust:auto;-webkit-text-stroke-width:0px;" class="qt-">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br></div><div><span style="font-style:normal;font-variant-caps:normal;font-weight:normal;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;-webkit-text-stroke-width:0px;text-decoration-line:none;text-decoration-style:initial;text-decoration-color:initial;float:none;display:inline !important;" class="qt-"><span class="font" style="font-family:Helvetica;"><span class="size" style="font-size:12px;">Only members subscribed via the mailman list are allowed to post.</span></span></span><br></div></div></blockquote></div></div></blockquote><div><br></div></body></html>