Adding almost devoid check for covar in ForAllCo

Summary:
For the sake of consistency of the dependent core, there is a restriction on
where a coercion variable can appear in ForAllCo: the coercion variable can
appear nowhere except in coherence coercions.

Currently this restriction is missing in Core. The goal of this patch is to add
the missing restriction.

After discussion, we decide: coercion variables can appear nowhere except in
`GRefl` and `Refl`. Relaxing the restriction to include `Refl` should not break
consistency, we premuse.

Test Plan: ./validate

Reviewers: goldfire, simonpj, bgamari

Reviewed By: goldfire

Subscribers: rwbarton, carter

GHC Trac Issues: #15757

Differential Revision: https://phabricator.haskell.org/D5231

4 files changed, 132 insertions, 23 deletions

diff --git a/compiler/coreSyn/CoreLint.hs b/compiler/coreSyn/CoreLint.hs
index 1cbfcd6c50..3aa668e952 100644
--- a/compiler/coreSyn/CoreLint.hs
+++ b/compiler/coreSyn/CoreLint.hs
@@ -1728,7 +1728,9 @@ lintCoercion (ForAllCo tv1 kind_co co)
 lintCoercion (ForAllCo cv1 kind_co co)
   -- forall over coercions
   = ASSERT( isCoVar cv1 )
