Commit 262cab0f authored by Simon Peyton Jones's avatar Simon Peyton Jones

Fix the constraint simplifier (Trac #7967)

Richard's bug report showed up a couple of subtleties in the constraint solver

* We can strengthen the kind invariants on CTyEqCan and CFunEqCan
    See Note [Kind orientation for CTyEqCan]
    and Note [Kind orientation for CFunEqCan] in TcRnTypes
  There are some changes to reOrient and checkKind in TcCanonical
  to support these stronger invarants.

* In TcSimplify we must make sure that we re-simplify if defaultTyVar
  does anything.  See Note [Must simplify after defaulting] in TcSimplify.

The usual round of refactoring follows!
parent 4aa7fc89
This diff is collapsed.
......@@ -243,9 +243,14 @@ spontaneousSolveStage workItem
= do { mb_solved <- trySpontaneousSolve workItem
; case mb_solved of
SPCantSolve
| CTyEqCan { cc_tyvar = tv, cc_ev = fl } <- workItem
| CTyEqCan { cc_tyvar = tv, cc_rhs = rhs, cc_ev = fl } <- workItem
-- Unsolved equality
-> do { n_kicked <- kickOutRewritable (ctEvFlavour fl) tv
-> do { untch <- getUntouchables
; traceTcS "Can't solve tyvar equality"
(vcat [ text "LHS:" <+> ppr tv <+> dcolon <+> ppr (tyVarKind tv)
, text "RHS:" <+> ppr rhs <+> dcolon <+> ppr (typeKind rhs)
, text "Untouchables =" <+> ppr untch ])
; n_kicked <- kickOutRewritable (ctEvFlavour fl) tv
; traceFireTcS workItem $
ptext (sLit "Kept as inert") <+> ppr_kicked n_kicked <> colon
<+> ppr workItem
......@@ -404,7 +409,8 @@ trySpontaneousSolve :: WorkItem -> TcS SPSolveResult
trySpontaneousSolve workItem@(CTyEqCan { cc_ev = gw
, cc_tyvar = tv1, cc_rhs = xi, cc_loc = d })
| isGiven gw
= return SPCantSolve
= do { traceTcS "No spontaneous solve for given" (ppr workItem)
; return SPCantSolve }
| Just tv2 <- tcGetTyVar_maybe xi
= do { tch1 <- isTouchableMetaTyVarTcS tv1
; tch2 <- isTouchableMetaTyVarTcS tv2
......@@ -412,21 +418,17 @@ trySpontaneousSolve workItem@(CTyEqCan { cc_ev = gw
(True, True) -> trySpontaneousEqTwoWay d gw tv1 tv2
(True, False) -> trySpontaneousEqOneWay d gw tv1 xi
(False, True) -> trySpontaneousEqOneWay d gw tv2 (mkTyVarTy tv1)
_ -> return SPCantSolve }
_ -> return SPCantSolve }
| otherwise
= do { tch1 <- isTouchableMetaTyVarTcS tv1
; if tch1 then trySpontaneousEqOneWay d gw tv1 xi
else do { untch <- getUntouchables
; traceTcS "Untouchable LHS, can't spontaneously solve workitem" $
vcat [text "Untouchables =" <+> ppr untch
, text "Workitem =" <+> ppr workItem ]
; return SPCantSolve }
}
else return SPCantSolve }
-- No need for
-- trySpontaneousSolve (CFunEqCan ...) = ...
-- See Note [No touchables as FunEq RHS] in TcSMonad
trySpontaneousSolve _ = return SPCantSolve
trySpontaneousSolve item = do { traceTcS "Spont: no tyvar on lhs" (ppr item)
; return SPCantSolve }
----------------
trySpontaneousEqOneWay :: CtLoc -> CtEvidence
......@@ -457,57 +459,6 @@ trySpontaneousEqTwoWay d gw tv1 tv2
nicer_to_update_tv2 = isSigTyVar tv1 || isSystemName (Var.varName tv2)
\end{code}
Note [Kind errors]
~~~~~~~~~~~~~~~~~~
Consider the wanted problem:
alpha ~ (# Int, Int #)
where alpha :: ArgKind and (# Int, Int #) :: (#). We can't spontaneously solve this constraint,
but we should rather reject the program that give rise to it. If 'trySpontaneousEqTwoWay'
simply returns @CantSolve@ then that wanted constraint is going to propagate all the way and
get quantified over in inference mode. That's bad because we do know at this point that the
constraint is insoluble. Instead, we call 'recKindErrorTcS' here, which will fail later on.
The same applies in canonicalization code in case of kind errors in the givens.
However, when we canonicalize givens we only check for compatibility (@compatKind@).
If there were a kind error in the givens, this means some form of inconsistency or dead code.
You may think that when we spontaneously solve wanteds we may have to look through the
bindings to determine the right kind of the RHS type. E.g one may be worried that xi is
@alpha@ where alpha :: ? and a previous spontaneous solving has set (alpha := f) with (f :: *).
But we orient our constraints so that spontaneously solved ones can rewrite all other constraint
so this situation can't happen.
Note [Spontaneous solving and kind compatibility]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Note that our canonical constraints insist that *all* equalities (tv ~
xi) or (F xis ~ rhs) require the LHS and the RHS to have *compatible*
the same kinds. ("compatible" means one is a subKind of the other.)
- It can't be *equal* kinds, because
b) wanted constraints don't necessarily have identical kinds
eg alpha::? ~ Int
b) a solved wanted constraint becomes a given
- SPJ thinks that *given* constraints (tv ~ tau) always have that
tau has a sub-kind of tv; and when solving wanted constraints
in trySpontaneousEqTwoWay we re-orient to achieve this.
- Note that the kind invariant is maintained by rewriting.
Eg wanted1 rewrites wanted2; if both were compatible kinds before,
wanted2 will be afterwards. Similarly givens.
Caveat:
- Givens from higher-rank, such as:
type family T b :: * -> * -> *
type instance T Bool = (->)
f :: forall a. ((T a ~ (->)) => ...) -> a -> ...
flop = f (...) True
Whereas we would be able to apply the type instance, we would not be able to
use the given (T Bool ~ (->)) in the body of 'flop'
Note [Avoid double unifications]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The spontaneous solver has to return a given which mentions the unified unification
......@@ -527,8 +478,6 @@ double unifications is the main reason we disallow touchable
unification variables as RHS of type family equations: F xis ~ alpha.
\begin{code}
----------------
solveWithIdentity :: CtLoc -> CtEvidence -> TcTyVar -> Xi -> TcS SPSolveResult
-- Solve with the identity coercion
-- Precondition: kind(xi) is a sub-kind of kind(tv)
......
......@@ -885,7 +885,8 @@ data Ct
cc_ev :: CtEvidence, -- See Note [Ct/evidence invariant]
-- The ctev_pred of the evidence is
-- of form (tv xi1 xi2 ... xin)
-- or (t1 ~ t2) where not (kind(t1) `compatKind` kind(t2)
-- or (tv1 ~ ty2) where the CTyEqCan kind invariant fails
-- or (F tys ~ ty) where the CFunEqCan kind invariant fails
-- See Note [CIrredEvCan constraints]
cc_loc :: CtLoc
}
......@@ -893,8 +894,8 @@ data Ct
| CTyEqCan { -- tv ~ xi (recall xi means function free)
-- Invariant:
-- * tv not in tvs(xi) (occurs check)
-- * typeKind xi `compatKind` typeKind tv
-- See Note [Spontaneous solving and kind compatibility]
-- * typeKind xi `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]
cc_tyvar :: TcTyVar,
......@@ -904,7 +905,8 @@ data Ct
| CFunEqCan { -- F xis ~ xi
-- Invariant: * isSynFamilyTyCon cc_fun
-- * typeKind (F xis) `compatKind` typeKind xi
-- * typeKind (F xis) `subKind` typeKind xi
-- See Note [Kind orientation for CFunEqCan]
cc_ev :: CtEvidence, -- See Note [Ct/evidence invariant]
cc_fun :: TyCon, -- A type function
cc_tyargs :: [Xi], -- Either under-saturated or exactly saturated
......@@ -926,6 +928,49 @@ data Ct
}
\end{code}
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), becuase if that gets into the inert set we'll
start replacing t's by s's, and that too is the wrong way round.
Hence in a CTyEqCan, (t:k1 ~ xi:k2) we require that k2 is a subkind of k1.
If the two have incompatible kinds, we just don't use a CTyEqCan at all.
See Note [Equalities with incompatible kinds] in TcCanonical
We can't require *equal* kinds, because
* wanted constraints don't necessarily have identical kinds
eg alpha::? ~ Int
* a solved wanted constraint becomes a given
Note [Kind orientation for CFunEqCan]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
For (F xis ~ rhs) we require that kind(rhs) is a subkind of kind(lhs).
This reallly only maters when rhs is an Open type variable (since only type
variables have Open kinds):
F ty ~ (a:Open)
which can happen, say, from
f :: F a b
f = undefined -- The a:Open comes from instantiating 'undefined'
Note that the kind invariant is maintained by rewriting.
Eg wanted1 rewrites wanted2; if both were compatible kinds before,
wanted2 will be afterwards. Similarly givens.
Caveat:
- Givens from higher-rank, such as:
type family T b :: * -> * -> *
type instance T Bool = (->)
f :: forall a. ((T a ~ (->)) => ...) -> a -> ...
flop = f (...) True
Whereas we would be able to apply the type instance, we would not be able to
use the given (T Bool ~ (->)) in the body of 'flop'
Note [CIrredEvCan constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
CIrredEvCan constraints are used for constraints that are "stuck"
......
......@@ -81,7 +81,7 @@ module TcSMonad (
newFlexiTcSTy, instFlexiTcS, instFlexiTcSHelperTcS,
cloneMetaTyVar,
compatKind, mkKindErrorCtxtTcS,
mkKindErrorCtxtTcS,
Untouchables, isTouchableMetaTyVarTcS, isFilledMetaTyVar_maybe,
zonkTyVarsAndFV,
......@@ -149,15 +149,11 @@ import Digraph
\begin{code}
compatKind :: Kind -> Kind -> Bool
compatKind k1 k2 = k1 `tcIsSubKind` k2 || k2 `tcIsSubKind` k1
mkKindErrorCtxtTcS :: Type -> Kind
-> Type -> Kind
-> ErrCtxt
mkKindErrorCtxtTcS ty1 ki1 ty2 ki2
= (False,TcM.mkKindErrorCtxt ty1 ty2 ki1 ki2)
\end{code}
%************************************************************************
......
......@@ -77,34 +77,53 @@ simplifyTop wanteds
simpl_top :: WantedConstraints -> TcS WantedConstraints
simpl_top wanteds
= do { wc_first_go <- nestTcS (solve_wanteds_and_drop wanteds)
; free_tvs <- TcS.zonkTyVarsAndFV (tyVarsOfWC wc_first_go)
; let meta_tvs = filterVarSet isMetaTyVar free_tvs
-- This is where the main work happens
; try_tyvar_defaulting wc_first_go }
try_tyvar_defaulting :: WantedConstraints -> TcS WantedConstraints
try_tyvar_defaulting wc
| isEmptyWC wc
= return wc
| otherwise
= do { free_tvs <- TcS.zonkTyVarsAndFV (tyVarsOfWC wc)
; let meta_tvs = varSetElems (filterVarSet isMetaTyVar free_tvs)
-- zonkTyVarsAndFV: the wc_first_go is not yet zonked
-- filter isMetaTyVar: we might have runtime-skolems in GHCi,
-- and we definitely don't want to try to assign to those!
; mapM_ defaultTyVar (varSetElems meta_tvs) -- Has unification side effects
; simpl_top_loop wc_first_go }
; meta_tvs' <- mapM defaultTyVar meta_tvs -- Has unification side effects
; if meta_tvs' == meta_tvs -- No defaulting took place;
-- (defaulting returns fresh vars)
then try_class_defaulting wc
else do { wc_residual <- nestTcS (solve_wanteds_and_drop wc)
-- See Note [Must simplify after defaulting]
; try_class_defaulting wc_residual } }
simpl_top_loop wc
try_class_defaulting :: WantedConstraints -> TcS WantedConstraints
try_class_defaulting wc
| isEmptyWC wc || insolubleWC wc
-- Don't do type-class defaulting if there are insolubles
-- Doing so is not going to solve the insolubles
= return wc
= return wc -- Don't do type-class defaulting if there are insolubles
-- Doing so is not going to solve the insolubles
| otherwise
= do { wc_residual <- nestTcS (solve_wanteds_and_drop wc)
; let wc_flat_approximate = approximateWC wc_residual
; something_happened <- applyDefaultingRules wc_flat_approximate
-- See Note [Top-level Defaulting Plan]
; if something_happened then
simpl_top_loop wc_residual
else
return wc_residual }
= do { something_happened <- applyDefaultingRules (approximateWC wc)
-- See Note [Top-level Defaulting Plan]
; if something_happened
then do { wc_residual <- nestTcS (solve_wanteds_and_drop wc)
; try_class_defaulting wc_residual }
else return wc }
\end{code}
Note [Must simplify after defaulting]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We may have a deeply buried constraint
(t:*) ~ (a:Open)
which we couldn't solve because of the kind incompatibility, and 'a' is free.
Then when we default 'a' we can solve the constraint. And we want to do
that before starting in on type classes. We MUST do it before reporting
errors, because it isn't an error! Trac #7967 was due to this.
Note [Top-level Defaulting Plan]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We have considered two design choices for where/when to apply defaulting.
(i) Do it in SimplCheck mode only /whenever/ you try to solve some
flat constraints, maybe deep inside the context of implications.
......
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