From 9218ea60faa744803fb41066aedd1da8f1bd9185 Mon Sep 17 00:00:00 2001 From: Simon Peyton Jones Date: Wed, 13 Sep 2017 09:26:26 +0100 Subject: Interim fix for a nasty type-matching bug The type matcher in types/Unify.hs was producing a substitution that had variables from the template in its range. Yikes! This patch, documented in Note [Matching in the presence of casts], is an interm fix. Richard and I don't like it much, and are pondering a better solution (Trac #14119). All this came up in investigating Trac #13910. Alas this patch doesn't fix #13910, which still has ASSERT failures, so I have not yet added a test. But the patch does fix a definite bug. --- compiler/types/Unify.hs | 68 +++++++++++++++++++++++++++++++++++++++++-------- 1 file changed, 58 insertions(+), 10 deletions(-) (limited to 'compiler') diff --git a/compiler/types/Unify.hs b/compiler/types/Unify.hs index c5b7e66e46..cb21899d3e 100644 --- a/compiler/types/Unify.hs +++ b/compiler/types/Unify.hs @@ -769,6 +769,41 @@ dependent/should_compile/KindEqualities2, we see, for example the constraint Num (Int |> (blah ; sym blah)). We naturally want to find a dictionary for that constraint, which requires dealing with coercions in this manner. + +Note [Matching in the presence of casts] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +When matching, it is crucial that no variables from the template +end up in the range of the matching substitution (obviously!). +When unifying, that's not a constraint; instead we take the fixpoint +of the substitution at the end. + +So what should we do with this, when matching? + unify_ty (tmpl |> co) tgt kco + +Previously, wrongly, we pushed 'co' in the (horrid) accumulating +'kco' argument like this: + unify_ty (tmpl |> co) tgt kco + = unify_ty tmpl tgt (kco ; co) + +But that is obviously wrong because 'co' (from the template) ends +up in 'kco', which in turn ends up in the range of the substitution. + +This all came up in Trac #13910. Because we match tycon arguments +left-to-right, the ambient substitution will already have a matching +substitution for any kinds; so there is an easy fix: just apply +the substitution-so-far to the coercion from the LHS. + +Note that + +* When matching, the first arg of unify_ty is always the template; + we never swap round. + +* The above argument is distressingly indirect. We seek a + better way. + +* One better way is to ensure that type patterns (the template + in the matchingn process) have no casts. See Trac #14119. + -} -------------- unify_ty: the main workhorse ----------- @@ -788,7 +823,12 @@ unify_ty env ty1 ty2 kco -- TODO: More commentary needed here | Just ty1' <- tcView ty1 = unify_ty env ty1' ty2 kco | Just ty2' <- tcView ty2 = unify_ty env ty1 ty2' kco - | CastTy ty1' co <- ty1 = unify_ty env ty1' ty2 (co `mkTransCo` kco) + | CastTy ty1' co <- ty1 = if um_unif env + then unify_ty env ty1' ty2 (co `mkTransCo` kco) + else -- See Note [Matching in the presence of casts] + do { subst <- getSubst env + ; let co' = substCo subst co + ; unify_ty env ty1' ty2 (co' `mkTransCo` kco) } | CastTy ty2' co <- ty2 = unify_ty env ty1 ty2' (kco `mkTransCo` mkSymCo co) unify_ty env (TyVarTy tv1) ty2 kco @@ -913,8 +953,8 @@ uVar env tv1 ty kco = do { -- Check to see whether tv1 is refined by the substitution subst <- getTvSubstEnv ; case (lookupVarEnv subst tv1) of - Just ty' | um_unif env -- Unifying, so - -> unify_ty env ty' ty kco -- call back into unify + Just ty' | um_unif env -- Unifying, so call + -> unify_ty env ty' ty kco -- back into unify | otherwise -> -- Matching, we don't want to just recur here. -- this is because the range of the subst is the target @@ -942,17 +982,19 @@ uUnrefined env tv1 ty2 ty2' kco | TyVarTy tv2 <- ty2' = do { let tv1' = umRnOccL env tv1 tv2' = umRnOccR env tv2 + ; unless (tv1' == tv2' && um_unif env) $ do + -- If we are unifying a ~ a, just return immediately + -- Do not extend the substitution -- See Note [Self-substitution when matching] - ; when (tv1' /= tv2' || not (um_unif env)) $ do - { subst <- getTvSubstEnv + -- Check to see whether tv2 is refined + { subst <- getTvSubstEnv ; case lookupVarEnv subst tv2 of { Just ty' | um_unif env -> uUnrefined env tv1 ty' ty' kco - ; _ -> do - { -- So both are unrefined + ; _ -> - -- And then bind one or the other, - -- depending on which is bindable + do { -- So both are unrefined + -- Bind one or the other, depending on which is bindable ; let b1 = tvBindFlagL env tv1 b2 = tvBindFlagR env tv2 ty1 = mkTyVarTy tv1 @@ -974,7 +1016,7 @@ uUnrefined env tv1 ty2 ty2' kco -- ty2 is not a type variable = do { occurs <- elemNiSubstSet tv1 (tyCoVarsOfType ty2') ; if um_unif env && occurs -- See Note [Self-substitution when matching] then maybeApart -- Occurs check, see Note [Fine-grained unification] - else do bindTv env tv1 (ty2 `mkCastTy` mkSymCo kco) } + else bindTv env tv1 (ty2 `mkCastTy` mkSymCo kco) } -- Bind tyvar to the synonym if poss elemNiSubstSet :: TyVar -> TyCoVarSet -> UM Bool @@ -1079,6 +1121,12 @@ getTvSubstEnv = UM $ \state -> Unifiable (state, um_tv_env state) getCvSubstEnv :: UM CvSubstEnv getCvSubstEnv = UM $ \state -> Unifiable (state, um_cv_env state) +getSubst :: UMEnv -> UM TCvSubst +getSubst env = do { tv_env <- getTvSubstEnv + ; cv_env <- getCvSubstEnv + ; let in_scope = rnInScopeSet (um_rn_env env) + ; return (mkTCvSubst in_scope (tv_env, cv_env)) } + extendTvEnv :: TyVar -> Type -> UM () extendTvEnv tv ty = UM $ \state -> Unifiable (state { um_tv_env = extendVarEnv (um_tv_env state) tv ty }, ()) -- cgit v1.2.1