Commit 5770029a authored by Simon Peyton Jones's avatar Simon Peyton Jones

Simon's major commit to re-engineer the constraint solver

The driving change is this:

* The canonical CFunEqCan constraints now have the form
       [G] F xis ~ fsk
       [W] F xis ~ fmv
  where fsk is a flatten-skolem, and fmv is a flatten-meta-variable
  Think of them as the name of the type-function application

See Note [The flattening story] in TcFlatten.  A flatten-meta-variable
is distinguishable by its MetaInfo of FlatMetaTv

This in turn led to an enormous cascade of other changes, which simplify
and modularise the constraint solver.  In particular:

* Basic data types
    * I got rid of inert_solved_funeqs altogether. It serves no useful
      role that inert_flat_cache does not solve.

    * I added wl_implics to the WorkList, as a convenient place to
      accumulate newly-emitted implications; see Note [Residual
      implications] in TcSMonad.

    * I eliminated tcs_ty_binds altogether. These were the bindings
      for unification variables that we have now solved by
      unification.  We kept them in a finite map and did the
      side-effecting unification later.  But in cannonicalisation we
      had to look up in the side-effected mutable tyvars anyway, so
      nothing was being gained.

      Our original idea was that the solver would be pure, and would
      be a no-op if you discarded its results, but this was already
      not-true for implications since we update their evidence
      bindings in an imperative way.  So rather than the uneasy
      compromise, it's now clearly imperative!

* I split out the flatten/unflatten code into a new module, TcFlatten

* I simplified and articulated explicitly the (rather hazy) invariants
  for the inert substitution inert_eqs.  See Note [eqCanRewrite] and
  See Note [Applying the inert substitution] in TcFlatten

* Unflattening is now done (by TcFlatten.unflatten) after solveFlats,
  before solving nested implications.  This turned out to simplify a
  lot of code. Previously, unflattening was done as part of zonking, at
  the very very end.

    * Eager unflattening allowed me to remove the unpleasant ic_fsks
      field of an Implication (hurrah)

    * Eager unflattening made the TcSimplify.floatEqualities function
      much simpler (just float equalities looking like a ~ ty, where a
      is an untouchable meta-tyvar).

    * Likewise the idea of "pushing wanteds in as givens" could be
      completely eliminated.

* I radically simplified the code that determines when there are
  'given' equalities, and hence whether we can float 'wanted' equalies
  out.  See TcSMonad.getNoGivenEqs, and Note [When does an implication
  have given equalities?].

  This allowed me to get rid of the unpleasant inert_no_eqs flag in InertCans.

* As part of this given-equality stuff, I fixed Trac #9211. See Note
  [Let-bound skolems] in TcSMonad

* Orientation of tyvar/tyvar equalities (a ~ b) was partly done during
  canonicalisation, but then repeated in the spontaneous-solve stage
  (trySpontaneousSolveTwoWay). Now it is done exclusively during
  canonicalisation, which keeps all the code in one place.  See
  Note [Canonical orientation for tyvar/tyvar equality constraints]
  in TcCanonical
