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 <[email protected]> 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 <[email protected]> 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 [email protected] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
