Job opening: compiling to categories

2017-08-05 Thread Conal Elliott
I have a job opening to work closely with me (at Target Digital) on the GHC plugin described in the paper *Compiling to Categories* as well as on applications, including machine learning. I’m especially looking for someone used to working inside of

How does GHC handle TcPluginContradiction?

2017-08-05 Thread 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 >

Re: How does GHC handle TcPluginContradiction?

2017-08-05 Thread 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

Re: How does GHC handle TcPluginContradiction?

2017-08-05 Thread 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

Re: How does GHC handle TcPluginContradiction?

2017-08-05 Thread 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