Writing a subtype function

[Izzy Meckler]

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