[Feature Request] Visible Forall

The Dependent Haskell Proposal mentions a dependent visible irrelevant quantifier: forall (...) ->. Now that we've got visible type application, thanks to Richard's tremendous efforts, I think we're pretty close to getting this quantifier (but surely I might be mistaken).

What worries me is the following line in the proposal:

One proposal is that @ would serve double-duty: it would override invisibility and also indicate a type argument. If this is the case, the forall (...) -> form would be essentially useless, as it would still require users to use @ to indicate parsing. Thus, forall (...) -> seems strictly worse than forall (...) .

The way I see it, forall (...) -> is not useless. It's actually essential if we want to get rid of Proxy (which I hope everyone agrees is a bit of a hack). Let me describe my use case to make it clear what I mean.

Ether is a library that defines tagged monad transformers and classes. Tags allow you to have multiple occurences of the same effect in your monad transformer stack, like multiple MonadStates or multiple MonadReaders. I don't want to steal your time so I won't go much in-depth. It should be enough to mention that tags are simply data types (possibly uninhabited) and they're passed via proxies. So instead of writing ask to get your MonadReader environment you write Ether.ask (Proxy :: Proxy MyTag) where MyTag is a tag indicating which environment you want (remember that now you can have more than one).

This all actually works quite nicely but proxies are ugly. I thought that I could get rid of them as soon as we get visible type application so the user can write Ether.ask @MyTag. Turns out it's not that simple.

Consider the type of Ether.ask :: forall tag r m . MonadReader tag r m => Proxy tag -> m r. To find an instance for MonadReader tag r m, we need the to know what the tag is. We use Proxy to specify it.

A naïve attempt to get rid of Proxy is to simply remove the argument, since the tag can now be specified using visible type application. The type becomes Ether.ask :: forall tag r m . MonadReader tag r m => m r. Unfortunately, this fails with an error:

src/Control/Monad/Ether/Reader/Class.hs:1:1: error:
    solveWanteds: too many iterations (limit = 4)
      Unsolved: WC {wc_simple =
                      [D] _ :: MonadReader tag r ((->) (r_a8gV -> r)) (CDictCan)
                      [W] $dMonadReader_a8gX :: MonadReader
                                                  tag_a8gU
                                                  r_a8gV
                                                  ((->) (a_a8h8 -> a_a8h8)) (CDictCan)
                      [W] hole{a8ki} :: m ~ (->) (r_a8gV -> r) (CNonCanonical)
                      [D] _ :: Monad ((->) (r_a8gV -> r)) (CDictCan)
                      [D] _ :: Applicative ((->) (r_a8gV -> r)) (CDictCan)
                      [D] _ :: Functor ((->) (r_a8gV -> r)) (CDictCan)}
      New superclasses found
      Set limit with -fconstraint-solver-iterations=n; n=0 for no limit

Increasing iterations limit makes no difference. I think I can understand why that happens. There's nothing in the type signature to specify what tag is, so the dictionary for MonadReader can't be found. We need to promise to the compiler that tag will be specified at call site. I believe this is where forall (...) -> comes into play. The type of Ether.ask should be forall tag -> forall r m . MonadReader tag r m => m r. This type signature is morally equivalent to the one with Proxy, so I'd expect that to work.

Thoughts?

goldfirere / ghc

[Feature Request] Visible Forall #67