Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC Commits: de44e69e by sheaf at 2025-09-19T05:16:51-04:00 Enable TcM plugins in initTc This commit ensures that we run typechecker plugins and defaulting plugins whenever we call initTc. In particular, this ensures that the pattern-match checker, which calls 'initTcDsForSolver' which calls 'initTc', runs with typechecker plugins enabled. This matters for situations like: merge :: Vec n a -> Vec n a -> Vec (2 * n) a merge Nil Nil = Nil merge (a <: as) (b <: bs) = a :< (b <: merge as bs) in which we need the typechecker plugin to run in order to tell us that the Givens would be inconsistent in the additional equation merge (_ <: _) Nil and thus that the equation is not needed. Fixes #26395 - - - - - 7 changed files: - compiler/GHC/HsToCore/Monad.hs - compiler/GHC/Tc/Module.hs - compiler/GHC/Tc/Utils/Monad.hs - + testsuite/tests/tcplugins/T26395.hs - + testsuite/tests/tcplugins/T26395.stderr - + testsuite/tests/tcplugins/T26395_Plugin.hs - testsuite/tests/tcplugins/all.T Changes: ===================================== compiler/GHC/HsToCore/Monad.hs ===================================== @@ -58,6 +58,7 @@ module GHC.HsToCore.Monad ( import GHC.Prelude import GHC.Driver.Env +import GHC.Driver.Env.KnotVars import GHC.Driver.DynFlags import GHC.Driver.Ppr import GHC.Driver.Config.Diagnostic @@ -117,7 +118,7 @@ import GHC.Utils.Panic import qualified GHC.Data.Strict as Strict import Data.IORef -import GHC.Driver.Env.KnotVars + import GHC.IO.Unsafe (unsafeInterleaveIO) {- ===================================== compiler/GHC/Tc/Module.hs ===================================== @@ -26,6 +26,7 @@ module GHC.Tc.Module ( runTcInteractive, -- Used by GHC API clients (#8878) withTcPlugins, -- Used by GHC API clients (#20499) withHoleFitPlugins, -- Used by GHC API clients (#20499) + withDefaultingPlugins, tcRnLookupName, tcRnGetInfo, tcRnModule, tcRnModuleTcRnM, @@ -53,7 +54,6 @@ import GHC.Driver.DynFlags import GHC.Driver.Config.Diagnostic import GHC.IO.Unsafe ( unsafeInterleaveIO ) -import GHC.Tc.Errors.Hole.Plugin ( HoleFitPluginR (..) ) import GHC.Tc.Errors.Types import {-# SOURCE #-} GHC.Tc.Gen.Splice ( finishTH, runRemoteModFinalizers ) import GHC.Tc.Gen.HsType @@ -141,7 +141,6 @@ import GHC.Types.Id as Id import GHC.Types.Id.Info( IdDetails(..) ) import GHC.Types.Var.Env import GHC.Types.TypeEnv -import GHC.Types.Unique.FM import GHC.Types.Name import GHC.Types.Name.Env import GHC.Types.Name.Set @@ -212,10 +211,6 @@ tcRnModule hsc_env mod_sum save_rn_syntax (text "Renamer/typechecker"<+>brackets (ppr this_mod)) (const ()) $ initTc hsc_env hsc_src save_rn_syntax this_mod real_loc $ - withTcPlugins hsc_env $ - withDefaultingPlugins hsc_env $ - withHoleFitPlugins hsc_env $ - tcRnModuleTcRnM hsc_env mod_sum parsedModule this_mod | otherwise @@ -3182,72 +3177,11 @@ hasTopUserName x {- ******************************************************************************** -Type Checker Plugins + Running plugins ******************************************************************************** -} -withTcPlugins :: HscEnv -> TcM a -> TcM a -withTcPlugins hsc_env m = - case catMaybes $ mapPlugins (hsc_plugins hsc_env) tcPlugin of - [] -> m -- Common fast case - plugins -> do - (solvers, rewriters, stops) <- - unzip3 `fmap` mapM start_plugin plugins - let - rewritersUniqFM :: UniqFM TyCon [TcPluginRewriter] - !rewritersUniqFM = sequenceUFMList rewriters - -- The following ensures that tcPluginStop is called even if a type - -- error occurs during compilation (Fix of #10078) - eitherRes <- tryM $ - updGblEnv (\e -> e { tcg_tc_plugin_solvers = solvers - , tcg_tc_plugin_rewriters = rewritersUniqFM }) m - mapM_ runTcPluginM stops - case eitherRes of - Left _ -> failM - Right res -> return res - where - start_plugin (TcPlugin start solve rewrite stop) = - do s <- runTcPluginM start - return (solve s, rewrite s, stop s) - -withDefaultingPlugins :: HscEnv -> TcM a -> TcM a -withDefaultingPlugins hsc_env m = - do case catMaybes $ mapPlugins (hsc_plugins hsc_env) defaultingPlugin of - [] -> m -- Common fast case - plugins -> do (plugins,stops) <- mapAndUnzipM start_plugin plugins - -- This ensures that dePluginStop is called even if a type - -- error occurs during compilation - eitherRes <- tryM $ do - updGblEnv (\e -> e { tcg_defaulting_plugins = plugins }) m - mapM_ runTcPluginM stops - case eitherRes of - Left _ -> failM - Right res -> return res - where - start_plugin (DefaultingPlugin start fill stop) = - do s <- runTcPluginM start - return (fill s, stop s) - -withHoleFitPlugins :: HscEnv -> TcM a -> TcM a -withHoleFitPlugins hsc_env m = - case catMaybes $ mapPlugins (hsc_plugins hsc_env) holeFitPlugin of - [] -> m -- Common fast case - plugins -> do (plugins,stops) <- mapAndUnzipM start_plugin plugins - -- This ensures that hfPluginStop is called even if a type - -- error occurs during compilation. - eitherRes <- tryM $ - updGblEnv (\e -> e { tcg_hf_plugins = plugins }) m - sequence_ stops - case eitherRes of - Left _ -> failM - Right res -> return res - where - start_plugin (HoleFitPluginR init plugin stop) = - do ref <- init - return (plugin ref, stop ref) - - runRenamerPlugin :: TcGblEnv -> HsGroup GhcRn -> TcM (TcGblEnv, HsGroup GhcRn) ===================================== compiler/GHC/Tc/Utils/Monad.hs ===================================== @@ -31,6 +31,9 @@ module GHC.Tc.Utils.Monad( updateEps, updateEps_, getHpt, getEpsAndHug, + -- * Initialising TcM plugins + withTcPlugins, withDefaultingPlugins, withHoleFitPlugins, + -- * Arrow scopes newArrowScope, escapeArrowScope, @@ -163,6 +166,7 @@ import GHC.Builtin.Names import GHC.Builtin.Types( zonkAnyTyCon ) import GHC.Tc.Errors.Types +import GHC.Tc.Errors.Hole.Plugin ( HoleFitPluginR (..) ) import GHC.Tc.Types -- Re-export all import GHC.Tc.Types.Constraint import GHC.Tc.Types.CtLoc @@ -183,13 +187,17 @@ import GHC.Unit.Module.Warnings import GHC.Unit.Home.PackageTable import GHC.Core.UsageEnv + +import GHC.Core.Coercion ( isReflCo ) import GHC.Core.Multiplicity import GHC.Core.InstEnv import GHC.Core.FamInstEnv import GHC.Core.Type( mkNumLitTy ) +import GHC.Core.TyCon ( TyCon ) import GHC.Driver.Env import GHC.Driver.Env.KnotVars +import GHC.Driver.Plugins ( Plugin(..), mapPlugins ) import GHC.Driver.Session import GHC.Driver.Config.Diagnostic @@ -226,7 +234,7 @@ import GHC.Types.SrcLoc import GHC.Types.Name.Env import GHC.Types.Name.Set import GHC.Types.Name.Ppr -import GHC.Types.Unique.FM ( emptyUFM ) +import GHC.Types.Unique.FM ( UniqFM, emptyUFM, sequenceUFMList ) import GHC.Types.Unique.DFM import GHC.Types.Unique.Supply import GHC.Types.Annotations @@ -240,8 +248,6 @@ import Data.IORef import Control.Monad import qualified Data.Map as Map -import GHC.Core.Coercion (isReflCo) - {- ************************************************************************ @@ -263,129 +269,139 @@ initTc :: HscEnv -- (error messages should have been printed already) initTc hsc_env hsc_src keep_rn_syntax mod loc do_this - = do { keep_var <- newIORef emptyNameSet ; - used_gre_var <- newIORef [] ; - th_var <- newIORef False ; - infer_var <- newIORef True ; - infer_reasons_var <- newIORef emptyMessages ; - dfun_n_var <- newIORef emptyOccSet ; - zany_n_var <- newIORef 0 ; - let { type_env_var = hsc_type_env_vars hsc_env }; - - dependent_files_var <- newIORef [] ; - dependent_dirs_var <- newIORef [] ; - static_wc_var <- newIORef emptyWC ; - cc_st_var <- newIORef newCostCentreState ; - th_topdecls_var <- newIORef [] ; - th_foreign_files_var <- newIORef [] ; - th_topnames_var <- newIORef emptyNameSet ; - th_modfinalizers_var <- newIORef [] ; - th_coreplugins_var <- newIORef [] ; - th_state_var <- newIORef Map.empty ; - th_remote_state_var <- newIORef Nothing ; - th_docs_var <- newIORef Map.empty ; - th_needed_deps_var <- newIORef ([], emptyUDFM) ; - next_wrapper_num <- newIORef emptyModuleEnv ; - let { - -- bangs to avoid leaking the env (#19356) - !dflags = hsc_dflags hsc_env ; - !mhome_unit = hsc_home_unit_maybe hsc_env; - !logger = hsc_logger hsc_env ; - - maybe_rn_syntax :: forall a. a -> Maybe a ; - maybe_rn_syntax empty_val - | logHasDumpFlag logger Opt_D_dump_rn_ast = Just empty_val - - | gopt Opt_WriteHie dflags = Just empty_val - - -- We want to serialize the documentation in the .hi-files, - -- and need to extract it from the renamed syntax first. - -- See 'GHC.HsToCore.Docs.extractDocs'. - | gopt Opt_Haddock dflags = Just empty_val - - | keep_rn_syntax = Just empty_val - | otherwise = Nothing ; - - gbl_env = TcGblEnv { - tcg_th_topdecls = th_topdecls_var, - tcg_th_foreign_files = th_foreign_files_var, - tcg_th_topnames = th_topnames_var, - tcg_th_modfinalizers = th_modfinalizers_var, - tcg_th_coreplugins = th_coreplugins_var, - tcg_th_state = th_state_var, - tcg_th_remote_state = th_remote_state_var, - tcg_th_docs = th_docs_var, - - tcg_mod = mod, - tcg_semantic_mod = homeModuleInstantiation mhome_unit mod, - tcg_src = hsc_src, - tcg_rdr_env = emptyGlobalRdrEnv, - tcg_fix_env = emptyNameEnv, - tcg_default = emptyDefaultEnv, - tcg_default_exports = emptyDefaultEnv, - tcg_type_env = emptyNameEnv, - tcg_type_env_var = type_env_var, - tcg_inst_env = emptyInstEnv, - tcg_fam_inst_env = emptyFamInstEnv, - tcg_ann_env = emptyAnnEnv, - tcg_complete_match_env = [], - tcg_th_used = th_var, - tcg_th_needed_deps = th_needed_deps_var, - tcg_exports = [], - tcg_imports = emptyImportAvails, - tcg_import_decls = [], - tcg_used_gres = used_gre_var, - tcg_dus = emptyDUs, - - tcg_rn_imports = [], - tcg_rn_exports = - if hsc_src == HsigFile - -- Always retain renamed syntax, so that we can give - -- better errors. (TODO: how?) - then Just [] - else maybe_rn_syntax [], - tcg_rn_decls = maybe_rn_syntax emptyRnGroup, - tcg_tr_module = Nothing, - tcg_binds = emptyLHsBinds, - tcg_imp_specs = [], - tcg_sigs = emptyNameSet, - tcg_ksigs = emptyNameSet, - tcg_ev_binds = emptyBag, - tcg_warns = emptyWarn, - tcg_anns = [], - tcg_tcs = [], - tcg_insts = [], - tcg_fam_insts = [], - tcg_rules = [], - tcg_fords = [], - tcg_patsyns = [], - tcg_merged = [], - tcg_dfun_n = dfun_n_var, - tcg_zany_n = zany_n_var, - tcg_keep = keep_var, - tcg_hdr_info = (Nothing,Nothing), - tcg_main = Nothing, - tcg_self_boot = NoSelfBoot, - tcg_safe_infer = infer_var, - tcg_safe_infer_reasons = infer_reasons_var, - tcg_dependent_files = dependent_files_var, - tcg_dependent_dirs = dependent_dirs_var, - tcg_tc_plugin_solvers = [], - tcg_tc_plugin_rewriters = emptyUFM, - tcg_defaulting_plugins = [], - tcg_hf_plugins = [], - tcg_top_loc = loc, - tcg_static_wc = static_wc_var, - tcg_complete_matches = [], - tcg_cc_st = cc_st_var, - tcg_next_wrapper_num = next_wrapper_num - } ; - } ; + = do { gbl_env <- initTcGblEnv hsc_env hsc_src keep_rn_syntax mod loc -- OK, here's the business end! - initTcWithGbl hsc_env gbl_env loc do_this + ; initTcWithGbl hsc_env gbl_env loc $ + + -- Make sure to initialise all TcM plugins from the ambient HscEnv. + -- + -- This ensures that all callers of 'initTc' enable plugins (#26395). + withTcPlugins hsc_env $ + withDefaultingPlugins hsc_env $ + withHoleFitPlugins hsc_env $ + + do_this } +-- | Create an empty 'TcGblEnv'. +initTcGblEnv :: HscEnv -> HscSource -> Bool -> Module -> RealSrcSpan -> IO TcGblEnv +initTcGblEnv hsc_env hsc_src keep_rn_syntax mod loc = + do { keep_var <- newIORef emptyNameSet + ; used_gre_var <- newIORef [] + ; th_var <- newIORef False + ; infer_var <- newIORef True + ; infer_reasons_var <- newIORef emptyMessages + ; dfun_n_var <- newIORef emptyOccSet + ; zany_n_var <- newIORef 0 + ; dependent_files_var <- newIORef [] + ; dependent_dirs_var <- newIORef [] + ; static_wc_var <- newIORef emptyWC + ; cc_st_var <- newIORef newCostCentreState + ; th_topdecls_var <- newIORef [] + ; th_foreign_files_var <- newIORef [] + ; th_topnames_var <- newIORef emptyNameSet + ; th_modfinalizers_var <- newIORef [] + ; th_coreplugins_var <- newIORef [] + ; th_state_var <- newIORef Map.empty + ; th_remote_state_var <- newIORef Nothing + ; th_docs_var <- newIORef Map.empty + ; th_needed_deps_var <- newIORef ([], emptyUDFM) + ; next_wrapper_num <- newIORef emptyModuleEnv + ; let + -- bangs to avoid leaking the env (#19356) + !dflags = hsc_dflags hsc_env + !mhome_unit = hsc_home_unit_maybe hsc_env + !logger = hsc_logger hsc_env + + maybe_rn_syntax :: forall a. a -> Maybe a ; + maybe_rn_syntax empty_val + | logHasDumpFlag logger Opt_D_dump_rn_ast = Just empty_val + + | gopt Opt_WriteHie dflags = Just empty_val + + -- We want to serialize the documentation in the .hi-files, + -- and need to extract it from the renamed syntax first. + -- See 'GHC.HsToCore.Docs.extractDocs'. + | gopt Opt_Haddock dflags = Just empty_val + + | keep_rn_syntax = Just empty_val + | otherwise = Nothing ; + + ; return $ TcGblEnv + { tcg_th_topdecls = th_topdecls_var + , tcg_th_foreign_files = th_foreign_files_var + , tcg_th_topnames = th_topnames_var + , tcg_th_modfinalizers = th_modfinalizers_var + , tcg_th_coreplugins = th_coreplugins_var + , tcg_th_state = th_state_var + , tcg_th_remote_state = th_remote_state_var + , tcg_th_docs = th_docs_var + + , tcg_mod = mod + , tcg_semantic_mod = homeModuleInstantiation mhome_unit mod + , tcg_src = hsc_src + , tcg_rdr_env = emptyGlobalRdrEnv + , tcg_fix_env = emptyNameEnv + , tcg_default = emptyDefaultEnv + , tcg_default_exports = emptyDefaultEnv + , tcg_type_env = emptyNameEnv + , tcg_type_env_var = hsc_type_env_vars hsc_env + , tcg_inst_env = emptyInstEnv + , tcg_fam_inst_env = emptyFamInstEnv + , tcg_ann_env = emptyAnnEnv + , tcg_complete_match_env = [] + , tcg_th_used = th_var + , tcg_th_needed_deps = th_needed_deps_var + , tcg_exports = [] + , tcg_imports = emptyImportAvails + , tcg_import_decls = [] + , tcg_used_gres = used_gre_var + , tcg_dus = emptyDUs + + , tcg_rn_imports = [] + , tcg_rn_exports = if hsc_src == HsigFile + -- Always retain renamed syntax, so that we can give + -- better errors. (TODO: how?) + then Just [] + else maybe_rn_syntax [] + , tcg_rn_decls = maybe_rn_syntax emptyRnGroup + , tcg_tr_module = Nothing + , tcg_binds = emptyLHsBinds + , tcg_imp_specs = [] + , tcg_sigs = emptyNameSet + , tcg_ksigs = emptyNameSet + , tcg_ev_binds = emptyBag + , tcg_warns = emptyWarn + , tcg_anns = [] + , tcg_tcs = [] + , tcg_insts = [] + , tcg_fam_insts = [] + , tcg_rules = [] + , tcg_fords = [] + , tcg_patsyns = [] + , tcg_merged = [] + , tcg_dfun_n = dfun_n_var + , tcg_zany_n = zany_n_var + , tcg_keep = keep_var + , tcg_hdr_info = (Nothing,Nothing) + , tcg_main = Nothing + , tcg_self_boot = NoSelfBoot + , tcg_safe_infer = infer_var + , tcg_safe_infer_reasons = infer_reasons_var + , tcg_dependent_files = dependent_files_var + , tcg_dependent_dirs = dependent_dirs_var + , tcg_tc_plugin_solvers = [] + , tcg_tc_plugin_rewriters = emptyUFM + , tcg_defaulting_plugins = [] + , tcg_hf_plugins = [] + , tcg_top_loc = loc + , tcg_static_wc = static_wc_var + , tcg_complete_matches = [] + , tcg_cc_st = cc_st_var + , tcg_next_wrapper_num = next_wrapper_num + } } + -- | Run a 'TcM' action in the context of an existing 'GblEnv'. initTcWithGbl :: HscEnv -> TcGblEnv @@ -686,6 +702,83 @@ withIfaceErr ctx do_this = do liftIO $ throwGhcExceptionIO (ProgramError (renderWithContext ctx msg)) Succeeded result -> return result +{- +************************************************************************ +* * + Initialising plugins for TcM +* * +************************************************************************ +-} + +-- | Initialise typechecker plugins, run the inner action, then stop +-- the typechecker plugins. +withTcPlugins :: HscEnv -> TcM a -> TcM a +withTcPlugins hsc_env m = + case catMaybes $ mapPlugins (hsc_plugins hsc_env) tcPlugin of + [] -> m -- Common fast case + plugins -> do + (solvers, rewriters, stops) <- + unzip3 `fmap` mapM start_plugin plugins + let + rewritersUniqFM :: UniqFM TyCon [TcPluginRewriter] + !rewritersUniqFM = sequenceUFMList rewriters + -- The following ensures that tcPluginStop is called even if a type + -- error occurs during compilation (Fix of #10078) + eitherRes <- tryM $ + updGblEnv (\e -> e { tcg_tc_plugin_solvers = solvers + , tcg_tc_plugin_rewriters = rewritersUniqFM }) + m + mapM_ runTcPluginM stops + case eitherRes of + Left _ -> failM + Right res -> return res + where + start_plugin (TcPlugin start solve rewrite stop) = + do s <- runTcPluginM start + return (solve s, rewrite s, stop s) + +-- | Initialise defaulting plugins, run the inner action, then stop +-- the defaulting plugins. +withDefaultingPlugins :: HscEnv -> TcM a -> TcM a +withDefaultingPlugins hsc_env m = + do case catMaybes $ mapPlugins (hsc_plugins hsc_env) defaultingPlugin of + [] -> m -- Common fast case + plugins -> do (plugins,stops) <- mapAndUnzipM start_plugin plugins + -- This ensures that dePluginStop is called even if a type + -- error occurs during compilation + eitherRes <- tryM $ do + updGblEnv (\e -> e { tcg_defaulting_plugins = plugins }) + m + mapM_ runTcPluginM stops + case eitherRes of + Left _ -> failM + Right res -> return res + where + start_plugin (DefaultingPlugin start fill stop) = + do s <- runTcPluginM start + return (fill s, stop s) + +-- | Initialise hole fit plugins, run the inner action, then stop +-- the hole fit plugins. +withHoleFitPlugins :: HscEnv -> TcM a -> TcM a +withHoleFitPlugins hsc_env m = + case catMaybes $ mapPlugins (hsc_plugins hsc_env) holeFitPlugin of + [] -> m -- Common fast case + plugins -> do (plugins,stops) <- mapAndUnzipM start_plugin plugins + -- This ensures that hfPluginStop is called even if a type + -- error occurs during compilation. + eitherRes <- tryM $ + updGblEnv (\e -> e { tcg_hf_plugins = plugins }) + m + sequence_ stops + case eitherRes of + Left _ -> failM + Right res -> return res + where + start_plugin (HoleFitPluginR init plugin stop) = + do ref <- init + return (plugin ref, stop ref) + {- ************************************************************************ * * ===================================== testsuite/tests/tcplugins/T26395.hs ===================================== @@ -0,0 +1,51 @@ + +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE StandaloneKindSignatures #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UnliftedDatatypes #-} + +{-# OPTIONS_GHC -fplugin=T26395_Plugin #-} + +{-# OPTIONS_GHC -Wincomplete-patterns #-} +{-# OPTIONS_GHC -Winaccessible-code #-} +{-# OPTIONS_GHC -Woverlapping-patterns #-} + +module T26395 where + +import Data.Kind +import GHC.TypeNats +import GHC.Exts ( UnliftedType ) + +-- This test verifies that typechecker plugins are enabled +-- when we run the solver for pattern-match checking. + +type Peano :: Nat -> UnliftedType +data Peano n where + Z :: Peano 0 + S :: Peano n -> Peano (1 + n) + +test1 :: Peano n -> Peano n -> Int +test1 Z Z = 0 +test1 (S n) (S m) = 1 + test1 n m + +{- +The following test doesn't work properly due to #26401: +the pattern-match checker reports a missing equation + + Z (S _) _ + +but there is no invocation of the solver of the form + + [G] n ~ 0 + [G] m ~ 1 + m1 + [G] (n-m) ~ m2 + +for which we could report the Givens as contradictory. + +test2 :: Peano n -> Peano m -> Peano (n - m) -> Int +test2 Z Z Z = 0 +test2 (S _) (S _) _ = 1 +test2 (S _) Z (S _) = 2 +-} ===================================== testsuite/tests/tcplugins/T26395.stderr ===================================== @@ -0,0 +1,2 @@ +[1 of 2] Compiling T26395_Plugin ( T26395_Plugin.hs, T26395_Plugin.o ) +[2 of 2] Compiling T26395 ( T26395.hs, T26395.o ) ===================================== testsuite/tests/tcplugins/T26395_Plugin.hs ===================================== @@ -0,0 +1,208 @@ +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MultiWayIf #-} +{-# LANGUAGE BlockArguments #-} +{-# LANGUAGE ViewPatterns #-} + +{-# OPTIONS_GHC -Wall -Wno-orphans #-} + +module T26395_Plugin where + +-- base +import Prelude hiding ( (<>) ) +import qualified Data.Semigroup as S +import Data.List ( partition ) +import Data.Maybe +import GHC.TypeNats + +-- ghc +import GHC.Builtin.Types.Literals +import GHC.Core.Predicate +import GHC.Core.TyCo.Rep +import GHC.Plugins +import GHC.Tc.Plugin +import GHC.Tc.Types +import GHC.Tc.Types.Constraint +import GHC.Tc.Types.Evidence +import GHC.Tc.Utils.TcType +import GHC.Types.Unique.Map + +-------------------------------------------------------------------------------- + +plugin :: Plugin +plugin = + defaultPlugin + { pluginRecompile = purePlugin + , tcPlugin = \ _-> Just $ + TcPlugin + { tcPluginInit = pure () + , tcPluginSolve = \ _ -> solve + , tcPluginRewrite = \ _ -> emptyUFM + , tcPluginStop = \ _ -> pure () + } + } + +solve :: EvBindsVar -> [Ct] -> [Ct] -> TcPluginM TcPluginSolveResult +solve _ givens wanteds + -- This plugin only reports inconsistencies among Given constraints. + | not $ null wanteds + = pure $ TcPluginOk [] [] + | otherwise + = do { let givenLinearExprs = mapMaybe linearExprCt_maybe givens + sols = solutions givenLinearExprs + + ; tcPluginTrace "solveLinearExprs" $ + vcat [ text "givens:" <+> ppr givens + , text "linExprs:" <+> ppr givenLinearExprs + , text "sols:" <+> ppr (take 1 sols) + ] + ; return $ + if null sols + then TcPluginContradiction givens + else TcPluginOk [] [] + } + +data LinearExpr = + LinearExpr + { constant :: Integer + , coeffs :: UniqMap TyVar Integer + } +instance Semigroup LinearExpr where + LinearExpr c xs <> LinearExpr d ys = + LinearExpr ( c + d ) ( plusMaybeUniqMap_C comb xs ys ) + where + comb a1 a2 = + let a = a1 + a2 + in if a == 0 + then Nothing + else Just a + +instance Monoid LinearExpr where + mempty = LinearExpr 0 emptyUniqMap + +mapLinearExpr :: (Integer -> Integer) -> LinearExpr -> LinearExpr +mapLinearExpr f (LinearExpr c xs) = LinearExpr (f c) (mapUniqMap f xs) + +minusLinearExpr :: LinearExpr -> LinearExpr -> LinearExpr +minusLinearExpr a b = a S.<> mapLinearExpr negate b + +instance Outputable LinearExpr where + ppr ( LinearExpr c xs ) = + hcat $ punctuate ( text " + " ) $ + ( ppr c : map ppr_var ( nonDetUniqMapToList xs ) ) + where + ppr_var ( tv, i ) + | i == 1 + = ppr tv + | i < 0 + = parens ( text "-" <> ppr (abs i) ) <> text "*" <> ppr tv + | otherwise + = ppr i <> text "*" <> ppr tv + +maxCoeff :: LinearExpr -> Double +maxCoeff ( LinearExpr c xs ) = + maximum ( map fromInteger ( c : nonDetEltsUniqMap xs ) ) + + +linearExprCt_maybe :: Ct -> Maybe LinearExpr +linearExprCt_maybe ct = + case classifyPredType (ctPred ct) of + EqPred NomEq lhs rhs + | all isNaturalTy [ typeKind lhs, typeKind rhs ] + , Just e1 <- linearExprTy_maybe lhs + , Just e2 <- linearExprTy_maybe rhs + -> Just $ e1 `minusLinearExpr` e2 + _ -> Nothing + +isNat :: Type -> Maybe Integer +isNat ty + | Just (NumTyLit n) <- isLitTy ty + = Just n + | otherwise + = Nothing + +linearExprTy_maybe :: Type -> Maybe LinearExpr +linearExprTy_maybe ty + | Just n <- isNat ty + = Just $ LinearExpr n emptyUniqMap + | Just (tc, args) <- splitTyConApp_maybe ty + = if | tc == typeNatAddTyCon + , [x, y] <- args + , Just e1 <- linearExprTy_maybe x + , Just e2 <- linearExprTy_maybe y + -> Just $ e1 S.<> e2 + | tc == typeNatSubTyCon + , [x,y] <- args + , Just e1 <- linearExprTy_maybe x + , Just e2 <- linearExprTy_maybe y + -> Just $ e1 `minusLinearExpr` e2 + | tc == typeNatMulTyCon + , [x, y] <- args + -> + if | Just ( LinearExpr n xs ) <- linearExprTy_maybe x + , isNullUniqMap xs + , Just e <- linearExprTy_maybe y + -> Just $ + if n == 0 + then mempty + else mapLinearExpr (n *) e + | Just ( LinearExpr n ys ) <- linearExprTy_maybe y + , isNullUniqMap ys + , Just e <- linearExprTy_maybe x + -> Just $ + if n == 0 + then mempty + else mapLinearExpr (fromIntegral n *) e + | otherwise + -> Nothing + | otherwise + -> Nothing + | Just tv <- getTyVar_maybe ty + = Just $ LinearExpr 0 ( unitUniqMap tv 1 ) + | otherwise + = Nothing + +-- Brute force algorithm to check whether a system of Diophantine +-- linear equations is solvable in natural numbers. +solutions :: [ LinearExpr ] -> [ UniqMap TyVar Natural ] +solutions eqs = + let + (constEqs, realEqs) = partition (isNullUniqMap . coeffs) eqs + d = length realEqs + fvs = nonDetKeysUniqMap $ plusUniqMapList ( map coeffs realEqs ) + in + if | any ( ( /= 0 ) . evalLinearExpr emptyUniqMap ) constEqs + -> [] + | d == 0 + -> [ emptyUniqMap ] + | otherwise + -> + let + m = maximum $ map maxCoeff realEqs + hadamardBound = sqrt ( fromIntegral $ d ^ d ) * m ^ d + tests = mkAssignments ( floor hadamardBound ) fvs + in + filter ( \ test -> isSolution test realEqs ) tests + + +mkAssignments :: Natural -> [ TyVar ] -> [ UniqMap TyVar Natural ] +mkAssignments _ [] = [ emptyUniqMap ] +mkAssignments b (v : vs) = + [ addToUniqMap rest v n + | n <- [ 0 .. b ] + , rest <- mkAssignments b vs + ] + +isSolution :: UniqMap TyVar Natural -> [ LinearExpr ] -> Bool +isSolution assig = + all ( \ expr -> evalLinearExpr assig expr == 0 ) + +evalLinearExpr :: UniqMap TyVar Natural -> LinearExpr -> Integer +evalLinearExpr vals ( LinearExpr c xs ) = nonDetFoldUniqMap aux c xs + where + aux ( tv, coeff ) !acc = acc + coeff * val + where + val :: Integer + val = case lookupUniqMap vals tv of + Nothing -> pprPanic "evalLinearExpr: missing tv" (ppr tv) + Just v -> fromIntegral v ===================================== testsuite/tests/tcplugins/all.T ===================================== @@ -110,6 +110,19 @@ test('TcPlugin_CtId' , '-dynamic -package ghc' if have_dynamic() else '-package ghc' ] ) +# Checks that we run type-checker plugins for pattern-match warnings. +test('T26395' + , [ extra_files( + [ 'T26395_Plugin.hs' + , 'T26395.hs' + ]) + , req_th + ] + , multimod_compile + , [ 'T26395.hs' + , '-dynamic -package ghc' if have_dynamic() else '-package ghc' ] + ) + test('T11462', [js_broken(22261), req_th, req_plugins], multi_compile, [None, [('T11462_Plugin.hs', '-package ghc'), ('T11462.hs', '')], '-dynamic' if have_dynamic() else '']) View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/de44e69ef2f8394c6448d4968d9a392b... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/de44e69ef2f8394c6448d4968d9a392b... You're receiving this email because of your account on gitlab.haskell.org.