Sharing in properties produces unprovable Coq propositions

[MajaRet]

Description

An impure Property is converted to False when converting it to a Coq Prop. This makes properties with more than one occurrence of a variable on their right-hand side unprovable.

Steps to Reproduce

Translate the following QuickCheck property on the issue-76 branch.

prop_refl :: Integer -> Property
prop_refl x = x === x

Then compute quickCheck (fun Shape Pos I => @prop_refl Shape Pos I Cbneed).

Expected behavior

The property should be provable via the reflexivity tactic.

Actual behavior

Because x occurs twice, sharing analysis will transform this property as follows.

prop :: Integer -> Property
prop_id x = let y = x in y === y

This will then be translated to

  share x >>=
  (fun (x0 : Free Shape Pos (Integer Shape Pos)) =>
     @eqProp Shape Pos (Integer Shape Pos) _ x0 x0).

Now, when we try to prove this property using call-by-need evaluation, share x will be an impure value, which means the whole Property will be impure. However, an impure Property is currently translated to the Coq Prop False, meaning the property becomes unprovable.

More specifically, the result of quickCheck (fun Shape Pos I => @prop_refl Shape Pos I Cbneed) is now

forall (x : Type) (x0 : x -> Type),
Injectable Share.Shape Share.Pos x x0 -> Free x x0 (Integer x x0) -> False : Prop
     : Prop

We should not simply prevent the generation of share/call operators in properties. Instead, we should try to allow impure properties and find an appropriate way to translate them into Coq Props.

Additional Notes

This behavior is not technically a bug and rather a consequence of the existing design, which does not allow impure properties. But since it causes call-by-need evaluation to be essentially unusable, I will keep it labeled as a bug.

The main branch does not currently behave like this unless let bindings are explicitly introduced in properties. However, the behavior will appear if the sharing analysis (#169) is merged, so we should find a solution before then.