How does GHC handle TcPluginContradiction?

[Edward Z. Yang]

Hi Nicolas,

While I am not 100% sure, I belive this is related to
the fact that currently inaccessible branches (a local
contradiction indicates inaccessibility) are not
being reported in GHC.  I reported this in
https://ghc.haskell.org/trac/ghc/ticket/12694
whose root cause was suggested might be
https://ghc.haskell.org/trac/ghc/ticket/12466

Edward

Excerpts from Nicolas Frisby's message of 2017-08-06 01:27:53 +0000:
> 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.