diff options
| author | Richard Eisenberg <rae@richarde.dev> | 2021-11-22 17:34:32 -0500 |
|---|---|---|
| committer | Simon Peyton Jones <simon.peytonjones@gmail.com> | 2023-01-11 08:30:42 +0000 |
| commit | aed1974e92366ab8e117734f308505684f70cddf (patch) | |
| tree | bbfe7fdd00f1e0ef8dacdcf8d070a07efa38561b /compiler/GHC/Tc/Utils/Unify.hs | |
| parent | 083f701553852c4460159cd6deb2515d3373714d (diff) | |
| download | haskell-wip/T20666.tar.gz | |
Refactor the treatment of loopy superclass dictswip/T20666
This patch completely re-engineers how we deal with loopy superclass
dictionaries in instance declarations. It fixes #20666 and #19690
The highlights are
* Recognise that the loopy-superclass business should use precisely
the Paterson conditions. This is much much nicer. See
Note [Recursive superclasses] in GHC.Tc.TyCl.Instance
* With that in mind, define "Paterson-smaller" in
Note [Paterson conditions] in GHC.Tc.Validity, and the new
data type `PatersonSize` in GHC.Tc.Utils.TcType, along with
functions to compute and compare PatsonSizes
* Use the new PatersonSize stuff when solving superclass constraints
See Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance
* In GHC.Tc.Solver.Monad.lookupInInerts, add a missing call to
prohibitedSuperClassSolve. This was the original cause of #20666.
* Treat (TypeError "stuff") as having PatersonSize zero. See
Note [Paterson size for type family applications] in GHC.Tc.Utils.TcType.
* Treat the head of a Wanted quantified constraint in the same way
as the superclass of an instance decl; this is what fixes #19690.
See GHC.Tc.Solver.Canonical Note [Solving a Wanted forall-constraint]
(Thanks to Matthew Craven for this insight.)
This entailed refactoring the GivenSc constructor of CtOrigin a bit,
to say whether it comes from an instance decl or quantified constraint.
* Some refactoring way in which redundant constraints are reported; we
don't want to complain about the extra, apparently-redundant
constraints that we must add to an instance decl because of the
loopy-superclass thing. I moved some work from GHC.Tc.Errors to
GHC.Tc.Solver.
* Add a new section to the user manual to describe the loopy
superclass issue and what rules it follows.
Diffstat (limited to 'compiler/GHC/Tc/Utils/Unify.hs')
| -rw-r--r-- | compiler/GHC/Tc/Utils/Unify.hs | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/compiler/GHC/Tc/Utils/Unify.hs b/compiler/GHC/Tc/Utils/Unify.hs index 41faa2fece..eea0ed95ef 100644 --- a/compiler/GHC/Tc/Utils/Unify.hs +++ b/compiler/GHC/Tc/Utils/Unify.hs @@ -1477,8 +1477,8 @@ tcSkolemiseScoped ctxt expected_ty thing_inside = do { deep_subsumption <- xoptM LangExt.DeepSubsumption ; let skolemise | deep_subsumption = deeplySkolemise | otherwise = topSkolemise - ; -- This (unpleasant) rec block allows us to pass skol_info to deeplySkolemise; - -- but skol_info can't be built until we have tv_prs + ; -- rec {..}: see Note [Keeping SkolemInfo inside a SkolemTv] + -- in GHC.Tc.Utils.TcType rec { (wrap, tv_prs, given, rho_ty) <- skolemise skol_info expected_ty ; skol_info <- mkSkolemInfo (SigSkol ctxt expected_ty tv_prs) } @@ -1495,7 +1495,9 @@ tcTopSkolemise ctxt expected_ty thing_inside = do { res <- thing_inside expected_ty ; return (idHsWrapper, res) } | otherwise - = do { rec { (wrap, tv_prs, given, rho_ty) <- topSkolemise skol_info expected_ty + = do { -- rec {..}: see Note [Keeping SkolemInfo inside a SkolemTv] + -- in GHC.Tc.Utils.TcType + rec { (wrap, tv_prs, given, rho_ty) <- topSkolemise skol_info expected_ty ; skol_info <- mkSkolemInfo (SigSkol ctxt expected_ty tv_prs) } ; let skol_tvs = map snd tv_prs |