Cannot apply lemma involving type class

[roboguy13]

I'm not totally sure what's happening here and unfortunately I haven't been able to figure out how to narrow this down to a minimal example so far.

I have a rule for a certain monad homomorphism:

{-# RULES "liftR-hom" [~]
      forall x f.
        liftR x >>= (liftR . f)
          =
        liftR (x >>= f)
  #-}

and I can transform a certain piece of code into:

(>>=) ▲ $dMonad ▲ ▲ (liftR ▲ (buttonE (I# 0)))
      ((.) ▲ ▲ ▲ (liftR ▲)
           (λ r →
              (>>) ▲ $fMonadR' ▲ ▲ (ledE (I# 0) r) (ledE (I# 1) (notB r))))

(everything before this line performs this transformation)

This looks like it fits the RULE to me, but I can't use lemmaForward "liftR-hom" (or more generally, anyBU $ lemmaForward "liftR-hom").

I think I ran into the same problem earlier with RULES regarding the left monad identity and monad associativity laws. I ended up working around it so I didn't need those transformations, but I'm pretty sure I really need this one.

It seems like it might have something to do with the type quantifiers or the type class dictionaries, but providing explicit types in the RULE doesn't seem to help.

Just in case, I also tried introducing lets for the lambda and for the application of buttonE to make it look even more like the RULE (in fact, it looked pretty much identical to it at that point), but that didn't lead anywhere.

[ecaustin]

If I recall from Drew's dissertation presentation, you have to specialize the rule to the particular type you are working with.

See the use of inst-lemma from his defense slides here: http://www.ittc.ku.edu/~afarmer/talks/defense.html#(23)

An entire proof of the left identity law for the list monad is shown on http://www.ittc.ku.edu/~afarmer/talks/defense.html#(27), hopefully that helps too.

[roboguy13]

@ecaustin It looks like it is already instantiated to the specific Monad (there is no m :: * -> * to instantiate):

HERMIT> eval "set-pp-type Detailed"
<...>

HERMIT> eval "show-lemma liftR-hom"
liftR-hom (Not Proven)
  ∀ (b ∷ *)
    (a ∷ *)
    ($dMonad ∷ Monad (StateT ([Bool], [Bool])
                             (ReaderT DeviceContext IO)))
    (x ∷ R' a)
    (f ∷ a → R' b).
  (>>=) (StateT ([Bool], [Bool]) (ReaderT DeviceContext IO)) $dMonad
        a b (liftR a x)
        ((.) (R' b) (StateT ([Bool], [Bool]) (ReaderT DeviceContext IO) b)
             a (liftR b) f)
  ≡
  liftR b ((>>=) R' $fMonadR' a b x f)
[Done]

[roboguy13]

Also, I was able to use the >> version of that lemma (liftR-hom_) successfully. I'm probably using the liftR-hom in a different way somehow, but I'm not sure which difference is the difference that's causing the problem.

[xich]

Can you set-pp-type Detailed and show both the target code and the rule?

[roboguy13]

@xich Sorry for the late reply! Here's what it looks like with set-pp-type Detailed:

HERMIT> display
(>>=) R $fMonadR Bool ()
      ((>>=) R $fMonadR (E Bool) Bool (buttonE (I# 0))
             (λ (x ∷ E Bool) → return R $fMonadR Bool (unLit x)))
      (λ (b ∷ Bool) →
         (>>) R $fMonadR () () (ledE (I# 0) (lit b))
              ((>>) R $fMonadR () () (ledE (I# 1) (lit (not b)))
                    (wait (I# 100))))
[Done]

HERMIT> lemmaForward ">>=-assoc"
*** Exception: server failure: Object (fromList [("exception",String "Rewrite failed:expression did not match left-hand side")]) : Rewrite failed:expression did not match left-hand side
HERMIT> eval "show-lemma \">>=-assoc\""
>>=-assoc (Assumed)
  ∀ (m ∷ * → *)
    (b ∷ *)
    (a ∷ *)
    (a ∷ *)
    ($dMonad ∷ Monad m)
    (m ∷ m a)
    (f ∷ a → m a)
    (g ∷ a → m b).
  (>>=) m $dMonad a b ((>>=) m $dMonad a a m f) g
  ≡
  (>>=) m $dMonad a b m (λ (e ∷ a) → (>>=) m $dMonad a b (f e) g)
[Done]

The code is here (the immediately relevant files are src/Main.hs and src/MainScript.hs): https://github.com/roboguy13/sunken/tree/2667c7000613edb7f9089606e752a871be15dd4b

[xich]

Hmmm, that does look right... can you unshadow the lemma (to distinguish the a's) just to make sure?

I guess I'll start improving the error messages until I can figure out why.

[roboguy13]

I might not understand how to unshadow it. I keep getting errors:

hermit<0> set-pp-type Detailed
module Main where
  unLit ∷ E Bool → Bool
  main ∷ IO ()
  main ∷ IO ()
hermit<0> rule-to-lemma ">>=-assoc"
>>=-assoc (Not Proven)
  ∀ (m ∷ * → *) (b ∷ *) (a ∷ *) (a ∷ *) ($dMonad ∷ Monad m) (m ∷ m a) (f ∷ a → m a) (g ∷ a → m b).
  (>>=) m $dMonad a b ((>>=) m $dMonad a a m f) g
  ≡
  (>>=) m $dMonad a b m (λ (e ∷ a) → (>>=) m $dMonad a b (f e) g)
hermit<1> prove-lemma ">>=-assoc"
Goal:
  ∀ (m ∷ * → *) (b ∷ *) (a ∷ *) (a ∷ *) ($dMonad ∷ Monad m) (m ∷ m a) (f ∷ a → m a) (g ∷ a → m b).
  (>>=) m $dMonad a b ((>>=) m $dMonad a a m f) g
  ≡
  (>>=) m $dMonad a b m (λ (e ∷ a) → (>>=) m $dMonad a b (f e) g)
proof<2> lhs unshadow
Error in expression: lhs unshadow
catchesM failed
proof<2> rhs unshadow
Error in expression: rhs unshadow
catchesM failed
proof<2> unshadow
Error in expression: unshadow
This rewrite can only succeed at core nodes.

Here's what the RULE definition looks like:

{-# RULES ">>=-assoc" [~]
      forall m f g.
        (m >>= f) >>= g
          =
        m >>= (\e -> f e >>= g)
  #-}

[xich]

There is a (poorly named) unshadow-quantified command.

[roboguy13]

Ahh, thanks. Here's what that looks like:

proof<2> unshadow-quantified 
Goal:
  ∀ (m ∷ * → *) (b ∷ *) (a ∷ *) (a0 ∷ *) ($dMonad ∷ Monad m) (m0 ∷ m a) (f ∷ a → m a0) (g ∷ a0 → m b).
  (>>=) m $dMonad a0 b ((>>=) m $dMonad a a0 m0 f) g
  ≡
  (>>=) m $dMonad a b m0 (λ (e ∷ a) → (>>=) m $dMonad a0 b (f e) g)

[roboguy13]

Well, I've been trying to trace the Equality list in HERMIT.Dictionary.Reasoning.birewrite, but that's proving harder than I thought it would be. I found ppEqualityT, but it looks like it ultimately needs to be in HermitM.

[xich]

Some debugging tips:

• All the monadic layers involved should have liftIO instances, so liftIO $ print ... is your friend.
• A lot of things can be turned into strings with showPpr. The DynFlags argument can be gotten from getDynFlags in most places.
• This particular problem is most likely to do with runFoldMatches and filterOutOfScope here: https://github.com/ku-fpg/hermit/blob/master/src/HERMIT/Dictionary/Fold.hs#L123

[roboguy13]

@xich Thanks! I'll take a look at those later. I found that if I monomorphize the RULE, it works fine. Maybe I need to monomorphize it in HERMIT somehow (I think I tried instDictionaries a week or two ago though and it didn't seem to work)?

This is what I ended up with:

{-# RULES ">>=-assoc" [~]
      forall (m :: R a) (f :: a -> R b) (g :: b -> R c).
        (m >>= f) >>= g
          =
        m >>= (\e -> f e >>= g)
  #-}

[xich]

Glad there is a workaround, but there is no fundamental reason that the more general rule shouldn't work... I suspect there is an interesting thing going on with the dictionary binders, but haven't had a chance to sit down and debug it.

[roboguy13]

@xich Unfortunately, the functions I've been looking at so far (runFoldMatches and filterOutOfScope) don't seem to have a way to get at a DynFlags value. I see that there is a unsafeGlobalDynFlags :: DynFlags, but that doesn't sound very safe...

Also, it looks like neither CoreExpr and Equality are Outputable.

I might be going in the wrong direction with this altogether, though

[xich]

Ah yes, those functions are pure... so trace is your friend (I believe HERMIT.GHC exports it, or you can use the one from Debug.Trace).

That is weird about Outputable... CoreExpr definitely was in versions prior to 7.10. Makes me wonder how this is compiling: https://github.com/ku-fpg/hermit/blob/master/src/HERMIT/PrettyPrinter/GHC.hs

Feel free to add a DynFlags argument to those functions while you debug.