Commit c80364f8 authored by simonpj@microsoft.com's avatar simonpj@microsoft.com

A (final) re-engineering of the new typechecker

Regression testing and user feedback for GHC 7.0 taught
us a lot.  This patch fixes numerous small bugs, and some
major ones (eg Trac #4484, #4492), and improves type
error messages.

The main changes are:

* Entirely remove the "skolem equivalance class" stuff;
  a very useful simplification

* Instead, when flattening "wanted" constraints we generate
  unification variables (not flatten-skolems) for the
  flattened type function application

* We then need a fixup pass at the end, TcSimplify.solveCTyFunEqs,
  which resolves any residual equalities of form
      F xi ~ alpha

* When we come across a definite failure (e.g. Int ~ [a]),
  we now defer reporting the error until the end, in case we
  learn more about 'a'.  That is particularly important for
  occurs-check errors.  These are called "frozen" type errors.

* Other improvements in error message generation.

* Better tracing messages
parent 9ba922ee
...@@ -475,9 +475,7 @@ hasEqualities givens = any (has_eq . evVarPred) givens ...@@ -475,9 +475,7 @@ hasEqualities givens = any (has_eq . evVarPred) givens
where where
has_eq (EqPred {}) = True has_eq (EqPred {}) = True
has_eq (IParam {}) = False has_eq (IParam {}) = False
has_eq (ClassP cls tys) = any has_eq (substTheta subst (classSCTheta cls)) has_eq (ClassP cls _tys) = any has_eq (classSCTheta cls)
where
subst = zipOpenTvSubst (classTyVars cls) tys
---------------- ----------------
tyVarsOfWanteds :: WantedConstraints -> TyVarSet tyVarsOfWanteds :: WantedConstraints -> TyVarSet
......
This diff is collapsed.
...@@ -3,8 +3,9 @@ module TcErrors( ...@@ -3,8 +3,9 @@ module TcErrors(
reportUnsolved, reportUnsolvedDeriv, reportUnsolved, reportUnsolvedDeriv,
reportUnsolvedWantedEvVars, warnDefaulting, reportUnsolvedWantedEvVars, warnDefaulting,
unifyCtxt, typeExtraInfoMsg, unifyCtxt, typeExtraInfoMsg,
kindErrorTcS, misMatchErrorTcS, flattenForAllErrorTcS,
occursCheckErrorTcS, solverDepthErrorTcS flattenForAllErrorTcS,
solverDepthErrorTcS
) where ) where
#include "HsVersions.h" #include "HsVersions.h"
...@@ -13,6 +14,8 @@ import TcRnMonad ...@@ -13,6 +14,8 @@ import TcRnMonad
import TcMType import TcMType
import TcSMonad import TcSMonad
import TcType import TcType
import TypeRep
import Inst import Inst
import InstEnv import InstEnv
...@@ -47,24 +50,126 @@ from the insts, or just whatever seems to be around in the monad just ...@@ -47,24 +50,126 @@ from the insts, or just whatever seems to be around in the monad just
now? now?
\begin{code} \begin{code}
reportUnsolved :: (CanonicalCts, Bag Implication) -> TcM () reportUnsolved :: (Bag WantedEvVar, Bag Implication) -> Bag FrozenError -> TcM ()
reportUnsolved (unsolved_flats, unsolved_implics) reportUnsolved (unsolved_flats, unsolved_implics) frozen_errors
| isEmptyBag unsolved | isEmptyBag unsolved && isEmptyBag frozen_errors
= return () = return ()
| otherwise | otherwise
= do { unsolved <- mapBagM zonkWanted unsolved = do { frozen_errors_zonked <- mapBagM zonk_frozen frozen_errors
; let frozen_tvs = tyVarsOfFrozen frozen_errors_zonked
; unsolved <- mapBagM zonkWanted unsolved
-- Zonk to un-flatten any flatten-skols -- Zonk to un-flatten any flatten-skols
; env0 <- tcInitTidyEnv ; env0 <- tcInitTidyEnv
; let tidy_env = tidyFreeTyVars env0 (tyVarsOfWanteds unsolved) ; let tidy_env = tidyFreeTyVars env0 $
tyVarsOfWanteds unsolved `unionVarSet` frozen_tvs
tidy_unsolved = tidyWanteds tidy_env unsolved tidy_unsolved = tidyWanteds tidy_env unsolved
err_ctxt = CEC { cec_encl = [] err_ctxt = CEC { cec_encl = []
, cec_extra = empty , cec_extra = empty
, cec_tidy = tidy_env } , cec_tidy = tidy_env
; traceTc "reportUnsolved" (ppr unsolved) }
; traceTc "reportUnsolved" (vcat [
text "Unsolved constraints =" <+> ppr unsolved,
text "Frozen errors =" <+> ppr frozen_errors_zonked ])
; let tidy_frozen_errors_zonked = tidyFrozen tidy_env frozen_errors_zonked
; reportTidyFrozens tidy_env tidy_frozen_errors_zonked
; reportTidyWanteds err_ctxt tidy_unsolved } ; reportTidyWanteds err_ctxt tidy_unsolved }
where where
unsolved = mkWantedConstraints unsolved_flats unsolved_implics unsolved = Bag.mapBag WcEvVar unsolved_flats `unionBags`
Bag.mapBag WcImplic unsolved_implics
zonk_frozen (FrozenError frknd fl ty1 ty2)
= do { ty1z <- zonkTcType ty1
; ty2z <- zonkTcType ty2
; return (FrozenError frknd fl ty1z ty2z) }
tyVarsOfFrozen fr
= unionVarSets $ bagToList (mapBag tvs_of_frozen fr)
tvs_of_frozen (FrozenError _ _ ty1 ty2) = tyVarsOfTypes [ty1,ty2]
tidyFrozen env fr = mapBag (tidy_frozen env) fr
tidy_frozen env (FrozenError frknd fl ty1 ty2)
= FrozenError frknd fl (tidyType env ty1) (tidyType env ty2)
reportTidyFrozens :: TidyEnv -> Bag FrozenError -> TcM ()
reportTidyFrozens tidy_env fr = mapBagM_ (reportTidyFrozen tidy_env) fr
reportTidyFrozen :: TidyEnv -> FrozenError -> TcM ()
reportTidyFrozen tidy_env err@(FrozenError _ fl _ty1 _ty2)
= do { let dec_errs = decompFrozenError err
init_err_ctxt = CEC { cec_encl = []
, cec_extra = empty
, cec_tidy = tidy_env }
; mapM_ (report_dec_err init_err_ctxt) dec_errs }
where
report_dec_err err_ctxt (ty1,ty2)
-- The only annoying thing here is that in the given case,
-- the ``Inaccessible code'' message will be printed once for
-- each decomposed equality.
= do { (tidy_env2,extra2)
<- if isGiven fl
then return (cec_tidy err_ctxt, inaccessible_msg)
else getWantedEqExtra emptyTvSubst (cec_tidy err_ctxt) loc_orig ty1 ty2
; let err_ctxt2 = err_ctxt { cec_tidy = tidy_env2
, cec_extra = cec_extra err_ctxt $$ extra2 }
; setCtFlavorLoc fl $
reportEqErr err_ctxt2 ty1 ty2
}
loc_orig | Wanted loc <- fl = ctLocOrigin loc
| Derived loc _ <- fl = ctLocOrigin loc
| otherwise = pprPanic "loc_orig" empty
inaccessible_msg
| Given loc <- fl
= hang (ptext (sLit "Inaccessible code in")) 2 (mk_what loc)
| otherwise = pprPanic "inaccessible_msg" empty
mk_what loc
= case ctLocOrigin loc of
PatSkol dc mc -> sep [ ptext (sLit "a pattern with constructor")
<+> quotes (ppr dc) <> comma
, ptext (sLit "in") <+> pprMatchContext mc ]
other_skol -> pprSkolInfo other_skol
decompFrozenError :: FrozenError -> [(TcType,TcType)]
-- Postcondition: will always return a non-empty list
decompFrozenError (FrozenError errk _fl ty1 ty2)
| OccCheckError <- errk
= dec_occ_check ty1 ty2
| otherwise
= [(ty1,ty2)]
where dec_occ_check :: TcType -> TcType -> [(TcType,TcType)]
-- This error arises from an original:
-- a ~ Maybe a
-- But by now the a has been substituted away, eg:
-- Int ~ Maybe Int
-- Maybe b ~ Maybe (Maybe b)
dec_occ_check ty1 ty2
| tcEqType ty1 ty2 = []
dec_occ_check ty1@(TyVarTy {}) ty2 = [(ty1,ty2)]
dec_occ_check (FunTy s1 t1) (FunTy s2 t2)
= let errs1 = dec_occ_check s1 s2
errs2 = dec_occ_check t1 t2
in errs1 ++ errs2
dec_occ_check ty1@(TyConApp fn1 tys1) ty2@(TyConApp fn2 tys2)
| fn1 == fn2 && length tys1 == length tys2
, not (isSynFamilyTyCon fn1)
= concatMap (\(t1,t2) -> dec_occ_check t1 t2) (zip tys1 tys2)
| otherwise
= [(ty1,ty2)]
dec_occ_check ty1 ty2
| Just (s1,t1) <- tcSplitAppTy_maybe ty1
, Just (s2,t2) <- tcSplitAppTy_maybe ty2
= let errs1 = dec_occ_check s1 s2
errs2 = dec_occ_check t1 t2
in errs1 ++ errs2
dec_occ_check ty1 ty2 = [(ty1,ty2)]
reportUnsolvedWantedEvVars :: Bag WantedEvVar -> TcM () reportUnsolvedWantedEvVars :: Bag WantedEvVar -> TcM ()
reportUnsolvedWantedEvVars wanteds reportUnsolvedWantedEvVars wanteds
...@@ -123,6 +228,13 @@ reportTidyWanteds ctxt unsolved ...@@ -123,6 +228,13 @@ reportTidyWanteds ctxt unsolved
; groupErrs (reportEqErrs ctxt) tv_eqs ; groupErrs (reportEqErrs ctxt) tv_eqs
; when (null tv_eqs) $ groupErrs (reportFlat ctxt) others ; when (null tv_eqs) $ groupErrs (reportFlat ctxt) others
; traceTc "rtw" (vcat [
text "unsolved =" <+> ppr unsolved,
text "tveqs =" <+> ppr tv_eqs,
text "others =" <+> ppr others,
text "ambigs =" <+> ppr ambigs ,
text "implics =" <+> ppr implics])
; when (null tv_eqs) $ mapBagM_ (reportTidyImplic ctxt) implics ; when (null tv_eqs) $ mapBagM_ (reportTidyImplic ctxt) implics
-- Only report ambiguity if no other errors (at all) happened -- Only report ambiguity if no other errors (at all) happened
...@@ -274,7 +386,7 @@ reportEqErrs ctxt eqs orig ...@@ -274,7 +386,7 @@ reportEqErrs ctxt eqs orig
report_one (EqPred ty1 ty2) report_one (EqPred ty1 ty2)
= do { (env1, extra) <- getWantedEqExtra emptyTvSubst env0 orig ty1 ty2 = do { (env1, extra) <- getWantedEqExtra emptyTvSubst env0 orig ty1 ty2
; let ctxt' = ctxt { cec_tidy = env1 ; let ctxt' = ctxt { cec_tidy = env1
, cec_extra = cec_extra ctxt $$ extra } , cec_extra = extra $$ cec_extra ctxt }
; reportEqErr ctxt' ty1 ty2 } ; reportEqErr ctxt' ty1 ty2 }
report_one pred report_one pred
= pprPanic "reportEqErrs" (ppr pred) = pprPanic "reportEqErrs" (ppr pred)
...@@ -284,11 +396,13 @@ reportEqErr :: ReportErrCtxt -> TcType -> TcType -> TcM () ...@@ -284,11 +396,13 @@ reportEqErr :: ReportErrCtxt -> TcType -> TcType -> TcM ()
reportEqErr ctxt ty1 ty2 reportEqErr ctxt ty1 ty2
| Just tv1 <- tcGetTyVar_maybe ty1 = reportTyVarEqErr ctxt tv1 ty2 | Just tv1 <- tcGetTyVar_maybe ty1 = reportTyVarEqErr ctxt tv1 ty2
| Just tv2 <- tcGetTyVar_maybe ty2 = reportTyVarEqErr ctxt tv2 ty1 | Just tv2 <- tcGetTyVar_maybe ty2 = reportTyVarEqErr ctxt tv2 ty1
| otherwise -- Neither side is a type variable | otherwise -- Neither side is a type variable
-- Since the unsolved constraint is canonical, -- Since the unsolved constraint is canonical,
-- it must therefore be of form (F tys ~ ty) -- it must therefore be of form (F tys ~ ty)
= addErrorReport ctxt (misMatchOrCND ctxt ty1 ty2 $$ mkTyFunInfoMsg ty1 ty2) = addErrorReport ctxt (misMatchOrCND ctxt ty1 ty2 $$ mkTyFunInfoMsg ty1 ty2)
reportTyVarEqErr :: ReportErrCtxt -> TcTyVar -> TcType -> TcM () reportTyVarEqErr :: ReportErrCtxt -> TcTyVar -> TcType -> TcM ()
-- tv1 and ty2 are already tidied -- tv1 and ty2 are already tidied
reportTyVarEqErr ctxt tv1 ty2 reportTyVarEqErr ctxt tv1 ty2
...@@ -300,14 +414,20 @@ reportTyVarEqErr ctxt tv1 ty2 ...@@ -300,14 +414,20 @@ reportTyVarEqErr ctxt tv1 ty2
| not is_meta1 | not is_meta1
= -- sk ~ ty, where ty isn't a meta-tyvar: mis-match = -- sk ~ ty, where ty isn't a meta-tyvar: mis-match
addErrTcM (addExtraInfo (misMatchOrCND ctxt ty1 ty2) addErrorReport (addExtraInfo ctxt ty1 ty2)
(cec_tidy ctxt) ty1 ty2) (misMatchOrCND ctxt ty1 ty2)
-- So tv is a meta tyvar, and presumably it is -- So tv is a meta tyvar, and presumably it is
-- an *untouchable* meta tyvar, else it'd have been unified -- an *untouchable* meta tyvar, else it'd have been unified
| not (k2 `isSubKind` k1) -- Kind error | not (k2 `isSubKind` k1) -- Kind error
= addErrorReport ctxt $ (kindErrorMsg (mkTyVarTy tv1) ty2) = addErrorReport ctxt $ (kindErrorMsg (mkTyVarTy tv1) ty2)
-- Occurs check
| tv1 `elemVarSet` tyVarsOfType ty2
= let occCheckMsg = hang (text "Occurs check: cannot construct the infinite type:") 2
(sep [ppr ty1, char '=', ppr ty2])
in addErrorReport ctxt occCheckMsg
-- Check for skolem escape -- Check for skolem escape
| (implic:_) <- cec_encl ctxt -- Get the innermost context | (implic:_) <- cec_encl ctxt -- Get the innermost context
, let esc_skols = varSetElems (tyVarsOfType ty2 `intersectVarSet` ic_skols implic) , let esc_skols = varSetElems (tyVarsOfType ty2 `intersectVarSet` ic_skols implic)
...@@ -334,15 +454,23 @@ reportTyVarEqErr ctxt tv1 ty2 ...@@ -334,15 +454,23 @@ reportTyVarEqErr ctxt tv1 ty2
, let implic_loc = ic_loc implic , let implic_loc = ic_loc implic
given = ic_given implic given = ic_given implic
= setCtLoc (ic_loc implic) $ = setCtLoc (ic_loc implic) $
do { let (env1, msg) = addExtraInfo (misMatchMsg ty1 ty2) (cec_tidy ctxt) ty1 ty2 do { let msg = misMatchMsg ty1 ty2
extra = vcat [ ptext (sLit "because") <+> ppr tv1 <+> ptext (sLit "is untouchable") extra = quotes (ppr tv1)
<+> sep [ ptext (sLit "is untouchable")
, ptext (sLit "inside the constraints") <+> pprEvVarTheta given , ptext (sLit "inside the constraints") <+> pprEvVarTheta given
, nest 2 (ptext (sLit "bound at") , ptext (sLit "bound at") <+> pprSkolInfo (ctLocOrigin implic_loc)]
<+> pprSkolInfo (ctLocOrigin implic_loc)) ] ; addErrorReport (addExtraInfo ctxt ty1 ty2) (msg $$ nest 2 extra) }
; addErrTcM (env1, msg $$ extra) }
| otherwise -- This can happen, by a recursive decomposition of frozen
-- occurs check constraints
-- Example: alpha ~ T Int alpha has frozen.
-- Then alpha gets unified to T beta gamma
-- So now we have T beta gamma ~ T Int (T beta gamma)
-- Decompose to (beta ~ Int, gamma ~ T beta gamma)
-- The (gamma ~ T beta gamma) is the occurs check, but
-- the (beta ~ Int) isn't an error at all. So return ()
= return ()
| otherwise -- I'm not sure how this can happen!
= addErrTcM (addExtraInfo (misMatchMsg ty1 ty2) (cec_tidy ctxt) ty1 ty2)
where where
is_meta1 = isMetaTyVar tv1 is_meta1 = isMetaTyVar tv1
k1 = tyVarKind tv1 k1 = tyVarKind tv1
...@@ -374,14 +502,14 @@ couldNotDeduce givens wanteds ...@@ -374,14 +502,14 @@ couldNotDeduce givens wanteds
, nest 2 $ ptext (sLit "from the context") , nest 2 $ ptext (sLit "from the context")
<+> pprEvVarTheta givens] <+> pprEvVarTheta givens]
addExtraInfo :: SDoc -> TidyEnv -> TcType -> TcType -> (TidyEnv, SDoc) addExtraInfo :: ReportErrCtxt -> TcType -> TcType -> ReportErrCtxt
-- This version is used by TcSimplify too, which doesn't track the -- Add on extra info about the types themselves
-- expected/acutal thing, so we just have ty1 ty2 here -- NB: The types themselves are already tidied
-- NB: The types are already tidied addExtraInfo ctxt ty1 ty2
addExtraInfo msg env ty1 ty2 = ctxt { cec_tidy = env2
= (env2, msg $$ nest 2 (extra1 $$ extra2)) , cec_extra = nest 2 (extra1 $$ extra2) $$ cec_extra ctxt }
where where
(env1, extra1) = typeExtraInfoMsg env ty1 (env1, extra1) = typeExtraInfoMsg (cec_tidy ctxt) ty1
(env2, extra2) = typeExtraInfoMsg env1 ty2 (env2, extra2) = typeExtraInfoMsg env1 ty2
misMatchMsg :: TcType -> TcType -> SDoc -- Types are already tidy misMatchMsg :: TcType -> TcType -> SDoc -- Types are already tidy
...@@ -659,46 +787,6 @@ are created by in RtClosureInspect.zonkRTTIType. ...@@ -659,46 +787,6 @@ are created by in RtClosureInspect.zonkRTTIType.
%************************************************************************ %************************************************************************
\begin{code} \begin{code}
kindErrorTcS :: CtFlavor -> TcType -> TcType -> TcS a
-- If there's a kind error, we don't want to blindly say "kind error"
-- We might, say, be unifying a skolem 'a' with a type 'Int',
-- in which case that's the error to report. So we set things
-- up to call reportEqErr, which does the business properly
kindErrorTcS fl ty1 ty2
= wrapEqErrTcS fl ty1 ty2 $ \ env0 ty1 ty2 extra ->
do { let ctxt = CEC { cec_encl = []
, cec_extra = extra
, cec_tidy = env0 }
; reportEqErr ctxt ty1 ty2
; failM
}
misMatchErrorTcS :: CtFlavor -> TcType -> TcType -> TcS a
misMatchErrorTcS fl ty1 ty2
= wrapEqErrTcS fl ty1 ty2 $ \ env0 ty1 ty2 extra ->
do { let msg = inaccessible_msg $$ misMatchMsg ty1 ty2
(env1, msg1) = addExtraInfo msg env0 ty1 ty2
; failWithTcM (env1, msg1 $$ extra) }
where
inaccessible_msg
= case fl of
Given loc -> hang (ptext (sLit "Inaccessible code in"))
2 (mk_what loc)
_ -> empty
mk_what loc
= case ctLocOrigin loc of
PatSkol dc mc -> sep [ ptext (sLit "a pattern with constructor")
<+> quotes (ppr dc) <> comma
, ptext (sLit "in") <+> pprMatchContext mc ]
other_skol -> pprSkolInfo other_skol
occursCheckErrorTcS :: CtFlavor -> TcTyVar -> TcType -> TcS a
occursCheckErrorTcS fl tv ty
= wrapEqErrTcS fl (mkTyVarTy tv) ty $ \ env0 ty1 ty2 extra2 ->
do { let extra1 = sep [ppr ty1, char '=', ppr ty2]
; failWithTcM (env0, hang msg 2 (extra1 $$ extra2)) }
where
msg = text $ "Occurs check: cannot construct the infinite type:"
solverDepthErrorTcS :: Int -> [CanonicalCt] -> TcS a solverDepthErrorTcS :: Int -> [CanonicalCt] -> TcS a
solverDepthErrorTcS depth stack solverDepthErrorTcS depth stack
...@@ -741,31 +829,6 @@ setCtFlavorLoc (Wanted loc) thing = setCtLoc loc thing ...@@ -741,31 +829,6 @@ setCtFlavorLoc (Wanted loc) thing = setCtLoc loc thing
setCtFlavorLoc (Derived loc _) thing = setCtLoc loc thing setCtFlavorLoc (Derived loc _) thing = setCtLoc loc thing
setCtFlavorLoc (Given loc) thing = setCtLoc loc thing setCtFlavorLoc (Given loc) thing = setCtLoc loc thing
wrapEqErrTcS :: CtFlavor -> TcType -> TcType
-> (TidyEnv -> TcType -> TcType -> SDoc -> TcM a)
-> TcS a
wrapEqErrTcS fl ty1 ty2 thing_inside
= do { ty_binds_var <- getTcSTyBinds
; wrapErrTcS $ setCtFlavorLoc fl $
do { -- Apply the current substitition
-- and zonk to get rid of flatten-skolems
; ty_binds_map <- readTcRef ty_binds_var
; let subst = mkOpenTvSubst (mapVarEnv snd ty_binds_map)
; env0 <- tcInitTidyEnv
; (env1, ty1) <- zonkSubstTidy env0 subst ty1
; (env2, ty2) <- zonkSubstTidy env1 subst ty2
; let do_wanted loc = do { (env3, extra) <- getWantedEqExtra subst env2
(ctLocOrigin loc) ty1 ty2
; thing_inside env3 ty1 ty2 extra }
; case fl of
Wanted loc -> do_wanted loc
Derived loc _ -> do_wanted loc
Given {} -> thing_inside env2 ty1 ty2 empty
-- We could print more info, but it
-- seems to be coming out already
} }
where
getWantedEqExtra :: TvSubst -> TidyEnv -> CtOrigin -> TcType -> TcType getWantedEqExtra :: TvSubst -> TidyEnv -> CtOrigin -> TcType -> TcType
-> TcM (TidyEnv, SDoc) -> TcM (TidyEnv, SDoc)
getWantedEqExtra subst env0 (TypeEqOrigin item) ty1 ty2 getWantedEqExtra subst env0 (TypeEqOrigin item) ty1 ty2
......
This diff is collapsed.
...@@ -37,7 +37,7 @@ module TcRnTypes( ...@@ -37,7 +37,7 @@ module TcRnTypes(
Implication(..), Implication(..),
CtLoc(..), ctLocSpan, ctLocOrigin, setCtLocOrigin, CtLoc(..), ctLocSpan, ctLocOrigin, setCtLocOrigin,
CtOrigin(..), EqOrigin(..), CtOrigin(..), EqOrigin(..),
WantedLoc, GivenLoc, WantedLoc, GivenLoc, pushErrCtxt,
SkolemInfo(..), SkolemInfo(..),
...@@ -879,12 +879,19 @@ ctLocOrigin (CtLoc o _ _) = o ...@@ -879,12 +879,19 @@ ctLocOrigin (CtLoc o _ _) = o
setCtLocOrigin :: CtLoc o -> o' -> CtLoc o' setCtLocOrigin :: CtLoc o -> o' -> CtLoc o'
setCtLocOrigin (CtLoc _ s c) o = CtLoc o s c setCtLocOrigin (CtLoc _ s c) o = CtLoc o s c
pushErrCtxt :: orig -> ErrCtxt -> CtLoc orig -> CtLoc orig
pushErrCtxt o err (CtLoc _ s errs) = CtLoc o s (err:errs)
pprArising :: CtOrigin -> SDoc pprArising :: CtOrigin -> SDoc
-- Used for the main, top-level error message
-- We've done special processing for TypeEq and FunDep origins
pprArising (TypeEqOrigin {}) = empty pprArising (TypeEqOrigin {}) = empty
pprArising FunDepOrigin = empty
pprArising orig = text "arising from" <+> ppr orig pprArising orig = text "arising from" <+> ppr orig
pprArisingAt :: CtLoc CtOrigin -> SDoc pprArisingAt :: Outputable o => CtLoc o -> SDoc
pprArisingAt (CtLoc o s _) = sep [pprArising o, text "at" <+> ppr s] pprArisingAt (CtLoc o s _) = sep [ text "arising from" <+> ppr o
, text "at" <+> ppr s]
------------------------------------------- -------------------------------------------
-- CtOrigin gives the origin of *wanted* constraints -- CtOrigin gives the origin of *wanted* constraints
...@@ -919,6 +926,7 @@ data CtOrigin ...@@ -919,6 +926,7 @@ data CtOrigin
| IfOrigin -- Arising from an if statement | IfOrigin -- Arising from an if statement
| ProcOrigin -- Arising from a proc expression | ProcOrigin -- Arising from a proc expression
| AnnOrigin -- An annotation | AnnOrigin -- An annotation
| FunDepOrigin
data EqOrigin data EqOrigin
= UnifyOrigin = UnifyOrigin
...@@ -953,6 +961,7 @@ pprO DoOrigin = ptext (sLit "a do statement") ...@@ -953,6 +961,7 @@ pprO DoOrigin = ptext (sLit "a do statement")
pprO ProcOrigin = ptext (sLit "a proc expression") pprO ProcOrigin = ptext (sLit "a proc expression")
pprO (TypeEqOrigin eq) = ptext (sLit "an equality") <+> ppr eq pprO (TypeEqOrigin eq) = ptext (sLit "an equality") <+> ppr eq
pprO AnnOrigin = ptext (sLit "an annotation") pprO AnnOrigin = ptext (sLit "an annotation")
pprO FunDepOrigin = ptext (sLit "a functional dependency")
instance Outputable EqOrigin where instance Outputable EqOrigin where
ppr (UnifyOrigin t1 t2) = ppr t1 <+> char '~' <+> ppr t2 ppr (UnifyOrigin t1 t2) = ppr t1 <+> char '~' <+> ppr t2
......
...@@ -12,11 +12,12 @@ module TcSMonad ( ...@@ -12,11 +12,12 @@ module TcSMonad (
makeGivens, makeSolvedByInst, makeGivens, makeSolvedByInst,
CtFlavor (..), isWanted, isGiven, isDerived, isDerivedSC, isDerivedByInst, CtFlavor (..), isWanted, isGiven, isDerived, isDerivedSC, isDerivedByInst,
isGivenCt, isWantedCt, isGivenCt, isWantedCt, pprFlavorArising,
DerivedOrig (..), DerivedOrig (..),
canRewrite, canSolve, canRewrite, canSolve,
combineCtLoc, mkGivenFlavor, combineCtLoc, mkGivenFlavor, mkWantedFlavor,
getWantedLoc,
TcS, runTcS, failTcS, panicTcS, traceTcS, traceTcS0, -- Basic functionality TcS, runTcS, failTcS, panicTcS, traceTcS, traceTcS0, -- Basic functionality
tryTcS, nestImplicTcS, recoverTcS, wrapErrTcS, wrapWarnTcS, tryTcS, nestImplicTcS, recoverTcS, wrapErrTcS, wrapWarnTcS,
...@@ -37,18 +38,20 @@ module TcSMonad ( ...@@ -37,18 +38,20 @@ module TcSMonad (
getInstEnvs, getFamInstEnvs, -- Getting the environments getInstEnvs, getFamInstEnvs, -- Getting the environments
getTopEnv, getGblEnv, getTcEvBinds, getUntouchables, getTopEnv, getGblEnv, getTcEvBinds, getUntouchables,
getTcEvBindsBag, getTcSContext, getTcSTyBinds, getTcSTyBindsMap, getTcEvBindsBag, getTcSContext, getTcSTyBinds, getTcSTyBindsMap, getTcSErrors,
getTcSErrorsBag, FrozenError (..),
addErrorTcS,
ErrorKind(..),
newFlattenSkolemTy, -- Flatten skolems newFlattenSkolemTy, -- Flatten skolems
instDFunTypes, -- Instantiation instDFunTypes, -- Instantiation
instDFunConstraints, instDFunConstraints,
newFlexiTcSTy,
isGoodRecEv, isGoodRecEv,
zonkTcTypeTcS, -- Zonk through the TyBinds of the Tcs Monad
compatKind, compatKind,
...@@ -111,6 +114,7 @@ import FunDeps ...@@ -111,6 +114,7 @@ import FunDeps
import TcRnTypes import TcRnTypes
import Control.Monad
import Data.IORef import Data.IORef
\end{code} \end{code}
...@@ -154,11 +158,7 @@ data CanonicalCt ...@@ -154,11 +158,7 @@ data CanonicalCt
-- * tv not in tvs(xi) (occurs check) -- * tv not in tvs(xi) (occurs check)
-- * If constraint is given then typeKind xi `compatKind` typeKind tv -- * If constraint is given then typeKind xi `compatKind` typeKind tv
-- See Note [Spontaneous solving and kind compatibility] -- See Note [Spontaneous solving and kind compatibility]
-- * If 'xi' is a flatten skolem then 'tv' can only be: -- * We prefer unification variables on the left *JUST* for efficiency
-- - a flatten skolem or a unification variable
-- i.e. equalities prefer flatten skolems in their LHS
-- See Note [Loopy Spontaneous Solving, Example 4]
-- Also related to [Flatten Skolem Equivalence Classes]
cc_id :: EvVar, cc_id :: EvVar,
cc_flavor :: CtFlavor, cc_flavor :: CtFlavor,
cc_tyvar :: TcTyVar, cc_tyvar :: TcTyVar,
...@@ -167,10 +167,8 @@ data CanonicalCt ...@@ -167,10 +167,8 @@ data CanonicalCt
| CFunEqCan { -- F xis ~ xi | CFunEqCan { -- F xis ~ xi
-- Invariant: * isSynFamilyTyCon cc_fun -- Invariant: * isSynFamilyTyCon cc_fun
-- * cc_rhs is not a touchable unification variable
-- See Note [No touchables as FunEq RHS]
-- * If constraint is given then -- * If constraint is given then
-- typeKind (TyConApp cc_fun cc_tyargs) `compatKind` typeKind cc_rhs -- typeKind (F xis) `compatKind` typeKind xi
cc_id :: EvVar, cc_id :: EvVar,
cc_flavor :: CtFlavor, cc_flavor :: CtFlavor,
cc_fun :: TyCon, -- A type function cc_fun :: TyCon, -- A type function
...@@ -233,26 +231,6 @@ instance Outputable CanonicalCt where ...@@ -233,26 +231,6 @@ instance Outputable CanonicalCt where
= ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyConApp tc tys, ty) = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyConApp tc tys, ty)
\end{code} \end{code}
Note [No touchables as FunEq RHS]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Notice that (F xis ~ beta), where beta is an touchable unification
variable, is not canonical. Why?
* If (F xis ~ beta) was the only wanted constraint, we'd
definitely want to spontaneously-unify it
* But suppose we had an earlier wanted (beta ~ Int), and
have already spontaneously unified it. Then we have an
identity given (id : beta ~ Int) in the inert set.
* But (F xis ~ beta) does not react with that given (because we
don't subsitute on the RHS of a function equality). So there's a
serious danger that we'd spontaneously unify it a second time.
Hence the invariant.
The invariant is
Note [Canonical implicit parameter constraints] Note [Canonical implicit parameter constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The type in a canonical implicit parameter constraint doesn't need to The type in a canonical implicit parameter constraint doesn't need to
...@@ -348,6 +326,19 @@ isDerivedByInst :: CtFlavor -> Bool ...@@ -348,6 +326,19 @@ isDerivedByInst :: CtFlavor -> Bool
isDerivedByInst (Derived _ DerInst) = True isDerivedByInst (Derived _ DerInst) = True
isDerivedByInst _ = False isDerivedByInst _ = False
pprFlavorArising :: CtFlavor -> SDoc
pprFlavorArising (Derived wl _) = pprArisingAt wl
pprFlavorArising (Wanted wl) = pprArisingAt wl
pprFlavorArising (Given gl) = pprArisingAt gl
getWantedLoc :: CanonicalCt -> WantedLoc
getWantedLoc ct