<div dir="ltr">I also just found issue #22 in Adam's uom github repository; it seems related.<div><br></div><div>"""</div><div><span style="color:rgb(36,41,46);font-family:-apple-system,BlinkMacSystemFont,"Segoe UI",Helvetica,Arial,sans-serif,"Apple Color Emoji","Segoe UI Emoji","Segoe UI Symbol";font-size:14px">The plugin is correctly reporting the constraint </span><code style="box-sizing:border-box;font-family:SFMono-Regular,Consolas,"Liberation Mono",Menlo,Courier,monospace;font-size:11.9px;padding:0.2em 0px;margin:0px;background-color:rgba(27,31,35,0.05);border-radius:3px;color:rgb(36,41,46)">Base "s" ~~ Base "m" ^: 2</code><span style="color:rgb(36,41,46);font-family:-apple-system,BlinkMacSystemFont,"Segoe UI",Helvetica,Arial,sans-serif,"Apple Color Emoji","Segoe UI Emoji","Segoe UI Symbol";font-size:14px"> as insoluble (note the use of </span><code style="box-sizing:border-box;font-family:SFMono-Regular,Consolas,"Liberation Mono",Menlo,Courier,monospace;font-size:11.9px;padding:0.2em 0px;margin:0px;background-color:rgba(27,31,35,0.05);border-radius:3px;color:rgb(36,41,46)">~~</code><span style="color:rgb(36,41,46);font-family:-apple-system,BlinkMacSystemFont,"Segoe UI",Helvetica,Arial,sans-serif,"Apple Color Emoji","Segoe UI Emoji","Segoe UI Symbol";font-size:14px">, which is a type family provided by </span><code style="box-sizing:border-box;font-family:SFMono-Regular,Consolas,"Liberation Mono",Menlo,Courier,monospace;font-size:11.9px;padding:0.2em 0px;margin:0px;background-color:rgba(27,31,35,0.05);border-radius:3px;color:rgb(36,41,46)">uom-plugin</code><span style="color:rgb(36,41,46);font-family:-apple-system,BlinkMacSystemFont,"Segoe UI",Helvetica,Arial,sans-serif,"Apple Color Emoji","Segoe UI Emoji","Segoe UI Symbol";font-size:14px"> that is a pseudo-synonym of </span><code style="box-sizing:border-box;font-family:SFMono-Regular,Consolas,"Liberation Mono",Menlo,Courier,monospace;font-size:11.9px;padding:0.2em 0px;margin:0px;background-color:rgba(27,31,35,0.05);border-radius:3px;color:rgb(36,41,46)">~</code><span style="color:rgb(36,41,46);font-family:-apple-system,BlinkMacSystemFont,"Segoe UI",Helvetica,Arial,sans-serif,"Apple Color Emoji","Segoe UI Emoji","Segoe UI Symbol";font-size:14px">). However, it turns out that the </span><a href="https://github.com/ghc/ghc/blob/ghc-8.0.1-release/compiler/typecheck/TcErrors.hs#L410-L415" style="box-sizing:border-box;color:rgb(3,102,214);text-decoration-line:none;font-family:-apple-system,BlinkMacSystemFont,"Segoe UI",Helvetica,Arial,sans-serif,"Apple Color Emoji","Segoe UI Emoji","Segoe UI Symbol";font-size:14px">GHC error-reporting machinery</a><span style="color:rgb(36,41,46);font-family:-apple-system,BlinkMacSystemFont,"Segoe UI",Helvetica,Arial,sans-serif,"Apple Color Emoji","Segoe UI Emoji","Segoe UI Symbol";font-size:14px"> requires a subtle invariant, namely that only certain kinds of constraint can be regarded as insoluble. Equalities are included, but not irreducible predicates such as </span><code style="box-sizing:border-box;font-family:SFMono-Regular,Consolas,"Liberation Mono",Menlo,Courier,monospace;font-size:11.9px;padding:0.2em 0px;margin:0px;background-color:rgba(27,31,35,0.05);border-radius:3px;color:rgb(36,41,46)">~~</code><span style="color:rgb(36,41,46);font-family:-apple-system,BlinkMacSystemFont,"Segoe UI",Helvetica,Arial,sans-serif,"Apple Color Emoji","Segoe UI Emoji","Segoe UI Symbol";font-size:14px">. Failure to respect this invariant means that errors are silently ignored.</span>  <br></div><div>"""</div><div><br></div><div>The insoluble constraints in my actual plugin is a genuine class, so this isn't an obvious perfect fit for my case.</div></div><br><div class="gmail_quote"><div dir="ltr">On Sat, Aug 5, 2017 at 7:46 PM Nicolas Frisby <<a href="mailto:nicolas.frisby@gmail.com">nicolas.frisby@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">Yes, thanks! I agree with you.<br><br>I just realized on my dog walk that, according to <a href="https://ghc.haskell.org/trac/ghc/wiki/Plugins/TypeChecker" target="_blank">https://ghc.haskell.org/trac/ghc/wiki/Plugins/TypeChecker</a>, "If the plugin finds a contradiction amongst the givens, it should return TcPluginContradiction containing the contradictory constraints. These will turn into inaccessible code errors."<div><br></div><div>And the brief demo in my previous email seems to indicate that "inaccessible code errors" are only realized as deferred type errors, with no static manifestation.</div><div><br></div><div>Thanks. -Nick</div></div><div dir="ltr"><div><br><div><br><div class="gmail_quote"><div dir="ltr">On Sat, Aug 5, 2017 at 7:27 PM Edward Z. Yang <<a href="mailto:ezyang@mit.edu" target="_blank">ezyang@mit.edu</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi Nicolas,<br>
<br>
While I am not 100% sure, I belive this is related to<br>
the fact that currently inaccessible branches (a local<br>
contradiction indicates inaccessibility) are not<br>
being reported in GHC.  I reported this in<br>
<a href="https://ghc.haskell.org/trac/ghc/ticket/12694" rel="noreferrer" target="_blank">https://ghc.haskell.org/trac/ghc/ticket/12694</a><br>
whose root cause was suggested might be<br>
<a href="https://ghc.haskell.org/trac/ghc/ticket/12466" rel="noreferrer" target="_blank">https://ghc.haskell.org/trac/ghc/ticket/12466</a><br>
<br>
Edward<br>
<br>
Excerpts from Nicolas Frisby's message of 2017-08-06 01:27:53 +0000:<br>
> My TC plugin is identifying a contradiction, but that is not preventing the<br>
> module from type checking, nor does GHC even raising a warning (with<br>
> -Wall). This is not the behavior I was expecting. How confused am I?<br>
><br>
> I've distilled the behavior that's confusing me down to the following<br>
> example<br>
><br>
> > module Test where<br>
> ><br>
> > class C a where f :: a -> ()<br>
><br>
> paired with a very silly plugin that always claims every constraint it sees<br>
> is a contradiction.<br>
><br>
> > module Contrarian (plugin) where<br>
> ><br>
> > import Plugins (Plugin(..),defaultPlugin)<br>
> > import TcPluginM (tcPluginIO)<br>
> > import TcRnTypes (TcPlugin(..),TcPluginResult(TcPluginContradiction))<br>
> ><br>
> > plugin :: Plugin<br>
> > plugin = defaultPlugin { tcPlugin = const (Just contrarianPlugin) }<br>
> ><br>
> > contrarianPlugin :: TcPlugin<br>
> > contrarianPlugin = TcPlugin {<br>
> >     tcPluginInit = return ()<br>
> >   ,<br>
> >     tcPluginSolve = \() given derived wanted -> do<br>
> >       tcPluginIO $ putStrLn "Alternative facts!"<br>
> >       return $ TcPluginContradiction $ given ++ derived ++ wanted<br>
> >   ,<br>
> >     tcPluginStop  = \() -> return ()<br>
> >   }<br>
><br>
> Please review the following GHCi session. We start *without* the plugin.<br>
><br>
>     $ ghc --interactive Test.hs<br>
>     GHCi, version 8.2.1: <a href="http://www.haskell.org/ghc/" rel="noreferrer" target="_blank">http://www.haskell.org/ghc/</a>  :? for help<br>
>     [1 of 1] Compiling Test             ( Test.hs, interpreted )<br>
>     Ok, 1 module loaded.<br>
>     *Test> f ()<br>
><br>
>     <interactive>:1:1: error:<br>
>         * No instance for (C ()) arising from a use of `f'<br>
>         * In the expression: f ()<br>
>           In an equation for `it': it = f ()<br>
><br>
> That behavior meets my expectations. Now let's add the plugin to see what<br>
> contradictions cause to happen --- my naive guess is that we should see the<br>
> same thing. (I don't really know what contradictions *should* cause GHC to<br>
> do *differently* than the above.) The following is a continuation of the<br>
> same session.<br>
><br>
>     *Test> :set -fplugin=Contrarian<br>
>     *Test> f ()<br>
>     Alternative facts!<br>
>     Alternative facts!<br>
>     Alternative facts!<br>
>     Alternative facts!<br>
>     *** Exception: <interactive>:3:1: error:<br>
>         * No instance for (C ()) arising from a use of `f'<br>
>         * In the expression: f ()<br>
>           In an equation for `it': it = f ()<br>
>     (deferred type error)<br>
>     *Test> :t f<br>
>     Alternative facts!<br>
>     f :: a -> ()<br>
><br>
> Interesting: claiming the constraint is a contradiction seems to convert<br>
> the type error to a deferred type error. Let's see if we can disable that<br>
> (since it's not the behavior I want).<br>
><br>
>     *Test> :set -fno-defer-type-errors<br>
>     *Test> :t f<br>
>     Alternative facts!<br>
>     f :: a -> ()<br>
>     *Test> f ()<br>
>     Alternative facts!<br>
>     Alternative facts!<br>
>     Alternative facts!<br>
>     Alternative facts!<br>
>     *** Exception: <interactive>:3:1: error:<br>
>         * No instance for (C ()) arising from a use of `f'<br>
>         * In the expression: f ()<br>
>           In an equation for `it': it = f ()<br>
>     (deferred type error)<br>
><br>
>     <interactive>:7:1: error:<br>
>         * No instance for (Show (a0 -> ())) arising from a use of `print'<br>
>             (maybe you haven't applied a function to enough arguments?)<br>
>         * In a stmt of an interactive GHCi command: print it<br>
>     *Test><br>
><br>
> I seems we can't disable this behavior. That makes it seem pretty<br>
> fundamental. So I'm guessing I'm confused about something, probably what<br>
> TcContradiction achieves in terms of the user experience.<br>
><br>
> The behavior I want is for my plugin to identify (relevant) contradictions<br>
> and incur a static type error as soon as possible. I thought contradictions<br>
> would achieve that, but I seem to be wrong.<br>
><br>
> What I should be expecting regarding contradictions?<br>
><br>
> How should I achieve my desired behavior? Perhaps I should try "solving"<br>
> the contradiction constraints via an appeal to a TypeError constraint<br>
> instead. Or maybe I should just leave the identified contradictions<br>
> unsolved?<br>
><br>
> Thanks. -Nick<br>
><br>
> PS - A big thank you to Adam Gundry and Christiaan Baaij (and probably<br>
> others) for the useful wiki pages, blog posts, and publications -- they've<br>
> been a huge help for my learning about the typechecker via plugins! I'm<br>
> very excited about this plugin, and I hope to share it soon, but I'd like<br>
> to understand it better before I do.<br>
</blockquote></div></div></div></div></blockquote></div>