[GHC] #14662: Partial type signatures + mutual recursion = confusion

6 messages
Open this post in threaded view
|

[GHC] #14662: Partial type signatures + mutual recursion = confusion

 #14662: Partial type signatures + mutual recursion = confusion -------------------------------------+-------------------------------------            Reporter:  goldfire       |             Owner:  (none)                Type:  bug            |            Status:  new            Priority:  normal         |         Milestone:           Component:  Compiler       |           Version:  8.2.2            Keywords:                 |  Operating System:  Unknown/Multiple        Architecture:                 |   Type of failure:  None/Unknown   Unknown/Multiple                   |           Test Case:                 |        Blocked By:            Blocking:                 |   Related Tickets: Differential Rev(s):                 |         Wiki Page: -------------------------------------+-------------------------------------  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. -- Ticket URL: GHC The Glasgow Haskell Compiler _______________________________________________ ghc-tickets mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Open this post in threaded view
|

Re: [GHC] #14662: Partial type signatures + mutual recursion = confusion

 #14662: Partial type signatures + mutual recursion = confusion -------------------------------------+-------------------------------------         Reporter:  goldfire          |                Owner:  (none)             Type:  bug               |               Status:  new         Priority:  normal            |            Milestone:        Component:  Compiler          |              Version:  8.2.2       Resolution:                    |             Keywords: Operating System:  Unknown/Multiple  |         Architecture:                                      |  Unknown/Multiple  Type of failure:  None/Unknown      |            Test Case:       Blocked By:                    |             Blocking:  Related Tickets:                    |  Differential Rev(s):        Wiki Page:                    | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: GHC The Glasgow Haskell Compiler _______________________________________________ ghc-tickets mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Open this post in threaded view
|

Re: [GHC] #14662: Partial type signatures + mutual recursion = confusion

 In reply to this post by GHC - devs mailing list #14662: Partial type signatures + mutual recursion = confusion -------------------------------------+-------------------------------------         Reporter:  goldfire          |                Owner:  (none)             Type:  bug               |               Status:  new         Priority:  normal            |            Milestone:        Component:  Compiler          |              Version:  8.2.2       Resolution:                    |             Keywords: Operating System:  Unknown/Multiple  |         Architecture:                                      |  Unknown/Multiple  Type of failure:  None/Unknown      |            Test Case:       Blocked By:                    |             Blocking:  Related Tickets:                    |  Differential Rev(s):        Wiki Page:                    | -------------------------------------+------------------------------------- Comment (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 `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. -- Ticket URL: GHC The Glasgow Haskell Compiler _______________________________________________ ghc-tickets mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Open this post in threaded view
|

Re: [GHC] #14662: Partial type signatures + mutual recursion = confusion

 In reply to this post by GHC - devs mailing list #14662: Partial type signatures + mutual recursion = confusion -------------------------------------+-------------------------------------         Reporter:  goldfire          |                Owner:  (none)             Type:  bug               |               Status:  new         Priority:  normal            |            Milestone:        Component:  Compiler          |              Version:  8.2.2       Resolution:                    |             Keywords: Operating System:  Unknown/Multiple  |         Architecture:                                      |  Unknown/Multiple  Type of failure:  None/Unknown      |            Test Case:       Blocked By:                    |             Blocking:  Related Tickets:                    |  Differential Rev(s):        Wiki Page:                    | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: GHC The Glasgow Haskell Compiler _______________________________________________ ghc-tickets mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets