<div dir="ltr"><div>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?</div><div><br></div><div>I've distilled the behavior that's confusing me down to the following example</div><div><br></div><div><div>> module Test where</div><div>>   <br></div><div>> class C a where f :: a -> ()</div><div><br></div></div><div>paired with a very silly plugin that always claims every constraint it sees is a contradiction.</div><div><br></div><div><div>> module Contrarian (plugin) where</div><div>>   <br></div><div>> import Plugins (Plugin(..),defaultPlugin)</div><div>> import TcPluginM (tcPluginIO)</div><div>> import TcRnTypes (TcPlugin(..),TcPluginResult(TcPluginContradiction))</div><div>>   <br></div><div>> plugin :: Plugin</div><div>> plugin = defaultPlugin { tcPlugin = const (Just contrarianPlugin) }</div><div>>   <br></div><div>> contrarianPlugin :: TcPlugin</div><div>> contrarianPlugin = TcPlugin {</div><div>>     tcPluginInit = return ()</div><div>>   ,</div><div>>     tcPluginSolve = \() given derived wanted -> do</div><div>>       tcPluginIO $ putStrLn "Alternative facts!"</div><div>>       return $ TcPluginContradiction $ given ++ derived ++ wanted</div><div>>   ,</div><div>>     tcPluginStop  = \() -> return ()</div><div>>   }</div></div><div><br></div><div>Please review the following GHCi session. We start *without* the plugin.</div><div><br></div><div><div>    $ ghc --interactive Test.hs</div><div>    GHCi, version 8.2.1: <a href="http://www.haskell.org/ghc/">http://www.haskell.org/ghc/</a>  :? for help</div><div>    [1 of 1] Compiling Test             ( Test.hs, interpreted )</div><div>    Ok, 1 module loaded.</div><div>    *Test> f ()</div><div>      <br></div><div>    <interactive>:1:1: error:</div><div>        * No instance for (C ()) arising from a use of `f'</div><div>        * In the expression: f ()</div><div>          In an equation for `it': it = f ()</div><div><br></div><div>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.</div><div><br></div><div>    *Test> :set -fplugin=Contrarian</div><div>    *Test> f ()</div><div>    Alternative facts!</div><div>    Alternative facts!</div><div>    Alternative facts!</div><div>    Alternative facts!</div><div>    *** Exception: <interactive>:3:1: error:</div><div>        * No instance for (C ()) arising from a use of `f'</div><div>        * In the expression: f ()</div><div>          In an equation for `it': it = f ()</div><div>    (deferred type error)</div><div>    *Test> :t f</div><div>    Alternative facts!</div><div>    f :: a -> ()</div><div><br></div><div>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).</div><div><br></div><div>    *Test> :set -fno-defer-type-errors</div><div>    *Test> :t f</div><div>    Alternative facts!</div><div>    f :: a -> ()</div><div>    *Test> f ()</div><div>    Alternative facts!</div><div>    Alternative facts!</div><div>    Alternative facts!</div><div>    Alternative facts!</div><div>    *** Exception: <interactive>:3:1: error:</div><div>        * No instance for (C ()) arising from a use of `f'</div><div>        * In the expression: f ()</div><div>          In an equation for `it': it = f ()</div><div>    (deferred type error)</div><div>      <br></div><div>    <interactive>:7:1: error:</div><div>        * No instance for (Show (a0 -> ())) arising from a use of `print'</div><div>            (maybe you haven't applied a function to enough arguments?)</div><div>        * In a stmt of an interactive GHCi command: print it</div><div>    *Test></div></div><div><br></div><div>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.</div><div><br></div><div>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.</div><div><br></div><div>What I should be expecting regarding contradictions?</div><div><br></div><div>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?</div><div><br></div><div>Thanks. -Nick</div><div><br></div><div><div>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.<br></div></div></div>