Opened 23 months ago
Last modified 18 months ago
#14662 new bug
Partial type signatures + mutual recursion = confusion
Reported by: | goldfire | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | |
Component: | Compiler | Version: | 8.2.2 |
Keywords: | PartialTypeSignatures | Cc: | |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | None/Unknown | Test Case: | |
Blocked By: | Blocking: | ||
Related Tickets: | Differential Rev(s): | ||
Wiki Page: |
Description
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) 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.
Change History (5)
comment:1 Changed 23 months ago by
comment:2 Changed 23 months ago by
OK. I see why polymorphic recursion is no good. But then can you explain Example 6? That's polymorphically recursive and is accepted. (It's accepted because the "use SigTv
s" rule for partial type signatures only works at the outermost level; nested forall
s don't benefit.)
The reason I dislike SigTv
s is this: When a user writes down a type variable, do they mean it to be unique (skolem) with a unique binding site, or could it stand for something else (a TauTv
)? We generally choose the former, but wildcards are the latter. These positions are all good. But a SigTv
is something in between: it's a type variable that can stand only for another type variable. Does it have a binding site? If yes, then what if we discover that it stands for something else? If no, then why do we say forall a
to introduce them (in the case of partial type signatures)? The whole thing seems very squishy to me.
I do understand why they came into being, and I agree that they solve real problems. But I think you'd have a hard time of writing a declarative specification of type inference that involves them.
comment:3 Changed 23 months ago by
Interestingly, this was changed three days ago.
Now, in HEAD, Example 3 and Example 4 are rejected with
• Can't quantify over ‘b’ bound by the partial type signature: g :: forall b. _ -> b -> b
I think this is an improvement in behavior, but it underscores how squishy this all is.
comment:4 Changed 20 months ago by
Keywords: | PartialTypeSignatures added |
---|
comment:5 Changed 18 months ago by
How about polymorphic recursion with a type wildcard only in the constraint ?
The minimal failing example I have is:
data App a where Pure :: a -> App a App :: App (a -> b) -> App a -> App b f :: _ => App a -> Maybe a f (App a b) = f a <*> f b f (Pure x) = pure x f _ = Nothing
Fails in 8.2.x and 8.4.2 with:
• Occurs check: cannot construct the infinite type: a ~ a1 -> a Expected type: App a Actual type: App (a1 -> a) • In the first argument of ‘f’, namely ‘a’ In the first argument of ‘(<*>)’, namely ‘f a’ In the expression: f a <*> f b • Relevant bindings include b :: App a1 (bound at /Users/pepe/scratch/debug/.stack-work/intero/intero19866fqh-TEMP.hs:13:10) a :: App (a1 -> a) (bound at /Users/pepe/scratch/debug/.stack-work/intero/intero19866fqh-TEMP.hs:13:8) f :: App a -> Maybe a (bound at /Users/pepe/scratch/debug/.stack-work/intero/intero19866fqh-TEMP.hs:13:1) (intero)
I recommend caution. Partial type signatures were implemented fairly quickly by a PhD student some time ago, but I have spent many hours since slowly fixing bugs in the implementation. It's much trickier than I supposed at first. (So I'm not blaming him! And its a very nice feature.)
Here's a core principle: partial type signatures go entirely via the
InferGen
plan: that is, we use only monomorphic rcursion exactly as if there was no signature. All the signature does is to impose a partial shape on the type of the RHS, including restricting some parts of that type to type variables -- hence theSigTvs
. (I don't share your dislike;SigTvs
are very nice actually.)Yes, you could imagine some kind of partial polymorphic recursion, but I don't think it makes sense. Eg
That wildcard might end up being
a
! If it did, then would the recursive occurrences get instantiate toInt->Int
andBool->Bool
. Certainly not.This way lies madness. The current implementation is quite complicated enough.
I agree that documentation is lacking: no, polymorphic recursion is absolutely not available for functions with a partial type signature.