17 Mai
2020
17 Mai
'20
00:49
+ (* TODO decompose the arrows to match on the result type and + then recursively search for the parameters' types *) + let constraints = Unif.unify ~checking:true t' t lctx in
Now that I think about it, this isn't right either: e.g. if a var in the environment currently has type ?t (i.e. a meta-variable not yet instantiated), the above Unif.unify will presumably use it quite happily (and instantiate the ?t to the type we're looking for), even though that's not a good idea. Or am I missing something? Stefan