Runtime typing resolution fails while using `dyn`

[teofr]

The following example shows some kind of problem (as far as I could tell) with how the runtime type checking works (I'm not too sure if this is a bug, or just a misunderstanding from my side)

(eq F (pfun (dyn A) (dyn B) => print "checking in"),
F (dyn 1) (dyn 2), print "done numbers",
refl.typstring F TyF, print TyF, print F,
F (dyn false) (dyn true), print "done booleans") ? 

Which outputs:

"checking in"
"done numbers"
"dyn -> dyn -> prop"
fun ~destruct0 ~destruct1 => newmeta (fun A => newmeta (fun B => and (eq (tuple ~destruct0 ~destruct1) (tuple (dyn A) (dyn B))) (print "checking in")))
Impossible.

If I change the true and false for 3 and 4 it works just fine.

I'll keep trying to narrow what's going on, but my guess is that the (fun A => ...) function is getting (for some reason) globally typed, instead of per application of F.

[teofr]

Another example:

hello : [A] A -> prop.

hello 1.
hello true.

chau : dyn -> prop.
chau (dyn A) :- hello A.

(eq F (pfun (dyn A) => hello A), refl.typstring F TyF, print TyF, F (dyn 1), F (dyn true)) ?
(eq F (fun x => newmeta (fun y => and (eq x (dyn y)) (hello y))), refl.typstring F TyF, print TyF, F (dyn 1), F (dyn true)) ?
(chau (dyn 1), chau (dyn true)) ?

The queries with the anonymous functions break, and both get the type dyn -> prop. The query with chau works just fine.

This is quite interesting, since anonymous function should behave like syntactic substitution.

[astampoulis]

Thanks for reporting this @teofr. This is a tricky issue that I'll try to explain below. The small version (if it helps) is that a single type unification variable is allocated for all uses of the anonymous predicate, as there is no type-level equivalent of newmeta. This is quite unintuitive, but it's expected behavior of how the core works right now, and I am not entirely sure about how we should proceed about resolving this.

As you have seen, what pfun (dyn A) => ... expands to is:

• introducing new unification variables as they are used inside the patterns
• forcing unification of the patterns with the input New unification variables will be generated in each invocation of the predicate. The same thing happens if a (named) top-level predicate was used instead of the anonymous predicate.

If we were to use fun directly, we would have to be careful, as the following would not do what we would want: eq F (fun a b => eq a (dyn A), eq b (dyn B)), F (dyn 1) (dyn 2), F (dyn "foo") (dyn "bar") This would fail, since only two unification variables are being created: A and B, and once they are unified with 1 and 2, they won't be able to be unified with anything else (or anything of a different type, for that matter). We'd have to use newmeta instead or the pfun shorthand syntax.

Now, when it comes to type variables, things are a bit more tricky, since there is no predicate to explicitly allocate a new type variable, and then say that a new unification variable has that type. (That level of type and term mixing is unfortunately outside what Makam can do right now). Roughly what I'm describing could be:

eq F (newtypemeta (fun t => newmetaOfType t (fun a => ...))

Maybe a different way to say this, is that if the type argument to dyn was explicit, the anonymous predicate would roughly expand to this:

fun x => newmeta (fun (y: T) => (eq x (@dyn [T] y))

When you use a named predicate, new type unification variables are created for all the type parameters, so in that case things work as expected. That's the one fix I can think of right now.

In terms of an actual solution to the issue, I am not sure if I'm seeing yet a way to do this without revisiting the core significantly. The core could allow the user to be more explicit about functions over types and type unification in general. I think that could make some other things more intuitive as well, but it's quite on the long-term side.

[teofr]

Thanks for the explanation, it was more or less what I thought could be happening.

Rewriting the anonymous function as an auxiliary predicate is a good-as-it-can-get hack, so not much to worry.

Feel free to close this issue, or leave it open as a warning.