+import GHC.Driver.Env.KnotVars

+

+        withDefaultingPlugins,

+                         Running plugins

+  -- * Initialising TcM plugins

+  withTcPlugins, withDefaultingPlugins, withHoleFitPlugins,

+

+import GHC.Tc.Errors.Hole.Plugin ( HoleFitPluginR (..) )

+

+import GHC.Core.Coercion ( isReflCo )

+import GHC.Core.TyCon ( TyCon )

+import GHC.Driver.Plugins ( Plugin(..), mapPlugins )

+import GHC.Types.Unique.FM ( UniqFM, emptyUFM, sequenceUFMList )

+ = do { gbl_env <- initTcGblEnv hsc_env hsc_src keep_rn_syntax mod loc

+      ;  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

+      } }

+

+{-

+************************************************************************

+*                                                                      *

+                 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)

+

+

+{-# 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

+-}

+[1 of 2] Compiling T26395_Plugin    ( T26395_Plugin.hs, T26395_Plugin.o )

+[2 of 2] Compiling T26395           ( T26395.hs, T26395.o )

+{-# 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

+# 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' ]

+    )

+