How does GHC handle TcPluginContradiction?

[Nicolas Frisby]

My TC plugin is identifying a contradiction, but that is not preventing the
module from type checking, nor does GHC even raising a warning (with
-Wall). This is not the behavior I was expecting. How confused am I?

I've distilled the behavior that's confusing me down to the following
example

> module Test where
>
> class C a where f :: a -> ()

paired with a very silly plugin that always claims every constraint it sees
is a contradiction.

> module Contrarian (plugin) where
>
> import Plugins (Plugin(..),defaultPlugin)
> import TcPluginM (tcPluginIO)
> import TcRnTypes (TcPlugin(..),TcPluginResult(TcPluginContradiction))
>
> plugin :: Plugin
> plugin = defaultPlugin { tcPlugin = const (Just contrarianPlugin) }
>
> contrarianPlugin :: TcPlugin
> contrarianPlugin = TcPlugin {
>     tcPluginInit = return ()
>   ,
>     tcPluginSolve = \() given derived wanted -> do
>       tcPluginIO $ putStrLn "Alternative facts!"
>       return $ TcPluginContradiction $ given ++ derived ++ wanted
>   ,
>     tcPluginStop  = \() -> return ()
>   }

Please review the following GHCi session. We start *without* the plugin.

    $ ghc --interactive Test.hs
    GHCi, version 8.2.1: http://www.haskell.org/ghc/  :? for help
    [1 of 1] Compiling Test             ( Test.hs, interpreted )
    Ok, 1 module loaded.
    *Test> f ()

    <interactive>:1:1: error:
        * No instance for (C ()) arising from a use of `f'
        * In the expression: f ()
          In an equation for `it': it = f ()

That behavior meets my expectations. Now let's add the plugin to see what
contradictions cause to happen --- my naive guess is that we should see the
same thing. (I don't really know what contradictions *should* cause GHC to
do *differently* than the above.) The following is a continuation of the
same session.

    *Test> :set -fplugin=Contrarian
    *Test> f ()
    Alternative facts!
    Alternative facts!
    Alternative facts!
    Alternative facts!
    *** Exception: <interactive>:3:1: error:
        * No instance for (C ()) arising from a use of `f'
        * In the expression: f ()
          In an equation for `it': it = f ()
    (deferred type error)
    *Test> :t f
    Alternative facts!
    f :: a -> ()

Interesting: claiming the constraint is a contradiction seems to convert
the type error to a deferred type error. Let's see if we can disable that
(since it's not the behavior I want).

    *Test> :set -fno-defer-type-errors
    *Test> :t f
    Alternative facts!
    f :: a -> ()
    *Test> f ()
    Alternative facts!
    Alternative facts!
    Alternative facts!
    Alternative facts!
    *** Exception: <interactive>:3:1: error:
        * No instance for (C ()) arising from a use of `f'
        * In the expression: f ()
          In an equation for `it': it = f ()
    (deferred type error)

    <interactive>:7:1: error:
        * No instance for (Show (a0 -> ())) arising from a use of `print'
            (maybe you haven't applied a function to enough arguments?)
        * In a stmt of an interactive GHCi command: print it
    *Test>

I seems we can't disable this behavior. That makes it seem pretty
fundamental. So I'm guessing I'm confused about something, probably what
TcContradiction achieves in terms of the user experience.

The behavior I want is for my plugin to identify (relevant) contradictions
and incur a static type error as soon as possible. I thought contradictions
would achieve that, but I seem to be wrong.

What I should be expecting regarding contradictions?

How should I achieve my desired behavior? Perhaps I should try "solving"
the contradiction constraints via an appeal to a TypeError constraint
instead. Or maybe I should just leave the identified contradictions
unsolved?

Thanks. -Nick

PS - A big thank you to Adam Gundry and Christiaan Baaij (and probably
others) for the useful wiki pages, blog posts, and publications -- they've
been a huge help for my learning about the typechecker via plugins! I'm
very excited about this plugin, and I hope to share it soon, but I'd like
to understand it better before I do.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20170806/e029fe8f/attachment.html>