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

[Simon Peyton-Jones]

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 at st-andrews.ac.uk]
|  Sent: 28 June 2012 11:11
|  To: Simon Peyton-Jones
|  Cc: thijsalkemade at gmail.com; glasgow-haskell-users at 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.