enable typechecker plugins within tcCheckSatisfiability
Motivation
As of GHC 8.6.5, with my plugin enabled, the compiler awkwardly tells me a pattern is missing (non-exhaustive), but when I add the pattern it tells it is inaccessible.
My brief investigation suggests this is because the pattern checker does not enable typechecker plugins, so it can't see the missing pattern is inaccessible, hence it warns non-exhaustive. But when that pattern is added, the typechecker plugin recognizes the contradiction when "simplifying Givens" (i.e. the formerly-missing pattern's context), and so it reports inaccessible. User catch 22.
Example
In the following example. Suppose the plugin can see that A B
and B A
are impossible, but GHC alone cannot.
data AB where
A :: MutuallyExclusivePredicate_1of2 => AB
B :: MutuallyExclusivePredicate_2of2 => AB
The behavior on f
is good and should not change.
{-# OPTIONS -fplugin=MyPlugin #-}
f :: AB -> ()
f B B = ()
f A B = () -- plugin reports contradiction when simplifying Givens, GHC reports inaccessible
f B A = () -- plugin reports contradiction when simplifying Givens, GHC reports inaccessible
But, the behavior for g
is bad and should change; g
should be warning free, but isn't.
{-# OPTIONS -fplugin=MyPlugin #-}
g :: AB -> ()
g A A = ()
g B B = ()
-- g A B = () -- bypassing plugin, pattern checker doesn't realize this is inaccessible; GHC reports non-exhaustive
-- g B A = () -- bypassing plugin, pattern checker doesn't realize this is inaccessible; GHC reports non-exhaustive
Proposal
It seems the pattern checker should use typechecker plugins when checking (absent) patterns for satisfiability. Specifically, as of aac18e9a08 - (tag: ghc-8.6.4-release) Bump to 8.6.4 (9 weeks ago) <Ben Gamari>
, my particular example seems fixed with just this trivial change to DsMonad.initTcDsForSolver
plus necessary export & import list changes (the pattern checker calls TcSimplify.tcCheckSatisfiability
, which calls DsMonad.initTcDsForSolver
).
diff --git a/compiler/deSugar/DsMonad.hs b/compiler/deSugar/DsMonad.hs
index 921276e4d8..72a1bdf124 100644
--- a/compiler/deSugar/DsMonad.hs
+++ b/compiler/deSugar/DsMonad.hs
@@ -247,6 +248,7 @@ initTcDsForSolver thing_inside
; liftIO $ initTc hsc_env HsSrcFile False mod loc $
updGblEnv (\tc_gbl -> tc_gbl { tcg_fam_inst_env = fam_inst_env }) $
+ TcRnDriver.withTcPlugins hsc_env $
thing_inside }
mkDsEnvs :: DynFlags -> Module -> GlobalRdrEnv -> TypeEnv -> FamInstEnv
I suspect it's significantly slower to use plugins for every pattern, so this would probably justify a new flag so a user can opt-out. (The flag should be implied by the presence of any typechecker plugins.)