[commit: ghc] wip/rae-new-coercible: Rewrite `Coercible` solver (1d29739)
git at git.haskell.org
git at git.haskell.org
Tue Dec 2 20:43:51 UTC 2014
Repository : ssh://git@git.haskell.org/ghc
On branch : wip/rae-new-coercible
Link : http://ghc.haskell.org/trac/ghc/changeset/1d29739aa690a43befd98b30223dabd93168ba5c/ghc
>---------------------------------------------------------------
commit 1d29739aa690a43befd98b30223dabd93168ba5c
Author: Richard Eisenberg <eir at cis.upenn.edu>
Date: Mon Dec 1 10:28:34 2014 -0500
Rewrite `Coercible` solver
Summary:
This is a rewrite of the algorithm to solve for Coercible "instances".
A preliminary form of these ideas is at
https://ghc.haskell.org/trac/ghc/wiki/Design/NewCoercibleSolver
The basic idea here is that the `EqPred` constructor of `PredTree`
now is parameterised by a new type `EqRel` (where
`data EqRel = NomEq | ReprEq`). Thus, every equality constraint can
now talk about nominal equality (the usual case) or representational
equality (the `Coercible` case).
This is a change from the previous
behavior where `Coercible` was just considered a regular class with
a special case in `matchClassInst`.
Because of this change, representational equalities are now
canonicalized just like nominal ones, allowing more equalities
to be solved -- in particular, the case at the top of #9117.
A knock-on effect is that the flattener must be aware of the
choice of equality relation, because the inert set now stores
both representational inert equalities alongside the nominal
inert equalities. Of course, we can use representational equalities
to rewrite only within another representational equality --
thus the parameterization of the flattener.
A nice side effect of this change is that I've introduced a new
type `CtFlavour`, which tracks G vs. W vs. D, removing some ugliness
in the flattener.
Test Plan: testsuite, a new T9117, and others TBD
Reviewers: simonpj, austin, nomeata
Subscribers: carter, thomie
Differential Revision: https://phabricator.haskell.org/D546
GHC Trac Issues: #9117
>---------------------------------------------------------------
1d29739aa690a43befd98b30223dabd93168ba5c
compiler/typecheck/TcCanonical.lhs | 0
compiler/typecheck/TcErrors.lhs | 0
compiler/typecheck/TcFlatten.lhs | 0
compiler/typecheck/TcSMonad.lhs | 11 ++++++++---
compiler/typecheck/TcValidity.lhs | 0
compiler/types/Coercion.hs | 2 --
6 files changed, 8 insertions(+), 5 deletions(-)
diff --git a/compiler/typecheck/TcSMonad.lhs b/compiler/typecheck/TcSMonad.lhs
index 80ff73b..c9b979d 100644
--- a/compiler/typecheck/TcSMonad.lhs
+++ b/compiler/typecheck/TcSMonad.lhs
@@ -818,7 +818,8 @@ splitInertCans iCans = (given,derived,wanted)
where
allCts = foldDicts (:) (inert_dicts iCans)
$ foldFunEqs (:) (inert_funeqs iCans)
- $ concat (varEnvElts (inert_eqs iCans))
+ $ concat (varEnvElts (inert_eqs iCans) ++
+ varEnvElts (inert_repr_eqs iCans))
(derived,other) = partition isDerivedCt allCts
(wanted,given) = partition isWantedCt other
@@ -838,8 +839,12 @@ removeInertCt is ct =
CFunEqCan { cc_fun = tf, cc_tyargs = tys } ->
is { inert_funeqs = delFunEq (inert_funeqs is) tf tys }
- CTyEqCan { cc_tyvar = x, cc_rhs = ty } ->
- is { inert_eqs = delTyEq (inert_eqs is) x ty }
+ CTyEqCan { cc_tyvar = x, cc_rhs = ty, cc_eq_rel = NomEq } ->
+ is { inert_eqs = delTyEq (inert_eqs is) x ty
+ , inert_repr_eqs = delTyEq (inert_repr_eqs is) x ty }
+
+ CTyEqCan { cc_tyvar = x, cc_rhs = ty, cc_eq_rel = ReprEq } ->
+ is { inert_repr_eqs = delTyEq (inert_repr_eqs is) x ty }
CIrredEvCan {} -> panic "removeInertCt: CIrredEvCan"
CNonCanonical {} -> panic "removeInertCt: CNonCanonical"
diff --git a/compiler/types/Coercion.hs b/compiler/types/Coercion.hs
index bb39207..2b5081a 100644
--- a/compiler/types/Coercion.hs
+++ b/compiler/types/Coercion.hs
@@ -1994,5 +1994,3 @@ instance IsCoercion Coercion where
gMkUnbranchedAxInstCo :: IsCoercion co
=> Role -> CoAxiom Unbranched -> [Type] -> co
gMkUnbranchedAxInstCo r ax = gMkAxInstCo r ax 0
-
-\end{code}
More information about the ghc-commits
mailing list