Richard,
I’ve taken another run at the constraint solver. It’s on wip/spj-tc-branch3 (you’ll need a forced update).
I think I can safely commit it to HEAD in the light of your earlier comments, so I’ll do that soon, but I thought I’d just give you (and other ghc-devs) a heads-up.
The two main commits are below. The former is small; the latter is the main event.
Simon
commit 570c3181342386b5cee1862f85a8ebed7d98d712
Author: Simon Peyton Jones
Date: Wed Nov 23 16:00:00 2016 +0000
Allow TyVars in TcTypes
Up to now we've had a rule that a TyVar can't apppear in a type
seen by the type checker; they should all be TcTyVars. But:
a) With -XTypeInType it becomes much harder to exclude them;
see Note [TcTyVars in the typechecker] in TcType.
b) It's unnecessary to exculde them; instead we can just treat
a TyVar just like vanillaSkolemTv.
This is what was causing an ASSERT error in
indexed-types/should_fail/T12041, reported in Trac #12826.
That patch allows a TyVar in a TcType. The most significant
change is to make Var.tcTyVarDetails return vanillaSkolemTv.
In fact it already did, but (a) it was not documented, and
(b) we never exploited it. Now we rely on it.
commit 6e6d93b8b713339dc5f74e8f93e35d0d94014d63
Author: Simon Peyton Jones
Date: Tue Oct 25 17:41:45 2016 +0100
Another major constraint-solver refactoring
This patch takes further my refactoring of the constraint
solver, which I've been doing over the last couple of months
in consultation with Richard.
It fixes a number of tricky bugs that made the constraint
solver actually go into a loop, including
Trac #12526
Trac #12444
Trac #12538
The main changes are these
* Flatten unification variables (fmvs/fuvs) appear on the LHS
of a tvar/tyvar equality; thus
fmv ~ alpha
and not
alpha ~ fmv
See Note [Put flatten unification variables on the left]
in TcUnify. This is implemented by TcUnify.swapOverTyVars.
* Don't reduce a "loopy" CFunEqCan where the fsk appears on
the LHS:
F t1 .. tn ~ fsk
where 'fsk' is free in t1..tn.
See Note [FunEq occurs-check principle] in TcInteract
This neatly stops some infinite loops that people reported;
and it allows us to delete some crufty code in reduce_top_fun_eq.
And it appears to be no loss whatsoever.
As well as fixing loops, ContextStack2 and T5837 both terminate
when they didn't before.
* Previously we generated "derived shadow" constraints from
Wanteds, but we could (and sometimes did; Trac #xxxx) repeatedly
generate a derived shadow from the same Wanted.
A big change in this patch is to have two kinds of Wanteds:
[WD] behaves like a pair of a Wanted and a Derived
[W] behaves like a Wanted only
See CtFlavour and ShadowInfo in TcRnTypes, and the ctev_nosh
field of a Wanted.
This turned out to be a lot simpler. A [WD] gets split into a
[W] and a [D] in TcSMonad.maybeEmitShaodow.
See TcSMonad Note [The improvement story and derived shadows]
* Rather than have a separate inert_model in the InertCans, I've
put the derived equalities back into inert_eqs. We weren't
gaining anything from a separate field.
* Previously we had a mode for the constraint solver in which it
would more aggressively solve Derived constraints; it was used
for simplifying the context of a 'deriving' clause, or a 'default'
delcaration, for example.
But the complexity wasn't worth it; now I just make proper Wanted
constraints. See TcMType.cloneWC
* Don't generate injectivity improvement for Givens; see
Note [No FunEq improvement for Givens] in TcInteract
* solveSimpleWanteds leaves the insolubles in-place rather than
returning them. Simpler.
I also did lots of work on comments.
