Instance inductivity as constraint

Question

I'm trying to express an idea that given

instance (MonadTrans t, MonadX m) => MonadX (t m)

it should follow, that any t1 (t2 ... (tn m)) is also MonadX as long as all tx have MonadTrans instance. However when i try to write it down it doesn't work:

{-# LANGUAGE BasicallyEverything #-}

data Dict c where
  Dict :: c => Dict c

class (forall m . Monad m => Monad (t m)) => MonadTrans t where
  lift :: Monad m => m a -> t m a

class    (c m, Monad m, forall t . (MonadTrans t, Monad (t m)) => c (t m)) => Foo c m
instance (c m, Monad m, forall t . (MonadTrans t, Monad (t m)) => c (t m)) => Foo c m

liftDict :: MonadTrans t => Dict (Foo c m) -> Dict (Foo c (t m))
liftDict Dict = Dict

This results in following error:

    • Could not deduce: c (t1 (t m)) arising from a use of ‘Dict’
      from the context: MonadTrans t
        bound by the type signature for:
                   liftDict :: forall (t :: (* -> *) -> * -> *)
                                      (c :: (* -> *) -> Constraint) (m :: * -> *).
                               MonadTrans t =>
                               Dict (Foo c m) -> Dict (Foo c (t m))
        at src/Lib.hs:85:1-64
      or from: Foo c m
        bound by a pattern with constructor:
                   Dict :: forall (a :: Constraint). a => Dict a,
                 in an equation for ‘liftDict’
        at src/Lib.hs:86:10-13
      or from: (MonadTrans t1, Monad (t1 (t m)))
        bound by a quantified context at src/Lib.hs:1:1
    • In the expression: Dict
      In an equation for ‘liftDict’: liftDict Dict = Dict
    • Relevant bindings include
        liftDict :: Dict (Foo c m) -> Dict (Foo c (t m))
          (bound at src/Lib.hs:86:1)
   |
86 | liftDict Dict = Dict

Is there any way to make it work?

It's not clear to me why you define a class `Foo`. This induction is already the case, the `instance (MonadTrans t, MonadX m) => MonadX (t m)` is sufficient to define it for an arbitrary level of transformers. — Willem Van Onsem, Jan 25 '22 at 17:39
`Foo` is there to put it into `Dict`. Yes it is unnecesary with `ImpredicativeTypes` on. The inductive instance is enough when the concrete `MonadX` is know, the question really is how to express that `c` is inductive such that i can perform induction once i provide `MonadTrans` instance — Ryba, Jan 25 '22 at 17:49
It's especially hard to prove a theorem that is not true. Whether `MonadX` carries through a transformer is not a given, and depends on the structure of `MonadX`. E.g. `MonadWriter` does not carry through `ContT` (b/c `listen` if I remember right). Do do this, you will have to clarify for yourself what constitutes a proper `MonadX` class before trying to convince the compiler of anything. — luqui, Jan 25 '22 at 18:29
@luqui The code is parameterized by `c` (which stands for `MonadX` here). That addresses the fact that this "depends on the structure of `MonadX`". If `MonadX` does not lift through arbitrary monad transformers, then OP's code cannot be instantiated, but that's besides the question's point. — Li-yao Xia, Jan 25 '22 at 18:32
On top of that I think that any such inductive instance will have to be overlapping. — Ryba, Jan 25 '22 at 18:36
I think `Monad` should be `c`, but then we get a stack overflow and I don't know what's going on. — Li-yao Xia, Jan 25 '22 at 18:38
`c :: (* -> *) -> Constraint` so i don't know what do you mean? An argument of `c` should also be a `Monad`: `(c m, Monad m)` — Ryba, Jan 25 '22 at 18:43

Daniel Wagner · Accepted Answer · 2022-01-25T19:53:11.237

You get the exact same error with the slightly simpler definition of Foo c m given here:

 (c m, Monad m, forall t. MonadTrans t => c (t m))
                                      ^^^ don't really need Monad (t m) here

Let's clarify some of the variable names, so that it's clear which variables are definitely equal and which aren't when writing liftDict.

Have:

MonadTrans t
    forall m'. Monad m' => Monad (t m')
Foo c m
    c m
    Monad m
    forall t'. MonadTrans t' => c (t' m)

Want:

Foo c (t m)
    c (t m)
    Monad (t m)
    forall t''. MonadTrans t'' => c (t'' (t m))

In the "want" category, c (t m) is easy -- we apply forall t'. MonadTrans t' => c (t' m) to our t'~t and MonadTrans t. The Monad (t m) is easy, too, by applying forall m'. Monad m' => Monad (t m') to m'~m and Monad m.

But that last one... is tricky! You want these to line up:

Have: forall t' . MonadTrans t'  => c (t'  m    )
Want: forall t''. MonadTrans t'' => c (t'' (t m))

But they don't quite line up. What's happened here is that m is a fixed monad, not an argument that we can specialize to our new choice of t m! Okay, so let's make it an argument.

class    (c m, Monad m, forall m' t . (Monad m', MonadTrans t) => c (t m')) => Foo c m
instance (c m, Monad m, forall m' t . (Monad m', MonadTrans t) => c (t m')) => Foo c m

This compiles! But it no longer says what we wanted, because the inductive step we've said here doesn't demand a c constraint. Luckily, we can add that back in without causing it to stop compiling:

class    (c m, Monad m, forall m' t . (c m', Monad m', MonadTrans t) => c (t m')) => Foo c m
instance (c m, Monad m, forall m' t . (c m', Monad m', MonadTrans t) => c (t m')) => Foo c m

I think you might find it intuitive to group these constraints slightly differently:

class ( (c m, Monad m) -- base case
      , forall m' t. (c m', Monad m', MonadTrans t) => c (t m')
      -- inductive hypothesis
      ) => Foo c m

But beware: this Foo probably has fewer instances than you think at first. In particular, for there to be a Foo c instance, there can be only one, fully general, instance of c for type-level applications.

Instance inductivity as constraint

1 Answers1