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

11 Jan 2018

      #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