[GHC] #16146: Trivial partial type signature kills type inference in the presence of GADTs

[GHC]

#16146: Trivial partial type signature kills type inference in the presence of
GADTs
-------------------------------------+-------------------------------------
        Reporter:  goldfire          |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.6.3
      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):

 Quite right in comment:6. We can't possibly instantiate a partial type. So
 then I got to thinking that we would check the ascribed expression first,
 followed by the subtype check (presumably after the partial type is no
 longer partial). But we should ''already'' be doing that. So I dived
 deeper, and I found more interesting things.

 We have, as before

 {{{#!hs
 data G a where
   G1 :: G Char
   G2 :: G Bool
 }}}

 I wish for this to be accepted:

 {{{#!hs
 foo :: forall a. G a -> a
 foo x = ((case x of
   G1 -> 'z'
   G2 -> True) :: _)
 }}}

 Why is it rejected today? It's not just that the wildcard is untouchable
 in the context of the GADT pattern-match. Here's what happens: we invent a
 new metavariable `_w` to stand for the wildcard. This `_w` is untouchable
 in the GADT pattern match, so we don't learn anything about it. Then,
 critically, we try to ''generalize'' the signature. This takes the
 unsolved metavariable `_w` and ''skolemizes'' it. So, later, when the
 subtype-checker tries to unify `_w` with the type variable `a`, it fails,
 as `_w` is a skolem.

 This behavior isn't entirely unreasonable. But note that I never asked for
 generalization. Contrast with the fact that (if I say `default ()`), GHC
 rejects

 {{{#!hs
 wurble :: _
 wurble x = x + 1
 }}}

 This is rejected because my partial type signature did not allow for any
 constraints (I need `Num a => a -> a`): GHC does not allow `_` to stand
 for `_ => _`. Yet GHC ''does'' allow `_` to stand for `forall a. a -> a`:
 changing `wurble` to be `wurble x = x` works just fine. This seems like
 inconsistent design, to me.

 So, I wonder if we should allow generalization in wildcards only by user
 request, with something like `forall _. _`, just like we do so currently
 for constraints. We could also have `forall a b c _ . ...`, just like we
 now can have an extra-constraints wildcard. (The `_` in `forall a b c _`
 isn't really a wildcard, but a request for generalization.) I'm not sure
 how implementable this is, but it's a decent thought experiment.

 Of course, the idea that "wildcards should not be generalized" reminded me
 of something else that should not be generalized: lets. And indeed we see
 some strange behavior around `let` and GADT inference. This isn't related
 to partial type signatures, but it's a bit more grist for the mill.
 Consider this:

 {{{#!hs
 bar :: G a -> a
 bar z = quux z
   where
     quux x = case x of
       G1 -> 'b'
       G2 -> True
 }}}

 This is rejected. `quux` is checked just like it were at top level, and we
 can't figure out its type. This is true even though bidirectional type-
 checking tells us that the type of `quux` should be `G a -> a`.

 However, earlier I argued that the problem is ''generalization''. So,
 let's suppress that urge of GHC's:

 {{{#!hs
 bar2 :: G a -> a
 bar2 z = quux2 z
   where
     quux2 x = case x of
       G1 -> const 'b' z
       G2 -> True
 }}}

 This is accepted! In the case-match for `G1`, I have an entirely-
 irrelevant use of the outer variable `z`. According to the rules for let-
 should-not-be-generalized, the appearance of a variable from an outer
 scope disables generalization. And so `quux2` is not generalized, meaning
 that its type still contains proper metavariables when we check that
 `quux2 z` has type `a`, and then GHC can infer the correct type.

 Relating back to partial type signatures, now we try

 {{{#!hs
 bar3 :: G a -> a
 bar3 z = quux3 z
   where
     quux3 :: _
     quux3 x = case x of
       G1 -> const 'b' z
       G2 -> True
 }}}

 The only change here is the partial type signature. Because GHC does not
 respect let-should-not-be-generalized in the presence of partial type
 signatures, this is rejected again.

 Bottom line: it's nice to have finer control over generalization. The work
 on let-should-not-be-generalized supposed that a good heuristic for when
 to stop generalization was the presence of a variable from an outer scope.
 This has indeed served us well, and I don't propose changing it. But it
 might be nice to give users a way to control this behavior more directly.
 Having a partial type signature `xyz :: _` might be a signal saying not to
 generalize something that ordinarily would (helpful in my `quux` example)
 and having a partial type signature `xyz :: forall _. _` might a signal
 saying to generalize something that ordinarily wouldn't. This is useful:
 See Section 10.2 of my (as-yet-unpublished)
 [https://cs.brynmawr.edu/~rae/papers/2018/stitch/stitch.pdf Stitch paper].
 (That section mentions 2 places where generalization is good.
 Interestingly, GHC has already adapted to the first point. The second
 point is of interest here, where I brutally just specified
 `-XNoMonoLocalBinds` in order to get generalization.)

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