Fix unsafe data constructor refinements

[AlecsFerra]

By allowing arbitrary refinements of data constructor we can prove easily false:

data F where
{-@ MkF :: {_:F | false} @-}
    MkF :: F

{-@ falseProof :: { false } @-}
falseProof = () ? MkF

Since deciding if assuming some proposition leads to a contradiction is impossible
and in practice the only usage of refining a data constructor is with data proposition Prop from ProofCombinators we can just allow refinements of the shape { v:T | prop v = foo }.

All the other occurrences (2) can be solved without resorting to refining the data constructor:

• isAdmit from ProofCombinators can actually just be defined as an Haskell function
• {-@ Count :: x:a -> {v:Count a | v == Count x } @-} from CountMonad.hs can pass verification without it

If the user for some reason still wants to assume stuff on some constructor can use assume explicitly.

[facundominguez]

There is one issue concerned with specs of GADTs (#2090) which is fine to close, I think. But Niki made efforts to fix another ticket that also uses non-trivial refinement types (#2349).

I don't have use cases of my own that require specs for the returned type of data constructors. I guess that if @nikivazou doesn't object, it should be fine to merge.

[facundominguez]

Is this not true anymore? I would expect it to remain valid.

[AlecsFerra]

It is still true bout you need --exact-data-cons or some other flag that triggers it

[facundominguez]

I'm curious about whether it is so easy to introduce accidentally False to deserve constraining the refinements of data constructors.

[facundominguez]

Does this need to be so strict? Maybe it is fine to allow both prop v = foo and foo = prop v.

[AlecsFerra]

No is fine also in the other direction, I just copied the way that is done in ProofCombinators

[AlecsFerra]

There is one issue concerned with specs of GADTs (#2090) which is fine to close, I think. But Niki made efforts to fix another ticket that also uses non-trivial refinement types (#2349).

All these issue seem to mixup Haskells type indexes with liquid value, for what Haskell is concerned GADTs indexes are types so it makes sense that they interact weirdly with LH, if someone wants type indexes that interact well with LH they should use Prop.

I'm curious if it is easy to introduce accidentally False to deserve constraining the refinements of data constructors.

You can introduce some proposition on that on it's own is not false but can be inconsistent with some other proposition that you assumed somewhere else, especially since the refinement of constructors feels like function refinement I think the user expects them to be a sound feature (at least I was super convinced they were safe to use), if they had assume before the constructor name then it would be a different story.

Also since I wasn't able to find any other reasonable (where reasonable I believe should also imply sound) usage I think is fine to disallow it. If users want do potentially unsound shenanigans they can always use the assume keyword.

Also F* totally diallows refining the return type of a constructor for example.