Philip If you develop a function that does what you want, and want to make it part of the GHC API, we'd definitely consider including it. But I don't want to promise to develop something just for you; I'm just too snowed under with other stuff. I really think the "holes" that Thijs is working on might be good for you. He has a prototype already I think. Simon | -----Original Message----- | From: "Philip K. F. Hölzenspies" [mailto:pkfh@st-andrews.ac.uk] | Sent: 28 June 2012 11:11 | To: Simon Peyton-Jones | Cc: thijsalkemade@gmail.com; glasgow-haskell-users@haskell.org | Subject: Re: API function to check whether one type fits "in" another | | 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.