# Rank-2-Types and the Scope

Hi!

i’m trying to understand rank-2-types and what a scope is. so i have started to play around with this type

``````data Foo u v = Foo u (u -> v)
``````

Now for example this fails with “Type Variable u has escaped its scope”:

``````foo :: forall a. a -> (forall u. Foo u a) -> a
foo a q@(Foo u f) = foo (f u) q
``````

In my naive world this should work because it is not necessary to know for the type-checker what `u` is inside the scope of `foo` - it is only used in the context of `f`.

anyway this can be done by moving some parts around and helping the type-checker understand that `u` really has nothing to do with `foo`

``````foo :: forall a. a -> (forall u. Foo u a) -> a
foo a q = foo (g q) q
where
g :: forall u. Foo u a -> a
g (Foo u f) = f u
``````

but this gets quite ugly when having something like `Array (forall u. Foo u a))` or `Maybe` etc. In this case using `map` will not work:

``````foo :: forall a. Array a -> (Array (forall u. Foo u a)) -> Array a
foo as qs = foo (g <\$> qs) qs
where
g :: forall u. Foo u a -> a
g (Foo u f) = f u
``````

where redefining `map` with `bind` is ok

``````foo :: forall a. Array a -> (Array (forall u. Foo u a)) -> Array a
foo as qs = foo (qs >>= (pure <<< g)) qs
where
g :: forall u. Foo u a -> a
g (Foo u f) = f u
``````

Somewhat this does not feel right.

Soooo, What is a scope? And what defines a scope? Especially the last example with the array seems odd - How to probably handle this case?

The issue with your first example pertains to where the `u` in `forall u. Foo u a` is being instantiated. The general intuition for `forall` is that you can think of it like a term-level lambda abstraction that takes a type as an argument. So in the case of `forall u. Foo u a`, this is intuitively a function from type `u` to `Foo u a`. Applying a type argument like this is called instantiation. In order to pattern match on `Foo u a` we must first instantiate it (apply a type argument), just like if you had `String -> Maybe Int` you would have to apply a `String` before you could pattern match on the `Maybe`. The `q` binder is binding to the instantiated `Foo`, and not the generalized `Foo`. Once it’s instantiated, it won’t typecheck as `forall u. Foo u a` just like `Maybe Int` won’t typecheck as `String -> Maybe Int`. When you pull it out into an intermediate `g`, the outer `q` is not being instantiated, so it will continue to typecheck. The confusion arises because these instantiations are implicit.

The issue with `Array (forall ...)` is that this is an impredicative type, which is an open research problem. There’s a whole host of literature on this, and even some new stuff. GHC is potentially getting something called “guarded” impredicativity which might help with cases like this.

Basically the compiler does not really attempt to deal with impredicativity. When and where to instantiate is kind of ambiguous. The workaround is to define a newtype, which gives the compiler clear boundaries for instantiation.

``````newtype GFoo a = GFoo (forall u. Foo u a)

-- No longer any impredicative types in this signature since
-- it's hidden under a constructor,
foo :: forall a. Array a -> Array (GFoo a) -> Array a
``````
4 Likes

The first example can be made clear by looking at what it desugars to:

``````foo :: forall a. a -> (forall u. Foo u a) -> a
foo a tmp = case tmp {- `u` is instantiated here -} of
q@(Foo u f) -> foo (f u) q
``````

So, you are binding `q` to the result of instantiating `tmp` with a fresh unknown. You can also manually write it as:

``````foo :: forall a. a -> (forall u. Foo u a) -> a
foo a q = case q of
Foo u f -> foo (f u) q
``````

Which works.