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

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
6 messages Options
Reply | Threaded
Open this post in threaded view
|

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

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
           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: <http://ghc.haskell.org/trac/ghc/ticket/14662>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

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

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 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: <http://ghc.haskell.org/trac/ghc/ticket/14662#comment:1>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

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

GHC - devs mailing list
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: <http://ghc.haskell.org/trac/ghc/ticket/14662#comment:2>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

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

GHC - devs mailing list
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: <http://ghc.haskell.org/trac/ghc/ticket/14662#comment:3>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

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

GHC - devs mailing list
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:
                                     |  PartialTypeSignatures
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Changes (by simonpj):

 * keywords:   => PartialTypeSignatures


--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14662#comment:4>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

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

GHC - devs mailing list
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:
                                     |  PartialTypeSignatures
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 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)
 }}}

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14662#comment:5>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets