[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 simonpj):

 > Who arranges for the members of the in-scope set to have substituted
 kinds?

 Well, if the in-scope set comes from the context (as in the simplifier or
 other places) all the `Var`s in the in-scope set are `OutIds`; that is,
 fully substituted.  It would be wrong to substitute again, because it's
 entirely OK to have a substitution that goes `a :-> [a]`, because the LHS
 is `InVars` and the RHS is `OutVaers`.  (This is not true during
 unification of course, but that's entirely separate.)

 E.g.  a substitution   [a :-> Proxy k (b::k),  k :-> *]  really means
 "replace `a` by `Proxy k (b::k)`" and NOT "then apply the subsituton to
 the result to get `Proxy * (b::*)`.  No no no.  Substitutions apply
 exactly once.

 (In this example the `k` in `Proxy k (b::k)` is an `OutTyVar` whereas the
 `k` in `k :-> *` is an `InTyVar`.)


 What if we build the in-scope set by taking the free vars of the range of
 the substitution?  Eg.
 {{{
 Substitute  [a :-> Proxy k (b::k)]
 in the type (a, b)
 }}}
 The in-scope set, from the range of the substitution, is {b,k}.   Do we
 need to apply the substitution to {b}?  No!  The range of the substitution
 is `OutVars` so we must not apply the substitution to it.

 A more delicate point is this: what if we build (part of) the in-scope set
 by taking the free vars of the type being substituted (see
 `substTyAddInScope` and `Note [The substitution invariant]` in`TyCoRep`?
 That's an `InType`!  eg
 {{{
 Substitute  [a :-> Int]
 in the type (a, b::k)
 }}}
 Now we get an in-scope set of `{b::k}`.  But although `b` appears in an
 `InType`, it must be an `OutTyVar` precisely because it is not
 substituted.  It must be bound somewhere outside, and it'd be wrong to
 substitute its kind at one of its occurrences and not at its binding site!

 So I think everything is fine.  But I really wish I had a clearer way to
 explain WHY it is fine.

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