<div dir="ltr">Thanks! Before you replied, I ended up just making it do (<span class="gmail-blob-code-inner">inst [``:'m`` |-> ``:tvarN``]) since it seemed like the type variable that appears is always 'm. </span><span class="gmail-blob-code-inner">I think your method is more portable.<br><br>I was actually confused in my initial question because I thought the displayed 'm was 'v. i.e. that the choice of type variable could be dependent on context where the term was constructed (hence needing something like cinst instead of a fixed inst on a type var).<br></span></div><div class="gmail_extra"><br><div class="gmail_quote">On Sun, Jan 15, 2017 at 10:23 PM, Ramana Kumar <span dir="ltr"><<a href="mailto:Ramana.Kumar@cl.cam.ac.uk" target="_blank">Ramana.Kumar@cl.cam.ac.uk</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">I don't know any more automated way to do this than you found. You<br>
could define a wrapper around mk_TypeId, like:<br>
<br>
val TypeId_arg_ty = type_of TypeId |> type_of |> dom_rng |> #1<br>
fun mki_TypeId x = mk_TypeId (cinst TypeId_arg_ty x)<br>
<div><div class="h5"><br>
On 16 January 2017 at 09:25, Yong Kiam <<a href="mailto:tanyongkiam@gmail.com">tanyongkiam@gmail.com</a>> wrote:<br>
> Hi dev,<br>
><br>
> I'm repairing the translator on env_refactor where the id type is defined<br>
> as:<br>
><br>
> ... id = Short of 'n | Long of 'm => id<br>
><br>
> The translator gets to a point where it constructs a term like ``Short foo:<br>
> ('v,tvarN) id``<br>
><br>
> However, it then tries to wrap it using mk_TypeId, where TypeId is a<br>
> constructor for:<br>
><br>
> ... tid_or_exn = TypeId of (modN,typeN) id | ...<br>
><br>
> (tvarN,modN,typeN, are all abbrevs for string)<br>
><br>
> but this fails because mk_TypeId does not instantiate 'v to modN.<br>
><br>
> I found that I could get around this manually using TypeBasePure.cinst<br>
> ``:(tvarN,tvarN) id`` , but is there a way that already automatically does<br>
> this?<br>
><br>
</div></div>> ______________________________<wbr>_________________<br>
> Developers mailing list<br>
> <a href="mailto:Developers@cakeml.org">Developers@cakeml.org</a><br>
> <a href="https://lists.cakeml.org/listinfo/developers" rel="noreferrer" target="_blank">https://lists.cakeml.org/<wbr>listinfo/developers</a><br>
><br>
</blockquote></div><br></div>