On 19 jul. 2012, at 19:28, Philip Holzenspies wrote:
Dear Simon, et al,
I finally got back around to working on this idea. I'm not yet quite sure
whether I've now understood it all. I have reread the latest edition of
System F with Type Equality Coercions (Jan 2011 version), so I
Dear Simon, et al,
I finally got back around to working on this idea. I'm not yet quite sure
whether I've now understood it all. I have reread the latest edition of System
F with Type Equality Coercions (Jan 2011 version), so I understand that
inference is now just percolating coercions
: 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
Philip
| What I'm looking for is a function
|
| fitsInto :: TermType - HoleType - Maybe [(TyVar,Type)]
Happily there is such a function, but you will need to become quite familiar
with GHC's type inference engine.
We need to tighten up the specification first. I believe that you have
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
L.S.,
I've come up with some minor progress myself, but I could still do with a
little help. The attached file is the smallest thing I could come up with to
replicate my problem.
I'm using tcMatchTy now to try and match two types, hoping to find TyVar
substitutions when the types unify. Given
