bringing functions into scope makes code to not compile

user_9271266 0
Viewed 74

Consider the following snipet

-- This compiles
import Control.Monad

v :: Monad m => m b
v = undefined

w :: Monad m => m c
w = undefined

h :: Monad m => a -> m c
h = v' >=> w'
 where v' :: Monad m1 => a -> m1 b
       v' = const v
       w' :: Monad m2 => b -> m2 c
       w' = const w

It compiles fine and is able to solve m ~ m1 ~ m2, but if we bring v and w into h scope, then it wont compile any more: Couldn't match type `m1' with `m'

-- This doesn't compiles but looks equivalent to h

h' :: Monad m => m b -> m c -> a -> m c
h' v w = v' >=> w'
  where v' :: Monad m1 => a -> m1 b
        v' = const v
        w' :: Monad m2 => b -> m2 c
        w' = const w

I would think that both h and h' are equivalent when type resolution comes into play, since not in h nor h' assumptions over m are made. But it turns out that h' needs the help of ScopedTypeVariables to specify the m ~ m1 ~ m2

I seems weird that GHC does not complain in the h but is does in h'. Why ScopedTypeVariables is needed to compile h' but it isn't to compile h?

For the record

Just in case you wonder this is the version of h' which compiles. But notice the question is why ScopedTypeVariables is not needed to compile h? instead of why ScopedTypeVariables is needed to compile h'?

{-# LANGUAGE ScopedTypeVariables #-}
h' :: forall m a b c. Monad m => m b -> m c -> a -> m c
h' v w = v' >=> w'
  where v' :: Monad m => a -> m b
        v' = const v
        w' :: Monad m => b -> m c
        w' = const w
haskell
2 Answers
{-# LANGUAGE ScopedTypeVariables, TypeFamilies, RankNTypes, UnicodeSyntax #-}

Remember that signatures with type variables (which don't come from an enclosing scope) are implicitly universally quantified. I.e. your first example is

v :: ∀ m b . Monad m => m b
v = undefined

w :: ∀ m c . Monad m => m c
w = undefined

h :: ∀ m a c . Monad m => a -> m c
h = v' >=> w'
 where v' :: ∀ m₁ b . Monad m₁ => a -> m₁ b
       v' = const v
       w' :: ∀ m₂ b c . Monad m₂ => b -> m₂ c
       w' = const w

Let's do some α-renaming here to make it all match up, which you can always do with universally-quantified bindings: (the compiler does this under the hood in the above example)

v :: ∀ m₁ b . Monad m₁ => m₁ b
v = undefined

w :: ∀ m₂ c . Monad m₂ => m₂ c
w = undefined

h :: ∀ m a ζ . Monad m => a -> m ζ
h = v' >=> w'
 where v' :: ∀ m₁ b . Monad m₁ => a -> m₁ b
       v' = const v
       w' :: ∀ m₂ b c . Monad m₂ => b -> m₂ c
       w' = const w

However, in your second example, the types of v and w are not universally quantified. Instead, they have m rigid from the signature of h'. Thus you can't then use them in a local definition that is quantified universally. You would have to constrain it back to be equal to the outer m, but that would defeat the point of quantifying in the first place.

h' :: ∀ m a b c . Monad m => m b -> m c -> a -> m c
h' v w = v' >=> w'
  where v' :: ∀ m₁ . (Monad m₁, m₁~m) => a -> m₁ b
        v' = const v
        w' :: ∀ m₂ . (Monad m₂, m₂~m) => b -> m₂ c
        w' = const w

(Here, the Monad m₁ / Monad m₂ constraints are redundant, because we already know Monad m at that spot.)

What you want instead is v and w to be universally quantified, as they are in the first example. This makes the type of h' a rank-2 type:

h' :: ∀ m a b c . Monad m
       => (∀ m₁ . Monad m₁ => m₁ b) -> (∀ m₂ . Monad m₂ => m₂ c) -> a -> m c
h' v w = v' >=> w'
  where v' :: ∀ m₁ . Monad m₁ => a -> m₁ b
        v' = const v
        w' :: ∀ m₂ . Monad m₂ => b -> m₂ c
        w' = const w
user_7459030

ScopedTypeVariables is not needed in the first case because the where definitions happen to be general enough.

I will clarify this point by inserting explicit type arguments @T, using TypeApplications.

Your first example actually means:

v :: forall m b. Monad m => m b
v = undefined

w :: forall m c. Monad m => m c
w = undefined

Note how v and w above expect two type arguments each. That is, we have to use them as in v @M @B :: M B (or let the compiuler infer the type arguments, of course).

Then h compiles because we can infer the correct type arguments. Again, I'll insert explicit foralls to make it clear:

h :: forall m a c. Monad m => a -> m c
h = (v' @m @a @T ) >=> (w' @m @T @c)
 where v' :: forall m1 a b. Monad m1 => a -> m1 b
       v' = const (v @m1 @b)
       w' :: forall m2 b c. Monad m2 => b -> m2 c
       w' = const (w @m2 @c)

where @T can be any arbitrary type. Indeed, GHC chooses GHC.Types.Any for that.

By comparison, your h' does not compile

h' :: Monad m => m b -> m c -> a -> m c
h' v w = v' >=> w'
  where v' :: Monad m1 => a1 -> m1 b1
        v' = const v
        w' :: Monad m2 => b2 -> m2 c2
        w' = const w

because here v is not a polymorphic value, we can't write v @m1 @b since v does not take any type arguments. We can only use v :: m b where m and b are type arguments for h', but we would need something of type m1 b1, where m1 and b1 are type arguments for v'.

user_32349590
Related