-    do { (_, k2) <- lintStarCoercion kind_co
+    do { lintL (almostDevoidCoVarOfCo cv1 co)
+               (text "Covar can only appear in Refl and GRefl: " <+> ppr co)
+       ; (_, k2) <- lintStarCoercion kind_co
        ; let cv2 = setVarType cv1 k2
        ; addInScopeVar cv1 $
     do {
diff --git a/compiler/types/Coercion.hs b/compiler/types/Coercion.hs
index c766046ea8..198cfd305f 100644
--- a/compiler/types/Coercion.hs
+++ b/compiler/types/Coercion.hs
@@ -717,6 +717,10 @@ We chose (2) for two reasons:
 * even if cv occurs in body_co, it is possible that cv does not occur in the kind
   of body_co. Therefore the check in coercionKind is inevitable.
 
+The last wrinkle is that cv can only appear in Refl and GRefl for the consistency
+of the type system. Thus the almostDevoidCoVarOfCo test.
+See Section 5.8.5.2 of Richard's thesis for more details.
+This check can cause liftCoSubst to fail.
 -}
 
 
@@ -724,26 +728,28 @@ We chose (2) for two reasons:
 -- The kind of the tycovar should be the left-hand kind of the kind coercion.
 -- See Note [Unused coercion variable in ForAllCo]
 mkForAllCo :: TyCoVar -> CoercionN -> Coercion -> Coercion
-mkForAllCo tv kind_co co
-  | ASSERT( varType tv `eqType` (pFst $ coercionKind kind_co)) True
+mkForAllCo v kind_co co
+  | ASSERT( varType v `eqType` (pFst $ coercionKind kind_co)) True
+  , ASSERT( isTyVar v || almostDevoidCoVarOfCo v co) True
   , Just (ty, r) <- isReflCo_maybe co
   , isGReflCo kind_co
-  = mkReflCo r (mkTyCoInvForAllTy tv ty)
+  = mkReflCo r (mkTyCoInvForAllTy v ty)
   | otherwise
-  = ForAllCo tv kind_co co
+  = ForAllCo v kind_co co
 
 -- | Like 'mkForAllCo', but the inner coercion shouldn't be an obvious
 -- reflexive coercion. For example, it is guaranteed in 'mkForAllCos'.
 -- The kind of the tycovar should be the left-hand kind of the kind coercion.
 mkForAllCo_NoRefl :: TyCoVar -> CoercionN -> Coercion -> Coercion
-mkForAllCo_NoRefl tv kind_co co
-  | ASSERT( varType tv `eqType` (pFst $ coercionKind kind_co)) True
+mkForAllCo_NoRefl v kind_co co
+  | ASSERT( varType v `eqType` (pFst $ coercionKind kind_co)) True
+  , ASSERT( isTyVar v || almostDevoidCoVarOfCo v co) True
   , ASSERT( not (isReflCo co)) True
-  , isCoVar tv
-  , not (tv `elemVarSet` tyCoVarsOfCo co)
+  , isCoVar v
+  , not (v `elemVarSet` tyCoVarsOfCo co)
   = FunCo (coercionRole co) kind_co co
   | otherwise
-  = ForAllCo tv kind_co co
+  = ForAllCo v kind_co co
 
 -- | Make nested ForAllCos
 mkForAllCos :: [(TyCoVar, CoercionN)] -> Coercion -> Coercion
@@ -759,20 +765,20 @@ mkForAllCos bndrs co
 -- | Make a Coercion quantified over a type/coercion variable;
 -- the variable has the same type in both sides of the coercion
 mkHomoForAllCos :: [TyCoVar] -> Coercion -> Coercion
-mkHomoForAllCos tvs co
+mkHomoForAllCos vs co
   | Just (ty, r) <- isReflCo_maybe co
-  = mkReflCo r (mkTyCoInvForAllTys tvs ty)
+  = mkReflCo r (mkTyCoInvForAllTys vs ty)
   | otherwise
-  = mkHomoForAllCos_NoRefl tvs co
+  = mkHomoForAllCos_NoRefl vs co
 
 -- | Like 'mkHomoForAllCos', but the inner coercion shouldn't be an obvious
 -- reflexive coercion. For example, it is guaranteed in 'mkHomoForAllCos'.
 mkHomoForAllCos_NoRefl :: [TyCoVar] -> Coercion -> Coercion
-mkHomoForAllCos_NoRefl tvs orig_co
+mkHomoForAllCos_NoRefl vs orig_co
   = ASSERT( not (isReflCo orig_co))
-    foldr go orig_co tvs
+    foldr go orig_co vs
   where
-    go tv co = mkForAllCo_NoRefl tv (mkNomReflCo (varType tv)) co
+    go v co = mkForAllCo_NoRefl v (mkNomReflCo (varType v)) co
 
 mkCoVarCo :: CoVar -> Coercion
 -- cv :: s ~# t
@@ -1827,9 +1833,18 @@ ty_co_subst lc role ty
     go r (AppTy ty1 ty2)   = mkAppCo (go r ty1) (go Nominal ty2)
     go r (TyConApp tc tys) = mkTyConAppCo r tc (zipWith go (tyConRolesX r tc) tys)
     go r (FunTy ty1 ty2)   = mkFunCo r (go r ty1) (go r ty2)
-    go r (ForAllTy (Bndr v _) ty)
-                           = let (lc', v', h) = liftCoSubstVarBndr lc v in
-                             mkForAllCo v' h $! ty_co_subst lc' r ty
+    go r t@(ForAllTy (Bndr v _) ty)
+       = let (lc', v', h) = liftCoSubstVarBndr lc v
+             body_co = ty_co_subst lc' r ty in
+         if isTyVar v' || almostDevoidCoVarOfCo v' body_co
+           -- Lifting a ForAllTy over a coercion variable could fail as ForAllCo
+           -- imposes an extra restriction on where a covar can appear. See last
+           -- wrinkle in Note [Unused coercion variable in ForAllCo].
+           -- We specifically check for this and panic because we know that
+           -- there's a hole in the type system here, and we'd rather panic than
+           -- fall into it.
+         then mkForAllCo v' h body_co
+         else pprPanic "ty_co_subst: covar is not almost devoid" (ppr t)
     go r ty@(LitTy {})     = ASSERT( r == Nominal )
                              mkNomReflCo ty
     go r (CastTy ty co)    = castCoercionKindI (go r ty) (substLeftCo lc co)
@@ -1871,7 +1886,7 @@ callback:
   FamInstEnv, therefore the input arg 'fun' returns a pair with polymophic type
   in snd.
   However in 'liftCoSubstVarBndr', we don't need the snd, so we use unit and
-  ignore the fourth componenet of the return value.
+  ignore the fourth component of the return value.
 
 liftCoSubstTyVarBndrUsing:
   Given
diff --git a/compiler/types/Coercion.hs-boot b/compiler/types/Coercion.hs-boot
index 89aab441de..322b127568 100644
--- a/compiler/types/Coercion.hs-boot
+++ b/compiler/types/Coercion.hs-boot
@@ -16,7 +16,7 @@ import Util
 mkReflCo :: Role -> Type -> Coercion
 mkTyConAppCo :: HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
 mkAppCo :: Coercion -> Coercion -> Coercion
-mkForAllCo :: TyVar -> Coercion -> Coercion -> Coercion
+mkForAllCo :: TyCoVar -> Coercion -> Coercion -> Coercion
 mkFunCo :: Role -> Coercion -> Coercion -> Coercion
 mkCoVarCo :: CoVar -> Coercion
 mkAxiomInstCo :: CoAxiom Branched -> BranchIndex -> [Coercion] -> Coercion
diff --git a/compiler/types/TyCoRep.hs b/compiler/types/TyCoRep.hs
index 4fb6b1c774..6a05978512 100644
--- a/compiler/types/TyCoRep.hs
+++ b/compiler/types/TyCoRep.hs
@@ -86,6 +86,7 @@ module TyCoRep (
         tyCoVarsOfCoDSet,
         tyCoFVsOfCo, tyCoFVsOfCos,
         tyCoVarsOfCoList, tyCoVarsOfProv,
+        almostDevoidCoVarOfCo,
         closeOverKinds,
         injectiveVarsOfBinder, injectiveVarsOfType,
 
@@ -1666,8 +1667,8 @@ tyCoVarsOfCos cos = ty_co_vars_of_cos cos emptyVarSet emptyVarSet
 
 ty_co_vars_of_co :: Coercion -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
 ty_co_vars_of_co (Refl ty)            is acc = ty_co_vars_of_type ty is acc
-ty_co_vars_of_co (GRefl _ ty mrefl)   is acc = ty_co_vars_of_type ty is $
-                                               ty_co_vars_of_mco mrefl is acc
+ty_co_vars_of_co (GRefl _ ty mco)     is acc = ty_co_vars_of_type ty is $
+                                               ty_co_vars_of_mco mco is acc
 ty_co_vars_of_co (TyConAppCo _ _ cos) is acc = ty_co_vars_of_cos cos is acc
 ty_co_vars_of_co (AppCo co arg)       is acc = ty_co_vars_of_co co is $
                                                ty_co_vars_of_co arg is acc
@@ -1889,6 +1890,97 @@ coVarsOfCo co = getCoVarSet (tyCoFVsOfCo co)
 coVarsOfCos :: [Coercion] -> CoVarSet
 coVarsOfCos cos = getCoVarSet (tyCoFVsOfCos cos)
 
+----- Whether a covar is /Almost Devoid/ in a type or coercion ----
+
+-- | Given a covar and a coercion, returns True if covar is almost devoid in
+-- the coercion. That is, covar can only appear in Refl and GRefl.
+-- See last wrinkle in Note [Unused coercion variable in ForAllCo] in Coercion
+almostDevoidCoVarOfCo :: CoVar -> Coercion -> Bool
+almostDevoidCoVarOfCo cv co =
+  almost_devoid_co_var_of_co co cv
+
+almost_devoid_co_var_of_co :: Coercion -> CoVar -> Bool
+almost_devoid_co_var_of_co (Refl {}) _ = True   -- covar is allowed in Refl and
+almost_devoid_co_var_of_co (GRefl {}) _ = True  -- GRefl, so we don't look into
+                                                -- the coercions
+almost_devoid_co_var_of_co (TyConAppCo _ _ cos) cv
+  = almost_devoid_co_var_of_cos cos cv
+almost_devoid_co_var_of_co (AppCo co arg) cv
+  = almost_devoid_co_var_of_co co cv
+  && almost_devoid_co_var_of_co arg cv
+almost_devoid_co_var_of_co (ForAllCo v kind_co co) cv
+  = almost_devoid_co_var_of_co kind_co cv
+  && (v == cv || almost_devoid_co_var_of_co co cv)
+almost_devoid_co_var_of_co (FunCo _ co1 co2) cv
+  = almost_devoid_co_var_of_co co1 cv
+  && almost_devoid_co_var_of_co co2 cv
+almost_devoid_co_var_of_co (CoVarCo v) cv = v /= cv
+almost_devoid_co_var_of_co (HoleCo h)  cv = (coHoleCoVar h) /= cv
+almost_devoid_co_var_of_co (AxiomInstCo _ _ cos) cv
+  = almost_devoid_co_var_of_cos cos cv
+almost_devoid_co_var_of_co (UnivCo p _ t1 t2) cv
+  = almost_devoid_co_var_of_prov p cv
+  && almost_devoid_co_var_of_type t1 cv
+  && almost_devoid_co_var_of_type t2 cv
+almost_devoid_co_var_of_co (SymCo co) cv
+  = almost_devoid_co_var_of_co co cv
+almost_devoid_co_var_of_co (TransCo co1 co2) cv
+  = almost_devoid_co_var_of_co co1 cv
+  && almost_devoid_co_var_of_co co2 cv
+almost_devoid_co_var_of_co (NthCo _ _ co) cv
+  = almost_devoid_co_var_of_co co cv
+almost_devoid_co_var_of_co (LRCo _ co) cv
+  = almost_devoid_co_var_of_co co cv
+almost_devoid_co_var_of_co (InstCo co arg) cv
+  = almost_devoid_co_var_of_co co cv
+  && almost_devoid_co_var_of_co arg cv
+almost_devoid_co_var_of_co (KindCo co) cv
+  = almost_devoid_co_var_of_co co cv
+almost_devoid_co_var_of_co (SubCo co) cv
+  = almost_devoid_co_var_of_co co cv
+almost_devoid_co_var_of_co (AxiomRuleCo _ cs) cv
+  = almost_devoid_co_var_of_cos cs cv
+
+almost_devoid_co_var_of_cos :: [Coercion] -> CoVar -> Bool
+almost_devoid_co_var_of_cos [] _ = True
+almost_devoid_co_var_of_cos (co:cos) cv
+  = almost_devoid_co_var_of_co co cv
+  && almost_devoid_co_var_of_cos cos cv
+
+almost_devoid_co_var_of_prov :: UnivCoProvenance -> CoVar -> Bool
+almost_devoid_co_var_of_prov (PhantomProv co) cv
+  = almost_devoid_co_var_of_co co cv
+almost_devoid_co_var_of_prov (ProofIrrelProv co) cv
+  = almost_devoid_co_var_of_co co cv
+almost_devoid_co_var_of_prov UnsafeCoerceProv _ = True
+almost_devoid_co_var_of_prov (PluginProv _) _ = True
+
+almost_devoid_co_var_of_type :: Type -> CoVar -> Bool
+almost_devoid_co_var_of_type (TyVarTy _) _ = True
+almost_devoid_co_var_of_type (TyConApp _ tys) cv
+  = almost_devoid_co_var_of_types tys cv
+almost_devoid_co_var_of_type (LitTy {}) _ = True
+almost_devoid_co_var_of_type (AppTy fun arg) cv
+  = almost_devoid_co_var_of_type fun cv
+  && almost_devoid_co_var_of_type arg cv
+almost_devoid_co_var_of_type (FunTy arg res) cv
+  = almost_devoid_co_var_of_type arg cv
+  && almost_devoid_co_var_of_type res cv
+almost_devoid_co_var_of_type (ForAllTy (Bndr v _) ty) cv
+  = almost_devoid_co_var_of_type (varType v) cv
+  && (v == cv || almost_devoid_co_var_of_type ty cv)
+almost_devoid_co_var_of_type (CastTy ty co) cv
+  = almost_devoid_co_var_of_type ty cv
+  && almost_devoid_co_var_of_co co cv
+almost_devoid_co_var_of_type (CoercionTy co) cv
+  = almost_devoid_co_var_of_co co cv
+
+almost_devoid_co_var_of_types :: [Type] -> CoVar -> Bool
+almost_devoid_co_var_of_types [] _ = True
+almost_devoid_co_var_of_types (ty:tys) cv
+  = almost_devoid_co_var_of_type ty cv
+  && almost_devoid_co_var_of_types tys cv
+
 ------------- Closing over kinds -----------------
 
 -- | Add the kind variables free in the kinds of the tyvars in the given set.