Dear Simon, et al,
Thank you very much for your reply. Some of the pointers you gave, I wouldn't
have come across, for not knowing to have to browse through the module Inst,
for example.
I read the OutsideIn paper (JFP), but that's a fair while back. I was pointed
to Thijs's work in progress at an Agda talk recently. The front-end we're
working on should be portable to any lambda-language with strong types, so the
availability of holes in Agda and Idris makes the implementation for those
back-ends a breeze.
There is one limiting consideration, however: We want to get this up and
running the next few weeks and we would like to keep things in-sync with the
developments on the different back-ends. This is why I'm trying to stay as
close as possible to the more "public" API parts (the things that are
documented and haven't changed significantly since at least 7.0.4).
In this light, I was wondering whether it's not worth having a function that
does all this plumbing in the API that is persistent through future versions,
much like pure interface to the parser (GHC.parser). Preferably it would look
something like:
typeCheck
:: DynFlags -- the flags
-> FilePath -- for source locations
-> Type -- expected
-> Type -- actual
-> Either
SomeSortOfErrorStructure
SomeSubstitutionAndOrConstraintTable
The implementation would have to make sure the pre-conditions of the type
arguments are met. Is this worth pursuing? Would be a significant amount of
work? Am I being pushy if I make this a feature-request?
Regards,
Philip
PS. I'm going to study the Trac you pointed to in more detail; browsing it was
already a learning experience about the whats and wheres of the GHC API.
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
