id summary reporter owner description type status priority milestone component version resolution keywords cc os architecture failure testcase blockedby blocking related differential wikipage
14662 Partial type signatures + mutual recursion = confusion goldfire "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." bug new normal Compiler 8.2.2 PartialTypeSignatures Unknown/Multiple Unknown/Multiple None/Unknown