It will be okay if you put 'p' back:
// `g` evaluates `f` and then frees it.
fn g(f: &t >> t?): int = let
val r = f()
val _ = cloptr_free($UN.castvwtp0(f))
prval p = view@ f // <-- here
prval () = view@f := p
in r end
>>val _ = cloptr_free($UN.castvwtp0(f))
The above line is safe. We just need to find a better way to name it :)
On Fri, Aug 3, 2018 at 3:55 PM, 'Yannick Duchêne' via ats-lang-users <
ats-lang-users@googlegroups.com> wrote:
> Here is sample, what’s important is in `g` marked `<-- here`:
>
> staload UN = "prelude/SATS/unsafe.sats" // Prerequisite.
> viewtypedef t = () -<cloptr> int // Prerequisite.
>
> fn h(): t = let
> val v = 1
> in lam(): int => v end
>
> // `g` evaluates `f` and then frees it.
> fn g(f: &t >> t?): int = let
> val r = f()
> val _ = cloptr_free($UN.castvwtp0(f))
> prval p = view@ f // <-- here
> in r end
>
> var f = h()
> val v = g(f)
>
>
> The presence of `prval p = view@ f` produce a type error in `in r end`,
> which is not about `r`, rather about `>> t?` which is treated as something
> returned too.
>
> I’m surprised this proof which does not go outside the function, can
> change the returned type of `f`.
>
> I encountered other similar effects, including one without proof, this one
> is the simplest one.
>
> For the anecdote, I came to this while testing if there are ways to free
> the cloptr without an unsafe cast.
>
> --
> You received this message because you are subscribed to the Google Groups
> "ats-lang-users" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to ats-lang-users+unsubscr...@googlegroups.com.
> To post to this group, send email to ats-lang-users@googlegroups.com.
> Visit this group at https://groups.google.com/group/ats-lang-users.
> To view this discussion on the web visit https://groups.google.com/d/
> msgid/ats-lang-users/acad14e7-3f3b-4daf-9105-78864b00034a%
> 40googlegroups.com
> <https://groups.google.com/d/msgid/ats-lang-users/acad14e7-3f3b-4daf-9105-78864b00034a%40googlegroups.com?utm_medium=email&utm_source=footer>
> .
>
--
You received this message because you are subscribed to the Google Groups
"ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to ats-lang-users+unsubscr...@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLr8S4MrpJpNhuyNwZOBM6hU2XVt18KdDX5NqWMLb0VHgA%40mail.gmail.com.
