inspection-testing 0.6.1 → 0.6.2
raw patch · 5 files changed
+159/−125 lines, 5 filesdep ~basedep ~ghc
Dependency ranges changed: base, ghc
Files
- ChangeLog.md +8/−0
- examples/MutualRecursion.hs +20/−0
- inspection-testing.cabal +1/−1
- src/Test/Inspection.hs +2/−2
- src/Test/Inspection/Core.hs +128/−122
ChangeLog.md view
@@ -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)
examples/MutualRecursion.hs view
@@ -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
inspection-testing.cabal view
@@ -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.
src/Test/Inspection.hs view
@@ -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
src/Test/Inspection/Core.hs view
@@ -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