diff --git a/ChangeLog.md b/ChangeLog.md --- a/ChangeLog.md +++ b/ChangeLog.md @@ -1,5 +1,13 @@ # Revision history for inspection-testing +## 0.6.2 -- 2025-06-13 + +* Fix an bug that would cause a GHC panic +* Fix `=/~` and `=/-` +* Syntax directed comparison of lets + +(all thanks Oleg Grenrus) + ## 0.6.1 -- 2025-06-11 * Improve presentation of term inequalities (thanks Oleg Grenrus) diff --git a/examples/MutualRecursion.hs b/examples/MutualRecursion.hs --- a/examples/MutualRecursion.hs +++ b/examples/MutualRecursion.hs @@ -30,6 +30,26 @@ inspect $ 'inf === 'inf2' inspect $ 'inf === 'inf3' +-- with local variable for let* +-- NOINLINE to prevent CSE +infl x = go0 + where + go0 = x : go1 + go1 = 'b' : go2 + go2 = 'c' : go0 +{-# NOINLINE infl #-} +infl' x = go0 + where + go1 = 'c' : go2 + go0 = x : go1 + go2 = 'b' : go0 +{-# NOINLINE infl' #-} + +-- See https://github.com/nomeata/inspection-testing/pull/88 +-- and https://github.com/nomeata/inspection-testing/issues/82 +-- Change to ===, this shouldn't panic. +inspect $ 'infl =/= 'infl' + letrec = let go0 = 'a' : go1 go1 = 'b' : go2 diff --git a/inspection-testing.cabal b/inspection-testing.cabal --- a/inspection-testing.cabal +++ b/inspection-testing.cabal @@ -1,5 +1,5 @@ name: inspection-testing -version: 0.6.1 +version: 0.6.2 synopsis: GHC plugin to do inspection testing description: Some carefully crafted libraries make promises to their users beyond functionality and performance. diff --git a/src/Test/Inspection.hs b/src/Test/Inspection.hs --- a/src/Test/Inspection.hs +++ b/src/Test/Inspection.hs @@ -212,7 +212,7 @@ -- -- @since 0.4.3.0 (=/-) :: Name -> Name -> Obligation -(=/-) = mkEquality False IgnoreTypesAndTicksEquiv +(=/-) = mkEquality True IgnoreTypesAndTicksEquiv infix 9 =/- -- | Declare two functions to be equal up to let binding ordering (see '(==~)'), @@ -220,7 +220,7 @@ -- -- @since 0.5 (=/~) :: Name -> Name -> Obligation -(=/~) = mkEquality False UnorderedLetsEquiv +(=/~) = mkEquality True UnorderedLetsEquiv infix 9 =/~ mkEquality :: Bool -> Equivalence -> Name -> Name -> Obligation diff --git a/src/Test/Inspection/Core.hs b/src/Test/Inspection/Core.hs --- a/src/Test/Inspection/Core.hs +++ b/src/Test/Inspection/Core.hs @@ -20,6 +20,7 @@ import GHC.Core.TyCo.Rep import GHC.Core.Type import GHC.Types.Var as Var +import GHC.Types.Var.Set (mkVarSet) import GHC.Types.Id import GHC.Types.Name import GHC.Types.Literal @@ -40,6 +41,7 @@ import TyCoRep import Type import Var +import VarSet (mkVarSet) import Id import Literal import Name @@ -135,7 +137,7 @@ pprSliceDifference slice1 slice2 | [(v1,e1)] <- slice1' , [(v2,e2)] <- slice2' - = pprSingletonSliceDifference v1 v2 e1 e2 + = pprSingletonSliceDifference (mkInScopeSet (mkVarSet (S.toList both))) v1 v2 e1 e2 | otherwise = hang (text "LHS" Outputable.<> colon) 4 (pprSlice slice1') $$ @@ -145,8 +147,8 @@ slice1' = filter (\(v,_) -> v `S.notMember` both) slice1 slice2' = filter (\(v,_) -> v `S.notMember` both) slice2 -pprSingletonSliceDifference :: Var -> Var -> CoreExpr -> CoreExpr -> SDoc -pprSingletonSliceDifference v1 v2 e1 e2 = +pprSingletonSliceDifference :: InScopeSet -> Var -> Var -> CoreExpr -> CoreExpr -> SDoc +pprSingletonSliceDifference iss v1 v2 e1 e2 = ctxDoc $ hang (text "LHS" Outputable.<> colon) 4 (hang (pprPrefixOcc v1) 2 (eqSign <+> pprCoreExpr e1')) $$ hang (text "RHS" Outputable.<> colon) 4 (hang (pprPrefixOcc v2) 2 (eqSign <+> pprCoreExpr e2')) @@ -166,7 +168,7 @@ | eqTypeX env (varType b1) (varType b2) = go t1 t2 ((b1,b2):ctxt) (rnBndr2 env b1 b2) where - go x y ctxt _env = (rename ctxt x, y, ctxt) + go x y ctxt _env = (rename iss ctxt x, y, ctxt) mkContextExpr :: [Var] -> CoreExpr mkContextExpr [] = ellipsis @@ -187,6 +189,31 @@ withLessDetail sdoc = withPprStyle defaultUserStyle sdoc #endif +-- | Equality name environment. +-- This environment contains top-level and let-bound definitions +-- (no lambda arguments). +data EqEnv = EqEnv !Int [(Var, (Int, CoreExpr))] [(Var, (Int, CoreExpr))] + +-- | Lookup left and right variables in EqEnv. +lookupEqEnv :: Var -> Var -> EqEnv -> Maybe (Int, Int, CoreExpr, CoreExpr) +lookupEqEnv x y (EqEnv _ env1 env2) + | Just (i, e1) <- lookup x env1 + , Just (j, e2) <- lookup y env2 + = Just (i, j, e1, e2) + + | otherwise + = Nothing + +initialEqEnv :: [(Var, CoreExpr)] -> [(Var, CoreExpr)] -> EqEnv +initialEqEnv ls rs = EqEnv 1 + [ (x, (0, e1)) | (x, e1) <- ls ] + [ (y, (0, e2)) | (y, e2) <- rs ] + +bindEqEnv :: [(Var, CoreExpr)] -> [(Var, CoreExpr)] -> EqEnv -> EqEnv +bindEqEnv ls rs (EqEnv i env1 env2)= EqEnv (i + 1) + ([ (x, (i, e1)) | (x, e1) <- ls ] ++ env1) + ([ (y, (i, e2)) | (y, e2) <- rs ] ++ env2) + -- | This is a heuristic, which only works if both slices -- have auxiliary variables in the right order. -- (This is mostly to work-around the buggy CSE in GHC-8.0) @@ -201,8 +228,7 @@ eqSlice' _ [] ((v,_) : _) = Left $ ppr v -- Mostly defensive programming (slices should not be empty) eqSlice' eqv slice1@((head1, def1) : _) slice2@((head2, def2) : _) = do - let env = mkRnEnv2 emptyInScopeSet - goSliceVars [] 0 env head1 def1 head2 def2 + goStart head1 def1 head2 def2 where -- ignore types and hpc ticks it :: Bool @@ -218,27 +244,25 @@ IgnoreTypesAndTicksEquiv -> False UnorderedLetsEquiv -> True - goSliceVars :: [SDoc] -> Int -> RnEnv2 -> Var -> CoreExpr -> Var -> CoreExpr -> Either SDoc () - goSliceVars ctx lv env x e1 y e2 = do - tracePut lv "SLICEVAR" (varToString x ++ " =?= " ++ varToString y) - - -- if x or y expressions are essentially a variable x' or y' respectively - -- add an obligation to check x' = y (or x = y'). + goStart :: Var -> CoreExpr -> Var -> CoreExpr -> Either SDoc () + goStart x e1 y e2 = do + tracePut 0 "TOP" (varToString x ++ " =?= " ++ varToString y) if | Just x' <- essentiallyVar e1 , Just e1' <- lookup x' slice1 - -> goSliceVars ctx lv env x' e1' y e2 + -> goStart x' e1' y e2 | Just y' <- essentiallyVar e2 , Just e2' <- lookup y' slice2 - -> goSliceVars ctx lv env x e1 y' e2' + -> goStart x e1 y' e2' -- otherwise if neither x and y expressions are variables -- 1. compare the expressions (already assuming that x and y are equal) -- 2. comparison may create new obligations, loop. | otherwise -> do - let env' = rnBndr2 env x y - go ctx lv env' e1 e2 + let env = rnBndr2 (mkRnEnv2 emptyInScopeSet) x y + ee = initialEqEnv slice1 slice2 + go [] 0 env ee e1 e2 essentiallyVar :: CoreExpr -> Maybe Var essentiallyVar (App e a) | it, isTyCoArg a = essentiallyVar e @@ -257,80 +281,108 @@ inequality [] err = Left err inequality ctx err = Left $ err $$ hang (text "in") 2 (vcat ctx) - go :: [SDoc] -> Int -> RnEnv2 -> CoreExpr -> CoreExpr -> Either SDoc () - go ctx lv env (essentiallyVar -> Just v1) (essentiallyVar -> Just v2) = do - if | v1 == v2 -> do - tracePut lv "VAR" (varToString v1 ++ " =?= " ++ varToString v2 ++ " SAME") - return () - | rnOccL env v1 == rnOccR env v2 -> do + go :: [SDoc] -> Int -> RnEnv2 -> EqEnv -> CoreExpr -> CoreExpr -> Either SDoc () + go ctx lv env ee (essentiallyVar -> Just v1) (essentiallyVar -> Just v2) = do + -- NOTE: The ordering of this checks is important. + -- + -- See example https://github.com/nomeata/inspection-testing/pull/89#issuecomment-2967774956 + -- GHC may use same name for local names in different bindings. + -- + -- Therefore we first check for already visited and lambda-bound variables. + -- (inRnEnvL/inRnEnvR checks are important so we don't confuse for unbound variables). + -- We need to this first to break loops of recursive definitions,. + -- + -- Then we test whether variables are top or local-let bound. + -- If so, we proceed to compare their definitions. + -- + -- Lastly we check whether variables are equal. + -- This case checks for any global names. + if + | inRnEnvL env v1 + , inRnEnvR env v2 + , rnOccL env v1 == rnOccR env v2 -> do tracePut lv "VAR" (varToString v1 ++ " =?= " ++ varToString v2 ++ " IN ENV") return () - | Just e1 <- lookup v1 slice1 - , Just e2 <- lookup v2 slice2 -> do - tracePut lv "VAR" (varToString v1 ++ " =?= " ++ varToString v2 ++ " OBLIGATION") - goSliceVars ctx lv env v1 e1 v2 e2 + + | Just (i, j, e1, e2) <- lookupEqEnv v1 v2 ee -> + -- we check that levels are the same + -- if they are not we fail immediately and not fall-back further. + if i == j + then do + tracePut lv "VAR" (varToString v1 ++ " =?= " ++ varToString v2 ++ " BOUND " ++ show i) + let ctx' = text "comparing definitions of" <+> ppr v1 <+> text "=?=" <+> ppr v2 : ctx + let env' = rnBndr2 env v1 v2 + go ctx' lv env' ee e1 e2 + else do + tracePut lv "VAR" (varToString v1 ++ " =?= " ++ varToString v2 ++ " BOUND IN DIFFERENT LETS " ++ show i ++ " /= " ++ show j) + inequality ctx $ hsep [ text "variables", ppr v1, text "and", ppr v2, text "are bound in different lets" ] + + | v1 == v2 -> do + tracePut lv "VAR" (varToString v1 ++ " =?= " ++ varToString v2 ++ " SAME") + return () + | otherwise -> do + tracePut lv "VAR" (varToString v1 ++ " =?= " ++ varToString v2 ++ " NOT EQUAL") inequality ctx $ hsep [ text "inequal variables", ppr v1, text "and", ppr v2 ] - go ctx lv _ (Lit lit1) (Lit lit2) = do + go ctx lv _ _ (Lit lit1) (Lit lit2) = do tracePut lv "LIT" "???" -- no Show for Literal :( unless (lit1 == lit2) $ inequality ctx $ sep [ text "inequal literals", ppr lit1, text "and", ppr lit2 ] - go ctx _ env (Type t1) (Type t2) = + go ctx _ env _ (Type t1) (Type t2) = goTypes ctx env t1 t2 - go ctx _ env (Coercion co1) (Coercion co2) = + go ctx _ env _ (Coercion co1) (Coercion co2) = goCoercions ctx env co1 co2 - go ctx lv env (Cast e1 _) e2 | it = go ctx lv env e1 e2 - go ctx lv env e1 (Cast e2 _) | it = go ctx lv env e1 e2 + go ctx lv env ee (Cast e1 _) e2 | it = go ctx lv env ee e1 e2 + go ctx lv env ee e1 (Cast e2 _) | it = go ctx lv env ee e1 e2 #if MIN_VERSION_ghc(9,0,0) - go ctx lv env (Case s b _ alts) e2 | it, Just e1 <- isUnsafeEqualityCase s b alts = go ctx lv env e1 e2 - go ctx lv env e1 (Case s b _ alts) | it, Just e2 <- isUnsafeEqualityCase s b alts = go ctx lv env e1 e2 + go ctx lv env ee (Case s b _ alts) e2 | it, Just e1 <- isUnsafeEqualityCase s b alts = go ctx lv env ee e1 e2 + go ctx lv env ee e1 (Case s b _ alts) | it, Just e2 <- isUnsafeEqualityCase s b alts = go ctx lv env ee e1 e2 #endif - go ctx lv env (Cast e1 co1) (Cast e2 co2) = traceBlock lv "CAST" "" $ \lv -> do + go ctx lv env ee (Cast e1 co1) (Cast e2 co2) = traceBlock lv "CAST" "" $ \lv -> do goCoercions ctx env co1 co2 - go ctx lv env e1 e2 + go ctx lv env ee e1 e2 - go ctx lv env (App e1 a) e2 | it, isTyCoArg a = go ctx lv env e1 e2 - go ctx lv env e1 (App e2 a) | it, isTyCoArg a = go ctx lv env e1 e2 - go ctx lv env (App f1 a1) (App f2 a2) = traceBlock lv "APP" "" $ \lv -> do - go ctx lv env f1 f2 - go ctx lv env a1 a2 - go ctx lv env (Tick HpcTick{} e1) e2 | it = go ctx lv env e1 e2 - go ctx lv env e1 (Tick HpcTick{} e2) | it = go ctx lv env e1 e2 - go ctx lv env (Tick SourceNote{} e1) e2 = go ctx lv env e1 e2 - go ctx lv env e1 (Tick SourceNote{} e2) = go ctx lv env e1 e2 - go ctx lv env (Tick n1 e1) (Tick n2 e2) = traceBlock lv "TICK" "" $ \lv -> do + go ctx lv env ee (App e1 a) e2 | it, isTyCoArg a = go ctx lv env ee e1 e2 + go ctx lv env ee e1 (App e2 a) | it, isTyCoArg a = go ctx lv env ee e1 e2 + go ctx lv env ee (App f1 a1) (App f2 a2) = traceBlock lv "APP" "" $ \lv -> do + go ctx lv env ee f1 f2 + go ctx lv env ee a1 a2 + go ctx lv env ee (Tick HpcTick{} e1) e2 | it = go ctx lv env ee e1 e2 + go ctx lv env ee e1 (Tick HpcTick{} e2) | it = go ctx lv env ee e1 e2 + go ctx lv env ee (Tick SourceNote{} e1) e2 = go ctx lv env ee e1 e2 + go ctx lv env ee e1 (Tick SourceNote{} e2) = go ctx lv env ee e1 e2 + go ctx lv env ee (Tick n1 e1) (Tick n2 e2) = traceBlock lv "TICK" "" $ \lv -> do unless (go_tick env n1 n2) $ inequality ctx $ text "inequal ticks" - go ctx lv env e1 e2 + go ctx lv env ee e1 e2 - go ctx lv env (Lam b e1) e2 | it, isTyCoVar b = go ctx lv env e1 e2 - go ctx lv env e1 (Lam b e2) | it, isTyCoVar b = go ctx lv env e1 e2 - go ctx lv env (Lam b1 e1) (Lam b2 e2) = traceBlock lv "LAM" (varToString b1 ++ " ~ " ++ varToString b2) $ \lv -> do - -- guard (it || eqTypeX env (varType b1) (varType b2)) -- TODO - go ctx lv (rnBndr2 env b1 b2) e1 e2 + go ctx lv env ee (Lam b e1) e2 | it, isTyCoVar b = go ctx lv env ee e1 e2 + go ctx lv env ee e1 (Lam b e2) | it, isTyCoVar b = go ctx lv env ee e1 e2 + go ctx lv env ee (Lam b1 e1) (Lam b2 e2) = traceBlock lv "LAM" (varToString b1 ++ " ~ " ++ varToString b2) $ \lv -> do + unless it $ goTypes ctx env (varType b1) (varType b2) + go ctx lv (rnBndr2 env b1 b2) ee e1 e2 - go ctx lv env e1@(Let _ _) e2@(Let _ _) + go ctx lv env ee e1@(Let _ _) e2@(Let _ _) | ul , (ps1, e1') <- peelLets e1 , (ps2, e2') <- peelLets e2 = traceBlock lv "LET" (showVars ps1 ++ " ~ " ++ showVars ps2) $ \lv -> do let ctx' = text "let bindings:" <+> pprVars ps1 <+> pprVars ps2 : ctx unless (equalLength ps1 ps2) $ inequality ctx $ text "different amount of bindings in let" - env' <- goBinds ctx' lv env ps1 ps2 - - go ctx lv env' e1' e2' + let ee' = bindEqEnv ps1 ps2 ee + go ctx' lv env ee' e1' e2' - go ctx lv env (Let (NonRec v1 r1) e1) (Let (NonRec v2 r2) e2) - = do go ctx lv env r1 r2 -- No need to check binder types, since RHSs match - go ctx lv (rnBndr2 env v1 v2) e1 e2 + go ctx lv env ee (Let (NonRec v1 r1) e1) (Let (NonRec v2 r2) e2) + = do go ctx lv env ee r1 r2 -- No need to check binder types, since RHSs match + go ctx lv (rnBndr2 env v1 v2) ee e1 e2 - go ctx lv env (Let (Rec ps1) e1) (Let (Rec ps2) e2) + go ctx lv env ee (Let (Rec ps1) e1) (Let (Rec ps2) e2) = do unless (equalLength ps1 ps2) $ inequality ctx $ text "different amount of bindings in recursive let" - sequence_ $ zipWith (go ctx lv env') rs1 rs2 - go ctx lv env' e1 e2 + sequence_ $ zipWith (go ctx lv env' ee) rs1 rs2 + go ctx lv env' ee e1 e2 where bs1, bs2 :: [CoreBndr] rs1, rs2 :: [CoreExpr] @@ -339,19 +391,20 @@ (bs2,rs2) = unzip ps2 env' = rnBndrs2 env bs1 bs2 - go ctx lv env (Case e1 b1 t1 a1) (Case e2 b2 t2 a2) + go ctx lv env ee (Case e1 b1 t1 a1) (Case e2 b2 t2 a2) | null a1 -- See Note [Empty case alternatives] in TrieMap , null a2 = do - go ctx lv env e1 e2 + go ctx lv env ee e1 e2 unless it $ goTypes ctx env t1 t2 | otherwise - = do unless (equalLength a1 a2) $ inequality ctx $ text "different amount of alternatives in case" - go ctx lv env e1 e2 - sequence_ $ zipWith (go_alt ctx lv (rnBndr2 env b1 b2)) a1 a2 + = traceBlock lv "CASE" "..." $ \lv -> do + unless (equalLength a1 a2) $ inequality ctx $ text "different amount of alternatives in case" + go ctx lv env ee e1 e2 + sequence_ $ zipWith (go_alt ctx lv (rnBndr2 env b1 b2) ee) a1 a2 - go ctx lv _ e1 e2 = do + go ctx lv _ _ e1 e2 = do tracePut lv "FAIL" (conToString e1 ++ " =/= " ++ conToString e2) inequality ctx $ sep [ text "inequal terms:", ppr e1, text "and", ppr e2] @@ -364,10 +417,11 @@ | otherwise = inequality ctx $ sep [ text "inequal types:", ppr t1, text "and", ppr t2 ] ----------- - go_alt :: [SDoc] -> Int -> RnEnv2 -> CoreAlt -> CoreAlt -> Either SDoc () - go_alt ctx lv env (Alt c1 bs1 e1) (Alt c2 bs2 e2) - = do unless (c1 == c2) $ inequality ctx $ sep [ text "inequal constructors:", ppr c1, text "and", ppr c2 ] - go ctx lv (rnBndrs2 env bs1 bs2) e1 e2 + go_alt :: [SDoc] -> Int -> RnEnv2 -> EqEnv -> CoreAlt -> CoreAlt -> Either SDoc () + go_alt ctx lv env ee (Alt c1 bs1 e1) (Alt c2 bs2 e2) + = traceBlock lv "ALT" "..." $ \lv -> do + unless (c1 == c2) $ inequality ctx $ sep [ text "inequal constructors:", ppr c1, text "and", ppr c2 ] + go ctx lv (rnBndrs2 env bs1 bs2) ee e1 e2 go_tick :: RnEnv2 -> CoreTickish -> CoreTickish -> Bool go_tick env Breakpoint{ breakpointId = lid, breakpointFVs = lids } Breakpoint{ breakpointId = rid, breakpointFVs = rids } @@ -378,40 +432,6 @@ peelLets (Let (Rec bs) e) = let (xs, e') = peelLets e in (bs ++ xs, e') peelLets e = ([], e) - goBinds :: [SDoc] -> Int -> RnEnv2 -> [(Var, CoreExpr)] -> [(Var, CoreExpr)] -> Either SDoc RnEnv2 - goBinds _ _ env [] [] = return env - goBinds ctx _ _ [] (_:_) = inequality ctx $ text "goBinds: missing binding" - goBinds ctx _ _ (_:_) [] = inequality ctx $ text "goBinds: missing binding" - goBinds ctx lv env [(v1,b1)] [(v2, b2)] = do - -- special case of singleton let bindings: - -- there is no choice, so we can save ourselves transforming sub-errors. - go ctx lv env b1 b2 - return (rnBndr2 env v1 v2) - - goBinds ctx lv env ((v1,b1):xs) ys' = findRight (v1 : map fst xs) (map fst ys') $ do - -- select a binding - ((v2,b2), ys) <- choices ys' - return $ do - let ctx' = hsep [text "trying", ppr v1, text "=", ppr v2] : ctx - traceBlock lv "LET*" (varToString v1 ++ " =?= " ++ varToString v2) $ \lv -> - go ctx' lv env b1 b2 - - -- continue with the rest of bindings, adding a pair as matching one. - goBinds ctx' lv (rnBndr2 env v1 v2) xs ys - ---TODO: rename -findRight :: [Var] -> [Var] -> [Either SDoc a] -> Either SDoc a -findRight ls rs = go [] - where - go errs [] = Left $ hang (text "Cannot align let bindings:" <+> pprVars ls <+> pprVars rs) 2 (vcatBullet errs) - go _ (x@(Right _) : _) = x - go errs (Left err : xs) = go (err : errs) xs - - pprVars = braces . hsep . map ppr - -vcatBullet :: [SDoc] -> SDoc -vcatBullet = vcat . map (text "*" <+>) - #if !MIN_VERSION_ghc(9,9,0) && MIN_VERSION_ghc(9,0,0) isUnsafeEqualityCase :: CoreExpr -> Id -> [CoreAlt] -> Maybe CoreExpr isUnsafeEqualityCase scrut _bndr [Alt _ _ rhs] @@ -451,20 +471,6 @@ conToString Type {} = "Type" conToString Coercion {} = "Coercion" --- | --- --- >>> choices "" --- [] --- --- >>> choices "abcde" --- [('a',"bcde"),('b',"acde"),('c',"abde"),('d',"abce"),('e',"abcd")] --- -choices :: [a] -> [(a, [a])] -choices = go id where - go :: ([a] -> [a]) -> [a] -> [(a, [a])] - go _ [] = [] - go f (x:xs) = (x, f xs) : go (f . (x :)) xs - -- | Returns @True@ if the given core expression mentions no type constructor -- anywhere that has the given name. freeOfType :: Slice -> [Name] -> Maybe (Var, CoreExpr) @@ -593,11 +599,11 @@ doesNotContainTypeClasses slice tcNs = allTyCons (\tc -> not (isClassTyCon tc) || isCTupleTyConName (getName tc) || any (getName tc ==) tcNs) slice -rename :: [(Var, Var)] -> CoreExpr -> CoreExpr -rename rn = substExpr' sub where +rename :: InScopeSet -> [(Var, Var)] -> CoreExpr -> CoreExpr +rename iss rn = substExpr' sub where -- convert RnEnv2 to Subst -- here we forget about tyvars and covars, but mostly this is good enough. - sub = mkOpenSubst emptyInScopeSet [ (v1, if isTyVar v2 then Type (mkTyVarTy v2) else if isCoVar v2 then Coercion (mkCoVarCo v2) else Var v2 ) | (v1, v2) <- rn] + sub = mkOpenSubst iss [ (v1, if isTyVar v2 then Type (mkTyVarTy v2) else if isCoVar v2 then Coercion (mkCoVarCo v2) else Var v2 ) | (v1, v2) <- rn] #if MIN_VERSION_GLASGOW_HASKELL(9,0,0,0) substExpr' = substExpr