[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.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