Re: Getting valid substitutions to work for subsumption

On May 18, 2017, at 5:27 PM, Simon Peyton Jones wrote:

I don't agree. If you call (tcSubsumes hole_ty ty) with closed types hole_ty, ty, it should return True if

I agree here. But it looks like Matthías's function gets the expected type as pushed down by bidirectional typechecking. This type will always be deeply skolemized before tcSubsumes can get a hold of it, so it won't be closed. Richard