[Git][ghc/ghc][wip/T23923-mikolaj-take-2] Fix according to the first round of Simon's instruction
Mikolaj Konarski (@Mikolaj)
gitlab at gitlab.haskell.org
Thu Feb 8 16:36:23 UTC 2024
Mikolaj Konarski pushed to branch wip/T23923-mikolaj-take-2 at Glasgow Haskell Compiler / GHC
Commits:
b69a0731 by Mikolaj Konarski at 2024-02-08T17:36:00+01:00
Fix according to the first round of Simon's instruction
- - - - -
7 changed files:
- compiler/GHC/Core/Coercion.hs
- compiler/GHC/Core/Lint.hs
- compiler/GHC/Core/TyCo/Rep.hs
- compiler/GHC/Types/Unique/DSet.hs
- testsuite/tests/tcplugins/CtIdPlugin.hs
- testsuite/tests/tcplugins/RewritePlugin.hs
- testsuite/tests/tcplugins/TyFamPlugin.hs
Changes:
=====================================
compiler/GHC/Core/Coercion.hs
=====================================
@@ -1522,7 +1522,7 @@ promoteCoercion co = case co of
UnivCo (PhantomProv kco) _ _ _ -> kco
UnivCo (ProofIrrelProv kco) _ _ _ -> kco
- UnivCo (PluginProv _ _) _ _ _ -> mkKindCo co -- !!!
+ UnivCo (PluginProv _ _) _ _ _ -> mkKindCo co
SymCo g
-> mkSymCo (promoteCoercion g)
=====================================
compiler/GHC/Core/Lint.hs
=====================================
@@ -1931,6 +1931,13 @@ checkTyCon :: TyCon -> LintM ()
checkTyCon tc
= checkL (not (isTcTyCon tc)) (text "Found TcTyCon:" <+> ppr tc)
+-------------------
+checkTyCoVarInScope :: Subst -> TyCoVar -> LintM ()
+checkTyCoVarInScope subst tcv
+ = checkL (tcv `isInScope` subst) $
+ hang (text "The type or coercion variable" <+> pprBndr LetBind tcv)
+ 2 (text "is out of scope")
+
-------------------
lintType :: Type -> LintM LintedType
@@ -1948,12 +1955,8 @@ lintType (TyVarTy tv)
-- In GHCi we may lint an expression with a free
-- type variable. Then it won't be in the
-- substitution, but it should be in scope
- Nothing | tv `isInScope` subst
- -> return (TyVarTy tv)
- | otherwise
- -> failWithL $
- hang (text "The type variable" <+> pprBndr LetBind tv)
- 2 (text "is out of scope")
+ Nothing -> do { checkTyCoVarInScope subst tv
+ ; return (TyVarTy tv) }
}
lintType ty@(AppTy t1 t2)
@@ -2325,15 +2328,8 @@ lintCoercion (CoVarCo cv)
= do { subst <- getSubst
; case lookupCoVar subst cv of
Just linted_co -> return linted_co ;
- Nothing
- | cv `isInScope` subst
- -> return (CoVarCo cv)
- | otherwise
- ->
- -- lintCoBndr always extends the substitution
- failWithL $
- hang (text "The coercion variable" <+> pprBndr LetBind cv)
- 2 (text "is out of scope")
+ Nothing -> do { checkTyCoVarInScope subst cv
+ ; return (CoVarCo cv) }
}
@@ -2532,7 +2528,12 @@ lintCoercion co@(UnivCo prov r ty1 ty2)
; check_kinds kco k1 k2
; return (ProofIrrelProv kco') }
- lint_prov _ _ prov@(PluginProv _ _) = return prov -- !!! do we want to add checkTyCoVarInScope, as in !3792. and refactor all other variable checks to use it?
+ lint_prov _ _ (PluginProv s cvs)
+ = do { subst <- getSubst
+ ; mapM_ (checkTyCoVarInScope subst) (dVarSetElems cvs)
+ -- Don't bother to return substituted fvs;
+ -- they don't matter to Lint
+ ; return (PluginProv s cvs) }
check_kinds kco k1 k2
= do { let Pair k1' k2' = coercionKind kco
=====================================
compiler/GHC/Core/TyCo/Rep.hs
=====================================
@@ -1896,10 +1896,9 @@ 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 _ cvs) = go_cvs env (dVarSetElems cvs) -- !!!
+ go_prov _ (PluginProv _ cvs) = go_cvs env cvs
- go_cvs _ [] = mempty
- go_cvs env (cv:cvs) = covar env cv `mappend` go_cvs env cvs
+ go_cvs env cvs = foldl' (\acc cv -> acc `mappend` covar env cv) mempty (dVarSetElems cvs)
-- | A view function that looks through nothing.
noView :: Type -> Maybe Type
=====================================
compiler/GHC/Types/Unique/DSet.hs
=====================================
@@ -125,18 +125,11 @@ partitionUniqDSet p = coerce . partitionUDFM p . getUniqDSet
-- See Note [UniqSet invariant] in GHC.Types.Unique.Set
mapUniqDSet :: Uniquable b => (a -> b) -> UniqDSet a -> UniqDSet b
-mapUniqDSet f = mkUniqDSet . map f . uniqDSetToList
-{- !!! why was this changed in !3792 at all? should we change it too?
-mapUniqDSet f s = foldl' (\s e -> addOneToUniqDSet s (f e)) emptyUniqDSet $
-
- Richard Eisenberg
- @rae ยท 3 years ago
- Developer
-
-Goodness gracious this is inefficient. It uses uniqDSetToList, which uses eltsUDFM, which uses sortBy! !! !!!!! No no no. Just use the Functor instance for IntMap, lifting through TaggedVal. No need to sort and then rebalance the map structure. No no no.
-
- uniqDSetToList s
--}
+mapUniqDSet f (UniqDSet m) = UniqDSet $ unsafeCastUDFMKey $ mapUDFM f m
+-- Simply apply `f` to each element, retaining all the structure unchanged.
+-- The identification of keys and elements prevents a derived Functor
+-- instance, but `unsafeCastUDFMKey` makes it possible to apply the strict
+-- mapping from DFM.
strictFoldUniqDSet :: (a -> r -> r) -> r -> UniqDSet a -> r
strictFoldUniqDSet k r s = foldl' (\r e -> k e r) r $
=====================================
testsuite/tests/tcplugins/CtIdPlugin.hs
=====================================
@@ -42,7 +42,7 @@ solver :: [String]
-> PluginDefs -> EvBindsVar -> [Ct] -> [Ct]
-> TcPluginM TcPluginSolveResult
solver _args defs ev givens wanteds = do
- let pluginCo = mkUnivCo (PluginProv "CtIdPlugin" emptyUniqDSet) Representational
+ let pluginCo = mkUnivCo (PluginProv "CtIdPlugin" emptyUniqDSet) Representational -- Empty is fine. This plugin does not use "givens". -- !!! is it true for this plugin as well?
let substEvidence ct ct' =
evCast (ctEvExpr $ ctEvidence ct') $ pluginCo (ctPred ct') (ctPred ct)
=====================================
testsuite/tests/tcplugins/RewritePlugin.hs
=====================================
@@ -87,5 +87,5 @@ mkTyFamReduction :: TyCon -> [ Type ] -> Type -> Reduction
mkTyFamReduction tyCon args res = Reduction co res
where
co :: Coercion
- co = mkUnivCo ( PluginProv "RewritePlugin" emptyUniqDSet) Nominal
+ co = mkUnivCo ( PluginProv "RewritePlugin" emptyUniqDSet) Nominal -- Empty is fine. This plugin does not use "givens". -- !!! is it true for this plugin as well?
( mkTyConApp tyCon args ) res
=====================================
testsuite/tests/tcplugins/TyFamPlugin.hs
=====================================
@@ -80,6 +80,6 @@ solveCt ( PluginDefs {..} ) ct@( classifyPredType . ctPred -> EqPred NomEq lhs r
, let
evTerm :: EvTerm
evTerm = EvExpr . Coercion
- $ mkUnivCo ( PluginProv "TyFamPlugin" emptyUniqDSet) Nominal lhs rhs -- !!! how do I take the free variables at this point? should we provide a smart constructor that computes the free variables? how about another that sets the empty set? would some plugins work fine with that?
+ $ mkUnivCo ( PluginProv "TyFamPlugin" emptyUniqDSet) Nominal lhs rhs -- Empty is fine. This plugin does not use "givens".
= pure $ Just ( evTerm, ct )
solveCt _ ct = pure Nothing
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/b69a0731e174b59abc84579c7859b19dd4b15d12
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/b69a0731e174b59abc84579c7859b19dd4b15d12
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20240208/644d3f7f/attachment-0001.html>
More information about the ghc-commits
mailing list