Commit 9a058b17 authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

Refactor the handling of kind errors

* Treat kind-equality constraints as *derived* equalities,
  with no evidence.  That is really what they are at the moment.

* Get rid of EvKindCast and friends.

* Postpone kind errors properly to the constraint solver
  (lots of small knock-on effects)

I moved SwapFlag to BasicTypes as well
parent 6a9542af
......@@ -66,6 +66,7 @@ module BasicTypes(
StrictnessMark(..), isMarkedStrict,
DefMethSpec(..),
SwapFlag(..), flipSwap, unSwap,
CompilerPhase(..), PhaseNum,
Activation(..), isActive, isActiveIn,
......@@ -123,6 +124,31 @@ type RepArity = Int
type Alignment = Int -- align to next N-byte boundary (N must be a power of 2).
\end{code}
%************************************************************************
%* *
Swap flag
%* *
%************************************************************************
\begin{code}
data SwapFlag
= NotSwapped -- Args are: actual, expected
| IsSwapped -- Args are: expected, actual
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
\end{code}
%************************************************************************
%* *
\subsection[FunctionOrData]{FunctionOrData}
......
......@@ -741,10 +741,6 @@ dsEvTerm (EvCast tm co)
-- 'v' is always a lifted evidence variable so it is
-- unnecessary to call varToCoreExpr v here.
dsEvTerm (EvKindCast v co)
= do { v' <- dsEvTerm v
; dsTcCoercion co $ (\_ -> v') }
dsEvTerm (EvDFunApp df tys tms) = do { tms' <- mapM dsEvTerm tms
; return (Var df `mkTyApps` tys `mkApps` tms') }
dsEvTerm (EvCoercion co) = dsTcCoercion co mkEqBox
......
......@@ -622,13 +622,17 @@ because now the 'b' has escaped its scope. We'd have to flatten to
and we have not begun to think about how to make that work!
\begin{code}
flattenTyVar :: CtLoc -> FlattenMode
-> CtFlavour -> TcTyVar -> TcS (Xi, TcCoercion)
flattenTyVar, flattenFinalTyVar
:: CtLoc -> FlattenMode
-> CtFlavour -> TcTyVar -> TcS (Xi, TcCoercion)
-- "Flattening" a type variable means to apply the substitution to it
-- The substitution is actually the union of the substitution in the TyBinds
-- for the unification variables that have been unified already with the inert
-- equalities, see Note [Spontaneously solved in TyBinds] in TcInteract.
flattenTyVar loc f ctxt tv
| not (isTcTyVar tv) -- Happens when flatten under a (forall a. ty)
= flattenFinalTyVar loc f ctxt tv -- So ty contains referneces to the non-TcTyVar a
| otherwise
= do { mb_ty <- isFilledMetaTyVar_maybe tv
; case mb_ty of {
Just ty -> flatten loc f ctxt ty ;
......@@ -655,13 +659,7 @@ flattenTyVar loc f ctxt tv
-- In fact, because of flavors, it couldn't possibly be idempotent,
-- this is explained in Note [Non-idempotent inert substitution]
Nothing ->
-- Done, but make sure the kind is zonked
do { let knd = tyVarKind tv
; (new_knd,_kind_co) <- flatten loc f ctxt knd
; let ty = mkTyVarTy (setVarType tv new_knd)
; return (ty, mkTcReflCo ty) }
Nothing -> flattenFinalTyVar loc f ctxt tv
} } } } } }
where
tv_eq_subst subst tv
......@@ -672,6 +670,13 @@ flattenTyVar loc f ctxt tv
-- NB: even if ct is Derived we are not going to
-- touch the actual coercion so we are fine.
| otherwise = Nothing
flattenFinalTyVar loc f ctxt tv
= -- Done, but make sure the kind is zonked
do { let knd = tyVarKind tv
; (new_knd,_kind_co) <- flatten loc f ctxt knd
; let ty = mkTyVarTy (setVarType tv new_knd)
; return (ty, mkTcReflCo ty) }
\end{code}
Note [Non-idempotent inert substitution]
......@@ -795,11 +800,11 @@ canEq loc ev ty1 ty2
Nothing -> return Stop
Just new_ev -> last_chance new_ev s1 s2 }
where
last_chance new_ev ty1 ty2
last_chance 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
= canDecomposableTyConApp loc ev tc1 tys1 tc2 tys2
| Just (s1,t1) <- tcSplitAppTy_maybe ty1
, Just (s2,t2) <- tcSplitAppTy_maybe ty2
......@@ -811,7 +816,7 @@ canEq loc ev ty1 ty2
; canEvVarsCreated loc ctevs }
| otherwise
= do { emitInsoluble (CNonCanonical { cc_ev = new_ev, cc_loc = loc })
= do { emitInsoluble (CNonCanonical { cc_ev = ev, cc_loc = loc })
; return Stop }
------------------------
......@@ -860,47 +865,25 @@ emitKindConstraint ct -- By now ct is canonical
_ -> continueWith ct
where
emit_kind_constraint loc ev ty1 ty2
emit_kind_constraint loc _ev ty1 ty2
| compatKind k1 k2 -- True when ty1,ty2 are themselves kinds,
= continueWith ct -- because then k1, k2 are BOX
| otherwise
= ASSERT( isKind k1 && isKind k2 )
do { mw <- newWantedEvVar (mkEqPred k1 k2)
; kev_tm <- case mw of
Cached ev_tm -> return ev_tm
Fresh kev -> do { emitWorkNC kind_co_loc [kev]
; return (ctEvTerm kev) }
; let xcomp [x] = mkEvKindCast x (evTermCoercion kev_tm)
xcomp _ = panic "emit_kind_constraint:can't happen"
xdecomp x = [mkEvKindCast x (evTermCoercion kev_tm)]
xev = XEvTerm xcomp xdecomp
; ctevs <- xCtFlavor ev [mkTcEqPred ty1 ty2] xev
-- Important: Do not cache original as Solved since we are supposed to
-- solve /exactly/ the same constraint later! Example:
-- (alpha :: kappa0)
-- (T :: *)
-- Equality is: (alpha ~ T), so we will emitConstraint (kappa0 ~ *) but
-- we don't want to say that (alpha ~ T) is now Solved!
--
-- We do need to do this xCtFlavor so that in the case of
-- -fdefer-type-errors we still make a demand on kev_tm
; case ctevs of
[] -> return Stop
[new_ctev] -> continueWith (ct { cc_ev = new_ctev })
_ -> panic "emitKindConstraint" }
do { mw <- newDerived (mkEqPred k1 k2)
; case mw of
Nothing -> return ()
Just kev -> emitWorkNC kind_co_loc [kev]
; continueWith ct }
where
k1 = typeKind ty1
k2 = typeKind ty2
ctxt = mkKindErrorCtxtTcS ty1 k1 ty2 k2
-- Always create a Wanted kind equality even if
-- you are decomposing a given constraint.
-- NB: DV finds this reasonable for now. Maybe we have to revisit.
kind_co_loc = pushErrCtxtSameOrigin ctxt loc
kind_co_loc = setCtLocOrigin loc (KindEqOrigin ty1 ty2 (ctLocOrigin loc))
\end{code}
Note [Make sure that insolubles are fully rewritten]
......
......@@ -126,14 +126,11 @@ report_unsolved mb_binds_var defer wanted
; let tidy_env = tidyFreeTyVars env0 free_tvs
free_tvs = tyVarsOfWC wanted
err_ctxt = CEC { cec_encl = []
, cec_insol = False
--errs_so_far || insolubleWC wanted
-- Don't report ambiguity errors if
-- there are any other solid errors
-- to report
, cec_tidy = tidy_env
, cec_defer = defer
, cec_suppress = False
, cec_suppress = insolubleWC wanted
-- Suppress all but insolubles if there are
-- any insoulubles, or earlier errors
, cec_binds = mb_binds_var }
; traceTc "reportUnsolved (after unflattening):" $
......@@ -151,9 +148,6 @@ data ReportErrCtxt
-- (innermost first)
-- ic_skols and givens are tidied, rest are not
, cec_tidy :: TidyEnv
, cec_insol :: Bool -- True <=> do not report errors involving
-- ambiguous errors
, cec_binds :: Maybe EvBindsVar
-- Nothinng <=> Report all errors, including holes; no bindings
-- Just ev <=> make some errors (depending on cec_defer)
......@@ -185,23 +179,20 @@ 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 }
reportWanteds :: ReportErrCtxt -> WantedConstraints -> TcM ()
reportWanteds ctxt (WC { wc_flat = flats, wc_insol = insols, wc_impl = implics })
= do { reportFlats ctxt tidy_cts
= do { reportFlats (ctxt { cec_suppress = False }) (mapBag (tidyCt env) insols)
; reportFlats ctxt (mapBag (tidyCt env) flats)
; mapBagM_ (reportImplic ctxt) implics }
where
env = cec_tidy ctxt
tidy_cts = mapBag (tidyCt env) (insols `unionBags` flats)
-- tidy_cts = mapBag (tidyCt env) (insols `unionBags` flats)
-- All the Derived ones have been filtered out alrady
-- by the constraint solver. This is ok; we don't want
-- to report unsolved Derived goals as error
......@@ -263,14 +254,6 @@ 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
......@@ -279,12 +262,10 @@ reportFlatErrs :: Reporter
reportFlatErrs
= tryReporters
[ ("Equalities", is_equality, mkGroupReporter mkEqErr) ]
(\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 })
(\ctxt cts -> do { 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
......@@ -558,10 +539,11 @@ mkEqErr1 :: ReportErrCtxt -> Ct -> TcM ErrMsg
mkEqErr1 ctxt ct
= do { (ctxt, binds_msg) <- relevantBindings ctxt ct
; (ctxt, orig) <- zonkTidyOrigin ctxt orig
; let (is_oriented, wanted_msg) = mk_wanted_extra orig
; if isGiven ev then
mkEqErr_help ctxt (inaccessible_msg orig $$ binds_msg) ct False ty1 ty2
mkEqErr_help ctxt (inaccessible_msg orig $$ binds_msg) ct Nothing ty1 ty2
else
mk_err binds_msg orig }
mkEqErr_help ctxt (wanted_msg $$ binds_msg) ct is_oriented ty1 ty2 }
where
ev = cc_ev ct
orig = ctLocOrigin (cc_loc ct)
......@@ -572,24 +554,26 @@ mkEqErr1 ctxt ct
-- If the types in the error message are the same as the types
-- we are unifying, don't add the extra expected/actual message
mk_err extra (TypeEqOrigin (UnifyOrigin { uo_actual = act, uo_expected = exp }))
| act `pickyEqType` ty1
, exp `pickyEqType` ty2 = mkEqErr_help ctxt extra ct True ty2 ty1
| exp `pickyEqType` ty1
, act `pickyEqType` ty2 = mkEqErr_help ctxt extra ct True ty1 ty2
| otherwise = mkEqErr_help ctxt extra1 ct False ty1 ty2
mk_wanted_extra orig@(TypeEqOrigin {})
= mkExpectedActualMsg ty1 ty2 orig
mk_wanted_extra (KindEqOrigin cty1 cty2 sub_o)
= (Nothing, msg1 $$ msg2)
where
extra1 = msg $$ extra
msg = mkExpectedActualMsg exp act
mk_err extra _ = mkEqErr_help ctxt extra ct False ty1 ty2
msg1 = hang (ptext (sLit "When matching types"))
2 (vcat [ ppr cty1 <+> dcolon <+> ppr (typeKind cty1)
, ppr cty2 <+> dcolon <+> ppr (typeKind cty2) ])
msg2 = case sub_o of
TypeEqOrigin {} -> snd (mkExpectedActualMsg cty1 cty2 sub_o)
_ -> empty
mk_wanted_extra _ = (Nothing, empty)
mkEqErr_help, reportEqErr
:: ReportErrCtxt -> SDoc
-> Ct
-> Bool -- True <=> Types are correct way round;
-- report "expected ty1, actual ty2"
-- False <=> Just report a mismatch without orientation
-- The ReportErrCtxt has expected/actual
-> Maybe SwapFlag -- Nothing <=> not sure
-> TcType -> TcType -> TcM ErrMsg
mkEqErr_help ctxt extra ct oriented ty1 ty2
| Just tv1 <- tcGetTyVar_maybe ty1 = mkTyVarEqErr ctxt extra ct oriented tv1 ty2
......@@ -601,7 +585,7 @@ reportEqErr ctxt extra1 ct oriented ty1 ty2
; mkErrorMsg ctxt' ct (vcat [ misMatchOrCND ctxt' ct oriented ty1 ty2
, extra2, extra1]) }
mkTyVarEqErr :: ReportErrCtxt -> SDoc -> Ct -> Bool -> TcTyVar -> TcType -> TcM ErrMsg
mkTyVarEqErr :: ReportErrCtxt -> SDoc -> Ct -> Maybe SwapFlag -> TcTyVar -> TcType -> TcM ErrMsg
-- tv1 and ty2 are already tidied
mkTyVarEqErr ctxt extra ct oriented tv1 ty2
-- Occurs check
......@@ -697,7 +681,7 @@ isUserSkolem ctxt tv
is_user_skol_info (InferSkol {}) = False
is_user_skol_info _ = True
misMatchOrCND :: ReportErrCtxt -> Ct -> Bool -> TcType -> TcType -> SDoc
misMatchOrCND :: ReportErrCtxt -> Ct -> Maybe SwapFlag -> TcType -> TcType -> SDoc
-- If oriented then ty1 is expected, ty2 is actual
misMatchOrCND ctxt ct oriented ty1 ty2
| null givens ||
......@@ -710,7 +694,7 @@ misMatchOrCND ctxt ct oriented ty1 ty2
= couldNotDeduce givens ([mkEqPred ty1 ty2], orig)
where
givens = getUserGivens ctxt
orig = TypeEqOrigin (UnifyOrigin ty1 ty2)
orig = TypeEqOrigin ty1 ty2
couldNotDeduce :: [UserGiven] -> (ThetaType, CtOrigin) -> SDoc
couldNotDeduce givens (wanteds, orig)
......@@ -763,10 +747,12 @@ kindErrorMsg ty1 ty2
k2 = typeKind ty2
--------------------
misMatchMsg :: Bool -> TcType -> TcType -> SDoc -- Types are already tidy
misMatchMsg :: Maybe SwapFlag -> TcType -> TcType -> SDoc -- Types are already tidy
-- If oriented then ty1 is expected, ty2 is actual
misMatchMsg oriented ty1 ty2
| oriented
misMatchMsg oriented ty1 ty2
| Just IsSwapped <- oriented
= misMatchMsg (Just NotSwapped) ty2 ty1
| Just NotSwapped <- oriented
= sep [ ptext (sLit "Couldn't match expected") <+> what <+> quotes (ppr ty1)
, nest 12 $ ptext (sLit "with actual") <+> what <+> quotes (ppr ty2) ]
| otherwise
......@@ -776,10 +762,16 @@ misMatchMsg oriented ty1 ty2
what | isKind ty1 = ptext (sLit "kind")
| otherwise = ptext (sLit "type")
mkExpectedActualMsg :: Type -> Type -> SDoc
mkExpectedActualMsg exp_ty act_ty
= vcat [ text "Expected type:" <+> ppr exp_ty
, text " Actual type:" <+> ppr act_ty ]
mkExpectedActualMsg :: Type -> Type -> CtOrigin -> (Maybe SwapFlag, SDoc)
mkExpectedActualMsg ty1 ty2 (TypeEqOrigin { uo_actual = act, uo_expected = exp })
| act `pickyEqType` ty1, exp `pickyEqType` ty2 = (Just IsSwapped, empty)
| exp `pickyEqType` ty1, act `pickyEqType` ty2 = (Just NotSwapped, empty)
| otherwise = (Nothing, msg)
where
msg = vcat [ text "Expected type:" <+> ppr exp
, text " Actual type:" <+> ppr act ]
mkExpectedActualMsg _ _ _ = panic "mkExprectedAcutalMsg"
\end{code}
Note [Reporting occurs-check errors]
......@@ -874,7 +866,7 @@ 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 && all_tyvars)
, if (has_ambig_tvs && not (null unifiers && null givens))
then vcat [ ambig_msg, binds_msg, potential_msg ]
else empty
, show_fixes (add_to_ctxt_fixes has_ambig_tvs ++ drv_fixes) ]
......@@ -1232,10 +1224,15 @@ zonkTidyOrigin ctxt (GivenOrigin skol_info)
= do { skol_info1 <- zonkSkolemInfo skol_info
; let (env1, skol_info2) = tidySkolemInfo (cec_tidy ctxt) skol_info1
; return (ctxt { cec_tidy = env1 }, GivenOrigin skol_info2) }
zonkTidyOrigin ctxt (TypeEqOrigin (UnifyOrigin { uo_actual = act, uo_expected = exp }))
zonkTidyOrigin ctxt (TypeEqOrigin { uo_actual = act, uo_expected = exp })
= do { (env1, act') <- zonkTidyTcType (cec_tidy ctxt) act
; (env2, exp') <- zonkTidyTcType env1 exp
; return ( ctxt { cec_tidy = env2 }
, TypeEqOrigin (UnifyOrigin { uo_actual = act', uo_expected = exp' })) }
, TypeEqOrigin { uo_actual = act', uo_expected = exp' }) }
zonkTidyOrigin ctxt (KindEqOrigin ty1 ty2 orig)
= do { (env1, ty1') <- zonkTidyTcType (cec_tidy ctxt) ty1
; (env2, ty2') <- zonkTidyTcType env1 ty2
; (ctxt2, orig') <- zonkTidyOrigin (ctxt { cec_tidy = env2 }) orig
; return (ctxt2, KindEqOrigin ty1' ty2' orig') }
zonkTidyOrigin ctxt orig = return (ctxt, orig)
\end{code}
......@@ -16,7 +16,7 @@ module TcEvidence (
EvBind(..), emptyTcEvBinds, isEmptyTcEvBinds,
EvTerm(..), mkEvCast, evVarsOfTerm, mkEvKindCast,
EvTerm(..), mkEvCast, evVarsOfTerm,
EvLit(..), evTermCoercion,
-- TcCoercion
......@@ -483,8 +483,6 @@ data EvTerm
-- dictionaries, even though the former have no
-- selector Id. We count up from _0_
| EvKindCast EvTerm TcCoercion -- See Note [EvKindCast]
| EvLit EvLit -- Dictionary for class "SingI" for type lits.
-- Note [EvLit]
......@@ -521,19 +519,6 @@ and the constraint
[G] g1 :: a~Bool
See Trac [7238]
Note [EvKindCast]
~~~~~~~~~~~~~~~~~
EvKindCast g kco is produced when we have a constraint (g : s1 ~ s2)
but the kinds of s1 and s2 (k1 and k2 respectively) don't match but
are rather equal by a coercion. You may think that this coercion will
always turn out to be ReflCo, so why is this needed? Because sometimes
we will want to defer kind errors until the runtime and in these cases
that coercion will be an 'error' term, which we want to evaluate rather
than silently forget about!
The relevant (and only) place where such a coercion is produced in
the simplifier is in TcCanonical.emitKindConstraint.
Note [EvBinds/EvTerm]
~~~~~~~~~~~~~~~~~~~~~
How evidence is created and updated. Bindings for dictionaries,
......@@ -595,11 +580,6 @@ mkEvCast ev lco
| isTcReflCo lco = ev
| otherwise = EvCast ev lco
mkEvKindCast :: EvTerm -> TcCoercion -> EvTerm
mkEvKindCast ev lco
| isTcReflCo lco = ev
| otherwise = EvKindCast ev lco
emptyTcEvBinds :: TcEvBinds
emptyTcEvBinds = EvBinds emptyBag
......@@ -625,7 +605,6 @@ evVarsOfTerm (EvSuperClass v _) = evVarsOfTerm v
evVarsOfTerm (EvCast tm co) = evVarsOfTerm tm `unionVarSet` coVarsOfTcCo co
evVarsOfTerm (EvTupleMk evs) = evVarsOfTerms evs
evVarsOfTerm (EvDelayedError _ _) = emptyVarSet
evVarsOfTerm (EvKindCast v co) = coVarsOfTcCo co `unionVarSet` evVarsOfTerm v
evVarsOfTerm (EvLit _) = emptyVarSet
evVarsOfTerms :: [EvTerm] -> VarSet
......@@ -683,7 +662,6 @@ instance Outputable EvBind where
instance Outputable EvTerm where
ppr (EvId v) = ppr v
ppr (EvCast v co) = ppr v <+> (ptext (sLit "`cast`")) <+> pprParendTcCo co
ppr (EvKindCast v co) = ppr v <+> (ptext (sLit "`kind-cast`")) <+> pprParendTcCo co
ppr (EvCoercion co) = ptext (sLit "CO") <+> ppr co
ppr (EvTupleSel v n) = ptext (sLit "tupsel") <> parens (ppr (v,n))
ppr (EvTupleMk vs) = ptext (sLit "tupmk") <+> ppr vs
......
......@@ -1117,11 +1117,6 @@ zonkEvTerm env (EvCoercion co) = do { co' <- zonkTcLCoToLCo env co
zonkEvTerm env (EvCast tm co) = do { tm' <- zonkEvTerm env tm
; co' <- zonkTcLCoToLCo env co
; return (mkEvCast tm' co') }
zonkEvTerm env (EvKindCast v co) = do { v' <- zonkEvTerm env v
; co' <- zonkTcLCoToLCo env co
; return (mkEvKindCast v' co') }
zonkEvTerm env (EvTupleSel tm n) = do { tm' <- zonkEvTerm env tm
; return (EvTupleSel tm' n) }
zonkEvTerm env (EvTupleMk tms) = do { tms' <- mapM (zonkEvTerm env) tms
......
......@@ -29,8 +29,7 @@ module TcHsType (
tcLHsType, tcCheckLHsType,
tcHsContext, tcInferApps, tcHsArgTys,
ExpKind(..), ekConstraint, expArgKind,
kindGeneralize,
kindGeneralize, checkKind,
-- Sort-checking kinds
tcLHsKind,
......@@ -967,7 +966,7 @@ kcTyClTyVars name (HsQTvs { hsq_kvs = kvs, hsq_tvs = hs_tvs }) thing_inside
; return (n, exp_k) }
kc_tv (L _ (KindedTyVar n hs_k)) exp_k
= do { k <- tcLHsKind hs_k
; _ <- unifyKind k exp_k
; checkKind k exp_k
; check_in_scope n exp_k
; return (n, k) }
......@@ -979,7 +978,7 @@ kcTyClTyVars name (HsQTvs { hsq_kvs = kvs, hsq_tvs = hs_tvs }) thing_inside
= do { mb_thing <- tcLookupLcl_maybe n
; case mb_thing of
Nothing -> return ()
Just (AThing k) -> discardResult (unifyKind k exp_k)
Just (AThing k) -> checkKind k exp_k
Just thing -> pprPanic "check_in_scope" (ppr thing) }
-----------------------
......@@ -1014,7 +1013,7 @@ tcTyClTyVars tycon (HsQTvs { hsq_kvs = hs_kvs, hsq_tvs = hs_tvs }) thing_inside
where
tc_hs_tv (L _ (UserTyVar n)) kind = return (mkTyVar n kind)
tc_hs_tv (L _ (KindedTyVar n hs_k)) kind = do { tc_kind <- tcLHsKind hs_k
; _ <- unifyKind kind tc_kind
; checkKind kind tc_kind
; return (mkTyVar n kind) }
-----------------------------------
......@@ -1274,8 +1273,15 @@ unifyKinds fun act_kinds
; mapM_ check (zip [1..] act_kinds)
; return kind }
checkKind :: TcKind -> TcKind -> TcM ()
checkKind act_kind exp_kind
= do { mb_subk <- unifyKindX act_kind exp_kind
; case mb_subk of
Just EQ -> return ()
_ -> unifyKindMisMatch act_kind exp_kind }
checkExpectedKind :: Outputable a => a -> TcKind -> ExpKind -> TcM ()
-- A fancy wrapper for 'unifyKind', which tries
-- A fancy wrapper for 'unifyKindX', which tries
-- to give decent error messages.
-- (checkExpectedKind ty act_kind exp_kind)
-- checks that the actual kind act_kind is compatible
......@@ -1283,12 +1289,13 @@ checkExpectedKind :: Outputable a => a -> TcKind -> ExpKind -> TcM ()
-- 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)
; (_, lie) <- captureConstraints (unifyKind act_kind exp_kind)
; mb_subk <- unifyKindX act_kind exp_kind
-- Kind unification only generates definite errors
; if isEmptyWC lie
then return () -- Unification succeeded
else do
; case mb_subk of {
Just LT -> return () ; -- act_kind is a sub-kind of exp_kind
Just EQ -> return () ; -- The two are equal
_other -> do
{ -- So there's an error
-- Now to find out what sort
......@@ -1334,7 +1341,7 @@ checkExpectedKind ty act_kind ek@(EK exp_kind ek_ctxt)
ptext (sLit "but") <+> quotes (ppr ty) <+>
ptext (sLit "has kind") <+> quotes (pprKind tidy_act_kind)]
; failWithTcM (env2, err) } }
; failWithTcM (env2, err) } } }
\end{code}
%************************************************************************
......@@ -1489,5 +1496,15 @@ badPatSigTvs sig_ty bad_tvs
ptext (sLit "but are actually discarded by a type synonym") ]
, ptext (sLit "To fix this, expand the type synonym")
, ptext (sLit "[Note: I hope to lift this restriction in due course]") ]
unifyKindMisMatch :: TcKind -> TcKind -> TcM a
unifyKindMisMatch ki1 ki2 = do
ki1' <- zonkTcKind ki1
ki2' <- zonkTcKind ki2
let msg = hang (ptext (sLit "Couldn't match kind"))
2 (sep [quotes (ppr ki1'),
ptext (sLit "against"),
quotes (ppr ki2')])
failWithTc msg
\end{code}
......@@ -65,7 +65,7 @@ module TcRnTypes(
CtLoc(..), ctLocSpan, ctLocEnv, ctLocOrigin,
ctLocDepth, bumpCtLocDepth,
setCtLocOrigin,
CtOrigin(..), EqOrigin(..),
CtOrigin(..),
pushErrCtxt, pushErrCtxtSameOrigin,
SkolemInfo(..),
......@@ -1480,7 +1480,11 @@ data CtOrigin
| SpecPragOrigin Name -- Specialisation pragma for identifier
| TypeEqOrigin EqOrigin
| TypeEqOrigin { uo_actual :: TcType
, uo_expected :: TcType }
| KindEqOrigin
TcType TcType -- A kind equality arising from unifying these two types
CtOrigin -- originally arising from this
| IPOccOrigin HsIPName -- Occurrence of an implicit parameter
......@@ -1510,14 +1514,6 @@ data CtOrigin
| FunDepOrigin
| HoleOrigin
data EqOrigin
= UnifyOrigin
{ uo_actual :: TcType
, uo_expected :: TcType }
instance Outputable CtOrigin where
ppr orig = pprO orig
pprO :: CtOrigin -> SDoc
pprO (GivenOrigin sk) = ppr sk
pprO (OccurrenceOf name) = hsep [ptext (sLit "a use of"), quotes (ppr name)]
......@@ -1544,12 +1540,13 @@ pprO DefaultOrigin = ptext (sLit "a 'default' declaration")
pprO DoOrigin = ptext (sLit "a do statement")
pprO MCompOrigin = ptext (sLit "a statement in a monad comprehension")
pprO ProcOrigin = ptext (sLit "a proc expression")
pprO (TypeEqOrigin eq) = ptext (sLit "an equality") <+> ppr eq
pprO (TypeEqOrigin t1 t2) = ptext (sLit "a type equality") <+> sep [ppr t1, char '~', ppr t2]
pprO (KindEqOrigin t1 t2 _) = ptext (sLit "a kind equality arising from") <+> sep [ppr t1, char '~', ppr t2]
pprO AnnOrigin = ptext (sLit "an annotation")
pprO FunDepOrigin = ptext (sLit "a functional dependency")
pprO HoleOrigin = ptext (sLit "a use of the hole") <+> quotes (ptext $ sLit "_")
instance Outputable EqOrigin where
ppr (UnifyOrigin t1 t2) = ppr t1 <+> char '~' <+> ppr t2
instance Outputable CtOrigin where
ppr = pprO
\end{code}
......@@ -28,7 +28,6 @@ module TcTyClsDecls (
import HsSyn
import HscTypes
import BuildTyCl
import TcUnify
import TcRnMonad
import TcEnv
import TcHsSyn
......@@ -659,7 +658,7 @@ tcTyDefn calc_isrec tc_name tvs kind
Nothing -> return ()
Just hs_k -> do { checkTc (kind_signatures) (badSigTyDecl tc_name)
; tc_kind <- tcLHsKind hs_k
; _ <- unifyKind kind tc_kind
; checkKind kind tc_kind
; return () }
; dataDeclChecks tc_name new_or_data stupid_theta cons
......@@ -771,12 +770,12 @@ kcTyDefn (TySynonym { td_synRhs = rhs_ty }) res_k
------------------
kcResultKind :: Maybe (LHsKind Name) -> Kind -> TcM ()