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

[Simon Peyton-Jones]

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