Add StepsProv constructor of UnivCoProvenance

15 files changed, 40 insertions, 1 deletions

diff --git a/compiler/GHC/Core/Coercion.hs b/compiler/GHC/Core/Coercion.hs
index 21e7202b96..46244b88a9 100644
--- a/compiler/GHC/Core/Coercion.hs
+++ b/compiler/GHC/Core/Coercion.hs
@@ -1352,6 +1352,7 @@ setNominalRole_maybe r co
       | case prov of PhantomProv _    -> False  -- should always be phantom
                      ProofIrrelProv _ -> True   -- it's always safe
                      PluginProv _     -> False  -- who knows? This choice is conservative.
+                     StepsProv _ _    -> True   -- it's always safe
       = Just $ UnivCo prov Nominal co1 co2
     setNominalRole_maybe_helper _ = Nothing
 
@@ -1457,8 +1458,11 @@ promoteCoercion co = case co of
 
     UnivCo (PhantomProv kco) _ _ _    -> kco
     UnivCo (ProofIrrelProv kco) _ _ _ -> kco
+
     UnivCo (PluginProv _) _ _ _       -> mkKindCo co
 
+    UnivCo (StepsProv _ _) _ _ _      -> ASSERT( False ) mkNomReflCo ki1
+
     SymCo g
       -> mkSymCo (promoteCoercion g)
 
@@ -2281,6 +2285,7 @@ seqProv :: UnivCoProvenance -> ()
 seqProv (PhantomProv co)    = seqCo co
 seqProv (ProofIrrelProv co) = seqCo co
 seqProv (PluginProv _)      = ()
+seqProv (StepsProv _ _)     = ()
 
 seqCos :: [Coercion] -> ()
 seqCos []       = ()
diff --git a/compiler/GHC/Core/Coercion/Opt.hs b/compiler/GHC/Core/Coercion/Opt.hs
index 66ba8ee8ab..9364e0d603 100644
--- a/compiler/GHC/Core/Coercion/Opt.hs
+++ b/compiler/GHC/Core/Coercion/Opt.hs
@@ -594,6 +594,7 @@ opt_univ env sym prov role oty1 oty2
 #endif
       ProofIrrelProv kco -> ProofIrrelProv $ opt_co4_wrap env sym False Nominal kco
       PluginProv _       -> prov
+      StepsProv _ _      -> prov
 
 -------------
 opt_transList :: HasDebugCallStack => InScopeSet -> [NormalCo] -> [NormalCo] -> [NormalCo]
diff --git a/compiler/GHC/Core/FVs.hs b/compiler/GHC/Core/FVs.hs
index cef3dc3cbe..22cc1de7e7 100644
--- a/compiler/GHC/Core/FVs.hs
+++ b/compiler/GHC/Core/FVs.hs
@@ -404,6 +404,7 @@ orphNamesOfProv :: UnivCoProvenance -> NameSet
 orphNamesOfProv (PhantomProv co)    = orphNamesOfCo co
 orphNamesOfProv (ProofIrrelProv co) = orphNamesOfCo co
 orphNamesOfProv (PluginProv _)      = emptyNameSet
+orphNamesOfProv (StepsProv _ _)     = emptyNameSet
 
 orphNamesOfCos :: [Coercion] -> NameSet
 orphNamesOfCos = orphNamesOfThings orphNamesOfCo
diff --git a/compiler/GHC/Core/Lint.hs b/compiler/GHC/Core/Lint.hs
index 3438f372fc..fdd7da96c0 100644
--- a/compiler/GHC/Core/Lint.hs
+++ b/compiler/GHC/Core/Lint.hs
@@ -2159,6 +2159,8 @@ lintCoercion co@(UnivCo prov r ty1 ty2)
 
      lint_prov _ _ prov@(PluginProv _) = return prov
 
