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 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) with GHC's use of SigTvs for partial type signatures. I don't have a better suggestion, but SigTvs never make me feel good.

Change History (5)

comment:1 Changed 23 months ago by simonpj

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 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 the SigTvs. (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

f :: forall a. _ -> a
f =  ...f @Int...f @Bool.....

That wildcard might end up being a! If it did, then would the recursive occurrences get instantiate to Int->Int and Bool->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.

comment:2 Changed 23 months ago by goldfire

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 SigTvs" rule for partial type signatures only works at the outermost level; nested foralls don't benefit.)

The reason I dislike SigTvs 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 in reply to:  description Changed 23 months ago by goldfire

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 simonpj

Keywords: PartialTypeSignatures added

comment:5 Changed 18 months ago by mnislaih

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)
Note: See TracTickets for help on using tickets.