## Partial type signatures + mutual recursion = confusion

I'm trying to understand better how partial type signatures interact with mutual recursion. This is all in 8.4.1-alpha1.

Example 1:

```
f :: forall a. _ -> a -> a
f _ x = g True x
g :: forall b. _ -> b -> b
g _ x = f 'x' x
```

This works -- no problem.

Example 2:

```
f :: forall a. _ -> a -> a
f _ x = snd (g True 'a', x)
g :: forall b. _ -> b -> b
g _ x = f 'x' x
```

This fails, explaining that GHC inferred `g :: Bool -> a -> a`

and that `a`

doesn't match `Char`

(in the second argument of the call site in the body of `f`

). This is unsatisfactory because clearly `g`

should be *instantiated* at `Char`

. The manual does say that polymorphic recursion isn't available with partial type signatures, and I suppose this is an example of polymorphic (mutual) recursion.

Example 3:

```
f :: forall a. _ -> a -> a
f _ x = snd (g True 'a', x)
where
g :: forall b. _ -> b -> b
g _ y = f 'x' y
```

This is accepted. This is the same example as the last one, but now `g`

is local. It does not capture any variables (including type variables) from `f`

, so it seems to me that it should be equivalent to Example 2. But somehow GHC is clever enough to accept.

Example 4:

```
thdOf3 (_, _, c) = c
f :: forall a. _ -> a -> a
f _ x = thdOf3 (g True 'a', g False 5, x)
where
g :: forall b. _ -> b -> b
g _ y = f 'x' y
```

This works, too. Note that `g`

is applied at several different types, so it really is being generalized.

Example 5:

```
f :: Int -> forall a. _ -> a -> a
f n _ x = snd (g n True 'a', x)
g :: Int -> forall b. _ -> b -> b
g n _ x = f n 'x' x
```

This is accepted. This is the same as Example 2, but each function now takes an `Int`

, which is simply passed back and forth. Evidently, when you write the type non-prenex, polymorphic recursion is OK.

Example 6:

```
f :: Int -> forall a. _ -> a -> a
f n _ x = snd (f n True 'x', x)
```

This is accepted, even though it's blatantly using polymorphic recursion.

Example 7:

```
f :: forall a. _ -> a -> a
f _ x = snd (f True 'x', x)
```

This is rejected as polymorphically recursive.

Something is fishy here. It's not the explicit prenex `forall`

s -- leaving those out doesn't change the behavior. I guess my big question is this:

- If the user quantifies a partial type signature (either by using
`forall`

, or just using an out-of-scope type variable and using Haskell's implicit quantification), why can't we use polymorphic recursion with that variable? I understand why we can't use polymorphic recursion with wildcards.

A little background for context: I'm struggling (in my work on #14066 (closed)) with GHC's use of `SigTv`

s for partial type signatures. I don't have a better suggestion, but `SigTv`

s never make me feel good.

## Trac metadata

Trac field | Value |
---|---|

Version | 8.2.2 |

Type | Bug |

TypeOfFailure | OtherFailure |

Priority | normal |

Resolution | Unresolved |

Component | Compiler |

Test case | |

Differential revisions | |

BlockedBy | |

Related | |

Blocking | |

CC | |

Operating system | |

Architecture |