+
+Note [Type lets]
+~~~~~~~~~~~~~~~~
+In the desugarer, it's very very convenient to be able to say (in effect)
+ let a = Int in <body>
+That is, use a type let. (See notes just below for why we want this.)
+
+We don't have type lets in Core, so the desugarer uses type lambda
+ (/\a. <body>) Int
+However, in the lambda form, we'd get lint errors from:
+ (/\a. let x::a = 4 in <body>) Int
+because (x::a) doesn't look compatible with (4::Int).
+
+So (HACK ALERT) the Lint phase does type-beta reduction "on the fly",
+as it were. It carries a type substitution (in this example [a -> Int])
+and applies this substitution before comparing types. The functin
+ lintTy :: Type -> LintM Type
+returns a substituted type; that's the only reason it returns anything.
+
+When we encounter a binder (like x::a) we must apply the substitution
+to the type of the binding variable. lintBinders does this.
+
+For Ids, the type-substituted Id is added to the in_scope set (which
+itself is part of the TvSubst we are carrying down), and when we
+find an occurence of an Id, we fetch it from the in-scope set.
+
+
+Why we need type let
+~~~~~~~~~~~~~~~~~~~~
+It's needed when dealing with desugarer output for GADTs. Consider
+ data T = forall a. T a (a->Int) Bool
+ f :: T -> ... ->
+ f (T x f True) = <e1>
+ f (T y g False) = <e2>
+After desugaring we get
+ f t b = case t of
+ T a (x::a) (f::a->Int) (b:Bool) ->
+ case b of
+ True -> <e1>
+ False -> (/\b. let y=x; g=f in <e2>) a
+And for a reason I now forget, the ...<e2>... can mention a; so
+we want Lint to know that b=a. Ugh.
+
+I tried quite hard to make the necessity for this go away, by changing the
+desugarer, but the fundamental problem is this:
+
+ T a (x::a) (y::Int) -> let fail::a = ...
+ in (/\b. ...(case ... of
+ True -> x::b
+ False -> fail)
+ ) a
+Now the inner case look as though it has incompatible branches.
+
+