How does GHC handle TcPluginContradiction?

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
4 messages Options
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

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.

_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: 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.
_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: How does GHC handle TcPluginContradiction?

Nicolas Frisby
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 <[hidden email]> 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.

_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: How does GHC handle TcPluginContradiction?

Nicolas Frisby
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 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 <[hidden email]> 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 <[hidden email]> 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.

_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Loading...