Re: Serialising evidence generated by typechecker plugins

2014-12-12 Thread Richard Eisenberg
| To: Iavor Diatchki; Eric Seidel | Cc: ghc-devs@haskell.org mailto:ghc-devs@haskell.org | Subject: Serialising evidence generated by typechecker plugins | | Hi folks, | | I've just discovered tcIfaceCoAxiomRule, which is used when typechecking | a coercion from

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
| To: Iavor Diatchki; Eric Seidel | Cc: ghc-devs@haskell.org | Subject: Serialising evidence generated by typechecker plugins | | 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

Re: Serialising evidence generated by typechecker plugins

2014-12-11 Thread Iavor Diatchki
: Serialising evidence generated by typechecker plugins | | 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