Wonderful, even more than I thought I needed (i.e., actually getting the evidence). Thanks Simon!
> On Feb 23, 2015, at 8:18 AM, Simon Peyton Jones <[email protected]> wrote: > > | I’m at a loss as to how to use TcUnify.tcSubType. My goal is to write a > | function of type > | > | Type -> Type -> Ghc Bool > > I assume you are talking here about the GHC API? tcSubType is usually called > during type inference, and it rightly does not return a Bool. Why? Because we > may not know whether it will succeed or fail until we have walked the entire > syntax tree of the program; perhaps there is a bit of code that forces a > crucial unification. > > So tcSubType returns a `HsWrapper`, which you can use to wrap a term of type > t1, to produce a term of type t2. > > It ALSO emits some constraints (in the monad) which can be solved later. If > the constraints are soluble, we have a proof that t1 is a subtype of t2. If > not, we don’t. > > In the context of the GHC API you probably need something like > > do { (_wrapper, constraints) <- captureConstraints (tcSubType t1 t2) > ; tcSimplifyTop constraints } > > The 'captureConstraints' grabs the constraints generated by tcSubType; the > tcSimplifyTop tries to solve them and reports errors. If you don’t want to > report errors, you can doubtless use some variant of tcSimplifyTop. > > I hope this helps > > Simon > > | -----Original Message----- > | From: ghc-devs [mailto:[email protected]] On Behalf Of Izzy > | Meckler > | Sent: 22 February 2015 06:12 > | To: [email protected] > | Subject: Writing a subtype function > | > | Hi all, > | > | I apologize if this isn’t the right place for this sort of question, but > | I’m at a loss as to how to use TcUnify.tcSubType. My goal is to write a > | function of type > | > | Type -> Type -> Ghc Bool > | > | which checks whether the first argument is a subtype of the second. I > | assume this is possible to do using TcUnify.tcSubType and > | runTcInteractive, but it’s not clear to me how. Any pointers here would > | be greatly appreciated. > | _______________________________________________ > | ghc-devs mailing list > | [email protected] > | http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs _______________________________________________ ghc-devs mailing list [email protected] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
