Nablas behaving differently to what the Lower Your Guards paper says
When accessing the long-distance information Nablas
with getLdiNablas
inside of the desugarer (specifically in dsExpr
) the returned Nablas
do not take into account the GADT type equalities and is missing the positive information about the cases. However, the way the Lower Your Guards paper describes Nablas
(which I'm assuming are supposed to represent the normalized refinement types since the symbol for those is a nabla in the paper) as having at most one matching pattern (invariant I4 - Single Solution). Why is that semantic difference there? I marked this issue a documentation issue since I was not able to find the explanation for the (possible) wrinkle in the comment for the Nabla
data type.