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.

1 files changed, 58 insertions, 10 deletions

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 }, ())