Make a FlatM monad, and use it to fix #7788 and #10079

Authored by goldfire on Feb 12 2015, 1:33 PM.


Trac Issues

This is as proposed in Trac #7788, comment:13
See the comments on FlatM for more

This first commit should have no change in functionality. It's just
plumbing, for now.

Test Plan


Diff Detail

rGHC Glasgow Haskell Compiler
Lint Skipped
Unit Tests Skipped
Build Status
Buildable 3404
Build 3431: GHC Patch Validation (amd64/Linux)
goldfire updated this revision to Diff 2224.Feb 12 2015, 1:33 PM
goldfire retitled this revision from to Make a FlatM monad, and use it to fix #7788 and #10079.
goldfire updated this object.
goldfire edited the test plan for this revision. (Show Details)
goldfire added reviewers: austin, simonpj.
goldfire updated the Trac tickets for this revision.
goldfire updated this revision to Diff 2390.Mar 8 2015, 12:07 AM

All the rest of the work to fix Trac #7788, Trac #8550, Trac #9554, Trac #10139, and
finish addressing concerns about Trac #10079.

See comment 14 of Trac #7788 for more background.

This has several test case failures, which don't seem easy to resolve. In particular, check out typecheck/should_compile/{T9117_2,tc159}. See also

goldfire updated this revision to Diff 2437.Mar 12 2015, 3:27 PM

Some smallish improvements to this patch. But problems remain!

  • Be more systematic about checking CtLoc depths.
  • New test for Trac #9117.
  • Remove debugging output.
  • Simplify treatment of AppTys in canonicalizer.
  • Tiny refactor around printing EvBinds without double brackets.
  • Testsuite wibbles.
goldfire updated this revision to Diff 2456.Mar 17 2015, 9:59 AM
  • Move newtype-unwrapping *back* to the canonicaliser.
  • Fix compiler errors left over from previous commit.
  • Comments only
  • Do the reflexivity check more eagerly. Fix testsuite wibbles.

This implements Simon's latest idea of checking reflexivity more
eagerly. There's a chance this commit is ready to land.

goldfire updated this revision to Diff 2460.Mar 17 2015, 12:08 PM
  • Performance testsuite wibbles, for the better.
simonpj accepted this revision.Mar 18 2015, 12:47 PM
simonpj edited edge metadata.

If this validates, let's just land it. Richard and I have talked about it quite a bit, and I think it's a real step forward.

I've noted one place where the comments could be improved, but in general I'd just like to check that all the various examples are explained in Notes. For example, we need to handle (N a ~R f a), where f normalises to a newtype. Etc. I forget all the cases we discussed but they are on the ticket or the wiki page you wrote recently. Let's not lose all those insights!

Plus: a good selection of the examples should be regression tests if poss, so that we don't accidentally undo a crucial fix!



Please give some examples that it won't catch.

Also remark that, crucially, it will catch this:

newtype N a = MkN ty
Wanted: N t ~$ ty[t/a]

(provided ty isn't headed with N). We "obviously" should be able to catch such a case (it's a single application of MkN), and provided we catch it, GND will work.

And eager reflexivity is just the ticket. It's not just an ad-hoc fix.

This revision is now accepted and ready to land.Mar 18 2015, 12:47 PM
goldfire closed this revision.Mar 23 2015, 11:30 AM

Committed with c1edbdfd9148ad9f74bfe41e76c524f3e775aaaa.