[commit: ghc] master: Make type-level evaluation work with :kind! (b2fa2d4)

[Iavor Diatchki]

Good idea! I made the change in commit
 19b8809c477f4d296cbd6c1736e9a288fdcd6220.




On Wed, Nov 13, 2013 at 6:57 PM, Simon Peyton-Jones
<simonpj at microsoft.com>wrote:

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