<div dir="ltr">Good idea! I made the change in commit  19b8809c477f4d296cbd6c1736e9a288fdcd6220.<div><br></div><div><br></div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Wed, Nov 13, 2013 at 6:57 PM, Simon Peyton-Jones <span dir="ltr"><<a href="mailto:simonpj@microsoft.com" target="_blank">simonpj@microsoft.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">That is indeed revolting.<br>
<br>
Why not make<br>
    sfMatchFam :: [Type] -> Maybe (CoAxiomRule, [Type], Type)<br>
thus getting rid of the TcCoercion, and baking in the flaky assumption by construction.<br>
<br>
Then I think you can put the whole definition of TcBuiltInSynFamily (with a non-Tc name) into CoAxiom.<br>
<br>
Would that work?<br>
<br>
Simon<br>
<div><div class="h5"><br>
| -----Original Message-----<br>
| From: ghc-commits [mailto:<a href="mailto:ghc-commits-bounces@haskell.org">ghc-commits-bounces@haskell.org</a>] On Behalf Of<br>
| <a href="mailto:git@git.haskell.org">git@git.haskell.org</a><br>
| Sent: 13 November 2013 00:37<br>
| To: <a href="mailto:ghc-commits@haskell.org">ghc-commits@haskell.org</a><br>
| Subject: [commit: ghc] master: Make type-level evaluation work with<br>
| :kind! (b2fa2d4)<br>
|<br>
| Repository : ssh://<a href="http://git@git.haskell.org/ghc" target="_blank">git@git.haskell.org/ghc</a><br>
|<br>
| On branch  : master<br>
| Link       :<br>
| <a href="http://ghc.haskell.org/trac/ghc/changeset/b2fa2d41032882d3cf67be083489c" target="_blank">http://ghc.haskell.org/trac/ghc/changeset/b2fa2d41032882d3cf67be083489c</a><br>
| bcbf9e4ec07/ghc<br>
|<br>
| >---------------------------------------------------------------<br>
|<br>
| commit b2fa2d41032882d3cf67be083489cbcbf9e4ec07<br>
| Author: Iavor S. Diatchki <<a href="mailto:diatchki@galois.com">diatchki@galois.com</a>><br>
| Date:   Tue Nov 12 16:36:23 2013 -0800<br>
|<br>
|     Make type-level evaluation work with :kind!<br>
|<br>
|     The main change is to add a case to `reduceTyFamApp_maybe` to<br>
| evaluate<br>
|     built-in type constructors (e.g., (+), (*), and friends).<br>
|<br>
|     To avoid problems with recursive modules, I moved the definition of<br>
|     TcBuiltInSynFamily from `FamInst` to `FamInstEnv`.  I am still not<br>
| sure if<br>
|     this is the right place.<br>
|<br>
|     There is also a wibble that it'd be nice to fix:<br>
|<br>
|     when we evaluate a built-in type function, using`sfMatchFam`, we<br>
| get<br>
|     a `TcCoercion`.  However, `reduceTyFamApp_maybe` needs a<br>
| `Corecion`.<br>
|     I couldn't find a nice way to convert between the two, so I<br>
| resorted to<br>
|     a bit of hack (marked with `XXX`).<br>
|<br>
|     The hack is that we happen to know that the built-in constructors<br>
| for<br>
|     the type-nat functions always return coercions of shape<br>
| `TcAxiomRuleCo`,<br>
|     with no assumptions, so it easy to convert `TcCoercion` to<br>
| `Coercion`<br>
|     in this one case.  This is enough to make things work, but it is<br>
| clearly<br>
|     a cludge.<br>
|<br>
|<br>
| >---------------------------------------------------------------<br>
|<br>
| b2fa2d41032882d3cf67be083489cbcbf9e4ec07<br>
|  compiler/<a href="http://ghc.mk" target="_blank">ghc.mk</a>                                    |    2 +-<br>
|  compiler/typecheck/FamInst.lhs                     |   27 +-----------<br>
|  compiler/typecheck/TcInteract.lhs                  |    2 +-<br>
|  compiler/typecheck/TcTypeNats.hs                   |    2 +-<br>
|  compiler/types/FamInstEnv.lhs                      |   43<br>
| +++++++++++++++++++-<br>
|  .../FamInst.lhs-boot => types/FamInstEnv.lhs-boot} |    2 +-<br>
|  compiler/types/TyCon.lhs                           |    2 +-<br>
|  7 files changed, 47 insertions(+), 33 deletions(-)<br>
|<br>
| Diff suppressed because of size. To see it, use:<br>
|<br>
|     git diff-tree --root --patch-with-stat --no-color --find-copies-<br>
| harder --ignore-space-at-eol --cc<br>
| b2fa2d41032882d3cf67be083489cbcbf9e4ec07<br>
| _______________________________________________<br>
| ghc-commits mailing list<br>
| <a href="mailto:ghc-commits@haskell.org">ghc-commits@haskell.org</a><br>
| <a href="http://www.haskell.org/mailman/listinfo/ghc-commits" target="_blank">http://www.haskell.org/mailman/listinfo/ghc-commits</a><br>
</div></div>_______________________________________________<br>
ghc-devs mailing list<br>
<a href="mailto:ghc-devs@haskell.org">ghc-devs@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/ghc-devs" target="_blank">http://www.haskell.org/mailman/listinfo/ghc-devs</a><br>
</blockquote></div><br></div>