Linear functions lose their linearity annotation when wrapped in a monad

[andrevidela]

Steps to Reproduce

module MonadFun

-- introduce linear bind and linear pure
interface LMonad m where
  pure : (1 _ : a) -> m a
  (>>=) : (1 _ : m a) -> (1 _ : (1 _ : a) -> m b) -> m b

fail : LMonad m => (1 _ : m ((1 _ : a) -> b)) -> (1 _ : a) -> m b
fail ma a = MonadFun.do f <- ma
                        ?what_is_f
                        MonadFun.pure (f a)

Expected Behavior

Typechecks.

Observed Behavior

Does not typecheck. It fails with error

Error: While processing right hand side of fail. Trying to
use linear name a in non-linear context.

MonadFun.idr:19:42--19:43
    |
 19 |                         MonadFun.pure (f a)
    |

If we ask the type for hole what_is_f we get

 0 b : Type
 0 m : Type -> Type
 1 a : a
 1 ma : m ((1 _ : a) -> b)
 1 f : a -> b
------------------------------
hot : ?m ?a

Which indicates that f has lost its linearity annotation.

However, if we wrap each linear function in its own constructor everything works as expected

infixr 1 #->

data (#->) : Type -> Type -> Type where
  LFun : (1 f : (1 _ : a) -> b) -> a #-> b

fail : LMonad m => m (a #-> b) #-> a #-> m b
fail = LFun $ \ma => LFun $ \a => do (LFun f) <- ma
                                     ?what_is_f
                                     MonadFun.pure (f a)

Here, what_is_f reports f having type (1 _ : a) -> b correctly

[ohad]

I'm guessing inference kicks coercion into action, since (1 _ : a) -> b is a subtype of a -> b. I think this might be expected behaviour (see next comment), but I'll let someone else decide.
If this is blocking you, here's a fix:

fail ma x = (>>=) {a = (1 _ : a) -> b} ma \f => pure (f x)

[ohad]

One reason why inference does that might be because we don't have multiplicity polymorphism. So when we guess a type for f, unification somehow guesses its argument to have multiplicity any. But I haven't delved deep into do notation nor multiplicities so far.

[ohad]

In general, do notation struggles when the types get complicated. I think idris2 is slightly better than idris1, but it's not perfect.
One (syntactic) extension that could help it is type-ascription on the left of <-, so you could write the nicer looking:

fail ma x = MondFun.do (f : (1 _ : a) -> b) <- ma
                       pure (f x)

(As a general principle, any binder should allow type-ascription, but I appreciate this is fiddly to implement.)

[andrevidela]

This is not an artefact of do notation since it arises with >>= too

[KyleDavidE]

See #670

[ohad]

This is not an artefact of do notation since it arises with >>= too

It's harder to avoid in do because we don't have access to the implicit argument of the function.

[KyleDavidE]

The thing is we should not need to explicitly set the argument, this is a bug with how type inference handles linear types, linking back to general weirdness with linearity subtyping (see #73)

[edwinb]

This, along with a few other things, is making me think we should not have the multiplicity subtyping during unification, because it's really just guessing anyway. On the one hand, it would be a pity to remove it because it's very convenient in a lot of places, but on the other hand, it seems clear it's not the right way to do things. I think I've almost always regretted it eventually when I've tried to introduce some form of subtyping.

Removing subtyping at least won't affect my own main use for linearity, which is in resource tracking, but it will mean that some of the things we've been playing with on using linearity for performance will be less useful (e.g. using multiplicity annotations as a hint to a memory allocator) because setting the linearity of an argument will then restrict where a function can be used. I suppose we'll have to find another way to achieve that - multiplicity polymorphism is something we should explore anyway.

QTT is a new thing, so we're still exploring how best to use it. But we should still make sure that type checking is sound while we're exploring the new possibilities.

[gallais]

These days we get:

Error: While processing right hand side of fail. There are 0 uses of linear name (implicit) _. 

Issue758.idr:14:25--14:35
 10 |                        mb
 11 | 
 12 | fail : LMonad m => (1 _ : m ((1 _ : a) -> b)) -> (1 _ : a) -> m b
 13 | fail ma a = Issue758.do f <- ma
 14 |                         ?what_is_f
                              ^^^^^^^^^^

Which suggests to me that

do f <- ma
   ?what_is_f
   pure (f a)

gets desugared to

ma >>= \ f => ?what_is_f >>= \ _ => pure (f a)

but ideally we'd want (and it does indeed work)

ma >>= \ f => ?what_is_f >> pure (f a)

where we have cunningly defined:

(>>) : LMonad m => (1 _ : m ()) -> (1 _ : m a) -> m a
ma >> mb = ma >>= \ () => mb

It should not be too much work to change the way we desugar these do blocks to give
the same special treatment to (>>) that we give to (>>=).

[gallais]

The fix itself was very easy.

The refactoring tied to the choice to make (>>) insist that its first
argument should be m () on the other hand... On the bright side it does
bring better inference in some cases. :)