parent ce9d6f25
......@@ -406,6 +406,7 @@ Library
TcUnify
TcInteract
TcCanonical
TcFlatten
TcSMonad
TcTypeNats
TcSplice
......
......@@ -2,22 +2,13 @@ ToDo:
* get rid of getEvTerm?
* Float only CTyEqCans. kind-incompatible things should be CNonCanonical,
so they won't float and generate a duplicate kind-unify message
Then we can stop disabling floating when there are insolubles,
and that will improve mc21 etc
* Note [Do not add duplicate derived isols]
This mostly doesn't apply now, except for the fundeps
* inert_funeqs, inert_eqs: keep only the CtEvidence.
They are all CFunEqCans, CTyEqCans
* remove/rewrite TcMType Note [Unflattening while zonking]
* Consider individual data tpyes for CFunEqCan etc
* Collapes CNonCanonical and CIrredCan
Remaining errors
============================
Unexpected failures:
......
......@@ -590,13 +590,12 @@ addClsInstsErr herald ispecs
\begin{code}
---------------- Getting free tyvars -------------------------
tyVarsOfCt :: Ct -> TcTyVarSet
-- NB: the
tyVarsOfCt (CTyEqCan { cc_tyvar = tv, cc_rhs = xi }) = extendVarSet (tyVarsOfType xi) tv
tyVarsOfCt (CFunEqCan { cc_tyargs = tys, cc_rhs = xi }) = tyVarsOfTypes (xi:tys)
tyVarsOfCt (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys
tyVarsOfCt (CIrredEvCan { cc_ev = ev }) = tyVarsOfType (ctEvPred ev)
tyVarsOfCt (CHoleCan { cc_ev = ev }) = tyVarsOfType (ctEvPred ev)
tyVarsOfCt (CNonCanonical { cc_ev = ev }) = tyVarsOfType (ctEvPred ev)
tyVarsOfCt (CTyEqCan { cc_tyvar = tv, cc_rhs = xi }) = extendVarSet (tyVarsOfType xi) tv
tyVarsOfCt (CFunEqCan { cc_tyargs = tys, cc_fsk = fsk }) = extendVarSet (tyVarsOfTypes tys) fsk
tyVarsOfCt (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys
tyVarsOfCt (CIrredEvCan { cc_ev = ev }) = tyVarsOfType (ctEvPred ev)
tyVarsOfCt (CHoleCan { cc_ev = ev }) = tyVarsOfType (ctEvPred ev)
tyVarsOfCt (CNonCanonical { cc_ev = ev }) = tyVarsOfType (ctEvPred ev)
tyVarsOfCts :: Cts -> TcTyVarSet
tyVarsOfCts = foldrBag (unionVarSet . tyVarsOfCt) emptyVarSet
......@@ -610,10 +609,10 @@ tyVarsOfWC (WC { wc_flat = flat, wc_impl = implic, wc_insol = insol })
tyVarsOfImplic :: Implication -> TyVarSet
-- Only called on *zonked* things, hence no need to worry about flatten-skolems
tyVarsOfImplic (Implic { ic_skols = skols, ic_fsks = fsks
, ic_given = givens, ic_wanted = wanted })
tyVarsOfImplic (Implic { ic_skols = skols
, ic_given = givens, ic_wanted = wanted })
= (tyVarsOfWC wanted `unionVarSet` tyVarsOfTypes (map evVarPred givens))
`delVarSetList` skols `delVarSetList` fsks
`delVarSetList` skols
tyVarsOfBag :: (a -> TyVarSet) -> Bag a -> TyVarSet
tyVarsOfBag tvs_of = foldrBag (unionVarSet . tvs_of) emptyVarSet
......
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
o%
%
% (c) The University of Glasgow 2006
% (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
%
......@@ -53,7 +53,7 @@ module TcMType (
zonkTcTyVarBndr, zonkTcType, zonkTcTypes, zonkTcThetaType,
zonkTcKind, defaultKindVarToStar,
zonkEvVar, zonkWC, zonkFlats, zonkId, zonkCt, zonkCts, zonkSkolemInfo,
zonkEvVar, zonkWC, zonkFlats, zonkId, zonkCt, zonkSkolemInfo,
tcGetGlobalTyVars,
) where
......@@ -63,10 +63,8 @@ module TcMType (
-- friends:
import TypeRep
import TcType
import TcEvidence
import Type
import Class
import TyCon
import Var
-- others:
......@@ -313,9 +311,10 @@ newMetaTyVar meta_info kind
= do { uniq <- newUnique
; let name = mkTcTyVarName uniq s
s = case meta_info of
PolyTv -> fsLit "s"
TauTv -> fsLit "t"
SigTv -> fsLit "a"
PolyTv -> fsLit "s"
TauTv -> fsLit "t"
FlatMetaTv -> fsLit "fmv"
SigTv -> fsLit "a"
; details <- newMetaDetails meta_info
; return (mkTcTyVar name kind details) }
......@@ -595,6 +594,7 @@ skolemiseUnboundMetaTyVar tv details
final_name = mkInternalName uniq (getOccName tv) span
final_tv = mkTcTyVar final_name final_kind details
; traceTc "Skolemising" (ppr tv <+> ptext (sLit ":=") <+> ppr final_tv)
; writeMetaTyVar tv (mkTyVarTy final_tv)
; return final_tv }
\end{code}
......@@ -667,7 +667,7 @@ a \/\a in the final result but all the occurrences of a will be zonked to ()
%************************************************************************
%* *
Zonking
Zonking types
%* *
%************************************************************************
......@@ -686,8 +686,6 @@ tcGetGlobalTyVars
where
\end{code}
----------------- Type variables
\begin{code}
zonkTcTypeAndFV :: TcType -> TcM TyVarSet
-- Zonk a type and take its free variables
......@@ -728,13 +726,15 @@ zonkTcPredType :: TcPredType -> TcM TcPredType
zonkTcPredType = zonkTcType
\end{code}
--------------- Constraints
%************************************************************************
%* *
Zonking constraints
%* *
%************************************************************************
\begin{code}
zonkImplication :: Implication -> TcM (Bag Implication)
zonkImplication implic@(Implic { ic_untch = untch
, ic_binds = binds_var
, ic_skols = skols
zonkImplication implic@(Implic { ic_skols = skols
, ic_given = given
, ic_wanted = wanted
, ic_info = info })
......@@ -742,12 +742,11 @@ zonkImplication implic@(Implic { ic_untch = untch
-- as Trac #7230 showed
; given' <- mapM zonkEvVar given
; info' <- zonkSkolemInfo info
; wanted' <- zonkWCRec binds_var untch wanted
; wanted' <- zonkWCRec wanted
; if isEmptyWC wanted'
then return emptyBag
else return $ unitBag $
implic { ic_fsks = [] -- Zonking removes all FlatSkol tyvars
, ic_skols = skols'
implic { ic_skols = skols'
, ic_given = given'
, ic_wanted = wanted'
, ic_info = info' } }
......@@ -757,105 +756,25 @@ zonkEvVar var = do { ty' <- zonkTcType (varType var)
; return (setVarType var ty') }
zonkWC :: EvBindsVar -- May add new bindings for wanted family equalities in here
-> WantedConstraints -> TcM WantedConstraints
zonkWC binds_var wc
= do { untch <- getUntouchables
; zonkWCRec binds_var untch wc }
zonkWC :: WantedConstraints -> TcM WantedConstraints
zonkWC wc = zonkWCRec wc
zonkWCRec :: EvBindsVar
-> Untouchables
-> WantedConstraints -> TcM WantedConstraints
zonkWCRec binds_var untch (WC { wc_flat = flat, wc_impl = implic, wc_insol = insol })
= do { flat' <- zonkFlats binds_var untch flat
zonkWCRec :: WantedConstraints -> TcM WantedConstraints
zonkWCRec (WC { wc_flat = flat, wc_impl = implic, wc_insol = insol })
= do { flat' <- zonkFlats flat
; implic' <- flatMapBagM zonkImplication implic
; insol' <- zonkCts insol -- No need to do the more elaborate zonkFlats thing
; insol' <- zonkFlats insol
; return (WC { wc_flat = flat', wc_impl = implic', wc_insol = insol' }) }
zonkFlats :: EvBindsVar -> Untouchables -> Cts -> TcM Cts
-- This zonks and unflattens a bunch of flat constraints
-- See Note [Unflattening while zonking]
zonkFlats binds_var untch cts
= do { -- See Note [How to unflatten]
cts <- foldrBagM unflatten_one emptyCts cts
; zonkCts cts }
where
unflatten_one orig_ct cts
= do { zct <- zonkCt orig_ct -- First we need to fully zonk
; mct <- try_zonk_fun_eq orig_ct zct -- Then try to solve if family equation
; return $ maybe cts (`consBag` cts) mct }
try_zonk_fun_eq orig_ct zct -- See Note [How to unflatten]
| EqPred ty_lhs ty_rhs <- classifyPredType (ctPred zct)
-- NB: zonking de-classifies the constraint,
-- so we can't look for CFunEqCan
, Just tv <- getTyVar_maybe ty_rhs
, ASSERT2( not (isFloatedTouchableMetaTyVar untch tv), ppr tv )
isTouchableMetaTyVar untch tv
, not (isSigTyVar tv) || isTyVarTy ty_lhs -- Never unify a SigTyVar with a non-tyvar
, typeKind ty_lhs `tcIsSubKind` tyVarKind tv -- c.f. TcInteract.trySpontaneousEqOneWay
, not (tv `elemVarSet` tyVarsOfType ty_lhs) -- Do not construct an infinite type
= ASSERT2( case tcSplitTyConApp_maybe ty_lhs of { Just (tc,_) -> isSynFamilyTyCon tc; _ -> False }, ppr orig_ct )
do { writeMetaTyVar tv ty_lhs
; let evterm = EvCoercion (mkTcNomReflCo ty_lhs)
evvar = ctev_evar (cc_ev zct)
; when (isWantedCt orig_ct) $ -- Can be derived (Trac #8129)
addTcEvBind binds_var evvar evterm
; traceTc "zonkFlats/unflattening" $
vcat [ text "zct = " <+> ppr zct,
text "binds_var = " <+> ppr binds_var ]
; return Nothing }
| otherwise
= return (Just zct)
\end{code}
Note [Unflattening while zonking]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
A bunch of wanted constraints could contain wanted equations of the form
(F taus ~ alpha) where alpha is either an ordinary unification variable, or
a flatten unification variable.
These are ordinary wanted constraints and can/should be solved by
ordinary unification alpha := F taus. However the constraint solving
algorithm does not do that, as their 'inert' form is F taus ~ alpha.
Hence, we need an extra step to 'unflatten' these equations by
performing unification. This unification, if it happens at the end of
constraint solving, cannot produce any more interactions in the
constraint solver so it is safe to do it as the very very last step.
We choose therefore to do it during zonking, in the function
zonkFlats. This is in analogy to the zonking of given "flatten skolems"
which are eliminated in favor of the underlying type that they are
equal to.
Note that, because we now have to affect *evidence* while zonking
(setting some evidence binds to identities), we have to pass to the
zonkWC function an evidence variable to collect all the extra
variables.
Note [How to unflatten]
~~~~~~~~~~~~~~~~~~~~~~~
How do we unflatten during zonking. Consider a bunch of flat constraints.
Consider them one by one. For each such constraint C
* Zonk C (to apply current substitution)
* If C is of form F tys ~ alpha,
where alpha is touchable
and alpha is not mentioned in tys
then unify alpha := F tys
and discard C
After processing all the flat constraints, zonk them again to propagate
the inforamtion from later ones to earlier ones. Eg
Start: (F alpha ~ beta, G Int ~ alpha)
Then we get beta := F alpha
alpha := G Int
but we must apply the second unification to the first constraint.
\begin{code}
zonkCts :: Cts -> TcM Cts
zonkCts = mapBagM zonkCt
zonkFlats :: Cts -> TcM Cts
zonkFlats cts = do { cts' <- mapBagM zonkCt' cts
; traceTc "zonkFlats done:" (ppr cts')
; return cts' }
zonkCt' :: Ct -> TcM Ct
zonkCt' ct = zonkCt ct
zonkCt :: Ct -> TcM Ct
zonkCt ct@(CHoleCan { cc_ev = ev })
......
......@@ -44,8 +44,8 @@ module TcRnTypes(
ArrowCtxt(NoArrowCtxt), newArrowScope, escapeArrowScope,
-- Canonical constraints
Xi, Ct(..), Cts, emptyCts, andCts, andManyCts, dropDerivedWC,
singleCt, listToCts, ctsElts, extendCts, extendCtsList,
Xi, Ct(..), Cts, emptyCts, andCts, andManyCts, pprCts,
singleCt, listToCts, ctsElts, consCts, snocCts, extendCtsList,
isEmptyCts, isCTyEqCan, isCFunEqCan,
isCDictCan_Maybe, isCFunEqCan_maybe,
isCIrredEvCan, isCNonCanonical, isWantedCt, isDerivedCt,
......@@ -56,6 +56,7 @@ module TcRnTypes(
WantedConstraints(..), insolubleWC, emptyWC, isEmptyWC,
andWC, unionsWC, addFlats, addImplics, mkFlatWC, addInsols,
dropDerivedWC,
Implication(..),
SubGoalCounter(..),
......@@ -72,10 +73,9 @@ module TcRnTypes(
CtEvidence(..),
mkGivenLoc,
isWanted, isGiven, isDerived,
canRewrite, canRewriteOrSame,
-- Pretty printing
pprEvVarTheta, pprWantedsWithLocs,
pprEvVarTheta,
pprEvVars, pprEvVarWithType,
pprArising, pprArisingAt,
......@@ -984,9 +984,9 @@ type Cts = Bag Ct
data Ct
-- Atomic canonical constraints
= CDictCan { -- e.g. Num xi
cc_ev :: CtEvidence, -- See Note [Ct/evidence invariant]
cc_ev :: CtEvidence, -- See Note [Ct/evidence invariant]
cc_class :: Class,
cc_tyargs :: [Xi]
cc_tyargs :: [Xi] -- cc_tyargs are function-free, hence Xi
}
| CIrredEvCan { -- These stand for yet-unusable predicates
......@@ -998,26 +998,43 @@ data Ct
-- See Note [CIrredEvCan constraints]
}
| CTyEqCan { -- tv ~ xi (recall xi means function free)
-- Invariant:
| CTyEqCan { -- tv ~ rhs
-- Invariants:
-- * See Note [Applying the inert substitution] in TcFlatten
-- * tv not in tvs(xi) (occurs check)
-- * typeKind xi `subKind` typeKind tv
-- * If tv is a TauTv, then rhs has no foralls
-- (this avoids substituting a forall for the tyvar in other types)
-- * typeKind ty `subKind` typeKind tv
-- See Note [Kind orientation for CTyEqCan]
-- * We prefer unification variables on the left *JUST* for efficiency
cc_ev :: CtEvidence, -- See Note [Ct/evidence invariant]
-- * rhs is not necessarily function-free,
-- but it has no top-level function.
-- E.g. a ~ [F b] is fine
-- but a ~ F b is not
-- * If rhs is also a tv, then it is oriented to give best chance of
-- unification happening; eg if rhs is touchable then lhs is too
cc_ev :: CtEvidence, -- See Note [Ct/evidence invariant]
cc_tyvar :: TcTyVar,
cc_rhs :: Xi
cc_rhs :: TcType -- Not necessarily function-free (hence not Xi)
-- See invariants above
}
| CFunEqCan { -- F xis ~ xi
-- Invariant: * isSynFamilyTyCon cc_fun
-- * typeKind (F xis) `subKind` typeKind xi
-- See Note [Kind orientation for CFunEqCan]
| CFunEqCan { -- F xis ~ fsk
-- Invariants:
-- * isSynFamilyTyCon cc_fun
-- * typeKind (F xis) = tyVarKind fsk
-- * always Nominal role
-- * always Given or Wanted, never Derived
cc_ev :: CtEvidence, -- See Note [Ct/evidence invariant]
cc_fun :: TyCon, -- A type function
cc_tyargs :: [Xi], -- Either under-saturated or exactly saturated
cc_rhs :: Xi -- *never* over-saturated (because if so
-- we should have decomposed)
cc_tyargs :: [Xi], -- cc_tyargs are function-free (hence Xi)
-- Either under-saturated or exactly saturated
-- *never* over-saturated (because if so
-- we should have decomposed)
cc_fsk :: TcTyVar -- [Given] always a FlatSkol skolem
-- [Wanted] always a FlatMetaTv unification variable
-- See Note [The flattening story] in TcFlatten
}
| CNonCanonical { -- See Note [NonCanonical Semantics]
......@@ -1033,11 +1050,13 @@ data Ct
Note [Kind orientation for CTyEqCan]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Given an equality (t:* ~ s:Open), we absolutely want to re-orient it.
We can't solve it by updating t:=s, ragardless of how touchable 't' is,
because the kinds don't work. Indeed we don't want to leave it with
the orientation (t ~ s), because if that gets into the inert set we'll
start replacing t's by s's, and that too is the wrong way round.
Given an equality (t:* ~ s:Open), we can't solve it by updating t:=s,
ragardless of how touchable 't' is, because the kinds don't work.
Instead we absolutely must re-orient it. Reason: if that gets into the
inert set we'll start replacing t's by s's, and that might make a
kind-correct type into a kind error. After re-orienting,
we may be able to solve by updating s:=t.
Hence in a CTyEqCan, (t:k1 ~ xi:k2) we require that k2 is a subkind of k1.
......@@ -1144,7 +1163,7 @@ comprehensible error. Particularly:
* Insoluble derived wanted equalities (e.g. [D] Int ~ Bool) may
arise from functional dependency interactions. We are careful
to keep a good CtOrigin on such constriants (FunDepOrigin1, FunDepOrigin2)
to keep a good CtOrigin on such constraints (FunDepOrigin1, FunDepOrigin2)
so that we can produce a good error message (Trac #9612)
Since we leave these Derived constraints in the residual WantedConstraints,
......@@ -1225,8 +1244,11 @@ listToCts = listToBag
ctsElts :: Cts -> [Ct]
ctsElts = bagToList
extendCts :: Cts -> Ct -> Cts
extendCts = snocBag
consCts :: Ct -> Cts -> Cts
consCts = consBag
snocCts :: Cts -> Ct -> Cts
snocCts = snocBag
extendCtsList :: Cts -> [Ct] -> Cts
extendCtsList cts xs | null xs = cts
......@@ -1240,6 +1262,9 @@ emptyCts = emptyBag
isEmptyCts :: Cts -> Bool
isEmptyCts = isEmptyBag
pprCts :: Cts -> SDoc
pprCts cts = vcat (map ppr (bagToList cts))
\end{code}
%************************************************************************
......@@ -1303,15 +1328,15 @@ addInsols wc cts
instance Outputable WantedConstraints where
ppr (WC {wc_flat = f, wc_impl = i, wc_insol = n})
= ptext (sLit "WC") <+> braces (vcat
[ if isEmptyBag f then empty else
ptext (sLit "wc_flat =") <+> pprBag ppr f
, if isEmptyBag i then empty else
ptext (sLit "wc_impl =") <+> pprBag ppr i
, if isEmptyBag n then empty else
ptext (sLit "wc_insol =") <+> pprBag ppr n ])
pprBag :: (a -> SDoc) -> Bag a -> SDoc
pprBag pp b = foldrBag (($$) . pp) empty b
[ ppr_bag (ptext (sLit "wc_flat")) f
, ppr_bag (ptext (sLit "wc_insol")) n
, ppr_bag (ptext (sLit "wc_impl")) i ])
ppr_bag :: Outputable a => SDoc -> Bag a -> SDoc
ppr_bag doc bag
| isEmptyBag bag = empty
| otherwise = hang (doc <+> equals)
2 (foldrBag (($$) . ppr) empty bag)
\end{code}
......@@ -1335,10 +1360,6 @@ data Implication
-- (order does not matter)
-- See Invariant (GivenInv) in TcType
ic_fsks :: [TcTyVar], -- Extra flatten-skolems introduced by
-- by flattening the givens
-- See Note [Given flatten-skolems]
ic_no_eqs :: Bool, -- True <=> ic_givens have no equalities, for sure
-- False <=> ic_givens might have equalities
......@@ -1354,19 +1375,19 @@ data Implication
}
instance Outputable Implication where
ppr (Implic { ic_untch = untch, ic_skols = skols, ic_fsks = fsks
ppr (Implic { ic_untch = untch, ic_skols = skols
, ic_given = given, ic_no_eqs = no_eqs
, ic_wanted = wanted
, ic_wanted = wanted, ic_insol = insol
, ic_binds = binds, ic_info = info })
= ptext (sLit "Implic") <+> braces
(sep [ ptext (sLit "Untouchables =") <+> ppr untch
, ptext (sLit "Skolems =") <+> pprTvBndrs skols
, ptext (sLit "Flatten-skolems =") <+> pprTvBndrs fsks
, ptext (sLit "No-eqs =") <+> ppr no_eqs
, ptext (sLit "Given =") <+> pprEvVars given
, ptext (sLit "Wanted =") <+> ppr wanted
, ptext (sLit "Binds =") <+> ppr binds
, pprSkolInfo info ])
= hang (ptext (sLit "Implic") <+> lbrace)
2 (sep [ ptext (sLit "Untouchables =") <+> ppr untch
, ptext (sLit "Skolems =") <+> pprTvBndrs skols
, ptext (sLit "No-eqs =") <+> ppr no_eqs
, ptext (sLit "Insol =") <+> ppr insol
, hang (ptext (sLit "Given =")) 2 (pprEvVars given)
, hang (ptext (sLit "Wanted =")) 2 (ppr wanted)
, ptext (sLit "Binds =") <+> ppr binds
, pprSkolInfo info ] <+> rbrace)
\end{code}
Note [Shadowing in a constraint]
......@@ -1437,12 +1458,6 @@ pprEvVarTheta ev_vars = pprTheta (map evVarPred ev_vars)
pprEvVarWithType :: EvVar -> SDoc
pprEvVarWithType v = ppr v <+> dcolon <+> pprType (evVarPred v)
pprWantedsWithLocs :: WantedConstraints -> SDoc
pprWantedsWithLocs wcs
= vcat [ pprBag ppr (wc_flat wcs)
, pprBag ppr (wc_impl wcs)
, pprBag ppr (wc_insol wcs) ]
\end{code}
%************************************************************************
......@@ -1524,49 +1539,8 @@ isGiven _ = False
isDerived :: CtEvidence -> Bool
isDerived (CtDerived {}) = True
isDerived _ = False
-----------------------------------------
canRewrite :: CtEvidence -> CtEvidence -> Bool
-- Very important function!
-- See Note [canRewrite and canRewriteOrSame]
canRewrite (CtGiven {}) _ = True
canRewrite (CtWanted {}) (CtDerived {}) = True
canRewrite (CtDerived {}) (CtDerived {}) = True -- Derived can't solve wanted/given
canRewrite _ _ = False -- No evidence for a derived, anyway
canRewriteOrSame :: CtEvidence -> CtEvidence -> Bool
canRewriteOrSame (CtGiven {}) _ = True
canRewriteOrSame (CtWanted {}) (CtWanted {}) = True
canRewriteOrSame (CtWanted {}) (CtDerived {}) = True
canRewriteOrSame (CtDerived {}) (CtDerived {}) = True
canRewriteOrSame _ _ = False
\end{code}
See Note [canRewrite and canRewriteOrSame]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
(canRewrite ct1 ct2) holds if the constraint ct1 can be used to solve ct2.
"To solve" means a reaction where the active parts of the two constraints match.
active(F xis ~ xi) = F xis
active(tv ~ xi) = tv
active(D xis) = D xis
active(IP nm ty) = nm
At the moment we don't allow Wanteds to rewrite Wanteds, because that can give
rise to very confusing type error messages. A good example is Trac #8450.
Here's another
f :: a -> Bool
f x = ( [x,'c'], [x,True] ) `seq` True
Here we get
[W] a ~ Char
[W] a ~ Bool
but we do not want to complain about Bool ~ Char!
NB: either (a `canRewrite` b) or (b `canRewrite` a)
or a==b
must hold
canRewriteOrSame is similar but returns True for Wanted/Wanted.
See the call sites for explanations.
%************************************************************************
%* *
......@@ -1690,11 +1664,13 @@ data CtLoc = CtLoc { ctl_origin :: CtOrigin
-- source location: tcl_loc :: SrcSpan
-- context: tcl_ctxt :: [ErrCtxt]
-- binder stack: tcl_bndrs :: [TcIdBinders]
-- level: tcl_untch :: Untouchables
mkGivenLoc :: SkolemInfo -> TcLclEnv -> CtLoc
mkGivenLoc skol_info env = CtLoc { ctl_origin = GivenOrigin skol_info
, ctl_env = env
, ctl_depth = initialSubGoalDepth }
mkGivenLoc :: Untouchables -> SkolemInfo -> TcLclEnv -> CtLoc
mkGivenLoc untch skol_info env
= CtLoc { ctl_origin = GivenOrigin skol_info
, ctl_env = env { tcl_untch = untch }
, ctl_depth = initialSubGoalDepth }
ctLocEnv :: CtLoc -> TcLclEnv
ctLocEnv = ctl_env
......@@ -1837,9 +1813,6 @@ pprSkolInfo UnkSkol = WARN( True, text "pprSkolInfo: UnkSkol" ) ptext (sLit "Unk
\begin{code}
data CtOrigin
= GivenOrigin SkolemInfo
| FlatSkolOrigin -- Flatten-skolems created for Givens
-- Note [When does an implication have given equalities?]
-- in TcSimplify
-- All the others are for *wanted* constraints
| OccurrenceOf Name -- Occurrence of an overloaded identifier
......@@ -1898,7 +1871,6 @@ data CtOrigin
| UnboundOccurrenceOf RdrName
| ListOrigin -- An overloaded list
ctoHerald :: SDoc
ctoHerald = ptext (sLit "arising from")
......@@ -1949,7 +1921,6 @@ pprCtOrigin simple_origin
----------------
pprCtO :: CtOrigin -> SDoc -- Ones that are short one-liners
pprCtO FlatSkolOrigin = ptext (sLit "a given flatten-skolem")
pprCtO (OccurrenceOf name) = hsep [ptext (sLit "a use of"), quotes (ppr name)]
pprCtO AppOrigin = ptext (sLit "an application")
pprCtO (SpecPragOrigin name) = hsep [ptext (sLit "a specialisation pragma for"), quotes (ppr name)]
......
......@@ -168,7 +168,6 @@ tcRule (HsRule name act hs_bndrs lhs fv_lhs rhs fv_rhs)
; rhs_binds_var <- newTcEvBinds
; emitImplication $ Implic { ic_untch = noUntouchables
, ic_skols = qtkvs
, ic_fsks = []
, ic_no_eqs = False
, ic_given = lhs_evs
, ic_wanted = rhs_wanted
......@@ -183,7 +182,6 @@ tcRule (HsRule name act hs_bndrs lhs fv_lhs rhs fv_rhs)
; lhs_binds_var <- newTcEvBinds
; emitImplication $ Implic { ic_untch = noUntouchables
, ic_skols = qtkvs
, ic_fsks = []
, ic_no_eqs = False
, ic_given = lhs_evs
, ic_wanted = other_lhs_wanted
......
This diff is collapsed.
This diff is collapsed.
......@@ -24,7 +24,8 @@ module TcType (
TcTyVar, TcTyVarSet, TcKind, TcCoVar,
-- Untouchables
Untouchables(..), noUntouchables, pushUntouchables, isTouchable,
Untouchables(..), noUntouchables, pushUntouchables,
strictlyDeeperThan, sameDepthAs, fskUntouchables,
--------------------------------
-- MetaDetails
......@@ -32,12 +33,14 @@ module TcType (
TcTyVarDetails(..), pprTcTyVarDetails, vanillaSkolemTv, superSkolemTv,
MetaDetails(Flexi, Indirect), MetaInfo(..),
isImmutableTyVar, isSkolemTyVar, isMetaTyVar, isMetaTyVarTy, isTyVarTy,
isSigTyVar, isOverlappableTyVar, isTyConableTyVar, isFlatSkolTyVar,