Equality rejected by ghc-proofs but accepted by inspection-testing

[Lysxia]

I'm trying to get a feeling for what works and what doesn't with ghc-proofs and inspection-testing, and I found this case where inspection-testing recognizes two equal functions but ghc-proofs doesn't. Shouldn't it only ever be the other way around?

http://lpaste.net/360116

[Lysxia]

#1 suggests that this kind of thing can happen, but I'm not sure why.

[nomeata]

ghc-proofs only runs the simplifier (and CSE), and with different settings relating to inlining. inspection-testing runs all of GHC’s optimizations (strictness analysis, call arity, worker-wrapper transformation etc.), so differences are not surprising in theory.

The example linked there is still curious…

[nomeata]

$ ghc-8.2 -O Test.hs 
[1 of 1] Compiling Test             ( Test.hs, Test.o )
GHC.Proof: Proving teq2 …
Proof failed
    Simplified LHS: a @ GHC.Types.Any @ GHC.Types.Any
    Simplified RHS: b @ GHC.Types.Any @ GHC.Types.Any

I think the problem here is insufficient inlining: ghc-proofs works by aggressively inlining, but GHC does not inline recursive definitions like these.

[Lysxia]

I'm surprised GHC can still optimize these sufficiently for inspection-testing to see that they are the same.

How could we make ghc-proofs work with recursive definitions? GHC doesn't expose unfoldings for them, does it? That seems to be the main obstacle.

[nomeata]

I'm surprised GHC can still optimize these sufficiently for inspection-testing to see that they are the same.

There isn’t anything to optimize: They are already just the same (up-to alpha equality)!

How could we make ghc-proofs work with recursive definitions? GHC doesn't expose unfoldings for them, does it? That seems to be the main obstacle.

Since they are in the same module, we can find the definition. So then we wrap them in local let’s, to get a single expression, and do what we have done before. That should be doable…

Do you have a real use-case for this one?

[Lysxia]

Here's an example from my profunctor-monad:

replicateP_
  :: (Profunctor p, Applicative (p [x]))
  => Int -> p x a -> p [x] [a]
replicateP_ 0 _ = pure []
replicateP_ n p = (:)
  <$> head =. p
  <*> tail =. replicateP_ (n - 1) p

where (=.) = lmap (= flip (.) for p ~ (->)).

I'd like to prove that, for all xs of length n, replicateP_ n id xs = xs. (Then more interesting things will follow by parametricity or something.) That requires some inductive reasoning that seems to fit in the scope of ghc-proofs.

Matters are probably also complicated by the precondition (which relates two inputs) and partiality, but let's try to consider them as orthogonal to this issue.

---

A simplified example would be:

id_list :: [a] -> [a]
id_list [] = []
id_list (x : xs) = x : id_list xs

Prove that for all xs, id xs = id_list xs.

[nomeata]

That requires some inductive reasoning that seems to fit in the scope of ghc-proofs.

Not sure if inductive reasoning really fits the scope of ghc-proofs: The idea of ghc-proofs is to use the compiler to transform, and then just check equality.

Does GHC really optimize id_list away? I don’t think so.

But we should make the equality check better, so that when the compiler /can/ optimize them to be equal (likely without inductive reasoning) that then ghc-proofs is happy. Maybe just using the same code as in https://github.com/nomeata/inspection-testing/blob/46558d36c8bccbad62cece2141da0b6633303be3/Test/Inspection/Core.hs#L88?