How does GHC handle TcPluginContradiction?

Sun Aug 6 04:58:10 UTC 2017

I also just found issue #22 in Adam's uom github repository; it seems
related.

"""
The plugin is correctly reporting the constraint Base "s" ~~ Base "m" ^: 2 as
insoluble (note the use of ~~, which is a type family provided by
uom-plugin that
is a pseudo-synonym of ~). However, it turns out that the GHC
error-reporting machinery
<https://github.com/ghc/ghc/blob/ghc-8.0.1-release/compiler/typecheck/TcErrors.hs#L410-L415>
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 ~~. Failure to respect this invariant means that errors
are silently ignored.
"""

The insoluble constraints in my actual plugin is a genuine class, so this
isn't an obvious perfect fit for my case.

On Sat, Aug 5, 2017 at 7:46 PM Nicolas Frisby <nicolas.frisby at gmail.com>
wrote:

> Yes, thanks! I agree with you.
>
> I just realized on my dog walk that, according to
> https://ghc.haskell.org/trac/ghc/wiki/Plugins/TypeChecker, "If the plugin
> finds a contradiction amongst the givens, it should return
> TcPluginContradiction containing the contradictory constraints. These will
> turn into inaccessible code errors."
>
> 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.
>
> Thanks. -Nick
>
>
> On Sat, Aug 5, 2017 at 7:27 PM Edward Z. Yang <ezyang at mit.edu> wrote:
>
>> 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.
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20170806/d17ab0a0/attachment.html>