Re: Writing a subtype function

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 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:ghc-devs-bounces@haskell.org] On Behalf Of Izzy | Meckler | Sent: 22 February 2015 06:12 | To: ghc-devs@haskell.org | 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 | ghc-devs@haskell.org | http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs