[GHC] #12780: Calling "do nothing" type checker plugin affects type checking when it shouldn't

[GHC]

#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.0.1
           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:
-------------------------------------+-------------------------------------
 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
 }}}

 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.

 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. I don't think this should happen.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12780>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler