[commit: ghc] master: Interim fix for a nasty type-matching bug (9218ea6)
git at git.haskell.org
git at git.haskell.org
Thu Sep 14 09:12:53 UTC 2017
Repository : ssh://git@git.haskell.org/ghc
On branch : master
Link : http://ghc.haskell.org/trac/ghc/changeset/9218ea60faa744803fb41066aedd1da8f1bd9185/ghc
>---------------------------------------------------------------
commit 9218ea60faa744803fb41066aedd1da8f1bd9185
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date: Wed Sep 13 09:26:26 2017 +0100
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.
>---------------------------------------------------------------
9218ea60faa744803fb41066aedd1da8f1bd9185
compiler/types/Unify.hs | 68 +++++++++++++++++++++++++++++++++++++++++--------
1 file changed, 58 insertions(+), 10 deletions(-)
diff --git a/compiler/types/Unify.hs b/compiler/types/Unify.hs
index c5b7e66..cb21899 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 }, ())
More information about the ghc-commits
mailing list