API function to check whether one type fits "in" another

["Philip K. F. Hölzenspies"]

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.