Serialising evidence generated by typechecker plugins

2014-12-11 Thread Adam Gundry
Hi folks, I've just discovered tcIfaceCoAxiomRule, which is used when typechecking a coercion from an interface file. It turns out that CoAxiomRules are represented in interface files by their names, so tcIfaceCoAxiomRule looks up this name in a map containing all the built-in

Re: Serialising evidence generated by typechecker plugins

2014-12-11 Thread Richard Eisenberg
I've been following the plugins stuff at a small distance. I'vm very interested as a user, but don't have the bandwidth to think deeply as an implementor. With that caveat, I have a proposal: Suppose plugin P is responsible for producing CoAxiomRule R while compiling module M. I think it's

RE: Serialising evidence generated by typechecker plugins

2014-12-11 Thread Simon Peyton Jones
Go ahead and make suggestions here. Since a CoAxiomRule embodies essentially arbitrary computation, it's hardly surprising that there's a fixed range of possibilities. I suppose that for extensibilty, any particular plugin could say TypeNats:Rule1, TypeNats:Rule etc, and recognise that at the

Re: Serialising evidence generated by typechecker plugins

2014-12-11 Thread Iavor Diatchki
Hello, the reason there's a function there is that the type-nats are using an infinite family of axioms (e..g, the axiom `AddDef` which can be applied to any two concrete number, so `AddDef 1 2 : (1 + 2) ~ 3`). Do you think it'd be possible to allow plugins to register a list of axioms, so that

Please test: release candidates for Cabal/cabal-install patch releases on the 1.18 and 1.20 branches

2014-12-11 Thread Johan Tibell
I've uploaded release candidates for Cabal/cabal-install patch releases on the 1.18 and 1.20 branches: https://www.haskell.org/cabal/release/cabal-1.18.1.5/Cabal-1.18.1.5.tar.gz https://www.haskell.org/cabal/release/cabal-install-1.18.0.6/cabal-install-1.18.0.6.tar.gz

Re: Please test: release candidates for Cabal/cabal-install patch releases on the 1.18 and 1.20 branches

2014-12-11 Thread Johan Tibell
Apparently this no longer works: cabal install http://www.haskell.org/cabal/release/cabal-1.20.0.3/Cabal-1.20.0.3.tar.gz http://www.haskell.org/cabal/release/cabal-install-1.20.0.4/cabal-install-1.20.0.4.tar.gz Some change on the web server side means that the web server tries to redirect to an