`a`

with a ( `forall t`

).
Impredicative in Coq means having `(Type : Type)`

.
- polymorphic types:

```
forall p. [p] -> [p] -- LEGAL
Int -> (forall p. [p] -> [p]) -- ILLEGAL
(forall p. [p] -> [p]) -> Int -- ILLEGAL
[forall a. a -> a] -- ILLEGAL
```

- Higher rank types:
`forall`

at the outermost level of a let-bound function, and to the left and right of arrows!

```
Int -> (forall p. [p] -> [p]) -- LEGAL
(forall p. [p] -> [p]) -> Int -- LEGAL
runST :: (forall s. ST s a) -> a -- LEGAL
[forall a. a -> a] -- ILLEGAL
```

- Impredicative type:

```
[forall a. a -> a]
```

- We can't type
`runST`

because of impredicativity:

```
($) :: forall a, forall b, (a -> b) -> a -> b
runST :: forall a, (forall s, ST s a) -> a -- LEGAL
st :: forall s. ST s Int
runST st -- YES
runST $ st -- NO
```

- Expanding out the example:

```
($) runST st
($) @ (forall s. ST s Int) @Int (runST @ Int) st
```

- Data structures of higher kinded things. For example. we might want to have
`[∀ a, a -> a]`

- We have
`ids :: [∀ a, a -> a]`

. I also have the function`id :: ∀ a, a -> a`

. I want to build`ids' = (:) id ids`

. That is, I want to cons an`id`

onto my list`ids`

. - How do we type infer this?

```
reverse :: ∀ a. [a] -> [a]
and :: [Bool] -> Bool
foo = \xs -> (reverse xs, and xs)
```

- Start with
`xs :: α`

where`α`

is a type variable. - Typecheck
`reverse xs`

. We need to instantiate`reverse`

. With what type?*that's what we need to figure out!* - (1) Instantiate: Use variable
`β`

. So we have that our occurence of`reverse`

has type`reverse :: [β] -> [β]`

. - (2) Constrain: We know that
`xs :: α`

and`reverse`

expects an input argument of type`[β]`

, so we set`α ~ [β]`

due to the call`reverse xs`

. - We now need to do
`and xs`

. (1)`and`

doesn't have any type variables, so we don't need to perform instantiation. (2) We can constrain the type, because`and :: [Bool] -> Bool`

, we can infer from`and xs`

that`α ~ [Bool]`

- We solve using
. We get*Robinson unification*`[β] ~ α ~ [Bool]`

or`β = Bool`

- The above works because
`α`

and`Β`

only stand for.*monotypes* - Our constraints are
, which can be solved by*equality constraints**Robinson unification* - And we have only
(principal solution)*one solution* - When trying to instantiate reverse, how do we instantiate it?
- Constraints become subsumption constraints
- Solving is harder
- No principal solution
- Consider
`incs :: [Int -> Int]`

, and`(:) id incs`

versus`(:) id ids`

.

- We want to infer
`(:) id ids`

- We know that the second argument
`ids`

had type`[∀ a, a -> a]`

- we need a type
`[p]`

for the second argument, because`(:) :: p -> [p] -> [p]`

- Thus we must have
`p ~ (∀ a, a -> a)`

- We got this information
*from the second argument* - So let's try to treat an application
`(f e1 e2 ... en)`

as a whole.

- Assume we want to figure out
`filter g ids`

. - start with
`filter :: ∀ p, (p -> Bool) -> [p] -> Bool`

- Instatiate
`filter`

with*instantiation variables*`κ`

to get`(κ -> Bool) -> [κ] -> Bool`

- Take a "quick look" at
`e1, e2`

to see if we know that`κ`

should be - We get from
`filter g ids`

that`κ := (∀ a, a -> a)`

. - Substitute for
`κ`

(1) the type that "quick look" learnt, if any, and (2) Aunification variable otherwise.*monomorphic* - Typecheck against the type. In this case, we learnt that
`κ := (∀ a, a -> a)`

, so we replace`κ`

with`(∀ a, a -> a)`

. - Note that this happens at each
!*call site*

- instantate function with unficiation variables, with the idea.
- instantiate function with a quick look at the calling context.
- We don't need fully saturated calls. We take a look at whatever we can see!
- Everything else is completely unchanged.