+     lint_prov _ _ prov@(StepsProv _ _) = return prov -- AMG TODO: actually lint this
+
      check_kinds kco k1 k2
        = do { let Pair k1' k2' = coercionKind kco
             ; ensureEqTys k1 k1' (mkBadUnivCoMsg CLeft  co)
diff --git a/compiler/GHC/Core/TyCo/FVs.hs b/compiler/GHC/Core/TyCo/FVs.hs
index 73ff22c85b..888e2a783d 100644
--- a/compiler/GHC/Core/TyCo/FVs.hs
+++ b/compiler/GHC/Core/TyCo/FVs.hs
@@ -650,6 +650,7 @@ tyCoFVsOfProv :: UnivCoProvenance -> FV
 tyCoFVsOfProv (PhantomProv co)    fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc
 tyCoFVsOfProv (ProofIrrelProv co) fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc
 tyCoFVsOfProv (PluginProv _)      fv_cand in_scope acc = emptyFV fv_cand in_scope acc
+tyCoFVsOfProv (StepsProv _ _)     fv_cand in_scope acc = emptyFV fv_cand in_scope acc
 
 tyCoFVsOfCos :: [Coercion] -> FV
 tyCoFVsOfCos []       fv_cand in_scope acc = emptyFV fv_cand in_scope acc
@@ -720,6 +721,7 @@ almost_devoid_co_var_of_prov (PhantomProv 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 (PluginProv _) _ = True
+almost_devoid_co_var_of_prov (StepsProv _ _) _ = True
 
 almost_devoid_co_var_of_type :: Type -> CoVar -> Bool
 almost_devoid_co_var_of_type (TyVarTy _) _ = True
diff --git a/compiler/GHC/Core/TyCo/Rep.hs b/compiler/GHC/Core/TyCo/Rep.hs
index aa5423d0f6..ee559ff36c 100644
--- a/compiler/GHC/Core/TyCo/Rep.hs
+++ b/compiler/GHC/Core/TyCo/Rep.hs
@@ -1540,12 +1540,16 @@ data UnivCoProvenance
   | PluginProv String  -- ^ From a plugin, which asserts that this coercion
                        --   is sound. The string is for the use of the plugin.
 
+  | StepsProv !Int !Int  -- ^ Stepping each side by the given number of type
+                         -- family reductions results in the same type.
+
   deriving Data.Data
 
 instance Outputable UnivCoProvenance where
   ppr (PhantomProv _)    = text "(phantom)"
   ppr (ProofIrrelProv _) = text "(proof irrel.)"
   ppr (PluginProv str)   = parens (text "plugin" <+> brackets (text str))
+  ppr (StepsProv m n)    = parens (text "steps" <+> ppr m <+> ppr n)
 
 -- | A coercion to be filled in by the type-checker. See Note [Coercion holes]
 data CoercionHole
@@ -1857,6 +1861,7 @@ foldTyCo (TyCoFolder { tcf_view       = view
     go_prov env (PhantomProv co)    = go_co env co
     go_prov env (ProofIrrelProv co) = go_co env co
     go_prov _   (PluginProv _)      = mempty
+    go_prov _   (StepsProv _ _)     = mempty
 
 {- *********************************************************************
 *                                                                      *
@@ -1913,6 +1918,7 @@ provSize :: UnivCoProvenance -> Int
 provSize (PhantomProv co)    = 1 + coercionSize co
 provSize (ProofIrrelProv co) = 1 + coercionSize co
 provSize (PluginProv _)      = 1
+provSize (StepsProv _ _)     = 1
 
 {-
 ************************************************************************
diff --git a/compiler/GHC/Core/TyCo/Subst.hs b/compiler/GHC/Core/TyCo/Subst.hs
index 39695bbc06..4b3831d882 100644
--- a/compiler/GHC/Core/TyCo/Subst.hs
+++ b/compiler/GHC/Core/TyCo/Subst.hs
@@ -852,6 +852,7 @@ subst_co subst co
     go_prov (PhantomProv kco)    = PhantomProv (go kco)
     go_prov (ProofIrrelProv kco) = ProofIrrelProv (go kco)
     go_prov p@(PluginProv _)     = p
+    go_prov p@(StepsProv _ _)    = p
 
     -- See Note [Substituting in a coercion hole]
     go_hole h@(CoercionHole { ch_co_var = cv })
diff --git a/compiler/GHC/Core/TyCo/Tidy.hs b/compiler/GHC/Core/TyCo/Tidy.hs
index d25135af06..d7091aab53 100644
--- a/compiler/GHC/Core/TyCo/Tidy.hs
+++ b/compiler/GHC/Core/TyCo/Tidy.hs
@@ -261,6 +261,7 @@ tidyCo env@(_, subst) co
     go_prov (PhantomProv co)    = PhantomProv $! go co
     go_prov (ProofIrrelProv co) = ProofIrrelProv $! go co
     go_prov p@(PluginProv _)    = p
+    go_prov p@(StepsProv _ _)   = p
 
 tidyCos :: TidyEnv -> [Coercion] -> [Coercion]
 tidyCos env = strictMap (tidyCo env)
diff --git a/compiler/GHC/Core/Type.hs b/compiler/GHC/Core/Type.hs
index 5ed621d404..02e5fc9d0c 100644
--- a/compiler/GHC/Core/Type.hs
+++ b/compiler/GHC/Core/Type.hs
@@ -581,6 +581,7 @@ expandTypeSynonyms ty
     go_prov subst (PhantomProv co)    = PhantomProv (go_co subst co)
     go_prov subst (ProofIrrelProv co) = ProofIrrelProv (go_co subst co)
     go_prov _     p@(PluginProv _)    = p
+    go_prov _     p@(StepsProv _ _)   = p
 
       -- the "False" and "const" are to accommodate the type of
       -- substForAllCoBndrUsing, which is general enough to
@@ -914,6 +915,7 @@ mapTyCoX (TyCoMapper { tcm_tyvar = tyvar
     go_prov env (PhantomProv co)    = PhantomProv <$> go_co env co
     go_prov env (ProofIrrelProv co) = ProofIrrelProv <$> go_co env co
     go_prov _   p@(PluginProv _)    = return p
+    go_prov _   p@(StepsProv _ _)   = return p
 
 
 {-
@@ -3107,6 +3109,7 @@ occCheckExpand vs_to_avoid ty
     go_prov cxt (PhantomProv co)    = PhantomProv <$> go_co cxt co
     go_prov cxt (ProofIrrelProv co) = ProofIrrelProv <$> go_co cxt co
     go_prov _   p@(PluginProv _)    = return p
+    go_prov _   p@(StepsProv _ _)   = return p
 
 
 {-
@@ -3161,6 +3164,7 @@ tyConsOfType ty
      go_prov (PhantomProv co)    = go_co co
      go_prov (ProofIrrelProv co) = go_co co
      go_prov (PluginProv _)      = emptyUniqSet
+     go_prov (StepsProv _ _)     = emptyUniqSet
         -- this last case can happen from the tyConsOfType used from
         -- checkTauTvUpdate
 
diff --git a/compiler/GHC/CoreToIface.hs b/compiler/GHC/CoreToIface.hs
index 307dfd4893..11a708ae6c 100644
--- a/compiler/GHC/CoreToIface.hs
+++ b/compiler/GHC/CoreToIface.hs
@@ -313,6 +313,7 @@ toIfaceCoercionX fr co
     go_prov (PhantomProv co)    = IfacePhantomProv (go co)
     go_prov (ProofIrrelProv co) = IfaceProofIrrelProv (go co)
     go_prov (PluginProv str)    = IfacePluginProv str
+    go_prov (StepsProv m n)     = IfaceStepsProv m n
 
 toIfaceTcArgs :: TyCon -> [Type] -> IfaceAppArgs
 toIfaceTcArgs = toIfaceTcArgsX emptyVarSet
diff --git a/compiler/GHC/Iface/Syntax.hs b/compiler/GHC/Iface/Syntax.hs
index dfc39fb244..3f675772c2 100644
--- a/compiler/GHC/Iface/Syntax.hs
+++ b/compiler/GHC/Iface/Syntax.hs
@@ -1690,6 +1690,7 @@ freeNamesIfProv :: IfaceUnivCoProv -> NameSet
 freeNamesIfProv (IfacePhantomProv co)    = freeNamesIfCoercion co
 freeNamesIfProv (IfaceProofIrrelProv co) = freeNamesIfCoercion co
 freeNamesIfProv (IfacePluginProv _)      = emptyNameSet
+freeNamesIfProv (IfaceStepsProv _ _)     = emptyNameSet
 
 freeNamesIfVarBndr :: VarBndr IfaceBndr vis -> NameSet
 freeNamesIfVarBndr (Bndr bndr _) = freeNamesIfBndr bndr
diff --git a/compiler/GHC/Iface/Type.hs b/compiler/GHC/Iface/Type.hs
index b90676f062..cd550d3f63 100644
--- a/compiler/GHC/Iface/Type.hs
+++ b/compiler/GHC/Iface/Type.hs
@@ -396,6 +396,7 @@ data IfaceUnivCoProv
   = IfacePhantomProv IfaceCoercion
   | IfaceProofIrrelProv IfaceCoercion
   | IfacePluginProv String
+  | IfaceStepsProv !Int !Int
 
 {- Note [Holes in IfaceCoercion]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -595,7 +596,7 @@ substIfaceType env ty
 
     go_prov (IfacePhantomProv co)    = IfacePhantomProv (go_co co)
     go_prov (IfaceProofIrrelProv co) = IfaceProofIrrelProv (go_co co)
-    go_prov (IfacePluginProv str)    = IfacePluginProv str
+    go_prov prov                     = prov
 
 substIfaceAppArgs :: IfaceTySubst -> IfaceAppArgs -> IfaceAppArgs
 substIfaceAppArgs env args
@@ -1744,6 +1745,8 @@ pprIfaceUnivCoProv (IfaceProofIrrelProv co)
   = text "irrel" <+> pprParendIfaceCoercion co
 pprIfaceUnivCoProv (IfacePluginProv s)
   = text "plugin" <+> doubleQuotes (text s)
+pprIfaceUnivCoProv (IfaceStepsProv m n)
+  = text "steps" <+> ppr m <+> ppr n
 
 -------------------
 instance Outputable IfaceTyCon where
@@ -2101,6 +2104,10 @@ instance Binary IfaceUnivCoProv where
   put_ bh (IfacePluginProv a) = do
           putByte bh 3
           put_ bh a
+  put_ bh (IfaceStepsProv a b) = do
+          putByte bh 4
+          put_ bh a
+          put_ bh b
 
   get bh = do
       tag <- getByte bh
@@ -2111,6 +2118,9 @@ instance Binary IfaceUnivCoProv where
                    return $ IfaceProofIrrelProv a
            3 -> do a <- get bh
                    return $ IfacePluginProv a
+           4 -> do a <- get bh
+                   b <- get bh
+                   return $ IfaceStepsProv a b
            _ -> panic ("get IfaceUnivCoProv " ++ show tag)
 
 
diff --git a/compiler/GHC/IfaceToCore.hs b/compiler/GHC/IfaceToCore.hs
index b3644633af..24a72fe39d 100644
--- a/compiler/GHC/IfaceToCore.hs
+++ b/compiler/GHC/IfaceToCore.hs
@@ -1418,6 +1418,8 @@ tcIfaceUnivCoProv :: IfaceUnivCoProv -> IfL UnivCoProvenance
 tcIfaceUnivCoProv (IfacePhantomProv kco)    = PhantomProv <$> tcIfaceCo kco
 tcIfaceUnivCoProv (IfaceProofIrrelProv kco) = ProofIrrelProv <$> tcIfaceCo kco
 tcIfaceUnivCoProv (IfacePluginProv str)     = return $ PluginProv str
+tcIfaceUnivCoProv (IfaceStepsProv m n)      = return $ StepsProv m n
+
 
 {-
 ************************************************************************
diff --git a/compiler/GHC/Tc/TyCl/Utils.hs b/compiler/GHC/Tc/TyCl/Utils.hs
index 6c8daa0d56..a66e92ea33 100644
--- a/compiler/GHC/Tc/TyCl/Utils.hs
+++ b/compiler/GHC/Tc/TyCl/Utils.hs
@@ -153,6 +153,7 @@ synonymTyConsOfType ty
      go_prov (PhantomProv co)     = go_co co
      go_prov (ProofIrrelProv co)  = go_co co
      go_prov (PluginProv _)       = emptyNameEnv
+     go_prov (StepsProv _ _)      = emptyNameEnv
 
      go_tc tc | isTypeSynonymTyCon tc = unitNameEnv (tyConName tc) tc
               | otherwise             = emptyNameEnv
diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs
index 519a2b37a8..c61a721ef3 100644
--- a/compiler/GHC/Tc/Utils/TcMType.hs
+++ b/compiler/GHC/Tc/Utils/TcMType.hs
@@ -1534,6 +1534,7 @@ collect_cand_qtvs_co orig_ty bound = go_co
     go_prov dv (PhantomProv co)    = go_co dv co
     go_prov dv (ProofIrrelProv co) = go_co dv co
     go_prov dv (PluginProv _)      = return dv
+    go_prov dv (StepsProv _ _)     = return dv
 
     go_cv :: CandidatesQTvs -> CoVar -> TcM CandidatesQTvs
     go_cv dv@(DV { dv_cvs = cvs }) cv