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

Good idea! I made the change in commit 19b8809c477f4d296cbd6c1736e9a288fdcd6220. On Wed, Nov 13, 2013 at 6:57 PM, Simon Peyton-Jones 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@haskell.org] On Behalf Of | git@git.haskell.org | Sent: 13 November 2013 00:37 | To: ghc-commits@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 | 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@haskell.org | http://www.haskell.org/mailman/listinfo/ghc-commits _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs