Calling "do nothing" type checker plugin affects type checking when it shouldn't
The following has been compiled against ghc version 8.1.20161022, my apologies if this bug has already been fixed.
The following program compiles fine:
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
main :: IO ()
main = return ()
type family F p = t | t -> p
type IsF p t = (C p, t ~ F p)
class C p where
f :: (IsF p t) => t
f = undefined
g :: (IsF p t) => t
g = f
But if we define a "do nothing" type checker plugin like so:
{-# OPTIONS_GHC -dynamic-too #-}
module MyPlugin (plugin) where
import Plugins (
Plugin(tcPlugin),
defaultPlugin, tcPlugin
)
import TcRnTypes (
TcPlugin(TcPlugin), tcPluginInit, tcPluginSolve, tcPluginStop,
TcPluginSolver,
TcPluginResult(TcPluginContradiction, TcPluginOk)
)
plugin :: Plugin
plugin = defaultPlugin { tcPlugin = const (Just myPlugin) }
myPlugin :: TcPlugin
myPlugin =
TcPlugin
{
tcPluginInit = return (),
tcPluginSolve = const solver,
tcPluginStop = const (return ())
}
solver :: TcPluginSolver
solver _ _ _ = return $ TcPluginOk [] []
And call it from our original source file by adding:
{-# OPTIONS_GHC -fplugin MyPlugin #-}
We get the following error:
pluginbug.hs:18:5: error:
• Could not deduce (C p0, t ~ F p0) arising from a use of ‘f’
from the context: IsF p t
bound by the type signature for:
g :: IsF p t => t
at pluginbug.hs:17:1-19
The type variable ‘p0’ is ambiguous
Relevant bindings include g :: t (bound at pluginbug.hs:18:1)
• In the expression: f
In an equation for ‘g’: g = f
Note that not just calling my "do nothing" type checking plugin does this, to be sure, instead I called ghc-typelits-natnormalise
like so:
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}
And the same error results.
One solution is to remove (C p)
from the IsF
type declaration, and instead adding it to g
s definition, like so:
--type IsF p t = (C p, t ~ F p)
type IsF p t = (t ~ F p)
--g :: (IsF p t) => t
g :: (C p, IsF p t) => t
In addition, either of the following two solutions will get the code to compile:
- Replacing the reference to
IsF p t
in the class signature witht ~ F p
like so:
-- f :: (IsF p t) => t
f :: (t ~ F p) => t
- Alternatively, expanding out
IsF p t
in the signature ofg
as follows:
--g :: (IsF p t) => t
g :: (C p, t ~ F p) => t
Note that is we remove the class C
entirely (making f
an ordinary function) the bug disappears, but if instead replace the class with a constraint C
like so:
type family C t :: Constraint
the bug still appears.
So it seems this bug needs four things to all occur for it to appear:
- A type constraint synonym in the calling code.
- A type constraint synonym in the called code.
- The type constraint synonym to contain a class constraint, or at least a non-equality one.
- A type checking plugin to be called.
Note that the error requires a type checking plugin to be called, if one does not override defaultPlugin
like so:
plugin = defaultPlugin { tcPlugin = const (Just myPlugin) }
and instead just does:
plugin = defaultPlugin
then the issue will not occur.
So in summary, it seems that calling a type checking plugin somehow affects ordinary type checking in particular circumstances. I don't think this should happen.