Generalize irrefutable patterns (static semantics like letbindings)
tl;dr It is not letbindings that should be generalized, it is **irrefutable** patterns that should be generalized.
I know GHC's trend has been to reduce the amount of letgeneralization we do (since it interacts poorly with GADTs). However, I was recently working with some useful rank2 definitions, and found that I would have really appreciated letstyle generalization for irrefutable pattern matches. Here is the motivating example:
{# LANGUAGE Rank2Types #}
{# OPTIONS_GHC fdefertypeerrors #}
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 clockindexed 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.

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 typeforall k. IntStreamK k
): we want to usek
bound by the type lambda insideIntStream
, but it is not yet in scope!

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))) }

f3
works, because the letbinding 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 asf2
, except that (1) the type application has been commoned up, and (2) thehd
/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 letbinding this fails to typecheck (since we can't generalize strict let bindings; they're just like case.)
 The important one: this does not work, because when we bind
x
andxs
, 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 letbindings 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/totalfunctionoftypeforallnmaybefnmaybeforallnfn)... but that's a story for another day.
#11700 (closed) seems a bit related.
Trac metadata
Trac field  Value 

Version  8.0.1 
Type  FeatureRequest 
TypeOfFailure  OtherFailure 
Priority  normal 
Resolution  Unresolved 
Component  Compiler (Type checker) 
Test case  
Differential revisions  
BlockedBy  
Related  
Blocking  
CC  simonpj 
Operating system  
Architecture 