Monoid.mappend does not preserve refinements of its elements

[nikivazou]

Consider two list of Nat

{-@ xs1, xs2 :: [Nat] @-}
xs1 = [3, 4] 
xs2 = [1, 2]

Liquid Haskell cannot prove that mappending xs and ys returns a list of Nats. Ie. the following fails

{-@ xs  :: [Nat] @-}
xs  = xs1 <> xs2 

As the type of mappend :: Monoid m => m -> m -> m has a type class constrain.

To fix this we can instantiate the mappend type before application. The following is decided SAFE:

{-@ xs'  :: [Nat] @-}
xs' = xs1 <+> xs2 

(<+>) :: [a] -> [a] -> [a]
(<+>) = (<>)

The above code is here

The above generalizes to polymorphic class methods. Liquid Haskell does not take advantage of the polymorphism because of the type class constrain.

[vikraman]

I think I have a similar problem here. I cannot prove properties about (==) :: Eq a => a -> a -> Bool instantiated to Int, but I can prove stuff about eqInt :: Int -> Int -> Bool ; eqInt x y = x == y.

[nikivazou]

@vikraman it is not the same problem: the Monoid m constraint removes the Nat info, as for example the mempty = -1 does not create a Nat. Eq a cannot create new values and Liquid Haskell (hard codedly) knows that, so it does not remove any information.

What "stuff" you cannot prove with (==) and you can prove with eqInt?

[vikraman]

I was hoping to just write

veqInt :: VerifiedEq Int
veqInt = VerifiedEq (==) (\_ -> simpleProof) (\_ _ -> simpleProof) (\_ _ _ -> simpleProof)

Since the Int is on the signature, (==) should get specialised to Int and the proofs are just trivial.

But now that I think about it, obviously (==) is not reflected and so this cannot work. If you can suggest some way to simplify these proofs, please let me know.

[ranjitjhala]

Grr. can't disable the "label"...

Anyway not sure if this needs to be kept open?

[ranjitjhala]

@nikivazou your original problem seems super researchy; not clear if/whether its related to the "proper" treatment of classes? (Don't think so...)

Anyway its odd that we need the "wrapper"; wonder why the constraint generation doesn't behave equivalently to it.