From a187566d4ce21b657fd5268373d0e3743d29d886 Mon Sep 17 00:00:00 2001 From: Manuel M T Chakravarty Date: Tue, 16 Sep 2008 15:12:54 +0000 Subject: [PATCH] Type families: bug fixes --- compiler/basicTypes/Var.lhs | 8 ++++---- compiler/typecheck/Inst.lhs | 12 +++++++++++- compiler/typecheck/TcSimplify.lhs | 19 ++++++++++++++++--- compiler/typecheck/TcTyFuns.lhs | 19 ++++++++++++++----- 4 files changed, 45 insertions(+), 13 deletions(-) diff --git a/compiler/basicTypes/Var.lhs b/compiler/basicTypes/Var.lhs index cb0a11b..eec6c80 100644 --- a/compiler/basicTypes/Var.lhs +++ b/compiler/basicTypes/Var.lhs @@ -273,8 +273,7 @@ mkTyVar name kind = ASSERT( not (isCoercionKind kind ) ) mkTcTyVar :: Name -> Kind -> TcTyVarDetails -> TyVar mkTcTyVar name kind details - = -- TOM: no longer valid assertion? - -- ASSERT( not (isCoercionKind kind) ) + = -- NB: 'kind' may be a coercion kind; cf, 'TcMType.newMetaCoVar' TcTyVar { varName = name, realUnique = getKeyFastInt (nameUnique name), varType = kind, @@ -391,8 +390,9 @@ isLocalIdVar (LocalId {}) = True isLocalIdVar _ = False isCoVar :: Var -> Bool -isCoVar (v@(TyVar {})) = isCoercionVar v -isCoVar _ = False +isCoVar (v@(TyVar {})) = isCoercionVar v +isCoVar (TcTyVar {varType = kind}) = isCoercionKind kind -- used during solving +isCoVar _ = False -- | 'isLocalVar' returns @True@ for type variables as well as local 'Id's -- These are the variables that we need to pay attention to when finding free diff --git a/compiler/typecheck/Inst.lhs b/compiler/typecheck/Inst.lhs index 1a8efe2..c009ebe 100644 --- a/compiler/typecheck/Inst.lhs +++ b/compiler/typecheck/Inst.lhs @@ -45,7 +45,8 @@ module Inst ( mkIdEqInstCo, mkSymEqInstCo, mkLeftTransEqInstCo, mkRightTransEqInstCo, mkAppEqInstCo, isValidWantedEqInst, - eitherEqInst, mkEqInst, mkEqInsts, mkWantedEqInst, finalizeEqInst, + eitherEqInst, mkEqInst, mkEqInsts, mkWantedEqInst, + wantedToLocalEqInst, finalizeEqInst, eqInstType, updateEqInstCoercion, eqInstCoercion, eqInstTys ) where @@ -1095,6 +1096,15 @@ mkWantedEqInst pred@(EqPred ty1 ty2) } mkWantedEqInst pred = pprPanic "mkWantedEqInst" (ppr pred) +-- Turn a wanted equality into a local that propagates the uninstantiated +-- coercion variable as witness. We need this to propagate wanted irreds into +-- attempts to solve implication constraints. +-- +wantedToLocalEqInst :: Inst -> Inst +wantedToLocalEqInst eq@(EqInst {tci_co = Left cotv}) + = eq {tci_co = Right (mkTyVarTy cotv)} +wantedToLocalEqInst eq = eq + -- Turn a wanted into a local EqInst (needed during type inference for -- signatures) -- diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs index 8a5ad1a..c285c5e 100644 --- a/compiler/typecheck/TcSimplify.lhs +++ b/compiler/typecheck/TcSimplify.lhs @@ -1673,7 +1673,7 @@ data RedEnv , red_try_me :: Inst -> WhatToDo , red_improve :: Bool -- True <=> do improvement , red_givens :: [Inst] -- All guaranteed rigid - -- Always dicts + -- Always dicts & equalities -- but see Note [Rigidity] , red_stack :: (Int, [Inst]) -- Recursion stack (for err msg) -- See Note [RedStack] @@ -1806,8 +1806,12 @@ reduceContext env wanteds0 -- as "given" all the dicts that were originally given, -- *or* for which we now have bindings, -- *or* which are now irreds - ; let implic_env = env { red_givens = givens ++ bound_dicts ++ - dict_irreds } + -- NB: Equality irreds need to be converted, as the recursive + -- invocation of the solver will still treat them as wanteds + -- otherwise. + ; let implic_env = env { red_givens + = givens ++ bound_dicts ++ + map wantedToLocalEqInst dict_irreds } ; (implic_binds_s, implic_irreds_s) <- mapAndUnzipM (reduceImplication implic_env) wanted_implics ; let implic_binds = unionManyBags implic_binds_s @@ -1928,6 +1932,12 @@ reduceList env@(RedEnv {red_stack = (n,stk)}) wanteds state -- Base case: we're done! reduce :: RedEnv -> Inst -> Avails -> TcM Avails reduce env wanted avails + + -- We don't reduce equalities here (and they must not end up as irreds + -- in the Avails!) + | isEqInst wanted + = return avails + -- It's the same as an existing inst, or a superclass thereof | Just _ <- findAvail avails wanted = do { traceTc (text "reduce: found " <+> ppr wanted) @@ -2388,6 +2398,9 @@ extractResults (Avails _ avails) wanteds = return (binds, bound_dicts, irreds) go binds bound_dicts irreds done (w:ws) + | isEqInst w + = go binds bound_dicts (w:irreds) done' ws + | Just done_ids@(done_id : rest_done_ids) <- lookupFM done w = if w_id `elem` done_ids then go binds bound_dicts irreds done ws diff --git a/compiler/typecheck/TcTyFuns.lhs b/compiler/typecheck/TcTyFuns.lhs index 2ad6233..84453bc 100644 --- a/compiler/typecheck/TcTyFuns.lhs +++ b/compiler/typecheck/TcTyFuns.lhs @@ -442,17 +442,21 @@ deriveEqInst rewrite ty1 ty2 co instance Outputable RewriteInst where ppr (RewriteFam {rwi_fam = fam, rwi_args = args, rwi_right = rhs, rwi_co =co}) - = hsep [ ppr co <+> text "::" + = hsep [ pprEqInstCo co <+> text "::" , ppr (mkTyConApp fam args) , text "~>" , ppr rhs ] ppr (RewriteVar {rwi_var = tv, rwi_right = rhs, rwi_co =co}) - = hsep [ ppr co <+> text "::" + = hsep [ pprEqInstCo co <+> text "::" , ppr tv , text "~>" , ppr rhs ] + +pprEqInstCo :: EqInstCo -> SDoc +pprEqInstCo (Left cotv) = ptext (sLit "Wanted") <+> ppr cotv +pprEqInstCo (Right co) = ptext (sLit "Local") <+> ppr co \end{code} The following functions turn an arbitrary equality into a set of normal @@ -579,7 +583,13 @@ checkOrientation :: Type -> Type -> EqInstCo -> Inst -> TcM [RewriteInst] -- NB: We cannot assume that the two types already have outermost type -- synonyms expanded due to the recursion in the case of type applications. checkOrientation ty1 ty2 co inst - = go ty1 ty2 + = do { traceTc $ ptext (sLit "checkOrientation of ") <+> + pprEqInstCo co <+> text "::" <+> + ppr ty1 <+> text "~" <+> ppr ty2 + ; eqs <- go ty1 ty2 + ; traceTc $ ptext (sLit "checkOrientation returns") <+> ppr eqs + ; return eqs + } where -- look through synonyms go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2 @@ -1050,8 +1060,7 @@ substitute eqs locals wanteds = subst eqs [] emptyBag locals wanteds = return (res, binds, locals, wanteds) subst (eq@(RewriteVar {rwi_var = tv, rwi_right = ty, rwi_co = co}):eqs) res binds locals wanteds - = do { traceTc $ ptext (sLit "TcTyFuns.substitute:") <+> ppr tv <+> - ptext (sLit "->") <+> ppr ty + = do { traceTc $ ptext (sLit "TcTyFuns.substitute:") <+> ppr eq ; let coSubst = zipOpenTvSubst [tv] [eqInstCoType co] tySubst = zipOpenTvSubst [tv] [ty] ; eqs' <- mapM (substEq eq coSubst tySubst) eqs -- 1.7.10.4