eval_Var_bug

[oshimayuki1124]

When you run the code below,
let f = fun x -> ((fun y -> y):?->?) x in let g = f in g (g 2 = 3);;
you will get an error message: Fatal error: exception Lambda_dti.Eval.Eval_bug("cannot cast value: 2").

I got the sentences below by debug-mode.

...
***** Cast-insertion *****
f: let f = fun 'x11,'x10 -> fun (x: 'x11) -> ((fun (y: 'x10) -> y): 'x10 -> 'x10 => ? -> ?) (x: 'x11 => ?) in (let g = fun 'x12 -> f['x12,ν] in g[bool] ((g[int] 2: ? => int) = 3))
U: ?
***** Eval *****
eval <-- let f = fun 'x11,'x10 -> fun (x: 'x11) -> ((fun (y: 'x10) -> y): 'x10 -> 'x10 => ? -> ?) (x: 'x11 => ?) in (let g = fun 'x12 -> f['x12,ν] in g[bool] ((g[int] 2: ? => int) = 3))
eval <-- fun (x: 'x11) -> ((fun (y: 'x10) -> y): 'x10 -> 'x10 => ? -> ?) (x: 'x11 => ?)
eval <-- let g = fun 'x12 -> f['x12,ν] in g[bool] ((g[int] 2: ? => int) = 3)
eval <-- f['x12,ν]
eval <-- g[bool] ((g[int] 2: ? => int) = 3)
eval <-- g[bool]
eval <-- (g[int] 2: ? => int) = 3
eval <-- g[int] 2: ? => int
eval <-- g[int] 2
eval <-- g[int]
eval <-- 2
eval <-- ((fun (y: 'x15) -> y): 'x15 -> 'x15 => ? -> ?) (x: 'x12 => ?)
eval <-- (fun (y: 'x15) -> y): 'x15 -> 'x15 => ? -> ?
eval <-- fun (y: 'x15) -> y
cast <-- : 'x15 -> 'x15 => ? -> ?
eval <-- x: 'x12 => ?
eval <-- x
cast <-- 2: 'x12 => ?
Fatal error: exception Lambda_dti.Eval.Eval_bug("cannot cast value: 2")

This shows that 'x12 is not substituted to int. This causes from eval in eval.ml which substitute types into type variables only once when evaluating Var.
To fix it, I let eval catch the set of type variables and types, and then give proc to substituted type.

However, this code only evaluates to blame after this modification, because ν is changed to fresh type variable in evaluating ... let g = f in ..., and this fresh type variable is no more freshed in evaluating g (g 2 =3).
This can be improved by correction in type inference process, but I didn't change it.

[ymyzk]

Thanks again for the contribution!

However, this code only evaluates to blame after this modification, because ν is changed to fresh type variable in evaluating ... let g = f in ..., and this fresh type variable is no more freshed in evaluating g (g 2 =3).
This can be improved by correction in type inference process, but I didn't change it.

I understand the limitation with the approach. As this project is not under active development and I have limited bandwidth for maintenance, I'll likely keep this it as is for the time being.