In the original code one can see that I'm just extracting an expression into a binding which is one of the basic things that haskell claims should be always possible.
Minimal case (created with the help of @dminuoso on freenode)
I'd like g to remain polymorphic (so that I can feed it to other functions that expect it to be):
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
main = do
let a :: forall t. Functor t => t () = undefined
let g :: forall u. Functor u => u () = a
pure ()
error:
source_file.hs:6:44:
Couldn't match expected type ‘forall (u :: * -> *).
Functor u =>
u ()’
with actual type ‘t0 ()’
When checking that: t0 ()
is more polymorphic than: forall (u :: * -> *). Functor u => u ()
In the expression: a
Original question (motivation) posted on #haskell IRC:
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
class Monad m => Monad' m where
instance Monad' IO where
f1 :: (forall m . Monad' m => m Int) -> IO Int
f1 g = do
let a :: forall n . Monad' n => n Int = g
a
-- this works
--f1 :: (forall m . Monad' m => m Int) -> IO Int
--f1 g = do
-- g
main = print $ "Hello, world!"
but I get:
source_file.hs:12:45:
Couldn't match expected type ‘forall (n :: * -> *).
Monad' n =>
n Int’
with actual type ‘m0 Int’
When checking that: m0 Int
is more polymorphic than: forall (n :: * -> *). Monad' n => n Int
In the expression: g
Based on https://ghc.haskell.org/trac/ghc/ticket/12587 I tried to explicitly apply the type to help the type-checker:
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
class Monad m => Monad' m where
instance Monad' IO where
f1 :: (forall m . Monad' m => m Int) -> IO Int
f1 g = do
let a :: forall n . Monad' n => n Int = g @n
a
main = print $ "Hello, world!"
but then I get:
main.hs:13:48: error: Not in scope: type variable ‘n’
What happens when you write
a :: forall f. Functor f => f ()
a = _
? Specifically, what type of expression is GHC looking for to fill the hole (_)? You might think it's looking for a forall f. Functor f => f (), but that's not quite right. Instead, a is actually a bit more like a function, and GHC implicitly inserts two arguments: one type argument named f with kind * -> *, and one instance of the constraint Functor f (which is unnamed, like all instances).
a :: forall f. Functor f => f ()
a @f {Functor f} = _
-- @-syntax is a currently proposed extension, {}-syntax is fake
GHC is looking for, in the context of type f :: * -> *; instance Functor f, a f (). This is the same difference as between looking for a (A -> B) -> C -> D and looking for a D in the context of f :: A -> B; c :: C. If I directly have solution :: (A -> B) -> C -> D, in the first case I can just write solution, but, in the second case, I must write out solution f c.
This is not what happens when you write
a :: forall f. Functor f => f () = _
Because you've used a pattern type signature, not a normal one, GHC no longer implicitly binds the type variable and the instance for you. GHC now, honestly and truly, wants you to fill that _ with a forall f. Functor f => f (). This is hard, as we'll see soon...
(I really don't think the thing Daniel Wagner has quoted is relevant here. I believe it's just referring to the difference (when ScopedTypeVariables is on and type a is not in scope) between the way that 5 :: Num a => a implicitly means 5 :: forall a. Num a => a and the way g :: a -> a = id doesn't mean g :: forall a. a -> a = id.)
What happens when you write
undefined
? Specifically, what is its type? You might think it's forall a. a, but that's not quite right. Yes, it's true that, all by itself, undefined has the type forall a. a, but GHC doesn't let you write undefined all by itself. Instead, every occurrence of undefined in an expression is always applied to a type argument. The above is implicitly rewritten to
undefined @_a0
and a new unification variable (which doesn't really have a name) _a0 is created. This expression has type _a0. If I use this expression in a context that requires an Int, then _a0 must be equal to Int, and GHC sets _a0 := Int, rewriting the expression to
undefined @Int
(Because _a0 can be set to something, it's called a unification variable. It's under "our", internal control. Above, f couldn't be set to anything. It's a given, and its under "their" (the user's), external control, which makes it a skolem variable.)
Usually, the automatic binding of type variables and the automatic application of unification variables works well. E.g., both of these work out fine:
undefined :: forall a. a
bot :: forall a. a
bot = undefined
Because they respectively expand as
(\@a -> undefined @a) :: forall a. a
bot :: forall a. a
bot @a = undefined @a
When you do
a :: forall f. Functor f => f () = undefined
, you make something very strange happen. As I said before, a pattern type signature with a forall doesn't introduce anything. The undefined on the RHS actually needs to be a forall f. Functor f => f (). The implicit application of unification variables still occurs:
a :: forall f. Functor f => f () = undefined @_a0
undefined @_a0 :: _a0, so _a0 ~ (forall f. Functor f => f ()) must hold. GHC thus has to set _a0 := (forall f. Functor f => f ()). Usually, this is a no-no, because this is impredicative polymorphism: setting a type variable to a type containing foralls. However, in sufficiently outdated GHCs, this is allowed for certain functions. That is, undefined is not defined with the type forall (a :: *). a, but forall (a :: OpenKind). a, where OpenKind allows for this impredicativity. That means your code goes through as
a :: forall f. Functor f => f () = undefined @(forall f. Functor f => f ())
If you write
a :: forall f. Functor f => f () = bot
, it won't work, as bot doesn't have the same magic sauce that undefined has. Additionally, this won't work in more recent GHCs, which have stamped out this weird kind of impredicative polymorphism. (Which I say is a very good thing).
Your definition of a, even with the pattern signature, does indeed come out with the desired type forall f. Functor f => f (). The issue is now in g:
g :: forall f. Functor f => f () = a
g, again, doesn't bind type f :: * -> * or instance Functor f. Meanwhile, a gets applied to some implicit stuff:
g :: forall f. Functor f => f () = a @_f0 {_}
But... the RHS now has type _f0 (), and the LHS wants it to have type forall f. Functor f => f (). These don't look alike. Therefore, type error.
As you can't stop the implicit application of a to a type variable and just write g = a, you must instead allow the implicit binding of type variables in g:
g :: forall f. Functor f => f ()
g = a
This works.