Allow unbound Refl binders in a RULE

Trac #13410 was failing because we had a RULE with a binder
   (c :: t~t)
and the /occurrences/ of c on the LHS were being optimised to Refl,
leaving a binder that would not be filled in by matching the LHS
of the rule.

I flirted with trying to ensure that occurrences (c :: t~t) are
not optimised to Relf, but that turned out to be fragile; it was
being done, for good reasons, in multiple places, including
  - TyCoRep.substCoVarBndr
  - Simplify.simplCast
  - Corecion.mkCoVarCo

So I fixed it in one place by making Rules.matchN deal happily
with an unbound binder (c :: t~t).  Quite easy.  See "Coercion
variables" in Note [Unbound RULE binders] in Rules.

In addition, I needed to make CoreLint be happy with an bound
RULE binder that is a Relf coercion variable

In debugging this, I was perplexed that occurrences of a variable
(c :: t~t) mysteriously turned into Refl.  I found out how it
was happening, and decided to move it:

* In TyCoRep.substCoVarBndr, do not substitute Refl for a
  binder (c :: t~t).

* In mkCoVarCo do not optimise (c :: t~t) to Refl.

Instead, we do this optimisation in optCoercion (specifically
opt_co4) where, surprisingly, the optimisation was /not/
being done.  This has no effect on what programs compile;
it just moves a relatively-expensive optimisation to optCoercion,
where it seems more properly to belong.  It's actually not clear
to me which is really "better", but this way round is less
surprising.

One small simplifying refactoring

* Eliminate TyCoRep.substCoVarBndrCallback, which was only
  called locally.

1 files changed, 7 insertions, 15 deletions

diff --git a/compiler/types/TyCoRep.hs b/compiler/types/TyCoRep.hs
index 8f9b1a5b45..52a0f1d8b4 100644
--- a/compiler/types/TyCoRep.hs
+++ b/compiler/types/TyCoRep.hs
@@ -112,7 +112,7 @@ module TyCoRep (
         substTyVar, substTyVars,
         substForAllCoBndr,
         substTyVarBndrCallback, substForAllCoBndrCallback,
-        substCoVarBndrCallback,
+        checkValidSubst, isValidTCvSubst,
 
         -- * Tidying type related things up for printing
         tidyType,      tidyTypes,
@@ -2367,21 +2367,13 @@ substTyVarBndrCallback subst_fn subst@(TCvSubst in_scope tenv cenv) old_var
         -- The uniqAway part makes sure the new variable is not already in scope
 
 substCoVarBndr :: TCvSubst -> CoVar -> (TCvSubst, CoVar)
-substCoVarBndr = substCoVarBndrCallback False substTy
-
-substCoVarBndrCallback :: Bool -- apply "sym" to the covar?
-                       -> (TCvSubst -> Type -> Type)
-                       -> TCvSubst -> CoVar -> (TCvSubst, CoVar)
-substCoVarBndrCallback sym subst_fun subst@(TCvSubst in_scope tenv cenv) old_var
+substCoVarBndr subst@(TCvSubst in_scope tenv cenv) old_var
   = ASSERT( isCoVar old_var )
     (TCvSubst (in_scope `extendInScopeSet` new_var) tenv new_cenv, new_var)
   where
-    -- When we substitute (co :: t1 ~ t2) we may get the identity (co :: t ~ t)
-    -- In that case, mkCoVarCo will return a ReflCoercion, and
-    -- we want to substitute that (not new_var) for old_var
-    new_co    = (if sym then mkSymCo else id) $ mkCoVarCo new_var
+    new_co         = mkCoVarCo new_var
     no_kind_change = all noFreeVarsOfType [t1, t2]
-    no_change = new_var == old_var && not (isReflCo new_co) && no_kind_change
+    no_change      = new_var == old_var && no_kind_change
 
     new_cenv | no_change = delVarEnv cenv old_var
              | otherwise = extendVarEnv cenv old_var new_co
@@ -2390,9 +2382,9 @@ substCoVarBndrCallback sym subst_fun subst@(TCvSubst in_scope tenv cenv) old_var
     subst_old_var = mkCoVar (varName old_var) new_var_type
 
     (_, _, t1, t2, role) = coVarKindsTypesRole old_var
-    t1' = subst_fun subst t1
-    t2' = subst_fun subst t2
-    new_var_type = uncurry (mkCoercionType role) (if sym then (t2', t1') else (t1', t2'))
+    t1' = substTy subst t1
+    t2' = substTy subst t2
+    new_var_type = mkCoercionType role t1' t2'
                   -- It's important to do the substitution for coercions,
                   -- because they can have free type variables