Eta expansion is required for higher rank types with constraints

[garyb]

This might already be known:

data Sequence t
  = Sequence (forall m a. (Monad m) => t (m a) -> m (t a))

-- This is fine
mkSequence :: forall t. (forall m a. (Monad m) => t (m a) -> m (t a)) -> Sequence t
mkSequence f = Sequence f

-- This is not:
mkSequence' :: forall t. (forall m a. (Monad m) => t (m a) -> m (t a)) -> Sequence t
mkSequence' = Sequence

Error in module Main:
Error in value declaration mkSequence':
Error checking that type
  forall t. (forall m a. (Prelude.Monad m) => t (m a) -> m (t a)) -> Main.Sequence t
subsumes type
  (forall m a. (Prelude.Monad m) => t1498 (m a) -> m (t1498 a)) -> Main.Sequence t1498
Error checking that type
  (forall m a. (Prelude.Monad m) => u1502 (m a) -> m (u1502 a)) -> Main.Sequence u1502
subsumes type
  (forall m a. (Prelude.Monad m) => t1498 (m a) -> m (t1498 a)) -> Main.Sequence t1498
Error checking that type
  forall m a. (Prelude.Monad m) => t1498 (m a) -> m (t1498 a)
subsumes type
  forall m a. (Prelude.Monad m) => u1502 (m a) -> m (u1502 a)
Error checking that type
  forall m. (Prelude.Monad m) => t1498 (m u1503) -> m (t1498 u1503)
subsumes type
  forall m a. (Prelude.Monad m) => u1502 (m a) -> m (u1502 a)
Error checking that type
  (Prelude.Monad u1504) => t1498 (u1504 u1503) -> u1504 (t1498 u1503)
subsumes type
  forall m a. (Prelude.Monad m) => u1502 (m a) -> m (u1502 a)
Error checking that type
  (Prelude.Monad u1504) => t1498 (u1504 u1503) -> u1504 (t1498 u1503)
subsumes type
  forall m. (Prelude.Monad m) => u1502 (m a1505) -> m (u1502 a1505)
Error checking that type
  (Prelude.Monad u1504) => t1498 (u1504 u1503) -> u1504 (t1498 u1503)
subsumes type
  (Prelude.Monad m1506) => u1502 (m1506 a1505) -> m1506 (u1502 a1505)
Error at examples\passing\SequenceDesugared.purs line 12, column 1 - line 12, column 15:
  Cannot unify constrained type
    (Prelude.Monad u1504) => t1498 (u1504 u1503) -> u1504 (t1498 u1503)
  with type
    (Prelude.Monad m1506) => u1502 (m1506 a1505) -> m1506 (u1502 a1505)

[paf31]

I did some more work on this, and I'm not sure there is an elegant solution. We could add a case to the unify function for when two instance heads are equal, but I'm not confident it would be a good idea. If we say that eta reduction is required whenever an irreducible term is checked against a rank-N function type, then I think that's a reasonable requirement. Think of it this way: in order to pass the dictionary around correctly, in the general case, we'd need to eta reduce in the typechecker anyway, and that's not really the job of the typechecker. The most term elaboration I'd like to do is dictionary insertion.

I think we should close this and work on eta reducing the dictionaries if we can.

[paf31]

Another option: we modify the subsumes function to bake eta reduction in, at the function rule:

If x at type c subsumes type a synthesizing term x'
and f x at type b subsumes type d synthesizing term y
then f at type a -> b subsumes type c -> d synthesizing term \x -> y

[garyb]

The latter option sounds good to me, are there any downsides to it?

My main reason for opening this is not that it's really all that bad, as there is a workaround at least, but it definitely seems like a wart. From the error message it is really not clear at all what is going on or that eta expansion would fix the error.

[paf31]

Moving to 0.9.

[paf31]

I don't think we can bake eta reduction into the subsumes rule actually. Notice that x is not mentioned in the conclusion in the suggested rule above. Also, it's not obvious how any elaboration on x would be propagated to f.

I would really like to avoid any sort of eta conversion in the elaborator actually. I'll think about how we might be able to fix this in the typing rules instead.