[GHC] #13959: substTyVar's definition is highly dubious

[GHC]

#13959: substTyVar's definition is highly dubious
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  patch
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.0.1
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):  Phab:D3732
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by goldfire):

 After a long debate, Simon and I came up with the following claim:

 '''(*) Claim''': If a tyvar is not in the domain of a substitution, then
 no variables in its kind are in the domain of a substitution.

 If (*) is true, then the change Phab:D3732 should be a no-op: precisely no
 behavior should change. And we can check (*) on the fly, which we should.

 Why should (*) be true? Here's some rough reasoning: a tyvar `a` whose
 kind mentions `k` must be bound in `k`'s scope. If we are substituting `k`
 (to `Type`, say), then we'll need to substitute both in `a`'s binding site
 and `a`'s scope. When we subst in the binding site (with
 `substTyVarBndr`), the subst is extended mapping `a:k` to `a:Type`; `a` is
 thus in the domain of the subst when we get to substing in `a`'s scope. If
 we've forgotten to call `substTyVarBndr`, then we're in deep trouble,
 anyway. Thus, all tyvars whose kinds mention `k` will be added to the
 subst by the time we get to their scope.

 But thinking about (*) led us to ponder this strange scenario: `forall k.
 forall (b :: k). forall k. forall (a :: k). Proxy [a,b]`. Is that well-
 kinded? Surely not, because `a` and `b` have different kinds: `a`'s kind
 is the more local `k` while `b`'s kind is the less local `k`. However,
 Core Lint is going to have a hard time with this. When Lint looks at
 `[a,b]`, it will ask for `a`'s kind and get `k`. It will ask for `b`'s
 kind and get `k`. And the `k`s will be equal! Core Lint will accept. This
 is horrible. This bug may have been lurking in GHC for ages.

 The remedy: don't do this. Specifically, we introduce

 '''(+) Rule''': When a tyvar `a` is brought into scope, all vars (type and
 term) whose type mentions `a` fall out of scope.

 Under (+), `b` is not in scope in `[a,b]` and we have a straightforward
 scoping error. We can check this in Lint. We couldn't quite convince
 ourselves that (+) is actually always respected during transformations,
 etc., but by adding a rule in Lint, we can discover when it doesn't. An
 alternative to (+) is

 (-) Rule: It is illegal to shadow a variable. That is, if `a` is in scope,
 we cannot bind `a`.

 (-) implies (+) and is easy to check for. However, it may not be so easy
 to uphold; Simon claims several places in GHC knowingly violate (-), and
 avoiding this violation may hurt performance. I'm worried that any code
 that violates (-) will sometimes fall afoul of (+) (but only in very
 obscure scenarios). Simon claims that the violations of (-) but not (+)
 involve closed types and therefore are safe w.r.t. (+). So we've agreed to
 check for (+) for now and see how that goes.

 As a sidenote: comment:7 and comment:9 concern term-level substitutions.
 At the term level, we have a real interest in commoning up occurrences (so
 that all occurrences of an Id `x` actually point to the same heap object)
 because of `IdInfo`. In types, on the other hand, we have an interest in
 avoiding forcing a `TCvSubst`'s `InScopeSet`, and so we don't use the same
 "look up in in-scope set" approach. So, essentially, comment:7 and
 comment:9 are red herrings.

 == Bottom line ==

 We have these tasks:

 1. Check for (*) in `substTyVar`. This is instead of the kind substitution
 discussed earlier in this ticket. Document (*).

 2. Update Core Lint to check (+). Document (+) in a nice Note.

 3. (Optional) If we blindly set `no_kind_change` to `False` in
 `substTyVarBndrCallback`, then substitutions ''will'' common up type
 variables by looking up type variables in the substitution. There's a
 chance this will have a performance benefit. Try and investigate.

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