Proposed changes to typechecker plugins API

Hi devs, I thought I should flag up some proposed changes relating to typechecker plugins, which Christiaan, Iavor and I have been discussing. The quick summary: * make it possible for plugins to create constraints (Phab:D909); * make it easier for plugins to define special type families; * embed CoreExpr in EvTerm. For more details, see the wiki page: https://ghc.haskell.org/trac/ghc/wiki/Plugins/TypeChecker#Post-7.10changesto... Questions/review/comments very welcome. Adam -- Adam Gundry, Haskell Consultant Well-Typed LLP, http://www.well-typed.com/

Hi Adam, I like the addition of the new* functions for creating constraints, that should make for a much nicer API than dealing directly with the CtEvidence constructors! I'm not so convinced however about embedding arbitrary CoreExprs in EvTerms. First of all, it feels a bit strange to generate CoreExprs before the desugarer (and we would have to add a `MonadThings TcPluginM` instance to generate Integer and String CoreExprs). But more importantly, based on your wiki page [1], it sounds like what we really want is a nice API for creating dictionaries. Eric [1]: https://ghc.haskell.org/trac/ghc/wiki/Plugins/TypeChecker#EmbeddingCoreExpri... On Wed, May 27, 2015, at 01:33, Adam Gundry wrote:
Hi devs,
I thought I should flag up some proposed changes relating to typechecker plugins, which Christiaan, Iavor and I have been discussing. The quick summary:
* make it possible for plugins to create constraints (Phab:D909);
* make it easier for plugins to define special type families;
* embed CoreExpr in EvTerm.
For more details, see the wiki page: https://ghc.haskell.org/trac/ghc/wiki/Plugins/TypeChecker#Post-7.10changesto...
Questions/review/comments very welcome.
Adam
-- Adam Gundry, Haskell Consultant Well-Typed LLP, http://www.well-typed.com/ _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

I like the general directional of travel here, with two specific points to make:
- Unlike Eric, I like embedding CoreExprs directly into EvTerms. Yes, it's a little funny to do so before desugaring, but there's precedent for such things (like embedding Coercions into TcCoercions and Types into HsTypes). If a close reading of the code indicates it would be better, this could be changed to embedding a HsExpr Id into EvTerms -- perhaps there would be less impedance mismatch this way. Then, the current special-case constructors become plain old functions, and we get nice future expandability.
- There's something getting smellier and smellier about type families. Here is the comment I posted to the wiki page, at the end of the "Defining type families" section [1]:
---
This makes me uncomfortable, in exactly the same way that I was made to feel uncomfortable in the comments starting with comment:4:ticket:9840. The fact that the new, (what I will call) external type families will behave differently than internal type families is further evidence that something is amiss. (The difference in behavior I'm referring to is the difference between matchFam and reduceTyFamApp_maybe.) This, of course, ties into #9636 as well and to some of the more esoteric issues that cropped up while working on #6018/​Phab:D202 and perhaps even #10327. I would love to approach this problem with the idea of making broader changes instead of looking for a minimal change just to support typechecker plugins better.
---
I don't have any grand ideas at the moment about this. But I do strongly feel that stepping back and considering the larger question of "What are type families?" would benefit us.
[1]: https://ghc.haskell.org/trac/ghc/wiki/Plugins/TypeChecker#Definingtypefamili...
Richard
On May 27, 2015, at 10:13 AM, Eric Seidel
Hi Adam,
I like the addition of the new* functions for creating constraints, that should make for a much nicer API than dealing directly with the CtEvidence constructors!
I'm not so convinced however about embedding arbitrary CoreExprs in EvTerms. First of all, it feels a bit strange to generate CoreExprs before the desugarer (and we would have to add a `MonadThings TcPluginM` instance to generate Integer and String CoreExprs).
But more importantly, based on your wiki page [1], it sounds like what we really want is a nice API for creating dictionaries.
Eric
[1]: https://ghc.haskell.org/trac/ghc/wiki/Plugins/TypeChecker#EmbeddingCoreExpri...
On Wed, May 27, 2015, at 01:33, Adam Gundry wrote:
Hi devs,
I thought I should flag up some proposed changes relating to typechecker plugins, which Christiaan, Iavor and I have been discussing. The quick summary:
* make it possible for plugins to create constraints (Phab:D909);
* make it easier for plugins to define special type families;
* embed CoreExpr in EvTerm.
For more details, see the wiki page: https://ghc.haskell.org/trac/ghc/wiki/Plugins/TypeChecker#Post-7.10changesto...
Questions/review/comments very welcome.
Adam
-- Adam Gundry, Haskell Consultant Well-Typed LLP, http://www.well-typed.com/ _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
participants (3)
-
Adam Gundry
-
Eric Seidel
-
Richard Eisenberg