[GHC] #12190: Generalize irrefutable patterns (static semantics like let-bindings)

[GHC]

#12190: Generalize irrefutable patterns (static semantics like let-bindings)
-------------------------------------+-------------------------------------
           Reporter:  ezyang         |             Owner:
               Type:  feature        |            Status:  new
  request                            |
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.0.1
  (Type checker)                     |
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  GHC rejects
  Unknown/Multiple                   |  valid program
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 tl;dr It is not let-bindings that should be generalized, it is
 **irrefutable** patterns that should be generalized.

 I know GHC's trend has been to reduce the amount of let-generalization we
 do (since it interacts poorly with GADTs).  However, I was recently
 working with some useful rank-2 definitions, and found that I would have
 really appreciated let-style generalization for irrefutable pattern
 matches.  Here is the motivating example:

 {{{
 {-# LANGUAGE Rank2Types #-}
 {-# OPTIONS_GHC -fdefer-type-errors #-}
 module X where

 data IntStreamK k
     = Cons { hd :: Int, tl :: IntStreamK k }
 data IntStream
     = IntStream { unIntStream :: forall k. IntStreamK k }

 f1, f2, f3, f4 :: IntStream -> IntStream

 -- Does not work, type variable escapes
 f1 (IntStream (Cons x xs)) = IntStream (Cons (x + 1) xs)

 -- OK
 f2 (IntStream s) = IntStream (Cons (hd s + 1) (tl s))

 -- Works UNLESS GADTs are enabled (uses let generalization)
 f3 (IntStream s) =
     let Cons x xs = s
     in IntStream (Cons (x + 1) xs)

 -- Does not work, type variable escapes
 f4 (IntStream ~(Cons x xs)) = IntStream (Cons (x + 1) xs)
 }}}

 `IntStreamK` is modeled off of a clock-indexed stream representation ala
 "Productive Coprogramming with Guarded Recursion" (c.f.,
 http://bentnib.org/productive.pdf), although I've simplified the type a
 bit for this example. The important thing in this example `IntStream`
 takes a `IntStreamK` which is universally quantified over the clock index.

 I want to define a simple function: take a stream and increment its head
 (without using a record update). There are a number of very similar
 looking definitions, but only some of them typecheck; in the rest, `xs`
 fails to be sufficiently generalized.

 1. `f1` is the most obvious code to write, but actually we can't elaborate
 this into Core:
 {{{
 f1 = \ (x :: IntStream) ->
        case x of { IntStream s ->
        case s @ ??? of { Cons x xs ->
        IntStream
          (\ (@ k) -> Cons @ k (x+1) xs ) }}
 }}}
    The problem arises when we consider what type we will apply to `s`
 (which has type `forall k. IntStreamK k`): we want to use `k` bound by the
 type lambda inside `IntStream`, but it is not yet in scope!

 2. `f2` works. Here is its Core elaboration:
 {{{
 f2 = \ (x :: IntStream) ->
        case x of { IntStream s ->
        IntStream
          (\ (@ k) -> Cons @ k (hd (s @ k) + 1) (tl (s @ k))) }
 }}}

 3. `f3` works, because the let-binding gets generalized. We end up with
 this Core elaboration:
 {{{
 f3 = \ (x :: IntStream) ->
        case x of { IntStream s ->
        let {
          y :: forall k. (Int, IntStreamK k)
          y =
            \ (@ k) -> case s @ k of { Cons x xs ->
              (x, xs) } in
        IntStream
          (\ (@ k) -> Cons @ k
                           ((case y of {(x, _) -> x}) + 1)
                           (case y of {(_, xs) -> xs})) }
 }}}
    (GHC's actual desugaring for `y` is a bit more complex so I shortened
 it.) Note that this core is effectively the same as `f2`, except that (1)
 the type application has been commoned up, and (2) the `hd`/`tl` functions
 are inlined. If we turn on GADTs (without NoMonoLocalBinds) GHC stops
 generalizing this let binding and thus fails to typecheck. If you make
 this a strict let-binding this fails to typecheck (since we can't
 generalize strict let bindings; they're just like case.)

 4. The important one: this does not work, because when we bind `x` and
 `xs`, we immediately apply the type application, but do not generalize so
 no suitable type is in scope. However, operationally, the core elaboration
 should be exactly the same as in (3). So it would be fine to generalize
 here: the static semantics are validated by elaborating irrefutable
 pattern matches into let bindings.

 So, it would be convenient for this application of irrefutable patterns
 were generalized; then I could write almost the obvious code and have GHC
 accept it. The same caveat with GADTs and let-bindings would apply: with
 GADTs enabled irrefutable patterns would not be generalized.

 Unfortunately, if we add another constructor to `Cons` there is NO total
 System FC program that works (e.g.
 http://stackoverflow.com/questions/7720108/total-function-of-type-
 forall-n-maybe-f-n-maybe-forall-n-f-n)... but that's a story for another
 day.

 #11700 seems a bit related.

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