Commit 3f2bd36c authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

Fiddling with kind errors

parent b00c29d2
......@@ -764,24 +764,7 @@ canEq loc ev ty1 ty2
| Just (tc1,tys1) <- tcSplitTyConApp_maybe ty1
, Just (tc2,tys2) <- tcSplitTyConApp_maybe ty2
, isDecomposableTyCon tc1 && isDecomposableTyCon tc2
= -- Generate equalities for each of the corresponding arguments
if (tc1 /= tc2 || length tys1 /= length tys2)
-- Fail straight away for better error messages
then canEqFailure loc ev ty1 ty2
else
do { let xcomp xs = EvCoercion (mkTcTyConAppCo tc1 (map evTermCoercion xs))
xdecomp x = zipWith (\_ i -> EvCoercion $ mkTcNthCo i (evTermCoercion x)) tys1 [0..]
xev = XEvTerm xcomp xdecomp
; ctevs <- xCtFlavor ev (zipWith mkTcEqPred tys1 tys2) xev
; canEvVarsCreated loc ctevs }
-- See Note [Equality between type applications]
-- Note [Care with type applications] in TcUnify
canEq loc ev ty1 ty2 -- e.g. F a b ~ Maybe c
-- where F has arity 1
| Just (s1,t1) <- tcSplitAppTy_maybe ty1
, Just (s2,t2) <- tcSplitAppTy_maybe ty2
= canEqAppTy loc ev s1 t1 s2 t2
= canDecomposableTyConApp loc ev tc1 tys1 tc2 tys2
canEq loc ev s1@(ForAllTy {}) s2@(ForAllTy {})
| tcIsForAllTy s1, tcIsForAllTy s2
......@@ -798,20 +781,53 @@ canEq loc ev s1@(ForAllTy {}) s2@(ForAllTy {})
= do { traceTcS "Ommitting decomposition of given polytype equality" $
pprEq s1 s2 -- See Note [Do not decompose given polytype equalities]
; return Stop }
canEq loc ev ty1 ty2 = canEqFailure loc ev ty1 ty2
-- The last remaining source of success is an application
-- e.g. F a b ~ Maybe c where F has arity 1
-- See Note [Equality between type applications]
-- Note [Care with type applications] in TcUnify
canEq loc ev ty1 ty2
= do { let flav = ctEvFlavour ev
; (s1, co1) <- flatten loc FMSubstOnly flav ty1
; (s2, co2) <- flatten loc FMSubstOnly flav ty2
; mb_ct <- rewriteCtFlavor ev (mkTcEqPred s1 s2) (mkHdEqPred s2 co1 co2)
; case mb_ct of
Nothing -> return Stop
Just new_ev -> last_chance new_ev s1 s2 }
where
last_chance new_ev ty1 ty2
| Just (tc1,tys1) <- tcSplitTyConApp_maybe ty1
, Just (tc2,tys2) <- tcSplitTyConApp_maybe ty2
, isDecomposableTyCon tc1 && isDecomposableTyCon tc2
= canDecomposableTyConApp loc new_ev tc1 tys1 tc2 tys2
| Just (s1,t1) <- tcSplitAppTy_maybe ty1
, Just (s2,t2) <- tcSplitAppTy_maybe ty2
= do { let xevcomp [x,y] = EvCoercion (mkTcAppCo (evTermCoercion x) (evTermCoercion y))
xevcomp _ = error "canEqAppTy: can't happen" -- Can't happen
xevdecomp x = let xco = evTermCoercion x
in [EvCoercion (mkTcLRCo CLeft xco), EvCoercion (mkTcLRCo CRight xco)]
; ctevs <- xCtFlavor ev [mkTcEqPred s1 s2, mkTcEqPred t1 t2] (XEvTerm xevcomp xevdecomp)
; canEvVarsCreated loc ctevs }
| otherwise
= do { emitInsoluble (CNonCanonical { cc_ev = new_ev, cc_loc = loc })
; return Stop }
------------------------
-- Type application
canEqAppTy :: CtLoc -> CtEvidence
-> Type -> Type -> Type -> Type
-> TcS StopOrContinue
canEqAppTy loc ev s1 t1 s2 t2
= ASSERT( not (isKind t1) && not (isKind t2) )
do { let xevcomp [x,y] = EvCoercion (mkTcAppCo (evTermCoercion x) (evTermCoercion y))
xevcomp _ = error "canEqAppTy: can't happen" -- Can't happen
xevdecomp x = let xco = evTermCoercion x
in [EvCoercion (mkTcLRCo CLeft xco), EvCoercion (mkTcLRCo CRight xco)]
; ctevs <- xCtFlavor ev [mkTcEqPred s1 s2, mkTcEqPred t1 t2] (XEvTerm xevcomp xevdecomp)
canDecomposableTyConApp :: CtLoc -> CtEvidence
-> TyCon -> [TcType]
-> TyCon -> [TcType]
-> TcS StopOrContinue
canDecomposableTyConApp loc ev tc1 tys1 tc2 tys2
| tc1 /= tc2 || length tys1 /= length tys2
-- Fail straight away for better error messages
= canEqFailure loc ev (mkTyConApp tc1 tys1) (mkTyConApp tc2 tys2)
| otherwise
= do { let xcomp xs = EvCoercion (mkTcTyConAppCo tc1 (map evTermCoercion xs))
xdecomp x = zipWith (\_ i -> EvCoercion $ mkTcNthCo i (evTermCoercion x)) tys1 [0..]
xev = XEvTerm xcomp xdecomp
; ctevs <- xCtFlavor ev (zipWith mkTcEqPred tys1 tys2) xev
; canEvVarsCreated loc ctevs }
canEqFailure :: CtLoc -> CtEvidence -> TcType -> TcType -> TcS StopOrContinue
......@@ -1100,7 +1116,8 @@ canEqLeaf :: CtLoc -> CtEvidence
-- saturated type function application).
-- Preconditions:
-- * one of the two arguments is variable or family applications
-- * one of the two arguments is variable
-- or an exactly-saturated family application
-- * the two types are not equal (looking through synonyms)
canEqLeaf loc ev s1 s2
| cls1 `re_orient` cls2
......
......@@ -104,8 +104,7 @@ reportUnsolved wanted
reportAllUnsolved :: WantedConstraints -> TcM ()
-- Report all unsolved goals, even if -fdefer-type-errors is on
-- See Note [Deferring coercion errors to runtime]
reportAllUnsolved wanted
= report_unsolved Nothing (panic "reportAllUnsolved") wanted
reportAllUnsolved wanted = report_unsolved Nothing False wanted
report_unsolved :: Maybe EvBindsVar -- cec_binds
-> Bool -- cec_defer
......@@ -123,11 +122,12 @@ report_unsolved mb_binds_var defer wanted
-- If we are deferring we are going to need /all/ evidence around,
-- including the evidence produced by unflattening (zonkWC)
; errs_so_far <- ifErrsM (return True) (return False)
-- ; errs_so_far <- ifErrsM (return True) (return False)
; let tidy_env = tidyFreeTyVars env0 free_tvs
free_tvs = tyVarsOfWC wanted
err_ctxt = CEC { cec_encl = []
, cec_insol = errs_so_far || insolubleWC wanted
, cec_insol = False
--errs_so_far || insolubleWC wanted
-- Don't report ambiguity errors if
-- there are any other solid errors
-- to report
......@@ -170,12 +170,12 @@ data ReportErrCtxt
reportImplic :: ReportErrCtxt -> Implication -> TcM ()
reportImplic ctxt implic@(Implic { ic_skols = tvs, ic_given = given
, ic_wanted = wanted, ic_binds = evb
, ic_insol = insoluble, ic_info = info })
, ic_insol = ic_insoluble, ic_info = info })
| BracketSkol <- info
, not insoluble -- For Template Haskell brackets report only
= return () -- definite errors. The whole thing will be re-checked
-- later when we plug it in, and meanwhile there may
-- certainly be un-satisfied constraints
, not ic_insoluble -- For Template Haskell brackets report only
= return () -- definite errors. The whole thing will be re-checked
-- later when we plug it in, and meanwhile there may
-- certainly be un-satisfied constraints
| otherwise
= reportWanteds ctxt' wanted
......@@ -185,8 +185,12 @@ reportImplic ctxt implic@(Implic { ic_skols = tvs, ic_given = given
implic' = implic { ic_skols = tvs'
, ic_given = map (tidyEvVar env2) given
, ic_info = info' }
insoluble' = case info of
InferSkol {} -> ic_insoluble
_ -> cec_insol ctxt
ctxt' = ctxt { cec_tidy = env2
, cec_encl = implic' : cec_encl ctxt
, cec_insol = insoluble'
, cec_binds = case cec_binds ctxt of
Nothing -> Nothing
Just {} -> Just evb }
......@@ -205,7 +209,8 @@ reportWanteds ctxt (WC { wc_flat = flats, wc_insol = insols, wc_impl = implics }
reportFlats :: ReportErrCtxt -> Cts -> TcM ()
reportFlats ctxt flats -- Here 'flats' includes insolble goals
= tryReporters
= traceTc "reportFlats" (ppr flats) >>
tryReporters
[ -- First deal with things that are utterly wrong
-- Like Int ~ Bool (incl nullary TyCons)
-- or Int ~ t a (AppTy on one side)
......@@ -215,13 +220,12 @@ reportFlats ctxt flats -- Here 'flats' includes insolble goals
-- Report equalities of form (a~ty). They are usually
-- skolem-equalities, and they cause confusing knock-on
-- effects in other errors; see test T4093b.
, ("Skolem equalities", skolem_eq, mkUniReporter mkEqErr1)
, ("Unambiguous", unambiguous, reportFlatErrs) ]
reportAmbigErrs
, ("Skolem equalities", skolem_eq, mkUniReporter mkEqErr1) ]
-- , ("Unambiguous", unambiguous, reportFlatErrs) ]
reportFlatErrs
ctxt (bagToList flats)
where
utterly_wrong, skolem_eq, unambiguous :: Ct -> PredTree -> Bool
utterly_wrong, skolem_eq :: Ct -> PredTree -> Bool
utterly_wrong _ (EqPred ty1 ty2) = isRigid ty1 && isRigid ty2
utterly_wrong _ _ = False
......@@ -230,6 +234,8 @@ reportFlats ctxt flats -- Here 'flats' includes insolble goals
skolem_eq _ (EqPred ty1 ty2) = isRigidOrSkol ty1 && isRigidOrSkol ty2
skolem_eq _ _ = False
{-
unambiguous :: Ct -> PredTree -> Bool
unambiguous ct pred
| not (any isAmbiguousTyVar (varSetElems (tyVarsOfCt ct)))
= True
......@@ -237,6 +243,7 @@ reportFlats ctxt flats -- Here 'flats' includes insolble goals
= case pred of
EqPred ty1 ty2 -> isNothing (isTyFun_maybe ty1) && isNothing (isTyFun_maybe ty2)
_ -> False
-}
---------------
isRigid, isRigidOrSkol :: Type -> Bool
......@@ -256,13 +263,14 @@ isTyFun_maybe ty = case tcSplitTyConApp_maybe ty of
_ -> Nothing
-----------------
{-
reportAmbigErrs :: Reporter
reportAmbigErrs ctxt cts
| cec_insol ctxt = return ()
| otherwise = reportFlatErrs ctxt cts
-- Only report ambiguity if no other errors (at all) happened
-- See Note [Avoiding spurious errors] in TcSimplify
-}
reportFlatErrs :: Reporter
-- Called once for non-ambigs, once for ambigs
-- Report equality errors, and others only if we've done all
......@@ -271,10 +279,12 @@ reportFlatErrs :: Reporter
reportFlatErrs
= tryReporters
[ ("Equalities", is_equality, mkGroupReporter mkEqErr) ]
(\ctxt cts -> do { let (dicts, ips, irreds) = go cts [] [] []
; mkGroupReporter mkIPErr ctxt ips
; mkGroupReporter mkIrredErr ctxt irreds
; mkGroupReporter mkDictErr ctxt dicts })
(\ctxt cts -> do { let ctxt' | cec_insol ctxt = ctxt { cec_suppress = True }
| otherwise = ctxt
; let (dicts, ips, irreds) = go cts [] [] []
; mkGroupReporter mkIPErr ctxt' ips
; mkGroupReporter mkIrredErr ctxt' irreds
; mkGroupReporter mkDictErr ctxt' dicts })
where
is_equality _ (EqPred {}) = True
is_equality _ _ = False
......@@ -282,7 +292,8 @@ reportFlatErrs
go [] dicts ips irreds
= (dicts, ips, irreds)
go (ct:cts) dicts ips irreds
| isIPPred (ctPred ct) = go cts dicts (ct:ips) irreds
| isIPPred (ctPred ct)
= go cts dicts (ct:ips) irreds
| otherwise
= case classifyPredType (ctPred ct) of
ClassPred {} -> go cts (ct:dicts) ips irreds
......@@ -376,6 +387,7 @@ tryReporters reporters deflt ctxt cts
-- Carry on with the rest, because we must make
-- deferred bindings for them if we have
-- -fdefer-type-errors
-- But suppress their error messages
where
(yeses, nos) = partition keep_me cts
keep_me ct = pred ct (classifyPredType (ctPred ct))
......@@ -593,13 +605,8 @@ mkTyVarEqErr :: ReportErrCtxt -> SDoc -> Ct -> Bool -> TcTyVar -> TcType -> TcM
-- tv1 and ty2 are already tidied
mkTyVarEqErr ctxt extra ct oriented tv1 ty2
-- Occurs check
| isNothing (occurCheckExpand tv1 ty2)
= let occCheckMsg = hang (text "Occurs check: cannot construct the infinite type:") 2
(sep [ppr ty1, char '~', ppr ty2])
in mkErrorMsg ctxt ct (occCheckMsg $$ extra)
| isSkolemTyVar tv1 -- ty2 won't be a meta-tyvar, or else the thing would
-- be oriented the other way round; see TcCanonical.reOrient
| isUserSkolem ctxt tv1 -- ty2 won't be a meta-tyvar, or else the thing would
-- be oriented the other way round; see TcCanonical.reOrient
|| isSigTyVar tv1 && not (isTyVarTy ty2)
= mkErrorMsg ctxt ct (vcat [ misMatchOrCND ctxt ct oriented ty1 ty2
, extraTyVarInfo ctxt ty1 ty2
......@@ -610,6 +617,11 @@ mkTyVarEqErr ctxt extra ct oriented tv1 ty2
| not (k2 `tcIsSubKind` k1) -- Kind error
= mkErrorMsg ctxt ct $ (kindErrorMsg (mkTyVarTy tv1) ty2 $$ extra)
| isNothing (occurCheckExpand tv1 ty2)
= let occCheckMsg = hang (text "Occurs check: cannot construct the infinite type:") 2
(sep [ppr ty1, char '~', ppr ty2])
in mkErrorMsg ctxt ct (occCheckMsg $$ extra)
-- Check for skolem escape
| (implic:_) <- cec_encl ctxt -- Get the innermost context
, Implic { ic_env = env, ic_skols = skols, ic_info = skol_info } <- implic
......@@ -674,6 +686,17 @@ mkEqInfoMsg ctxt ct ty1 ty2
<+> ptext (sLit "is a type function, and may not be injective")
| otherwise = empty
isUserSkolem :: ReportErrCtxt -> TcTyVar -> Bool
-- See Note [Reporting occurs-check errors]
isUserSkolem ctxt tv
= isSkolemTyVar tv && any is_user_skol_tv (cec_encl ctxt)
where
is_user_skol_tv (Implic { ic_skols = sks, ic_info = skol_info })
= tv `elem` sks && is_user_skol_info skol_info
is_user_skol_info (InferSkol {}) = False
is_user_skol_info _ = True
misMatchOrCND :: ReportErrCtxt -> Ct -> Bool -> TcType -> TcType -> SDoc
-- If oriented then ty1 is expected, ty2 is actual
misMatchOrCND ctxt ct oriented ty1 ty2
......@@ -759,6 +782,24 @@ mkExpectedActualMsg exp_ty act_ty
, text " Actual type:" <+> ppr act_ty ]
\end{code}
Note [Reporting occurs-check errors]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Given (a ~ [a]), if 'a' is a rigid type variable bound by a user-supplied
type signature, then the best thing is to report that we can't unify
a with [a], because a is a skolem variable. That avoids the confusing
"occur-check" error message.
But nowadays when inferring the type of a function with no type signature,
even if there are errors inside, we still generalise its signature and
carry on. For example
f x = x:x
Here we will infer somethiing like
f :: forall a. a -> [a]
with a suspended error of (a ~ [a]). So 'a' is now a skolem, but not
one bound by the programmer! Here we really should report an occurs check.
So isUserSkolem distinguishes the two.
Note [Non-injective type functions]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
It's very confusing to get a message like
......@@ -814,6 +855,7 @@ mk_dict_err ctxt (ct, (matches, unifiers, safe_haskell))
| null matches -- No matches but perhaps several unifiers
= do { (ctxt, is_ambig, ambig_msg) <- mkAmbigMsg ctxt [ct]
; (ctxt, binds_msg) <- relevantBindings ctxt ct
; traceTc "mk_dict_err" (ppr ct $$ ppr is_ambig $$ ambig_msg)
; return (ctxt, cannot_resolve_msg is_ambig binds_msg ambig_msg) }
| not safe_haskell -- Some matches => overlap errors
......@@ -832,8 +874,8 @@ mk_dict_err ctxt (ct, (matches, unifiers, safe_haskell))
cannot_resolve_msg has_ambig_tvs binds_msg ambig_msg
= vcat [ addArising orig (no_inst_herald <+> pprParendType pred)
, vcat (pp_givens givens)
, if has_ambig_tvs && (not (null unifiers) || not (null givens))
then ambig_msg $$ binds_msg $$ potential_msg
, if (has_ambig_tvs && all_tyvars)
then vcat [ ambig_msg, binds_msg, potential_msg ]
else empty
, show_fixes (add_to_ctxt_fixes has_ambig_tvs ++ drv_fixes) ]
......
......@@ -29,7 +29,7 @@ module TcHsType (
tcLHsType, tcCheckLHsType,
tcHsContext, tcInferApps, tcHsArgTys,
ExpKind(..), ekConstraint, expArgKind, checkExpectedKind,
ExpKind(..), ekConstraint, expArgKind,
kindGeneralize,
-- Sort-checking kinds
......@@ -1281,59 +1281,60 @@ checkExpectedKind :: Outputable a => a -> TcKind -> ExpKind -> TcM ()
-- checks that the actual kind act_kind is compatible
-- with the expected kind exp_kind
-- The first argument, ty, is used only in the error message generation
checkExpectedKind ty act_kind ek@(EK exp_kind ek_ctxt) = do
traceTc "checkExpectedKind" (ppr ty $$ ppr act_kind $$ ppr ek)
(_errs, mb_r) <- tryTc (unifyKind act_kind exp_kind)
case mb_r of
Just _ -> return () -- Unification succeeded
Nothing -> do
-- So there's definitely an error
-- Now to find out what sort
exp_kind <- zonkTcKind exp_kind
act_kind <- zonkTcKind act_kind
env0 <- tcInitTidyEnv
let (exp_as, _) = splitKindFunTys exp_kind
(act_as, _) = splitKindFunTys act_kind
n_exp_as = length exp_as
n_act_as = length act_as
n_diff_as = n_act_as - n_exp_as
(env1, tidy_exp_kind) = tidyOpenKind env0 exp_kind
(env2, tidy_act_kind) = tidyOpenKind env1 act_kind
err | n_exp_as < n_act_as -- E.g. [Maybe]
= ptext (sLit "Expecting") <+>
speakN n_diff_as <+> ptext (sLit "more argument") <>
(if n_diff_as > 1 then char 's' else empty) <+>
ptext (sLit "to") <+> quotes (ppr ty)
-- Now n_exp_as >= n_act_as. In the next two cases,
-- n_exp_as == 0, and hence so is n_act_as
| isConstraintKind tidy_act_kind
= text "Predicate" <+> quotes (ppr ty) <+> text "used as a type"
| isConstraintKind tidy_exp_kind
= text "Type of kind" <+> ppr tidy_act_kind <+> text "used as a constraint"
| isLiftedTypeKind exp_kind && isUnliftedTypeKind act_kind
= ptext (sLit "Expecting a lifted type, but") <+> quotes (ppr ty)
<+> ptext (sLit "is unlifted")
| isUnliftedTypeKind exp_kind && isLiftedTypeKind act_kind
= ptext (sLit "Expecting an unlifted type, but") <+> quotes (ppr ty)
<+> ptext (sLit "is lifted")
| otherwise -- E.g. Monad [Int]
= ptext (sLit "Kind mis-match") $$ more_info
more_info = sep [ ek_ctxt <+> ptext (sLit "kind")
<+> quotes (pprKind tidy_exp_kind) <> comma,
ptext (sLit "but") <+> quotes (ppr ty) <+>
ptext (sLit "has kind") <+> quotes (pprKind tidy_act_kind)]
failWithTcM (env2, err)
checkExpectedKind ty act_kind ek@(EK exp_kind ek_ctxt)
= do { traceTc "checkExpectedKind" (ppr ty $$ ppr act_kind $$ ppr ek)
; (_, lie) <- captureConstraints (unifyKind act_kind exp_kind)
-- Kind unification only generates definite errors
; if isEmptyWC lie
then return () -- Unification succeeded
else do
{ -- So there's an error
-- Now to find out what sort
exp_kind <- zonkTcKind exp_kind
; act_kind <- zonkTcKind act_kind
; env0 <- tcInitTidyEnv
; let (exp_as, _) = splitKindFunTys exp_kind
(act_as, _) = splitKindFunTys act_kind
n_exp_as = length exp_as
n_act_as = length act_as
n_diff_as = n_act_as - n_exp_as
(env1, tidy_exp_kind) = tidyOpenKind env0 exp_kind
(env2, tidy_act_kind) = tidyOpenKind env1 act_kind
err | n_exp_as < n_act_as -- E.g. [Maybe]
= ptext (sLit "Expecting") <+>
speakN n_diff_as <+> ptext (sLit "more argument") <>
(if n_diff_as > 1 then char 's' else empty) <+>
ptext (sLit "to") <+> quotes (ppr ty)
-- Now n_exp_as >= n_act_as. In the next two cases,
-- n_exp_as == 0, and hence so is n_act_as
| isConstraintKind tidy_act_kind
= text "Predicate" <+> quotes (ppr ty) <+> text "used as a type"
| isConstraintKind tidy_exp_kind
= text "Type of kind" <+> ppr tidy_act_kind <+> text "used as a constraint"
| isLiftedTypeKind exp_kind && isUnliftedTypeKind act_kind
= ptext (sLit "Expecting a lifted type, but") <+> quotes (ppr ty)
<+> ptext (sLit "is unlifted")
| isUnliftedTypeKind exp_kind && isLiftedTypeKind act_kind
= ptext (sLit "Expecting an unlifted type, but") <+> quotes (ppr ty)
<+> ptext (sLit "is lifted")
| otherwise -- E.g. Monad [Int]
= ptext (sLit "Kind mis-match") $$ more_info
more_info = sep [ ek_ctxt <+> ptext (sLit "kind")
<+> quotes (pprKind tidy_exp_kind) <> comma,
ptext (sLit "but") <+> quotes (ppr ty) <+>
ptext (sLit "has kind") <+> quotes (pprKind tidy_act_kind)]
; failWithTcM (env2, err) } }
\end{code}
%************************************************************************
......
......@@ -573,7 +573,9 @@ tcFamInstDecl1 :: TyCon -> FamInstDecl Name -> TcM FamInst
tcFamInstDecl1 fam_tc decl@(FamInstDecl { fid_tycon = fam_tc_name
, fid_defn = TySynonym {} })
= do { -- (0) Check it's an open type family
checkTc (isOpenSynFamilyTyCon fam_tc)
checkTc (isFamilyTyCon fam_tc) (notFamily fam_tc)
; checkTc (isSynTyCon fam_tc) (wrongKindOfFamily fam_tc)
; checkTc (isOpenSynFamilyTyCon fam_tc)
(notOpenFamily fam_tc)
-- (1) do the work of verifying the synonym
......
......@@ -457,6 +457,7 @@ trySpontaneousEqOneWay :: CtLoc -> CtEvidence
-- tv is a MetaTyVar, not untouchable
trySpontaneousEqOneWay d gw tv xi
| not (isSigTyVar tv) || isTyVarTy xi
, typeKind xi `tcIsSubKind` tyVarKind tv
= solveWithIdentity d gw tv xi
| otherwise -- Still can't solve, sig tyvar and non-variable rhs
= return SPCantSolve
......@@ -467,10 +468,12 @@ trySpontaneousEqTwoWay :: CtLoc -> CtEvidence
-- Both tyvars are *touchable* MetaTyvars so there is only a chance for kind error here
trySpontaneousEqTwoWay d gw tv1 tv2
= do { let k1_sub_k2 = k1 `tcIsSubKind` k2
; if k1_sub_k2 && nicer_to_update_tv2
then solveWithIdentity d gw tv2 (mkTyVarTy tv1)
else solveWithIdentity d gw tv1 (mkTyVarTy tv2) }
| k1 `tcIsSubKind` k2 && nicer_to_update_tv2
= solveWithIdentity d gw tv2 (mkTyVarTy tv1)
| k2 `tcIsSubKind` k1
= solveWithIdentity d gw tv1 (mkTyVarTy tv2)
| otherwise
= return SPCantSolve
where
k1 = tyVarKind tv1
k2 = tyVarKind tv2
......
......@@ -1129,12 +1129,12 @@ instance Outputable Implication where
, ic_wanted = wanted
, ic_binds = binds, ic_info = info })
= ptext (sLit "Implic") <+> braces
(sep [ ptext (sLit "Untouchables = ") <+> ppr untch
, ptext (sLit "Skolems = ") <+> ppr skols
, ptext (sLit "Flatten-skolems = ") <+> ppr fsks
, ptext (sLit "Given = ") <+> pprEvVars given
, ptext (sLit "Wanted = ") <+> ppr wanted
, ptext (sLit "Binds = ") <+> ppr binds
(sep [ ptext (sLit "Untouchables =") <+> ppr untch
, ptext (sLit "Skolems =") <+> ppr skols
, ptext (sLit "Flatten-skolems =") <+> ppr fsks
, ptext (sLit "Given =") <+> pprEvVars given
, ptext (sLit "Wanted =") <+> ppr wanted
, ptext (sLit "Binds =") <+> ppr binds
, pprSkolInfo info ])
\end{code}
......
......@@ -19,7 +19,7 @@ module TcUnify (
checkConstraints, newImplication,
-- Various unifications
unifyType, unifyTypeList, unifyTheta, unifyKind, unifyKindEq,
unifyType, unifyTypeList, unifyTheta, unifyKind,
--------------------------------
-- Holes
......@@ -59,7 +59,7 @@ import VarEnv
import ErrUtils
import DynFlags
import BasicTypes
import Maybes ( allMaybes )
import Maybes ( allMaybes, isJust )
import Util
import Outputable
import FastString
......@@ -516,6 +516,10 @@ instance Outputable SwapFlag where
ppr IsSwapped = ptext (sLit "Is-swapped")
ppr NotSwapped = ptext (sLit "Not-swapped")
flipSwap :: SwapFlag -> SwapFlag
flipSwap IsSwapped = NotSwapped
flipSwap NotSwapped = IsSwapped
unSwap :: SwapFlag -> (a->a->b) -> a -> a -> b
unSwap NotSwapped f a b = f a b
unSwap IsSwapped f a b = f b a
......@@ -810,9 +814,12 @@ uUnfilledVars origin swapped tv1 details1 tv2 details2
= do { traceTc "uUnfilledVars" ( text "trying to unify" <+> ppr k1
<+> text "with" <+> ppr k2)
; let ctxt = mkKindErrorCtxt ty1 ty2 k1 k2
; sub_kind <- addErrCtxtM ctxt $ unifyKind k1 k2
; mb_sub_kind <- addErrCtxtM ctxt $ unifyKind k1 k2
; case mb_sub_kind of {
Nothing -> unSwap swapped (uType_defer origin) (mkTyVarTy tv1) ty2 ;
Just sub_kind ->
; case (sub_kind, details1, details2) of
case (sub_kind, details1, details2) of
-- k1 < k2, so update tv2
(LT, _, MetaTv { mtv_ref = ref2 }) -> updateMeta tv2 ref2 ty1
......@@ -829,7 +836,7 @@ uUnfilledVars origin swapped tv1 details1 tv2 details2
-- Can't do it in-place, so defer
-- This happens for skolems of all sorts
(_, _, _) -> unSwap swapped (uType_defer origin) ty1 ty2 }
(_, _, _) -> unSwap swapped (uType_defer origin) ty1 ty2 } }
where
k1 = tyVarKind tv1
k2 = tyVarKind tv2
......@@ -876,8 +883,9 @@ checkTauTvUpdate tv ty
unifyKind (tyVarKind tv) (typeKind ty')
; case sub_k of
LT -> return Nothing
_ -> return (ok ty') }
Nothing -> return Nothing
Just LT -> return Nothing
_ -> return (ok ty') }
where
ok :: TcType -> Maybe TcType
-- Checks that tv does not occur in the arg type
......@@ -1080,47 +1088,47 @@ matchExpectedFunKind _ = return Nothing
-----------------
unifyKind :: TcKind -- k1 (actual)
-> TcKind -- k2 (expected)
-> TcM Ordering -- Returns the relation between the kinds
-- LT <=> k1 is a sub-kind of k2
-> TcM (Maybe Ordering)
-- Returns the relation between the kinds
-- Just LT <=> k1 is a sub-kind of k2
-- Nothing <=> incomparable
-- unifyKind deals with the top-level sub-kinding story
-- but recurses into the simpler unifyKindEq for any sub-terms
-- The sub-kinding stuff only applies at top level
unifyKind (TyVarTy kv1) k2 = uKVar False unifyKind EQ kv1 k2
unifyKind k1 (TyVarTy kv2) = uKVar True unifyKind EQ kv2 k1
unifyKind (TyVarTy kv1) k2 = uKVar NotSwapped unifyKind kv1 k2
unifyKind k1 (TyVarTy kv2) = uKVar IsSwapped unifyKind kv2 k1
unifyKind k1 k2 -- See Note [Expanding synonyms during unification]
| Just k1' <- tcView k1 = unifyKind k1' k2
| Just k2' <- tcView k2 = unifyKind k1 k2'
unifyKind k1@(TyConApp kc1 []) k2@(TyConApp kc2 [])
| kc1 == kc2 = return EQ
| kc1 `tcIsSubKindCon` kc2 = return LT
| kc2 `tcIsSubKindCon` kc1 = return GT
| kc1 == kc2 = return (Just EQ)
| kc1 `tcIsSubKindCon` kc2 = return (Just LT)
| kc2 `tcIsSubKindCon` kc1 = return (Just GT)
| otherwise = unifyKindMisMatch k1 k2
unifyKind k1 k2 = do { unifyKindEq k1 k2; return EQ }
unifyKind k1 k2 = unifyKindEq k1 k2
-- In all other cases, let unifyKindEq do the work
uKVar :: Bool -> (TcKind -> TcKind -> TcM a) -> a
-> MetaKindVar -> TcKind -> TcM a
uKVar isFlipped unify_kind eq_res kv1 k2
uKVar :: SwapFlag -> (TcKind -> TcKind -> TcM (Maybe Ordering))
-> MetaKindVar -> TcKind -> TcM (Maybe Ordering)
uKVar swapped unify_kind kv1 k2
| isTcTyVar kv1, isMetaTyVar kv1 -- See Note [Unifying kind variables]
= do { mb_k1 <- readMetaTyVar kv1
; case mb_k1 of
Flexi -> do { uUnboundKVar kv1 k2; return eq_res }
Indirect k1 -> if isFlipped then unify_kind k2 k1
else unify_kind k1 k2 }
Flexi -> uUnboundKVar kv1 k2
Indirect k1 -> unSwap swapped unify_kind k1 k2 }
| TyVarTy kv2 <- k2, kv1 == kv2
= return eq_res
= return (Just EQ)
| TyVarTy kv2 <- k2, isTcTyVar kv2, isMetaTyVar kv2
= uKVar (not isFlipped) unify_kind eq_res kv2 (TyVarTy kv1)
= uKVar (flipSwap swapped) unify_kind kv2 (TyVarTy kv1)
| otherwise = if isFlipped
then unifyKindMisMatch k2 (TyVarTy kv1)
else unifyKindMisMatch (TyVarTy kv1) k2
| otherwise
= unSwap swapped unifyKindMisMatch (TyVarTy kv1) k2
{- Note [Unifying kind variables]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
......@@ -1138,49 +1146,49 @@ Hence the isTcTyVar tests before using isMetaTyVar.