Partial type signatures + mutual recursion = confusion (#14662) · Issues · Glasgow Haskell Compiler / GHC

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 foralls -- 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 SigTvs for partial type signatures. I don't have a better suggestion, but SigTvs 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

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

Example 1:

```hs
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:

```hs
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:

```hs
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:

```hs
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:

```hs
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:

```hs
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:

```hs
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) 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.

<details><summary>Trac metadata</summary>

| 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           |              |

</details>