Specs of local definitions #2325
Comments
|
Here's another proposal: We should always link the spec to a recursive binding if there is more than one closest binding at the same source location. If there are no recursive bindings, just pick any of the closest bindings. We could have only non-recursive bindings if we are trying to annotate a non-recursive value or function. I don't expect to have to decide between multiple recursive bindings, or bindings that have different types. We will have to consider those cases when they happen. To implement the change, the local bindings are collected here, and they are only used here. I'm storing the work in progress for this strategy here: |
|
Here's another example that doesn't work with the above strategy. Desugars to The it cannot show that Normally, LH would be able to infer a suitable refinement type for |
|
Another complicated case arises when compiling loopU has a recursive binding called Without break points, verification fails with Similar to the example in the previous comment, these errors are avoided by giving an explicit type signature to |
|
I think there is a simpler solution here: give the local function a Haskell type signature. When you do that, GHC will not generate an auxiliary local binding. Here's your example: We get this from Now your job is much easier I think. This works for mutual recursion. Functions that have a complete type signature always go this route. |
|
Thanks @simonpj for having a look. I guess at this point it is a matter of quality of the user experience. Should we have LH complain when a spec is given for a local binding that has no type signature? Adding the signature is always going to be some hassle, and it may be worse if Would it be possible to talk the desugarer into avoiding auxiliary bindings regardless of the presence of type signatures? Perhaps this would be ideal from the user perspective. |
|
Surely the Haskell type sig is just a subset of the LH spec? Easy!
I'm afraid it would not. It's to do with typechecking mutual recursion. The recursive loop is monomorphic, even though the external interface is polymorphic. |
Yes ... when the spec is complete. Sometimes the user could leave it to GHC. e.g. Is the guarantee to eliminate auxiliary bindings via explicit type signatures something the desugarer could have tests for?
That's good to know. We need to collect more examples, though. With the last tuning of Core transformations, the need for explicit type signatures is not surfacing in tests. But there is no design at work to stop it from coming back later. |
Specs of local definitions have been problematic for some time now. In what follows I explain why this is brittle, and what we can do to improve it.
The problem
Ideally, local specs work as follows:
In the above program, the
gospec is linked to thegolocal definition.However, sometimes GHC might desugar to the following core.
The
gospec is still linked to thegolocal definition. But note thatgois no longer a recursive definition.go2is a recursive definition, but it cannot be proved to terminate because the termination metrics are attached togoinstead ofgo2.This case used to pass in the testsuite because a-normalization would rearrange it to
(I'm eliding the other effects of a-normalization here)
and,
goandgo2Vars are mapped to the samegosymbol in LH. This is because when GHC generatesgo2it gives it the same string name asgobut a different unique. Moreover,go2is given the same source location asgo, which is the main attribute that LH uses to decide what to attach a spec to.Slight changes to the example or GHC are likely to upset this equilibrium, though, as I have encountered in practice already.
Earlier measures
Liquid Haskell does some transformations on the desugared expressions, in an attempt to prevent this sort of trouble. For this case, this inlineLoopBreaker transformation would apply if the output of desugaring were instead:
Note that there is an eta reduction, and the parameters
b1andb2are no longer present.inlineLoopBreakerwould then produce almost the original program as written by the user.While we could try to accommodate this case in the same transformation, I would prefer that we aimed for a simpler solution, or one that could survive to more tweaks to desugaring.
A simpler solution
Perhaps Liquid Haskell should flag an error when there is a spec to a local binding, and there are multiple such local bindings with the same name and source location. This would cause the above program to fail verification.
The user then could stop GHC from generating a
go2binding ifgois given an explicit type signature. The following example would pass verification because there is only onegobinding with the closest source location.{-@ sum2D :: Vec2D -> Nat -> Nat -> Int @-} sum2D :: Vec2D -> Int -> Int -> Int sum2D a n m = go n m where {-@ go :: ink:Nat -> joe:Nat -> Int / [ink, joe] @-} go :: Int -> Int -> Int go 0 0 = a 0 0 go i j | j == 0 = a i 0 + go (i-1) m | otherwise = a i j + go i (j-1)Is this enough of a remedy?
The text was updated successfully, but these errors were encountered: