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 |