\begin{code}
module TcSimplify(
simplifyInfer, simplifySuperClass,
simplifyDefault, simplifyDeriv, simplifyBracket,
simplifyRule, simplifyTop, simplifyInteractive
) where
#include "HsVersions.h"
import HsSyn
import TcRnMonad
import TcErrors
import TcCanonical
import TcMType
import TcType
import TcSMonad
import TcInteract
import Inst
import Var
import VarSet
import VarEnv
import TypeRep
import Name
import NameEnv ( emptyNameEnv )
import Bag
import ListSetOps
import Util
import PrelInfo
import PrelNames
import Class ( classKey )
import BasicTypes ( RuleName )
import Data.List ( partition )
import Outputable
import FastString
\end{code}
*********************************************************************************
* *
* External interface *
* *
*********************************************************************************
\begin{code}
simplifyTop :: WantedConstraints -> TcM (Bag EvBind)
simplifyTop wanteds
= simplifyCheck SimplCheck wanteds
simplifyInteractive :: WantedConstraints -> TcM (Bag EvBind)
simplifyInteractive wanteds
= simplifyCheck SimplInteractive wanteds
simplifyDefault :: ThetaType
-> TcM ()
simplifyDefault theta
= do { loc <- getCtLoc DefaultOrigin
; wanted <- newWantedEvVars theta
; let wanted_bag = listToBag [WcEvVar (WantedEvVar w loc) | w <- wanted]
; _ignored_ev_binds <- simplifyCheck SimplCheck wanted_bag
; return () }
\end{code}
simplifyBracket is used when simplifying the constraints arising from
a Template Haskell bracket [| ... |]. We want to check that there aren't
any constraints that can't be satisfied (e.g. Show Foo, where Foo has no
Show instance), but we aren't otherwise interested in the results.
Nor do we care about ambiguous dictionaries etc. We will type check
this bracket again at its usage site.
\begin{code}
simplifyBracket :: WantedConstraints -> TcM ()
simplifyBracket wanteds
= do { zonked_wanteds <- mapBagM zonkWanted wanteds
; _ <- simplifyAsMuchAsPossible SimplInfer zonked_wanteds
; return () }
\end{code}
*********************************************************************************
* *
* Deriving
* *
***********************************************************************************
\begin{code}
simplifyDeriv :: CtOrigin
-> [TyVar]
-> ThetaType
-> TcM ThetaType
simplifyDeriv orig tvs theta
= do { tvs_skols <- tcInstSkolTyVars InstSkol tvs
; let skol_subst = zipTopTvSubst tvs $ map mkTyVarTy tvs_skols
; loc <- getCtLoc orig
; wanted <- newWantedEvVars (substTheta skol_subst theta)
; let wanted_bag = listToBag [WcEvVar (WantedEvVar w loc) | w <- wanted]
; traceTc "simlifyDeriv" (ppr tvs $$ ppr theta $$ ppr wanted)
; (unsolved, _binds) <- simplifyAsMuchAsPossible SimplInfer wanted_bag
; let (good, bad) = partition validDerivPred $
foldrBag ((:) . wantedEvVarPred) [] unsolved
subst_skol = zipTopTvSubst tvs_skols $ map mkTyVarTy tvs
; reportUnsolvedDeriv bad loc
; return $ substTheta subst_skol good }
\end{code}
Note [Exotic derived instance contexts]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In a 'derived' instance declaration, we *infer* the context. It's a
bit unclear what rules we should apply for this; the Haskell report is
silent. Obviously, constraints like (Eq a) are fine, but what about
data T f a = MkT (f a) deriving( Eq )
where we'd get an Eq (f a) constraint. That's probably fine too.
One could go further: consider
data T a b c = MkT (Foo a b c) deriving( Eq )
instance (C Int a, Eq b, Eq c) => Eq (Foo a b c)
Notice that this instance (just) satisfies the Paterson termination
conditions. Then we *could* derive an instance decl like this:
instance (C Int a, Eq b, Eq c) => Eq (T a b c)
even though there is no instance for (C Int a), because there just
*might* be an instance for, say, (C Int Bool) at a site where we
need the equality instance for T's.
However, this seems pretty exotic, and it's quite tricky to allow
this, and yet give sensible error messages in the (much more common)
case where we really want that instance decl for C.
So for now we simply require that the derived instance context
should have only type-variable constraints.
Here is another example:
data Fix f = In (f (Fix f)) deriving( Eq )
Here, if we are prepared to allow -XUndecidableInstances we
could derive the instance
instance Eq (f (Fix f)) => Eq (Fix f)
but this is so delicate that I don't think it should happen inside
'deriving'. If you want this, write it yourself!
NB: if you want to lift this condition, make sure you still meet the
termination conditions! If not, the deriving mechanism generates
larger and larger constraints. Example:
data Succ a = S a
data Seq a = Cons a (Seq (Succ a)) | Nil deriving Show
Note the lack of a Show instance for Succ. First we'll generate
instance (Show (Succ a), Show a) => Show (Seq a)
and then
instance (Show (Succ (Succ a)), Show (Succ a), Show a) => Show (Seq a)
and so on. Instead we want to complain of no instance for (Show (Succ a)).
The bottom line
~~~~~~~~~~~~~~~
Allow constraints which consist only of type variables, with no repeats.
*********************************************************************************
* *
* Inference
* *
***********************************************************************************
\begin{code}
simplifyInfer :: Bool
-> TcTyVarSet
-> WantedConstraints
-> TcM ([TcTyVar],
[EvVar],
TcEvBinds)
simplifyInfer apply_mr tau_tvs wanted
| isEmptyBag wanted
= do { zonked_tau_tvs <- zonkTcTyVarsAndFV tau_tvs
; gbl_tvs <- tcGetGlobalTyVars
; qtvs <- zonkQuantifiedTyVars (varSetElems (zonked_tau_tvs `minusVarSet` gbl_tvs))
; return (qtvs, [], emptyTcEvBinds) }
| otherwise
= do { zonked_wanted <- mapBagM zonkWanted wanted
; traceTc "simplifyInfer {" $ vcat
[ ptext (sLit "apply_mr =") <+> ppr apply_mr
, ptext (sLit "wanted =") <+> ppr zonked_wanted
, ptext (sLit "tau_tvs =") <+> ppr tau_tvs
]
; gbl_tvs <- tcGetGlobalTyVars
; zonked_tau_tvs <- zonkTcTyVarsAndFV tau_tvs
; let proto_qtvs = growWanteds gbl_tvs zonked_wanted $
zonked_tau_tvs `minusVarSet` gbl_tvs
(perhaps_bound, surely_free)
= partitionBag (quantifyMeWC proto_qtvs) zonked_wanted
; emitConstraints surely_free
; traceTc "sinf" $ vcat
[ ptext (sLit "perhaps_bound =") <+> ppr perhaps_bound
, ptext (sLit "surely_free =") <+> ppr surely_free
]
; (simplified_perhaps_bound, tc_binds)
<- simplifyAsMuchAsPossible SimplInfer perhaps_bound
; gbl_tvs <- tcGetGlobalTyVars
; zonked_tau_tvs <- zonkTcTyVarsAndFV tau_tvs
; zonked_simples <- mapBagM zonkWantedEvVar simplified_perhaps_bound
; let init_tvs = zonked_tau_tvs `minusVarSet` gbl_tvs
mr_qtvs = init_tvs `minusVarSet` constrained_tvs
constrained_tvs = tyVarsOfWantedEvVars zonked_simples
qtvs = growWantedEVs gbl_tvs zonked_simples init_tvs
(final_qtvs, (bound, free))
| apply_mr = (mr_qtvs, (emptyBag, zonked_simples))
| otherwise = (qtvs, partitionBag (quantifyMe qtvs) zonked_simples)
; traceTc "end simplifyInfer }" $
vcat [ ptext (sLit "apply_mr =") <+> ppr apply_mr
, text "wanted = " <+> ppr zonked_wanted
, text "qtvs = " <+> ppr final_qtvs
, text "free = " <+> ppr free
, text "bound = " <+> ppr bound ]
; emitConstraints (mapBag WcEvVar free)
; qtvs_to_return <- zonkQuantifiedTyVars (varSetElems final_qtvs)
; let bound_evvars = bagToList $ mapBag wantedEvVarToVar bound
; return (qtvs_to_return, bound_evvars, EvBinds tc_binds) }
simplifyAsMuchAsPossible :: SimplContext -> WantedConstraints
-> TcM (Bag WantedEvVar, Bag EvBind)
simplifyAsMuchAsPossible ctxt wanteds
= do { let untch = NoUntouchables
; ((unsolved_flats, unsolved_implics), frozen_errors, ev_binds)
<- runTcS ctxt untch $
simplifyApproxLoop 0 wanteds
; reportUnsolved (emptyBag, unsolved_implics) frozen_errors
; return (unsolved_flats, ev_binds) }
where
simplifyApproxLoop :: Int -> WantedConstraints
-> TcS (Bag WantedEvVar, Bag Implication)
simplifyApproxLoop n wanteds
| n > 10
= pprPanic "simplifyApproxLoop loops!" (ppr n <+> text "iterations")
| otherwise
= do { traceTcS "simplifyApproxLoop" (vcat
[ ptext (sLit "Wanted = ") <+> ppr wanteds ])
; (unsolved_flats, unsolved_implics) <- solveWanteds emptyInert wanteds
; let (extra_flats, thiner_unsolved_implics)
= approximateImplications unsolved_implics
unsolved
= Bag.mapBag WcEvVar unsolved_flats `unionBags`
Bag.mapBag WcImplic thiner_unsolved_implics
;
if isEmptyBag extra_flats
then do { traceTcS "simplifyApproxLoopRes" (vcat
[ ptext (sLit "Wanted = ") <+> ppr wanteds
, ptext (sLit "Result = ") <+> ppr unsolved_flats ])
; return (unsolved_flats, unsolved_implics) }
else
simplifyApproxLoop (n+1) (extra_flats `unionBags` unsolved)
}
approximateImplications :: Bag Implication -> (WantedConstraints, Bag Implication)
approximateImplications impls
= splitBag (do_implic emptyVarSet) impls
where
do_wanted :: TcTyVarSet -> WantedConstraint
-> (WantedConstraints, WantedConstraints)
do_wanted skols (WcImplic impl)
= let (fl_w, mb_impl) = do_implic skols impl
in (fl_w, mapBag WcImplic mb_impl)
do_wanted skols wc@(WcEvVar wev)
| tyVarsOfWantedEvVar wev `disjointVarSet` skols = (unitBag wc, emptyBag)
| otherwise = (emptyBag, unitBag wc)
do_implic :: TcTyVarSet -> Implication
-> (WantedConstraints, Bag Implication)
do_implic skols impl@(Implic { ic_skols = skols', ic_wanted = wanted })
= (floatable_wanted, if isEmptyBag rest_wanted then emptyBag
else unitBag impl{ ic_wanted = rest_wanted } )
where
(floatable_wanted, rest_wanted)
= splitBag (do_wanted (skols `unionVarSet` skols')) wanted
splitBag :: (a -> (WantedConstraints, Bag a))
-> Bag a -> (WantedConstraints, Bag a)
splitBag f bag = foldrBag do_one (emptyBag,emptyBag) bag
where
do_one x (b1,b2)
= (wcs `unionBags` b1, imps `unionBags` b2)
where
(wcs, imps) = f x
\end{code}
\begin{code}
growWantedEVs :: TyVarSet -> Bag WantedEvVar -> TyVarSet -> TyVarSet
growWanteds :: TyVarSet -> Bag WantedConstraint -> TyVarSet -> TyVarSet
growWanteds gbl_tvs ws tvs
| isEmptyBag ws = tvs
| otherwise = fixVarSet (\tvs -> foldrBag (growWanted gbl_tvs) tvs ws) tvs
growWantedEVs gbl_tvs ws tvs
| isEmptyBag ws = tvs
| otherwise = fixVarSet (\tvs -> foldrBag (growWantedEV gbl_tvs) tvs ws) tvs
growEvVar :: TyVarSet -> EvVar -> TyVarSet -> TyVarSet
growWantedEV :: TyVarSet -> WantedEvVar -> TyVarSet -> TyVarSet
growWanted :: TyVarSet -> WantedConstraint -> TyVarSet -> TyVarSet
growEvVar gbl_tvs ev tvs
= tvs `unionVarSet` (ev_tvs `minusVarSet` gbl_tvs)
where
ev_tvs = growPredTyVars (evVarPred ev) tvs
growWantedEV gbl_tvs wev tvs = growEvVar gbl_tvs (wantedEvVarToVar wev) tvs
growWanted gbl_tvs (WcEvVar wev) tvs
= growWantedEV gbl_tvs wev tvs
growWanted gbl_tvs (WcImplic implic) tvs
= foldrBag (growWanted inner_gbl_tvs)
(foldr (growEvVar inner_gbl_tvs) tvs (ic_given implic))
(ic_wanted implic)
where
inner_gbl_tvs = gbl_tvs `unionVarSet` ic_skols implic
quantifyMe :: TyVarSet
-> WantedEvVar
-> Bool
quantifyMe qtvs wev
| isIPPred pred = True
| otherwise = tyVarsOfPred pred `intersectsVarSet` qtvs
where
pred = wantedEvVarPred wev
quantifyMeWC :: TyVarSet -> WantedConstraint -> Bool
quantifyMeWC qtvs (WcImplic implic)
= (tyVarsOfEvVars (ic_given implic) `intersectsVarSet` inner_qtvs)
|| anyBag (quantifyMeWC inner_qtvs) (ic_wanted implic)
where
inner_qtvs = qtvs `minusVarSet` ic_skols implic
quantifyMeWC qtvs (WcEvVar wev)
= quantifyMe qtvs wev
\end{code}
Note [Avoid unecessary constraint simplification]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When inferring the type of a let-binding, with simplifyInfer,
try to avoid unnecessariliy simplifying class constraints.
Doing so aids sharing, but it also helps with delicate
situations like
instance C t => C [t] where ..
f :: C [t] => ....
f x = let g y = ...(constraint C [t])...
in ...
When inferring a type for 'g', we don't want to apply the
instance decl, because then we can't satisfy (C t). So we
just notice that g isn't quantified over 't' and partition
the contraints before simplifying.
This only half-works, but then let-generalisation only half-works.
Note [Inheriting implicit parameters]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider this:
f x = (x::Int) + ?y
where f is *not* a top-level binding.
From the RHS of f we'll get the constraint (?y::Int).
There are two types we might infer for f:
f :: Int -> Int
(so we get ?y from the context of f's definition), or
f :: (?y::Int) => Int -> Int
At first you might think the first was better, becuase then
?y behaves like a free variable of the definition, rather than
having to be passed at each call site. But of course, the WHOLE
IDEA is that ?y should be passed at each call site (that's what
dynamic binding means) so we'd better infer the second.
BOTTOM LINE: when *inferring types* you *must* quantify
over implicit parameters. See the predicate isFreeWhenInferring.
*********************************************************************************
* *
* Superclasses *
* *
***********************************************************************************
When constructing evidence for superclasses in an instance declaration,
* we MUST have the "self" dictionary available, but
* we must NOT have its superclasses derived from "self"
Moreover, we must *completely* solve the constraints right now,
not wrap them in an implication constraint to solve later. Why?
Because when that implication constraint is solved there may
be some unrelated other solved top-level constraints that
recursively depend on the superclass we are building. Consider
class Ord a => C a where
instance C [Int] where ...
Then we get
dCListInt :: C [Int]
dCListInt = MkC $cNum ...
$cNum :: Ord [Int] -- The superclass
$cNum = let self = dCListInt in
Now, if there is some *other* top-level constraint solved
looking like
foo :: Ord [Int]
foo = scsel dCInt
we must not solve the (Ord [Int]) wanted from foo!!
\begin{code}
simplifySuperClass :: EvVar
-> WantedConstraints
-> TcM ()
simplifySuperClass self wanteds
= do { wanteds <- mapBagM zonkWanted wanteds
; loc <- getCtLoc NoScSkol
; ((unsolved_flats,unsolved_impls), frozen_errors, ev_binds)
<- runTcS SimplCheck NoUntouchables $
do { can_self <- canGivens loc [self]
; let inert = foldlBag updInertSet emptyInert can_self
; solveWanteds inert wanteds }
; ASSERT2( isEmptyBag ev_binds, ppr ev_binds )
reportUnsolved (unsolved_flats,unsolved_impls) frozen_errors }
\end{code}
*********************************************************************************
* *
* RULES *
* *
***********************************************************************************
Note [Simplifying RULE lhs constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
On the LHS of transformation rules we only simplify only equalitis,
but not dictionaries. We want to keep dictionaries unsimplified, to
serve as the available stuff for the RHS of the rule. We *do* want to
simplify equalities, however, to detect ill-typed rules that cannot be
applied.
Implementation: the TcSFlags carried by the TcSMonad controls the
amount of simplification, so simplifyRuleLhs just sets the flag
appropriately.
Example. Consider the following left-hand side of a rule
f (x == y) (y > z) = ...
If we typecheck this expression we get constraints
d1 :: Ord a, d2 :: Eq a
We do NOT want to "simplify" to the LHS
forall x::a, y::a, z::a, d1::Ord a.
f ((==) (eqFromOrd d1) x y) ((>) d1 y z) = ...
Instead we want
forall x::a, y::a, z::a, d1::Ord a, d2::Eq a.
f ((==) d2 x y) ((>) d1 y z) = ...
Here is another example:
fromIntegral :: (Integral a, Num b) => a -> b
{-# RULES "foo" fromIntegral = id :: Int -> Int #-}
In the rule, a=b=Int, and Num Int is a superclass of Integral Int. But
we *dont* want to get
forall dIntegralInt.
fromIntegral Int Int dIntegralInt (scsel dIntegralInt) = id Int
because the scsel will mess up RULE matching. Instead we want
forall dIntegralInt, dNumInt.
fromIntegral Int Int dIntegralInt dNumInt = id Int
Even if we have
g (x == y) (y == z) = ..
where the two dictionaries are *identical*, we do NOT WANT
forall x::a, y::a, z::a, d1::Eq a
f ((==) d1 x y) ((>) d1 y z) = ...
because that will only match if the dict args are (visibly) equal.
Instead we want to quantify over the dictionaries separately.
In short, simplifyRuleLhs must *only* squash equalities, leaving
all dicts unchanged, with absolutely no sharing.
HOWEVER, under a nested implication things are different
Consider
f :: (forall a. Eq a => a->a) -> Bool -> ...
{-# RULES "foo" forall (v::forall b. Eq b => b->b).
f b True = ...
#=}
Here we *must* solve the wanted (Eq a) from the given (Eq a)
resulting from skolemising the agument type of g. So we
revert to SimplCheck when going under an implication.
\begin{code}
simplifyRule :: RuleName
-> [TcTyVar]
-> WantedConstraints
-> WantedConstraints
-> TcM ([EvVar],
TcEvBinds,
TcEvBinds)
simplifyRule name tv_bndrs lhs_wanted rhs_wanted
= do { zonked_lhs <- mapBagM zonkWanted lhs_wanted
; (lhs_residual, lhs_binds) <- simplifyAsMuchAsPossible SimplRuleLhs zonked_lhs
; let (eqs, dicts) = partitionBag (isEqPred . wantedEvVarPred) lhs_residual
lhs_dicts = map wantedEvVarToVar (bagToList dicts)
; reportUnsolvedWantedEvVars eqs
; rhs_binds_var@(EvBindsVar evb_ref _) <- newTcEvBinds
; loc <- getCtLoc (RuleSkol name)
; rhs_binds1 <- simplifyCheck SimplCheck $ unitBag $ WcImplic $
Implic { ic_untch = NoUntouchables
, ic_env = emptyNameEnv
, ic_skols = mkVarSet tv_bndrs
, ic_scoped = panic "emitImplication"
, ic_given = lhs_dicts
, ic_wanted = rhs_wanted
, ic_binds = rhs_binds_var
, ic_loc = loc }
; rhs_binds2 <- readTcRef evb_ref
; return ( lhs_dicts
, EvBinds lhs_binds
, EvBinds (rhs_binds1 `unionBags` evBindMapBinds rhs_binds2)) }
\end{code}
*********************************************************************************
* *
* Main Simplifier *
* *
***********************************************************************************
\begin{code}
simplifyCheck :: SimplContext
-> WantedConstraints
-> TcM (Bag EvBind)
simplifyCheck ctxt wanteds
= do { wanteds <- mapBagM zonkWanted wanteds
; traceTc "simplifyCheck {" (vcat
[ ptext (sLit "wanted =") <+> ppr wanteds ])
; (unsolved, frozen_errors, ev_binds)
<- runTcS ctxt NoUntouchables $ solveWanteds emptyInert wanteds
; traceTc "simplifyCheck }" $
ptext (sLit "unsolved =") <+> ppr unsolved
; reportUnsolved unsolved frozen_errors
; return ev_binds }
solveWanteds :: InertSet
-> WantedConstraints
-> TcS (Bag WantedEvVar,
Bag Implication)
solveWanteds inert wanteds
= do { let (flat_wanteds, implic_wanteds) = splitWanteds wanteds
; can_flats <- canWanteds $ bagToList flat_wanteds
; traceTcS "solveWanteds {" $
vcat [ text "wanteds =" <+> ppr wanteds
, text "inert =" <+> ppr inert ]
; (unsolved_flats, unsolved_implics)
<- simpl_loop 1 inert can_flats implic_wanteds
; bb <- getTcEvBindsBag
; tb <- getTcSTyBindsMap
; traceTcS "solveWanteds }" $
vcat [ text "unsolved_flats =" <+> ppr unsolved_flats
, text "unsolved_implics =" <+> ppr unsolved_implics
, text "current evbinds =" <+> vcat (map ppr (varEnvElts bb))
, text "current tybinds =" <+> vcat (map ppr (varEnvElts tb))
]
; solveCTyFunEqs unsolved_flats unsolved_implics
}
where
simpl_loop :: Int
-> InertSet
-> CanonicalCts
-> Bag Implication
-> TcS (CanonicalCts, Bag Implication)
simpl_loop n inert can_ws implics
| n>10
= trace "solveWanteds: loop" $
do { traceTcS "solveWanteds: loop" (ppr inert)
; return (can_ws, implics) }
| otherwise
= do { traceTcS "solveWanteds: simpl_loop start {" $
vcat [ text "n =" <+> ppr n
, text "can_ws =" <+> ppr can_ws
, text "implics =" <+> ppr implics
, text "inert =" <+> ppr inert ]
; inert1 <- solveInteract inert can_ws
; let (inert2, unsolved_flats) = extractUnsolved inert1
; traceTcS "solveWanteds: done flats" $
vcat [ text "inerts =" <+> ppr inert2
, text "unsolved =" <+> ppr unsolved_flats ]
; inert_for_implics <- solveInteract inert2 (makeGivens unsolved_flats)
; traceTcS "solveWanteds: doing nested implications {" $
vcat [ text "inerts_for_implics =" <+> ppr inert_for_implics
, text "implics =" <+> ppr implics ]
; (implic_eqs, unsolved_implics)
<- flatMapBagPairM (solveImplication inert_for_implics) implics
; traceTcS "solveWanteds: done nested implications }" $
vcat [ text "implic_eqs =" <+> ppr implic_eqs
, text "unsolved_implics =" <+> ppr unsolved_implics ]
; final_eqs <- if not (isEmptyBag implic_eqs)
then return implic_eqs
else applyDefaultingRules inert2 unsolved_flats
; traceTcS "solveWanteds: simpl_loop end }" $
vcat [ text "final_eqs =" <+> ppr final_eqs
, text "unsolved_flats =" <+> ppr unsolved_flats
, text "unsolved_implics =" <+> ppr unsolved_implics ]
; if isEmptyBag final_eqs then
return (unsolved_flats, unsolved_implics)
else
do { can_final_eqs <- canWanteds (Bag.bagToList final_eqs)
; simpl_loop (n+1) inert2
(can_final_eqs `andCCan` unsolved_flats) unsolved_implics
} }
solveImplication :: InertSet
-> Implication
-> TcS (Bag WantedEvVar,
Bag Implication)
solveImplication inert
imp@(Implic { ic_untch = untch
, ic_binds = ev_binds
, ic_skols = skols
, ic_given = givens
, ic_wanted = wanteds
, ic_loc = loc })
= nestImplicTcS ev_binds untch $
recoverTcS (return (emptyBag, emptyBag)) $
do { traceTcS "solveImplication {" (ppr imp)
; can_givens <- canGivens loc givens
; given_inert <- solveInteract inert can_givens
; (unsolved_flats, unsolved_implics) <- solveWanteds given_inert wanteds
; let (res_flat_free, res_flat_bound)
= floatEqualities skols givens unsolved_flats
unsolved = Bag.mapBag WcEvVar res_flat_bound `unionBags`
Bag.mapBag WcImplic unsolved_implics
; traceTcS "solveImplication end }" $ vcat
[ text "res_flat_free =" <+> ppr res_flat_free
, text "res_flat_bound =" <+> ppr res_flat_bound
, text "unsolved_implics =" <+> ppr unsolved_implics ]
; let res_bag | isEmptyBag unsolved = emptyBag
| otherwise = unitBag (imp { ic_wanted = unsolved })
; return (res_flat_free, res_bag) }
floatEqualities :: TcTyVarSet -> [EvVar]
-> Bag WantedEvVar -> (Bag WantedEvVar, Bag WantedEvVar)
floatEqualities skols can_given wanteds
| hasEqualities can_given = (emptyBag, wanteds)
| otherwise = partitionBag is_floatable wanteds
where is_floatable :: WantedEvVar -> Bool
is_floatable (WantedEvVar cv _)
| isCoVar cv = skols `disjointVarSet` predTvs_under_fsks (coVarPred cv)
is_floatable _wv = False
tvs_under_fsks :: Type -> TyVarSet
tvs_under_fsks (TyVarTy tv)
| not (isTcTyVar tv) = unitVarSet tv
| FlatSkol ty <- tcTyVarDetails tv = tvs_under_fsks ty
| otherwise = unitVarSet tv
tvs_under_fsks (TyConApp _ tys) = unionVarSets (map tvs_under_fsks tys)
tvs_under_fsks (PredTy sty) = predTvs_under_fsks sty
tvs_under_fsks (FunTy arg res) = tvs_under_fsks arg `unionVarSet` tvs_under_fsks res
tvs_under_fsks (AppTy fun arg) = tvs_under_fsks fun `unionVarSet` tvs_under_fsks arg
tvs_under_fsks (ForAllTy tv ty)
| isTyVar tv = inner_tvs `delVarSet` tv
| otherwise =
inner_tvs `unionVarSet` tvs_under_fsks (tyVarKind tv)
where
inner_tvs = tvs_under_fsks ty
predTvs_under_fsks :: PredType -> TyVarSet
predTvs_under_fsks (IParam _ ty) = tvs_under_fsks ty
predTvs_under_fsks (ClassP _ tys) = unionVarSets (map tvs_under_fsks tys)
predTvs_under_fsks (EqPred ty1 ty2) = tvs_under_fsks ty1 `unionVarSet` tvs_under_fsks ty2
\end{code}
Note [Float Equalities out of Implications]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We want to float equalities out of vanilla existentials, but *not* out
of GADT pattern matches.
Note [Preparing inert set for implications]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Before solving the nested implications, we convert any unsolved flat wanteds
to givens, and add them to the inert set. Reasons:
a) In checking mode, suppresses unnecessary errors. We already have
on unsolved-wanted error; adding it to the givens prevents any
consequential errors from showing uop
b) More importantly, in inference mode, we are going to quantify over this
constraint, and we *don't* want to quantify over any constraints that
are deducible from it.
The unsolved wanteds are *canonical* but they may not be *inert*,
because when made into a given they might interact with other givens.
Hence the call to solveInteract. Example:
Original inert set = (d :_g D a) /\ (co :_w a ~ [beta])
We were not able to solve (a ~w [beta]) but we can't just assume it as
given because the resulting set is not inert. Hence we have to do a
'solveInteract' step first
\begin{code}
solveCTyFunEqs :: CanonicalCts -> Bag Implication -> TcS (Bag WantedEvVar, Bag Implication)
solveCTyFunEqs cts implics
= do { untch <- getUntouchables
; let (unsolved_can_cts, funeq_bnds) = getSolvableCTyFunEqs untch cts
; traceTcS "defaultCTyFunEqs" (vcat [text "Trying to default family equations:"
, ppr funeq_bnds
])
; mapM_ solve_one funeq_bnds
; let final_unsolved
= Bag.mapBag (subst_wevar funeq_bnds . deCanonicaliseWanted) unsolved_can_cts
final_implics
= Bag.mapBag (subst_impl funeq_bnds) implics
; return (final_unsolved, final_implics) }
where solve_one (tv,(ty,cv,fl))
| not (typeKind ty `isSubKind` tyVarKind tv)
= addErrorTcS KindError fl (mkTyVarTy tv) ty
| otherwise = setWantedTyBind tv ty >> setWantedCoBind cv ty
subst_wanted :: FunEqBinds -> WantedConstraint -> WantedConstraint
subst_wanted funeq_bnds (WcEvVar wv) = WcEvVar (subst_wevar funeq_bnds wv)
subst_wanted funeq_bnds (WcImplic impl) = WcImplic (subst_impl funeq_bnds impl)
subst_wevar :: FunEqBinds -> WantedEvVar -> WantedEvVar
subst_wevar funeq_bnds (WantedEvVar v loc)
= let orig_ty = varType v
new_ty = substFunEqBnds funeq_bnds orig_ty
in WantedEvVar (setVarType v new_ty) loc
subst_impl :: FunEqBinds -> Implication -> Implication
subst_impl funeq_bnds impl@(Implic { ic_wanted = ws })
= impl { ic_wanted = Bag.mapBag (subst_wanted funeq_bnds) ws }
type FunEqBinds = [(TcTyVar,(TcType,CoVar,CtFlavor))]
getSolvableCTyFunEqs :: Untouchables
-> CanonicalCts
-> (CanonicalCts, FunEqBinds)
getSolvableCTyFunEqs untch cts
= Bag.foldlBag dflt_funeq (emptyCCan, []) cts
where dflt_funeq (cts_in, extra_binds) ct@(CFunEqCan { cc_id = cv
, cc_flavor = fl
, cc_fun = tc
, cc_tyargs = xis
, cc_rhs = xi })
| Just tv <- tcGetTyVar_maybe xi
, isTouchableMetaTyVar_InRange untch tv
, Nothing <- lookup tv extra_binds
= ASSERT ( isWanted fl )
let ty_orig = mkTyConApp tc xis
ty_bind = substFunEqBnds extra_binds ty_orig
in if tv `elemVarSet` tyVarsOfType ty_bind
then (cts_in `extendCCans` ct, extra_binds)
else (cts_in, (tv,(ty_bind,cv,fl)):extra_binds)
dflt_funeq (cts_in, extra_binds) ct = (cts_in `extendCCans` ct, extra_binds)
substFunEqBnds :: FunEqBinds -> TcType -> TcType
substFunEqBnds bnds ty
= foldr (\(x,(t,_cv,_fl)) xy -> substTyWith [x] [t] xy) ty bnds
\end{code}
Note [Solving Family Equations]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
After we are done with simplification we may be left with constraints of the form:
[Wanted] F xis ~ beta
If 'beta' is a touchable unification variable not already bound in the TyBinds
then we'd like to create a binding for it, effectively "defaulting" it to be 'F xis'.
When is it ok to do so?
1) 'beta' must not already be defaulted to something. Example:
[Wanted] F Int ~ beta <~ Will default [beta := F Int]
[Wanted] F Char ~ beta <~ Already defaulted, can't default again. We
have to report this as unsolved.
2) However, we must still do an occurs check when defaulting (F xis ~ beta), to
set [beta := F xis] only if beta is not among the free variables of xis.
3) Notice that 'beta' can't be bound in ty binds already because we rewrite RHS
of type family equations. See Inert Set invariants in TcInteract.
*********************************************************************************
* *
* Defaulting and disamgiguation *
* *
*********************************************************************************
Basic plan behind applyDefaulting rules:
Step 1:
Split wanteds into defaultable groups, `groups' and the rest `rest_wanted'
For each defaultable group, do:
For each possible substitution for [alpha |-> tau] where `alpha' is the
group's variable, do:
1) Make up new TcEvBinds
2) Extend TcS with (groupVariable
3) given_inert <- solveOne inert (given : a ~ tau)
4) (final_inert,unsolved) <- solveWanted (given_inert) (group_constraints)
5) if unsolved == empty then
sneakyUnify a |-> tau
write the evidence bins
return (final_inert ++ group_constraints,[])
-- will contain the info (alpha |-> tau)!!
goto next defaultable group
if unsolved <> empty then
throw away evidence binds
try next substitution
If you've run out of substitutions for this group, too bad, you failed
return (inert,group)
goto next defaultable group
Step 2:
Collect all the (canonical-cts, wanteds) gathered this way.
- Do a solveGiven over the canonical-cts to make sure they are inert
------------------------------------------------------------------------------------------
\begin{code}
applyDefaultingRules :: InertSet
-> CanonicalCts
-> TcS (Bag WantedEvVar)
applyDefaultingRules inert wanteds
| isEmptyBag wanteds
= return emptyBag
| otherwise
= do { untch <- getUntouchables
; tv_cts <- mapM (defaultTyVar untch) $
varSetElems (tyVarsOfCDicts wanteds)
; info@(_, default_tys, _) <- getDefaultInfo
; let groups = findDefaultableGroups info untch wanteds
; deflt_cts <- mapM (disambigGroup default_tys inert) groups
; traceTcS "deflt2" (vcat [ text "Tyvar defaults =" <+> ppr tv_cts
, text "Type defaults =" <+> ppr deflt_cts])
; return (unionManyBags deflt_cts `unionBags` unionManyBags tv_cts) }
defaultTyVar :: Untouchables -> TcTyVar -> TcS (Bag WantedEvVar)
defaultTyVar untch the_tv
| isTouchableMetaTyVar_InRange untch the_tv
, not (k `eqKind` default_k)
= do { ev <- TcSMonad.newKindConstraint the_tv default_k
; let loc = CtLoc DefaultOrigin (getSrcSpan the_tv) []
; return (unitBag (WantedEvVar ev loc)) }
| otherwise
= return emptyBag
where
k = tyVarKind the_tv
default_k = defaultKind k
findDefaultableGroups
:: ( SimplContext
, [Type]
, (Bool,Bool) )
-> Untouchables
-> CanonicalCts
-> [[(CanonicalCt,TcTyVar)]]
findDefaultableGroups (ctxt, default_tys, (ovl_strings, extended_defaults))
untch wanteds
| not (performDefaulting ctxt) = []
| null default_tys = []
| otherwise = filter is_defaultable_group (equivClasses cmp_tv unaries)
where
unaries :: [(CanonicalCt, TcTyVar)]
non_unaries :: [CanonicalCt]
(unaries, non_unaries) = partitionWith find_unary (bagToList wanteds)
find_unary cc@(CDictCan { cc_tyargs = [ty] })
| Just tv <- tcGetTyVar_maybe ty
= Left (cc, tv)
find_unary cc = Right cc
bad_tvs :: TcTyVarSet
bad_tvs = foldr (unionVarSet . tyVarsOfCanonical) emptyVarSet non_unaries
cmp_tv (_,tv1) (_,tv2) = tv1 `compare` tv2
is_defaultable_group ds@((_,tv):_)
= isTyConableTyVar tv
&& not (tv `elemVarSet` bad_tvs)
&& isTouchableMetaTyVar_InRange untch tv
&& defaultable_classes [cc_class cc | (cc,_) <- ds]
is_defaultable_group [] = panic "defaultable_group"
defaultable_classes clss
| extended_defaults = any isInteractiveClass clss
| otherwise = all is_std_class clss && (any is_num_class clss)
isInteractiveClass cls
= is_num_class cls || (classKey cls `elem` [showClassKey, eqClassKey, ordClassKey])
is_num_class cls = isNumericClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
is_std_class cls = isStandardClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
disambigGroup :: [Type]
-> InertSet
-> [(CanonicalCt, TcTyVar)]
-> TcS (Bag WantedEvVar)
disambigGroup [] _inert _grp
= return emptyBag
disambigGroup (default_ty:default_tys) inert group
= do { traceTcS "disambigGroup" (ppr group $$ ppr default_ty)
; let ct_loc = get_ct_loc (cc_flavor the_ct)
; ev <- TcSMonad.newWantedCoVar (mkTyVarTy the_tv) default_ty
; let wanted_eq = CTyEqCan { cc_id = ev
, cc_flavor = Wanted ct_loc
, cc_tyvar = the_tv
, cc_rhs = default_ty }
; success <- tryTcS $
do { final_inert <- solveInteract inert(listToBag $ wanted_eq:wanteds)
; let (_, unsolved) = extractUnsolved final_inert
; errs <- getTcSErrorsBag
; return (isEmptyBag unsolved && isEmptyBag errs) }
; case success of
True ->
do { wrapWarnTcS $ warnDefaulting wanted_ev_vars default_ty
; traceTcS "disambigGroup succeeded" (ppr default_ty)
; return (unitBag $ WantedEvVar ev ct_loc) }
False ->
do { traceTcS "disambigGroup failed, will try other default types" (ppr default_ty)
; disambigGroup default_tys inert group } }
where
((the_ct,the_tv):_) = group
wanteds = map fst group
wanted_ev_vars = map deCanonicaliseWanted wanteds
get_ct_loc (Wanted l) = l
get_ct_loc _ = panic "Asked to disambiguate given or derived!"
\end{code}
Note [Avoiding spurious errors]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When doing the unification for defaulting, we check for skolem
type variables, and simply don't default them. For example:
f = (*) -- Monomorphic
g :: Num a => a -> a
g x = f x x
Here, we get a complaint when checking the type signature for g,
that g isn't polymorphic enough; but then we get another one when
dealing with the (Num a) context arising from f's definition;
we try to unify a with Int (to default it), but find that it's
already been unified with the rigid variable from g's type sig