Proposed changes to typechecker plugins API

[Richard Eisenberg]

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#Definingtypefamilies

Richard


On May 27, 2015, at 10:13 AM, Eric Seidel <eric at seidel.io> wrote:

> 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#EmbeddingCoreExprinEvTerm
> 
> 
> 
> 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.10changestoTcPluginMAPI
>> 
>> Questions/review/comments very welcome.
>> 
>> Adam
>> 
>> 
>> -- 
>> Adam Gundry, Haskell Consultant
>> Well-Typed LLP, http://www.well-typed.com/
>> _______________________________________________
>> ghc-devs mailing list
>> ghc-devs at haskell.org
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs