API function to check whether one type fits "in" another
"Philip K. F. Hölzenspies"
pkfh at st-andrews.ac.uk
Thu Jun 28 12:11:26 CEST 2012
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:
:: DynFlags -- the flags
-> FilePath -- for source locations
-> Type -- expected
-> Type -- actual
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?
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.
More information about the Glasgow-haskell-users