Commit 3cfee57a authored by Richard Eisenberg's avatar Richard Eisenberg
Browse files

Remove solveSomeEqualities

I had thought that it was necessary to solve kind-level equalities
before validity-checking a type, but I was wrong. This patch simply
deletes code. Hooray!
parent 02cc8f0c
......@@ -53,7 +53,7 @@ import TcMType
import TcValidity
import TcUnify
import TcIface
import TcSimplify ( solveEqualities, solveSomeEqualities )
import TcSimplify ( solveEqualities )
import TcType
import TcHsSyn( zonkSigType )
import Inst ( tcInstBinders, tcInstBindersX, tcInstBinderX )
......@@ -221,14 +221,13 @@ tc_hs_sig_type_and_gen sig_ty kind
; kindGeneralizeType ty }
tc_hs_sig_type :: LHsSigType Name -> Kind -> TcM Type
-- May emit constraints; uses solveSomeEqualities internally.
-- May emit constraints
-- No zonking or validity checking
tc_hs_sig_type = tc_hs_sig_type_x solveSomeEqualities
tc_hs_sig_type = tc_hs_sig_type_x id
-- Version of tc_hs_sig_type parameterized over how it should solve
-- equalities
tc_hs_sig_type_x :: (forall a. TcM a -> TcM a) -- solveSomeEqualities
-- or solveEqualities
tc_hs_sig_type_x :: (forall a. TcM a -> TcM a) -- id or solveEqualities
-> LHsSigType Name -> Kind
-> TcM Type
tc_hs_sig_type_x solve (HsIB { hsib_body = hs_ty
......@@ -288,10 +287,7 @@ tcHsVectInst ty
tcHsTypeApp :: LHsWcType Name -> Kind -> TcM Type
tcHsTypeApp wc_ty kind
| HsWC { hswc_wcs = sig_wcs, hswc_body = hs_ty } <- wc_ty
-- use solveSomeEqualities b/c we are in an expression
-- See Note [solveEqualities vs solveSomeEqualities] in TcSimplify
= do { ty <- solveSomeEqualities $
tcWildCardBindersX newWildTyVar sig_wcs $ \ _ ->
= do { ty <- tcWildCardBindersX newWildTyVar sig_wcs $ \ _ ->
tcCheckLHsType hs_ty kind
; ty <- zonkTcType ty
; checkValidType TypeAppCtxt ty
......@@ -1772,25 +1768,6 @@ It isn't essential for correctness.
* *
************************************************************************
Note [Solving equalities in partial type signatures]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We treat a partial type signature as a "shape constraint" to impose on
the term:
* We make no attempt to kind-generalise it
* We instantiate the explicit and implicit foralls with SigTvs
* We instantiate the wildcards with meta tyvars
We /do/ call solveSomeEqualities, and then zonk to propagate the result of
solveSomeEqualities, mainly so that functions like matchExpectedFunTys will
be able to decompose the type, and hence higher-rank signatures will
work. Ugh! For example
f :: (forall a. a->a) -> _
f x = (x True, x 'c')
Because we are not generalizing, etc., solveSomeEqualities is appropriate.
See also Note [solveEqualities vs solveSomeEqualities] in TcSimplify.
-}
tcHsPartialSigType
......@@ -1807,9 +1784,7 @@ tcHsPartialSigType ctxt sig_ty
, (explicit_hs_tvs, L _ hs_ctxt, hs_tau) <- splitLHsSigmaTy hs_ty
= addSigCtxt ctxt hs_ty $
do { (implicit_tvs, (wcs, wcx, explicit_tvs, theta, tau))
<- -- See Note [Solving equalities in partial type signatures]
solveSomeEqualities $
tcWildCardBindersX newWildTyVar sig_wcs $ \ wcs ->
<- tcWildCardBindersX newWildTyVar sig_wcs $ \ wcs ->
tcImplicitTKBndrsX new_implicit_tv implicit_hs_tvs $
tcExplicitTKBndrsX newSigTyVar explicit_hs_tvs $ \ explicit_tvs ->
do { -- Instantiate the type-class context; but if there
......@@ -1869,9 +1844,7 @@ tcHsPatSigType ctxt sig_ty
, HsIB { hsib_vars = sig_vars, hsib_body = hs_ty } <- ib_ty
= addSigCtxt ctxt hs_ty $
do { (implicit_tvs, (wcs, sig_ty))
<- -- See Note [Solving equalities in partial type signatures]
solveSomeEqualities $
tcWildCardBindersX newWildTyVar sig_wcs $ \ wcs ->
<- tcWildCardBindersX newWildTyVar sig_wcs $ \ wcs ->
tcImplicitTKBndrsX new_implicit_tv sig_vars $
do { sig_ty <- tcHsOpenType hs_ty
; return ((wcs, sig_ty), allBoundVariables sig_ty) }
......
......@@ -6,7 +6,7 @@ module TcSimplify(
simplifyAmbiguityCheck,
simplifyDefault,
simplifyTop, simplifyTopImplic, captureTopConstraints,
simplifyInteractive, solveSomeEqualities, solveEqualities,
simplifyInteractive, solveEqualities,
simplifyWantedsTcM,
tcCheckSatisfiability,
......@@ -128,68 +128,8 @@ simplifyTop wanteds
; return (evBindMapBinds binds1 `unionBags` binds2) }
{- Note [solveEqualities vs solveSomeEqualities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When kind-checking a type, GHC might generate equality constraints. (We know
it will generate only *equalities*, not e.g. class constraints, because types
don't contain class methods.) What should we do with these constraints?
Before we can effectively zonk, generalize, or validity-check a type, we need
to solve these equalities. The functions solveEqualities and solveSomeEqualities
do precisely this.
solveEqualities solves *all* equality constraints generated by the thing_inside.
If any constraints are unable to be solved, fail. This is appropriate for a top-
level type where we absolutely must, say, generalize right away. For example,
in
data G (a :: k) where
MkG :: G Maybe
The type G Maybe will make equality constraints that must be handled pronto.
solveSomeEqualities, on the other hand, does the best it can, re-emitting those
constraints it can't solve. This is appropriate when, for example, a type
appears in the middle of an expression (either a type annotation or a visible
type application) and there may be givens that have a bearing on whether or
not a type-level equality is soluble. The use of solveEqualities in an type
annotation is what gave rise to #13337.
Why have solveSomeEqualities at all, instead of just letting all equality
constraints go where all the other constraints do? Because we want to nail what
equalities we can before doing validity checking. Otherwise, the validity checker
may see casts and other nonsense in what should be a simple type.
How to choose between these?
Use solveEqualities when any of the following apply:
* you are about to kind-generalize
* you are about to call zonkTcTypeToType
* you are in a top-level context, not inside of any expression
Use solveSomeEqualities when:
* none of the above applies
-}
-- | Type-check a thing that emits only equality constraints, then
-- solve as many constraints as possible. Re-emits any unsolved constraints.
-- Never fails. This is useful when you're in a context where emitting
-- constraints is a good idea (e.g., in a expression type signature) but
-- you also want to use a function from TcValidity. TcValidity wants the
-- type to be as well-defined as possible. So this does what it can.
-- See also Note [solveEqualities vs solveSomeEqualities]
solveSomeEqualities :: TcM a -> TcM a
solveSomeEqualities thing_inside
= do { (result, wanted) <- captureConstraints thing_inside
; traceTc "solveSomeEqualities {" $ text "wanted = " <+> ppr wanted
; final_wc <- runTcSEqualities $ simpl_top wanted
; traceTc "End solveESomequalities }" empty
; emitConstraints final_wc
; return result }
-- | Type-check a thing that emits only equality constraints, then
-- solve those constraints. Fails outright if there is trouble.
-- See also Note [solveEqualities vs solveSomeEqualities]
solveEqualities :: TcM a -> TcM a
solveEqualities thing_inside
= checkNoErrs $ -- See Note [Fail fast on kind errors]
......
......@@ -5,10 +5,3 @@ T11976.hs:7:20: error:
• In an expression type signature: Lens _ _ _
In the expression: undefined :: Lens _ _ _
In an equation for ‘foo’: foo = undefined :: Lens _ _ _
T11976.hs:7:20: error:
• Expecting one fewer arguments to ‘Lens w0 w1’
Expected kind ‘k0 -> *’, but ‘Lens w0 w1’ has kind ‘*’
• In the type ‘Lens _ _ _’
In an expression type signature: Lens _ _ _
In the expression: undefined :: Lens _ _ _
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment