Commit 9218ea60 authored by Simon Peyton Jones's avatar Simon Peyton Jones

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.
parent a38acda6
......@@ -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 }, ())
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment