#12780: Calling "do nothing" type checker plugin affects type checking when it shouldn't -------------------------------------+------------------------------------- Reporter: clinton | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Description changed by clinton: @@ -101,2 +101,36 @@ - But I'm unsure why this should be necessary, and I certainly don't think - this should only be necessary if one calls a type checker plugin. + In addition, either of the following two solutions will get the code to + compile: + + 1. Replacing the reference to `IsF p t` in the class signature with `t ~ F + p` like so: + + {{{#!hs + -- f :: (IsF p t) => t + f :: (t ~ F p) => t + }}} + + 2. Alternatively, expanding out `IsF p t` in the signature of `g` as + follows: + + {{{#!hs + --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: + + {{{#!hs + type family C t :: Constraint + }}} + + the bug still appears. + + So it seems this bug needs four things to all occur for it to appear: + + 1. A type constraint synonym in the calling code. + 2. A type constraint synonym in the called code. + 3. The type constraint synonym to contain a class constraint, or at least + a non-equality one. + 4. A type checking plugin to be called. @@ -120,1 +154,2 @@ - affects ordinary type checking. I don't think this should happen. + affects ordinary type checking in particular circumstances. I don't think + this should happen. New description: 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: {{{#!hs {-# 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: {{{#!hs {-# 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: {{{#!hs {-# 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: {{{#!hs {-# 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: {{{#!hs --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: 1. Replacing the reference to `IsF p t` in the class signature with `t ~ F p` like so: {{{#!hs -- f :: (IsF p t) => t f :: (t ~ F p) => t }}} 2. Alternatively, expanding out `IsF p t` in the signature of `g` as follows: {{{#!hs --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: {{{#!hs type family C t :: Constraint }}} the bug still appears. So it seems this bug needs four things to all occur for it to appear: 1. A type constraint synonym in the calling code. 2. A type constraint synonym in the called code. 3. The type constraint synonym to contain a class constraint, or at least a non-equality one. 4. 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: {{{#!hs plugin = defaultPlugin { tcPlugin = const (Just myPlugin) } }}} and instead just does: {{{#!hs 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. -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12780#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler